--- title: "A Δ₀ description of the constructible hierarchy" module: L.GCH.HierarchyDescription lang: en site: "Bedrock" description: "A Δ₀ description of the constructible hierarchy" stage: "Proving GCH" reading_order: 106 canonical: https://bedrock.institute/en/L.GCH.HierarchyDescription.html html: L.GCH.HierarchyDescription.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/HierarchyDescription.lagda.md prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.LevyHierarchy, FOL.Manipulation.ConstantOccurrences, FOL.Manipulation.ConstantMapping, FOL.Manipulation.Relabelling, FOL.Absoluteness, FOL.Semantics, V.Hierarchy, V.Coding, L.Constructible, L.Ordinal, L.Axioms.Basic, L.Axioms.Numerals, L.Coding.Expressions, L.Coding.NumeralBound, L.Coding.CodeSet, L.Coding.Model, L.Coding.Quantification, L.Coding.CodeDomain, L.Coding.EnvironmentTower, L.Hierarchy, L.GCH.SkolemHull, L.Coding.SatisfactionGraphSet, L.GCH.SatisfactionDescription, L.GCH.DefinablePowerSetDescription, L.GCH.AdequateStages] routes: [gch-descriptions, hulls-and-counting] translations: [https://bedrock.institute/zh/L.GCH.HierarchyDescription.md, https://bedrock.institute/ja/L.GCH.HierarchyDescription.md] agent_guide: /llms.txt license: CC-BY-NC-SA-4.0 --- The later condensation argument must transport the assertion that a set is the constructible stage at a given ordinal. Since elementarity transports formulas rather than the external operation `Lset`, this chapter builds a bounded object-language formula that recognizes the same stage relation, using a third set as a common bound for all auxiliary witnesses. ```agda {-# OPTIONS --cubical --safe --guardedness #-} ``` The construction is classical only through one fixed instance of excluded middle. Bounded existential formulas are nevertheless read as propositionally truncated existence, so classical background does not turn the hidden tables into chosen global data. ```agda open import Base.Prelude open import Base.Classical using ( LEM ) ``` Fix a universe level `ℓ` and excluded middle for propositions at level `ℓ-suc ℓ`. Every formula, reader, and final correctness theorem in the chapter is relative to this one explicit classical hypothesis. ```agda module L.GCH.HierarchyDescription {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where ``` The object language needs only membership, conjunction, truth, falsity, and bounded quantifiers. These constructors admit structural Δ₀ witnesses. Later, proving that no constants occur allows the constant domain to be changed to the empty alphabet, making the final three-variable formula parameter-free without removing its free variables. ```agda open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; var; _∈̇_; _∧̇_; ⊤̇; ⊥̇; ∃̇∈; ∀̇∈ ) open import FOL.LevyHierarchy using ( Δ₀; checkΔ₀; δ-∧; δ-∃∈ ) open import FOL.Manipulation.ConstantOccurrences using ( countFo ) open import FOL.Manipulation.ConstantMapping using ( embed ) ``` A bounded formula can be read both inside the constructible carrier and in the ambient cumulative hierarchy. Δ₀ absoluteness identifies those readings. Membership induction will validate table rows from lower rows, while extensionality will turn the two resulting membership implications into equality of stages. ```agda open import FOL.Manipulation.Relabelling using ( embed-⊨; mapΔ₀ ) import FOL.Absoluteness import FOL.Semantics open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-induction; extensionalV ) open import V.Coding {ℓ} using ( pr ) ``` The stage `Lset b` is assembled from the definable power sets of earlier stages: its members come from some `𝒟ₒ (Lset c)` with `c ∈ b`, and each such contribution lies in `Lset b`. The inward and outward membership rules express these two directions; ordinal facts ensure that the indices used later really are stage indices. ```agda open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-in; Lset-out; Lset-mono; 𝒟ₒ ) open import L.Ordinal {ℓ} using ( mem-ord; suc-ord; #∈ω ) open import L.Axioms.Basic {ℓ} using ( LsetS; Lset-suc ) open import L.Axioms.Numerals {ℓ} using ( numeralL-fst ) ``` Recognizing one definable power set internally requires formula codes, a satisfaction table, and an environment tower. Ordered-pair encodings then join each stage index to its recorded value. These auxiliary sets will all be bounded by the same witness set `z`, keeping the complete description within Δ₀. ```agda open import L.Coding.Expressions {ℓ} using ( sucAtL ) open import L.Coding.NumeralBound {ℓ} lem using ( module Bound ) open import L.Coding.CodeSet {ℓ} lem using ( AllCodes ) open import L.Coding.Model {ℓ} using ( container ) open import L.Coding.Quantification {ℓ} using ``` The components of a set-coded pair cannot be projected by an unbounded operation inside the object language. Instead, bounded component formulas range through a small container and read or fill the pair there. Ten named slots hold the numeral tags used by the coding descriptions, and shifting those names keeps them aligned when new witnesses extend the environment. ```agda ( sh; i0; i1; i2; i3; i8; f0; f1; f2; f3; f4; f5; f6; f7; f8; f9 ; down; suc-out; suc-in; sndEx; sndAll; bothAll ; sndEx-out; sndAll-in; bothAll-in; fillSnd; useSnd; useBoth; sndS ) open import L.Coding.CodeDomain {ℓ} using ( Tags; shN ) open import L.Coding.EnvironmentTower {ℓ} lem using ( nn; module Tower ) ``` Three semantic specifications meet here. A hierarchy table records pairs `(c,Lset c)` below a bound; the satisfaction description recognizes the genuine code, environment, and satisfaction data over a stage; and the definable-power-set description recognizes the set `𝒟ₒ (Lset c)`. Soundness will recover only the table properties `Values` and `Entries`, whereas completeness begins with the exact specification `IsHier`. ```agda open import L.Hierarchy {ℓ} lem using ( hierL-spec; IsHier; hier-out; hier-in; Values; Entries ) open import L.GCH.SkolemHull {ℓ} lem using ( module Cnt; erase-Δ₀; isOrd-at-p; Δ₀-isOrd-at-p; _⊨ₚ_ ) open import L.Coding.SatisfactionGraphSet {ℓ} lem using ( module SatGraph ) open import L.GCH.SatisfactionDescription {ℓ} lem using ( satAt; sat-complete ) open import L.GCH.DefinablePowerSetDescription {ℓ} lem using ( defAt; def-sound; def-complete ) ``` Completeness needs one common stage containing every auxiliary witness. If `γ` is adequate and `c ∈ γ`, then `Lset γ` contains the hierarchy table, code set, satisfaction table, and environment tower required at `c`; successor closure also places the next stage there, while `ω ∈ γ` supplies all ten finite numeral tags. ```agda open import L.GCH.AdequateStages {ℓ} lem using ( Adequate; module Adequate; module At; Lset∈suc ) ``` An environment is a finite vector of constructible sets. Introducing a bounded witness places it at the front and shifts every older slot by one; finite indices make those shifts explicit. This bookkeeping is what lets the same stage, table, and bound names survive through several nested quantifiers. ```agda open import Cubical.Data.Nat using ( _+_ ) open import Cubical.Data.Vec using ( _∷_; []; map; lookup ) open import Cubical.Data.Sigma using ( _×_ ) open import Cubical.Data.Unit using ( tt ) open import Cubical.Data.FinData using ( toℕ; weakenFin ) ``` Existential satisfaction retains only propositional truncation: it records that suitable data exist and forgets which data were used. Every later elimination therefore targets a proposition. In particular, membership is proposition-valued and equality of cumulative-hierarchy sets is a proposition, so the two conclusions needed in the proof are legitimate targets. ```agda open import Cubical.Functions.Logic using ( ⇔toPath ) import Cubical.Data.Empty as Empty import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∥_∥₁; ∣_∣₁; squash₁ ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet ) ``` The ten finite tags are represented by the von Neumann numerals inside the hierarchy. Zero is the empty set, each following tag is obtained by set-theoretic successor, and all ten lie in `ω`. Membership readers connect these ambient sets with their presentations as elements of the constructible carrier. ```agda open import Cubical.HITs.CumulativeHierarchy.Properties using ( ∈∈ₛ ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( ∅; ∅-empty; module InfinitySet ) open InfinitySet {ℓ} using ( #_; sucV; ω ) ``` Write `S` for the carrier of the constructible model. Its elements present ambient sets together with proofs of constructibility. All hidden tables and witnesses are quantified over this carrier, and the final visible slots will likewise present the value `a`, its stage index `p`, and the common bound `z`. ```agda open hPropStructure 𝒮ʟ using ( S ) ``` Satisfaction inside `L` and satisfaction in the ambient hierarchy use different structures but agree on Δ₀ formulas whose parameters come from `L`. The lemma `abs₀` is the bridge between them. This bridge will let completeness build the formula internally and soundness read the transported formula back as an ambient equality of stages. ```agda module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using ( _^_; _⊨ᵐ_; abs₀ ) open AbsL using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ ) module SemVᵃ = FOL.Semantics 𝒮ᵥ ``` The formula `defIn w z N body` uses four nested bounded existentials to place a satisfaction table `T`, a code set `C`, an environment tower `E`, and a value `d` inside `z`. The satisfaction description validates `T`, `C`, and `E` over the value at `w`; the power-set description identifies `d` with its definable power set; and `body` states what is required of that `d`. Satisfaction retains only the propositional truncation of these witnesses, and the formula does not characterize `z` uniquely. ```agda defIn : ∀ {k} → Fin k → Fin k → (Fin 10 → Fin k) → Formula S (4 + k) → Formula S k defIn w z N body = ∃̇∈ (var z) (∃̇∈ (var (sh 1 z)) (∃̇∈ (var (sh 2 z)) (∃̇∈ (var (sh 3 z)) (satAt i3 (sh 4 w) i2 i1 (shN 4 N) ∧̇ (defAt i0 (sh 4 w) i3 i2 (shN 4 N) ∧̇ body))))) ``` The inward inclusion `intoAt` says that each `x ∈ v` is accounted for by an earlier stage index `c ∈ b`: some pair-shaped member of `f` records a value `w` at `c`, and `x` belongs to the definable power set of `w`. In bounded notation its outer shape is `∀[ x ∈ v ] ∃[ c ∈ b ] ...`; the remaining bounded witnesses expose the row and the data used to recognize that power set. ```agda intoAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m intoAt v b f z N = ∀̇∈ (var v) (∃̇∈ (var (sh 1 b)) (∃̇∈ (var (sh 2 f)) (sndEx i0 i1 (defIn i0 (sh 5 z) (shN 5 N) (var i8 ∈̇ var i0))))) ``` The reverse inclusion `overAt` ranges over `c ∈ b` and over members of `f` that are presented as pairs `(c,w)`. For each such presentation, every element of the definable power set of `w` must belong to `v`. The clause says nothing about a member of `f` that has no such pair presentation, so it must not be read as excluding arbitrary junk from the whole candidate table. ```agda overAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m overAt v b f z N = ∀̇∈ (var b) (∀̇∈ (var (sh 1 f)) (sndAll i0 i1 (defIn i0 (sh 4 z) (shN 4 N) (∀̇∈ (var i0) (var i0 ∈̇ var (sh 9 v)))))) ``` The conjunction `stepAt` combines the two inclusions. Relative to the pair rows recorded below `b`, `intoAt` says that `v` has no additional members, while `overAt` says that none of the definable-power-set contributions is missing. Correct table values are a separate hypothesis of the later read lemma. ```agda stepAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m stepAt v b f z N = intoAt v b f z N ∧̇ overAt v b f z N ``` The first half of `approxAt` gives coverage: every `c ∈ b` has some pair-shaped entry in `f`. The second half tests `stepAt w c f z N` whenever a member of `f` is presented as a pair `(c,w)`. It does not say that every member of `f` is a pair or that every recorded first component lies below `b`. Accordingly, `approx-out` will recover exactly `Values f b × Entries f b`, not equality with the entire hierarchy graph and not a global no-junk property. ```agda approxAt : ∀ {m} → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m approxAt f b z N = ∀̇∈ (var b) (∃̇∈ (var (sh 1 f)) (sndEx i0 i1 ⊤̇)) ∧̇ ∀̇∈ (var f) (bothAll i0 (stepAt i0 i1 (sh 4 f) (sh 4 z) (shN 4 N))) ``` The clause `hierAt a p f z N` joins an approximation below `p` to one final step at `p`. If the approximation supplies `Values` and `Entries`, the final step identifies `a` with `Lset p`; conversely, an exact hierarchy table `IsHier p f` and adequate supplies fill both conjuncts. This is the local stage relation that the final three-variable formula will hide behind bounded witnesses. ```agda hierAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m hierAt a p f z N = approxAt f p z N ∧̇ stepAt a p f z N ``` The tag clause pins the ten slots to the numerals: the first slot has no members, so it is the empty set. ```agda pins : ∀ {m} → (Fin 10 → Fin m) → Formula S m pins N = ∀̇∈ (var (N f0)) ⊥̇ ∧̇ ( sucAtL (N f0) (N f1) ∧̇ ( sucAtL (N f1) (N f2) ∧̇ ( sucAtL (N f2) (N f3) ∧̇ ( sucAtL (N f3) (N f4) ∧̇ ( sucAtL (N f4) (N f5) ∧̇ ( sucAtL (N f5) (N f6) ``` The remaining nine slots are linked by nine successor assertions, so the ten slots are exactly the numerals zero through nine. ```agda ∧̇ ( sucAtL (N f6) (N f7) ∧̇ ( sucAtL (N f7) (N f8) ∧̇ sucAtL (N f8) (N f9) )))))))) ``` ## The bounded clauses of the hierarchy table To use the ten tags in later descriptions, their object-language pinning must agree with the semantic record `Tags γ N`. The next two lemmas prove both directions: one reads numeral equalities from `pins`, and the other reconstructs `pins` from those equalities. ```agda module PinsRead {m : ℕ} (N : Fin 10 → Fin m) (γ : S ^ m) where ``` Reading the tag clause first shows that the first slot is empty: it has no members. ```agda pins-out : ⟨ γ ⊨ pins N ⟩ → Tags γ N pins-out (h0 , hs) = go where q0 : fst (lookup (N f0) γ) ≡ # 0 q0 = extensionalV (λ y → ⇔toPath ``` Emptiness is an extensionality argument in both directions: any member of the first slot would contradict the falsity clause, and the empty set has no members to begin with. ```agda (λ y∈ → Empty.rec* (h0 (down (lookup (N f0) γ) y y∈) y∈)) (λ y∈ → Empty.rec (∅-empty y (∈∈ₛ {a = y} {b = ∅} .fst y∈)))) ``` The auxiliary lemma `up` advances one link of the numeral chain. If slot `i` denotes `# k` and `sucAtL i j` holds, its sound reading identifies slot `j` with `sucV (# k)`, hence with the numeral `# (suc k)`. ```agda up : (i j : Fin m) (k : ℕ) → ⟨ γ ⊨ sucAtL i j ⟩ → fst (lookup i γ) ≡ # k → fst (lookup j γ) ≡ # (suc k) up i j k h q = suc-out i j γ h ∙ cong sucV q ``` Starting from the equality for zero, the first five successor clauses yield `q1` through `q5`. Thus the slots named by `f1` through `f5` are identified successively with the numerals one through five. ```agda q1 = up (N f0) (N f1) 0 (hs .fst) q0 q2 = up (N f1) (N f2) 1 (hs .snd .fst) q1 q3 = up (N f2) (N f3) 2 (hs .snd .snd .fst) q2 q4 = up (N f3) (N f4) 3 (hs .snd .snd .snd .fst) q3 q5 = up (N f4) (N f5) 4 (hs .snd .snd .snd .snd .fst) q4 ``` The remaining four successor clauses continue the same chain, producing `q6` through `q9`. This identifies the slots `f6` through `f9` with the numerals six through nine and completes the numerical part of the reading. ```agda q6 = up (N f5) (N f6) 5 (hs .snd .snd .snd .snd .snd .fst) q5 q7 = up (N f6) (N f7) 6 (hs .snd .snd .snd .snd .snd .snd .fst) q6 q8 = up (N f7) (N f8) 7 (hs .snd .snd .snd .snd .snd .snd .snd .fst) q7 q9 = up (N f8) (N f9) 8 (hs .snd .snd .snd .snd .snd .snd .snd .snd) q8 ``` The record `Tags γ N` asks for the corresponding numeral equality at each element of `Fin 10`. The first four cases return `q0`, `q1`, `q2`, and `q3`, matching the tags zero through three. ```agda go : Tags γ N go zero = q0 go (suc zero) = q1 go (suc (suc zero)) = q2 go (suc (suc (suc zero))) = q3 ``` The next five cases of `go` return `q4` through `q8`. Written as nested successors, these patterns exhaust the tags four through eight without introducing any additional arithmetic argument. ```agda go (suc (suc (suc (suc zero)))) = q4 go (suc (suc (suc (suc (suc zero))))) = q5 go (suc (suc (suc (suc (suc (suc zero)))))) = q6 go (suc (suc (suc (suc (suc (suc (suc zero))))))) = q7 go (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) = q8 ``` The sole remaining case of `Fin 10` is the ninth successor of zero, and it returns `q9`. The case analysis now supplies all ten numeral equalities required by `Tags γ N`. ```agda go (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))) = q9 ``` For the converse direction, suppose the slots already satisfy `Tags γ N`. A purported member of the zero slot transports along its tag equality to a member of the empty set and is therefore impossible. The same tag equalities then provide the data from which the nine successor clauses are filled. ```agda pins-in : Tags γ N → ⟨ γ ⊨ pins N ⟩ pins-in tg = (λ x x∈ → Empty.rec (∅-empty (fst x) (∈∈ₛ {a = fst x} {b = ∅} .fst (subst (λ u → ⟨ fst x ∈ u ⟩) (tg f0) x∈)))) , ( st f0 f1 refl , ( st f1 f2 refl , ( st f2 f3 refl , ( st f3 f4 refl , ( st f4 f5 refl , ( st f5 f6 refl ``` Each successor clause is reconstructed by applying the inward successor reader after transporting both tag slots along their numeral equalities. ```agda , ( st f6 f7 refl , ( st f7 f8 refl , st f8 f9 refl )))))))) where st : (j k : Fin 10) → # (toℕ k) ≡ sucV (# (toℕ j)) → ⟨ γ ⊨ sucAtL (N j) (N k) ⟩ st j k e = suc-in (N j) (N k) γ (tg k ∙ e ∙ cong sucV (sym (tg j))) ``` Fix an environment `δ` whose ten named slots have the required numeral values. Let `Wv` be the underlying set at `w` and `Zv` the underlying set at `z`. The first is the stage over which definability is interpreted, and the second is the common bound in which the four witnesses must lie. ```agda module DefInRead {k : ℕ} (w z : Fin k) (N : Fin 10 → Fin k) (body : Formula S (4 + k)) (δ : S ^ k) (tg : Tags δ N) where private Wv = fst (lookup w δ) Zv = fst (lookup z δ) ``` The four witnesses are bound successively as `T`, `C`, `E`, and `d`. Since each new binder extends the front of the environment, the body is evaluated at `d ∷ E ∷ C ∷ T ∷ δ`. Thus its first four slots refer, in order, to the definable-power-set value, the environment tower, the code set, and the satisfaction table. ```agda δ4 : (T C E d : S) → S ^ (4 + k) δ4 T C E d = d ∷ E ∷ C ∷ T ∷ δ ``` Reading `defIn` preserves the propositional truncation around four witnesses `T`, `C`, `E`, and `d`. Its conclusion deliberately retains only that `d ∈ z`, that `d = 𝒟ₒ Wv`, and that the body holds in the extended environment. Membership of `T`, `C`, and `E` in `z`, together with the internal satisfaction and power-set proofs, is consumed while deriving this weaker statement. ```agda defIn-out : ⟨ δ ⊨ defIn w z N body ⟩ → ∥ Σ[ T ∈ S ] Σ[ C ∈ S ] Σ[ E ∈ S ] Σ[ d ∈ S ] (⟨ fst d ∈ Zv ⟩ × ((fst d ≡ 𝒟ₒ Wv) × ⟨ δ4 T C E d ⊨ body ⟩)) ∥₁ defIn-out = PT.rec squash₁ (λ { (T , (T∈ , h1)) → PT.rec squash₁ (λ { (C , (C∈ , h2)) → PT.rec squash₁ (λ { (E , (E∈ , h3)) → PT.map (λ { (d , (d∈ , (hs , (hd , hb)))) → ``` After the four nested truncations have exposed the witnesses, `def-sound` combines the satisfaction description `hs` with the definable-power-set description `hd`. Its conclusion is the one equality retained here, namely `d = 𝒟ₒ Wv`; the body proof is passed through unchanged. ```agda T , C , E , d , ( d∈ , ( def-sound i0 (sh 4 w) i3 i2 i1 (shN 4 N) (δ4 T C E d) (lookup w δ) refl tg hs hd , hb )) }) h3 }) h2 }) h1 }) ``` Conversely, proving `defIn` from semantic data requires explicit genuine witnesses. One supplies a constructible carrier `W` represented at `w`, the four sets and their memberships in `z`, their identifications with the genuine satisfaction table, code set, environment tower, and definable power set, and a proof of the body. This direction therefore assumes data that the outward reading intentionally forgets. ```agda defIn-in : (W : S) → Wv ≡ fst W → (T C E d : S) → ⟨ fst T ∈ Zv ⟩ → ⟨ fst C ∈ Zv ⟩ → ⟨ fst E ∈ Zv ⟩ → ⟨ fst d ∈ Zv ⟩ → fst T ≡ fst (SatGraph.pairs W) → fst C ≡ fst (AllCodes W) → fst E ≡ fst (Tower.tower W) → fst d ≡ 𝒟ₒ (fst W) → ⟨ δ4 T C E d ⊨ body ⟩ → ⟨ δ ⊨ defIn w z N body ⟩ defIn-in W qw T C E d T∈ C∈ E∈ d∈ qT qC qE qd hb = ``` For the inward reading, `sat-complete` first proves that the genuine satisfaction table, code set, and environment tower satisfy `satAt`. Using that proof and the supplied equality for `d`, `def-complete` proves the definable-power-set clause. The given body proof completes the conjunction, after which the four witnesses and their memberships are introduced under the nested propositional truncations. ```agda ∣ T , ( T∈ , ∣ C , ( C∈ , ∣ E , ( E∈ , ∣ d , ( d∈ , ( hs , ( def-complete i0 (sh 4 w) i3 i2 i1 (shN 4 N) (δ4 T C E d) W qw tg hs qd , hb ))) ∣₁ ) ∣₁ ) ∣₁ ) ∣₁ where hs : ⟨ δ4 T C E d ⊨ satAt i3 (sh 4 w) i2 i1 (shN 4 N) ⟩ hs = sat-complete i3 (sh 4 w) i2 i1 (shN 4 N) (δ4 T C E d) W qw qT qC qE tg ``` The predicate `Supply` says that, for an ordinal `c`, all four witnesses needed by `defIn` already lie inside the common bound: the satisfaction graph, code set, and environment tower of the stage `Lset c`, together with the next stage `Lset (sucV c)`. ```agda Supply : (Zv : V ℓ) (c : V ℓ) → IsOrd c → Type (ℓ-suc ℓ) Supply Zv c oc = ⟨ fst (SatGraph.pairs (LsetS c oc)) ∈ Zv ⟩ × ( ⟨ fst (AllCodes (LsetS c oc)) ∈ Zv ⟩ × ( ⟨ fst (Tower.tower (LsetS c oc)) ∈ Zv ⟩ ``` The fourth component is the next stage, which is what the successor step of the approximation needs. ```agda × ⟨ Lset (sucV c) ∈ Zv ⟩ )) ``` Now fix one proposed hierarchy step in an environment `γ`. Write `Vv` for the proposed result, `Bv` for the set of earlier indices, and `Fv` for the underlying candidate table. The question is whether the two bounded inclusions force `Vv` to equal `Lset Bv` once the relevant rows of `Fv` are known to be correct and present. ```agda module StepRead {m : ℕ} (v b f z : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (tg : Tags γ N) where private Vv = fst (lookup v γ) Bv = fst (lookup b γ) Fv = fst (lookup f γ) ``` Let `Zv` denote the underlying common bound. It controls where the auxiliary satisfaction, code, tower, and definable-power-set witnesses may be found. The equality sought from the step does not mention `Zv`; the bound enables the description without becoming part of the resulting stage value. ```agda Zv = fst (lookup z γ) ``` In the inward body, `d` is the definable power set recognized by `defIn`, and `x` is the member introduced by the outer bounded universal over `v`. The atomic body says `x ∈ d`. Once the recorded value `w` is identified with `Lset c`, this becomes membership in `𝒟ₒ (Lset c)` for some `c ∈ b`. ```agda intoBody : Formula S (5 + m) intoBody = defIn i0 (sh 5 z) (shN 5 N) (var i8 ∈̇ var i0) ``` The `over` body is a definable-power-set description whose inner formula says that every member of the described set belongs to the proposed next value. This gives the reverse inclusion needed for the union equality. ```agda overBody : Formula S (4 + m) overBody = defIn i0 (sh 4 z) (shN 4 N) (∀̇∈ (var i0) (var i0 ∈̇ var (sh 9 v))) ``` The read lemma for one step assumes separately that every pair row below `Bv` has the correct value (`Values`) and that every index below `Bv` has its canonical row (`Entries`). Under precisely these two hypotheses, the two halves of `stepAt` give opposite membership implications, and extensionality yields `Vv = Lset Bv`. These assumptions control the relevant pair rows only; they do not exclude unrelated members of the candidate table. ```agda step-out : ⟨ γ ⊨ stepAt v b f z N ⟩ → Values (lookup f γ) Bv → Entries (lookup f γ) Bv → Vv ≡ Lset Bv step-out (hi , ho) vals ents = extensionalV (λ x → ⇔toPath (fwd x) (bwd x)) where fwd : (x : V ℓ) → ⟨ x ∈ Vv ⟩ → ⟨ x ∈ Lset Bv ⟩ fwd x x∈ = PT.rec (snd (x ∈ Lset Bv)) (λ { (c , (c∈ , h1)) → PT.rec (snd (x ∈ Lset Bv)) ``` For the forward inclusion, `intoAt` supplies a stage index `c ∈ Bv`, a pair row `(c,w)` in the table, and a definable-power-set value `d` containing `x`. The `Values` hypothesis identifies `w` with `Lset c`, so `d = 𝒟ₒ (Lset c)`. The inward stage rule `Lset-in` then carries `x` from that contribution into `Lset Bv`. ```agda (λ { (q , (q∈ , h2)) → PT.rec (snd (x ∈ Lset Bv)) (λ { (w , s , (eq , h3)) → PT.rec (snd (x ∈ Lset Bv)) (λ { (T , C , E , d , (d∈ , (qd , hx))) → Lset-in Bv (fst c) x c∈ (subst (λ u → ⟨ x ∈ u ⟩) (qd ∙ cong 𝒟ₒ (vals c w c∈ (subst (λ u → ⟨ u ∈ Fv ⟩) eq q∈))) hx) }) ``` The nested existential readers preserve truncation at every stage. First `sndEx-out` recovers merely a second component `w` from the pair-shaped table entry; then `defIn-out` recovers merely the auxiliary data and the equality identifying `d` with the definable power set of `w`. Each truncation is eliminated directly into the membership proposition `x ∈ Lset Bv`. ```agda (DefInRead.defIn-out i0 (sh 5 z) (shN 5 N) (var i8 ∈̇ var i0) (w ∷ s ∷ q ∷ c ∷ xS ∷ γ) tg h3) }) (sndEx-out i0 i1 intoBody (q ∷ c ∷ xS ∷ γ) h2) }) h1 }) (hi xS x∈) where ``` The proof begins with an ambient member `x ∈ Vv`, but the formula is interpreted over the constructible carrier `S`. The operation `down` uses that membership to present `x` as a carrier element `xS`; placing `xS` at the front of the environment makes the newly bound slot denote the same underlying set `x`. ```agda xS : S xS = down (lookup v γ) x x∈ ``` The backward direction of `step-out` sends a member of the genuine stage `Lset Bv` into the proposed value `Vv`. It eliminates the truncated stage decomposition of `Lset Bv`, reducing the claim to an earlier stage `δ` whose definable power set contains `x`. ```agda bwd : (x : V ℓ) → ⟨ x ∈ Lset Bv ⟩ → ⟨ x ∈ Vv ⟩ bwd x x∈ = PT.rec (snd (x ∈ Vv)) put (Lset-out Bv x x∈) where put : Σ[ δ ∈ V ℓ ] (⟨ δ ∈ Bv ⟩ × ⟨ x ∈ 𝒟ₒ (Lset δ) ⟩) → ⟨ x ∈ Vv ⟩ put (δ , (δ∈ , xD)) = PT.rec (snd (x ∈ Vv)) ``` Once `Lset-out` has exhibited an earlier index `δ`, completeness supplies the canonical table entry `(δ, Lset δ)`. The `over` clause applies to this entry, and `defIn-out` identifies its bounded set `d` with `𝒟ₒ (Lset δ)`. Its universal body therefore sends the given `x` into the proposed value `Vv`. This direction uses the canonical entry supplied by `Entries`; it does not need a separate appeal to `Values`. ```agda (λ { (T , C , E , d , (d∈ , (qd , hsub))) → hsub (down d x (subst (λ u → ⟨ x ∈ u ⟩) (sym qd) xD)) (subst (λ u → ⟨ x ∈ u ⟩) (sym qd) xD) }) (DefInRead.defIn-out i0 (sh 4 z) (shN 4 N) (∀̇∈ (var i0) (var i0 ∈̇ var (sh 9 v))) (w ∷ container q c w refl .fst ∷ q ∷ c ∷ γ) tg (useSnd i0 (q ∷ c ∷ γ) c w refl overBody i1 refl (ho c δ∈ q (ents c δ∈)))) ``` The two named objects are the coded argument and the coded pair: both are presented by descending along their membership proofs into carrier elements. ```agda where c : S c = down (lookup b γ) δ δ∈ q : S q = down (lookup f γ) (pr δ (Lset δ)) (ents c δ∈) ``` The value `w` of the row is read from the pair presentation, and is the component consumed by the satisfaction of the body. ```agda w : S w = sndS q δ (Lset δ) refl ``` The inward direction of the step clause requires five hypotheses: ordinality of the bound, the identification of the proposed value with the stage at the bound, correctness and completeness of the table at the bound, and a supply function placing every auxiliary witness for each member of the bound inside the witness bound. The proof splits into the two conjuncts. ```agda step-in : (ob : IsOrd Bv) → Vv ≡ Lset Bv → Values (lookup f γ) Bv → Entries (lookup f γ) Bv → ((c : V ℓ) (oc : IsOrd c) → ⟨ c ∈ Bv ⟩ → Supply Zv c oc) → ⟨ γ ⊨ stepAt v b f z N ⟩ step-in ob vq vals ents sup = into , over where ``` The `into` conjunct reads outward from a member `x` of the proposed value: the truncated decomposition of the stage at the bound names an earlier ordinal and a definable-power-set membership, which the existence introduction fills into the two bounded quantifiers. ```agda into : ⟨ γ ⊨ intoAt v b f z N ⟩ into x x∈ = PT.rec squash₁ put (Lset-out Bv (fst x) (subst (λ u → ⟨ fst x ∈ u ⟩) vq x∈)) where put : Σ[ δ ∈ V ℓ ] (⟨ δ ∈ Bv ⟩ × ⟨ fst x ∈ 𝒟ₒ (Lset δ) ⟩) → ⟨ (x ∷ γ) ⊨ ∃̇∈ (var (sh 1 b)) (∃̇∈ (var (sh 2 f)) (sndEx i0 i1 intoBody)) ⟩ ``` The nested bounded existentials are filled without extracting data from propositional truncation. The proof presents `δ` as the carrier element `c`, uses `Entries` to present the canonical pair as `q`, and supplies the pair decomposition through `fillSnd`; the remaining body is `hb`. Each constructor retains the truncation built into `∃[]-syntax`, which is appropriate because satisfaction is a proposition. ```agda put (δ , (δ∈ , xD)) = ∣ c , ( δ∈ , ∣ q , ( ents c δ∈ , fillSnd i0 (q ∷ c ∷ x ∷ γ) c w refl intoBody hb i1 refl ) ∣₁ ) ∣₁ where oδ : IsOrd δ oδ = mem-ord {A = Bv} ob δ δ∈ ``` The three carrier elements have different sources. The membership `δ ∈ Bv` presents the earlier index as `c`; membership of the canonical pair in the table presents that pair as `q`; and ordinality of `δ` lets `LsetS` present the stage `Lset δ` as `w`. Keeping these sources distinct matters when the bounded witnesses are assembled. ```agda c : S c = down (lookup b γ) δ δ∈ q : S q = down (lookup f γ) (pr δ (Lset δ)) (ents c δ∈) w : S ``` Here `w` is the genuine stage `Lset δ` in the constructible carrier. Applying the supply hypothesis at `δ` gives membership evidence in `Zv` for its satisfaction table, code set, environment tower, and successor stage. With those four bounds and their defining equalities, `defIn-in` reduces the remaining obligation to the mathematical fact that `x ∈ 𝒟ₒ (Lset δ)`. ```agda w = LsetS δ oδ s = sup δ oδ δ∈ hb : ⟨ (w ∷ container q c w refl .fst ∷ q ∷ c ∷ x ∷ γ) ⊨ intoBody ⟩ hb = DefInRead.defIn-in i0 (sh 5 z) (shN 5 N) (var i8 ∈̇ var i0) (w ∷ container q c w refl .fst ∷ q ∷ c ∷ x ∷ γ) tg w refl ``` The four bounded objects are the genuine satisfaction table, code set, environment tower, and `Lset (sucV δ)`. The supply hypothesis proves that each lies in `Zv`, while reflexivity identifies the first three with the structures expected by the descriptions. Finally `Lset-suc δ` identifies the fourth with `𝒟ₒ (Lset δ)`, so the original membership of `x` can be transported into the formula body. ```agda (SatGraph.pairs w) (AllCodes w) (Tower.tower w) (LsetS (sucV δ) (suc-ord oδ)) (s .fst) (s .snd .fst) (s .snd .snd .fst) (s .snd .snd .snd) refl refl refl (Lset-suc δ) (subst (λ u → ⟨ fst x ∈ u ⟩) (sym (Lset-suc δ)) xD) ``` For the `over` conjunct, fix `c ∈ Bv`, a member `q` of the table, and a presentation of `q` as the pair `(c,w)`. Correctness then identifies `w` with `Lset c`. The remaining task is uniform in `y`: every `y ∈ 𝒟ₒ w` must belong to the proposed value `Vv`. This is the second inclusion needed to identify the proposed value with the stage at `Bv`. ```agda over : ⟨ γ ⊨ overAt v b f z N ⟩ over c c∈ q q∈ = sndAll-in i0 i1 overBody (q ∷ c ∷ γ) (λ w s s∈ w∈ e → let wq : fst w ≡ Lset (fst c) wq = vals c w c∈ (subst (λ u → ⟨ u ∈ Fv ⟩) e q∈) oc : IsOrd (fst c) ``` Ordinality of `c` is inherited from the bound; the stage is presented as a carrier element; and the supply function produces the four witnesses at `c`. ```agda oc = mem-ord {A = Bv} ob (fst c) c∈ W : S W = LsetS (fst c) oc s' = sup (fst c) oc c∈ in DefInRead.defIn-in i0 (sh 4 z) (shN 4 N) (∀̇∈ (var i0) (var i0 ∈̇ var (sh 9 v))) ``` The supply at `c` bounds the genuine satisfaction table, code set, environment tower, and successor stage, so `defIn-in` can establish the definable-power-set description. If `y` belongs to the set described there, `Lset-suc c` turns this into membership in `𝒟ₒ (Lset c)`, and `Lset-in` uses `c ∈ Bv` to place `y` in `Lset Bv`. Transport along `Vv ≡ Lset Bv` then yields the required membership in the proposed value. ```agda (w ∷ s ∷ q ∷ c ∷ γ) tg W wq (SatGraph.pairs W) (AllCodes W) (Tower.tower W) (LsetS (sucV (fst c)) (suc-ord oc)) (s' .fst) (s' .snd .fst) (s' .snd .snd .fst) (s' .snd .snd .snd) refl refl refl (Lset-suc (fst c)) (λ y y∈d → subst (λ u → ⟨ fst y ∈ u ⟩) (sym vq) (Lset-in Bv (fst c) (fst y) c∈ (subst (λ u → ⟨ fst y ∈ u ⟩) (Lset-suc (fst c)) y∈d)))) ``` The approximation reader is parameterized by the table, the bound, the witness bound, the tag map and the environment. The three underlying sets are named once. ```agda module ApproxRead {m : ℕ} (f b z : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (tg : Tags γ N) where private Fv = fst (lookup f γ) Bv = fst (lookup b γ) Zv = fst (lookup z γ) ``` The step body is the step clause at the four shifted slots. ```agda stepBody : Formula S (4 + m) stepBody = stepAt i0 i1 (sh 4 f) (sh 4 z) (shN 4 N) ``` The outward reading of the approximation clause produces correctness and completeness of the table at the bound. The predicate `P` records what must be proved about each argument: that its recorded value is the stage at the argument. Note carefully what is and is not claimed: the result is exactly `Values` and `Entries`; it does not say that the table contains no non-pair members or no entries whose first component lies outside the bound. ```agda approx-out : ⟨ γ ⊨ approxAt f b z N ⟩ → IsOrd Bv → Values (lookup f γ) Bv × Entries (lookup f γ) Bv approx-out (hd , hs) ob = vals , ents where P : V ℓ → Type (ℓ-suc ℓ) P c = ⟨ c ∈ Bv ⟩ → (w : S) → ⟨ pr c (fst w) ∈ Fv ⟩ → fst w ≡ Lset c ``` Coverage says that for each `c ∈ Bv` there merely exists a table member that presents a pair with first component `c`. Reading that pair exposes a value `w` and maps the original membership proof to the canonical pair notation `pr c w`. The result remains propositionally truncated, so `entryOf` supplies existence for later propositional reasoning without choosing a value globally. ```agda entryOf : (c : S) → ⟨ fst c ∈ Bv ⟩ → ∥ Σ[ w ∈ S ] ⟨ pr (fst c) (fst w) ∈ Fv ⟩ ∥₁ entryOf c c∈ = PT.rec squash₁ (λ { (q , (q∈ , h)) → PT.map (λ { (w , s , (e , _)) → w , subst (λ u → ⟨ u ∈ Fv ⟩) e q∈ }) (sndEx-out i0 i1 ⊤̇ (q ∷ c ∷ γ) h) }) (hd c c∈) ``` The induction step validates an arbitrary recorded pair `(c,w)` with `c ∈ Bv`. Its membership proof lets the second approximation clause supply `stepAt w c`; the induction hypothesis gives correctness at every argument below `c`, and coverage will give the matching canonical entries there. `StepRead.step-out` can then conclude that the recorded value is exactly `Lset c`. ```agda step : (c : V ℓ) → ((y : V ℓ) → ⟨ y ∈ c ⟩ → P y) → P c step c IH c∈ w rec = StepRead.step-out i0 i1 (sh 4 f) (sh 4 z) (shN 4 N) env tg (useBoth i0 (q ∷ γ) cS w refl stepBody (hs q rec)) vals' ents' where ``` The proof now presents the relevant sets inside the constructible carrier. The membership `c ∈ Bv` yields the carrier element `cS`, and the assumed membership of `pr c (fst w)` in the table yields `q`. The value `w` is already a carrier element supplied to the induction predicate; the next environment places these three presentations in the slots expected by the step formula. ```agda cS : S cS = down (lookup b γ) c c∈ q : S q = down (lookup f γ) (pr c (fst w)) rec env : S ^ (4 + m) ``` The extended environment assembles the four slots for the step reading. Ordinality of the bound restricts smaller arguments to below the bound, and the correctness reading at smaller arguments is the restriction of the induction hypothesis. ```agda env = w ∷ cS ∷ container q cS w refl .fst ∷ q ∷ γ in' : (y : S) → ⟨ fst y ∈ c ⟩ → ⟨ fst y ∈ Bv ⟩ in' y y∈ = ob .fst {x = c} {y = fst y} y∈ c∈ vals' : Values (lookup f γ) c vals' y w' y∈ rec' = IH (fst y) y∈ (in' y y∈) w' rec' ``` Completeness at smaller arguments is recovered by the same restriction: for each smaller argument, the truncated entry is consumed, and the value equation from the induction hypothesis transports the canonical entry into place. ```agda ents' : Entries (lookup f γ) c ents' y y∈ = PT.rec (snd (pr (fst y) (Lset (fst y)) ∈ Fv)) (λ { (w' , rec') → subst (λ u → ⟨ pr (fst y) u ∈ Fv ⟩) (IH (fst y) y∈ (in' y y∈) w' rec') rec' }) (entryOf y (in' y y∈)) ``` Correctness below `Bv` is obtained by ambient membership induction on the underlying argument `c`. The predicate `P c` is conditional on `c ∈ Bv`; this membership both restricts the theorem to the required bound and, through ordinality of `Bv`, makes every smaller argument eligible for the induction hypothesis. Applying the induction result to an arbitrary recorded value gives `Values`. ```agda vals : Values (lookup f γ) Bv vals c w c∈ rec = ∈-induction {P = P} step (fst c) c∈ w rec ``` Completeness at the bound composes the truncated entry with the correctness just proved: the value equation transports the recorded entry to the canonical one. ```agda ents : Entries (lookup f γ) Bv ents c c∈ = PT.rec (snd (pr (fst c) (Lset (fst c)) ∈ Fv)) (λ { (w , rec) → subst (λ u → ⟨ pr (fst c) u ∈ Fv ⟩) (vals c w c∈ rec) rec }) (entryOf c c∈) ``` The inward direction of the approximation clause starts from the stronger semantic hypothesis that the table realizes the hierarchy at the bound. This asymmetry is intentional: the outward direction proves only the two table conditions, while the inward direction consumes the full hierarchy specification. ```agda approx-in : (ob : IsOrd Bv) → IsHier Bv (lookup f γ) → ((c : V ℓ) (oc : IsOrd c) → ⟨ c ∈ Bv ⟩ → Supply Zv c oc) → ⟨ γ ⊨ approxAt f b z N ⟩ approx-in ob sp sup = dom , steps where ``` The outward reading of the hierarchy specification says that every recorded pair has its argument below the bound and its value equal to the stage there. ```agda hout : (c w : S) → ⟨ pr (fst c) (fst w) ∈ Fv ⟩ → ⟨ fst c ∈ Bv ⟩ × (fst w ≡ Lset (fst c)) hout = hier-out Bv ob (lookup f γ) sp ``` The inward reading says that every canonical pair below the bound is recorded. ```agda hin : (c : S) → ⟨ fst c ∈ Bv ⟩ → ⟨ pr (fst c) (Lset (fst c)) ∈ Fv ⟩ hin = hier-in Bv ob (lookup f γ) sp ``` The domain conjunct is proved by presenting the stage at each argument below the bound and injecting the canonical pair into the table. ```agda dom : ⟨ γ ⊨ ∀̇∈ (var b) (∃̇∈ (var (sh 1 f)) (sndEx i0 i1 ⊤̇)) ⟩ dom c c∈ = ∣ q , ( hin c c∈ , fillSnd i0 (q ∷ c ∷ γ) c w refl ⊤̇ (λ z → z) i1 refl ) ∣₁ where w : S w = LsetS (fst c) (mem-ord {A = Bv} ob (fst c) c∈) ``` The canonical pair is presented by descending along its membership proof into the carrier. ```agda q : S q = down (lookup f γ) (pr (fst c) (Lset (fst c))) (hin c c∈) ``` The second approximation conjunct must be proved for every member `q` of the table and every presentation of `q` as a pair `(c,w)`. Under such a presentation, the exact hierarchy specification yields both `c ∈ Bv` and `w ≡ Lset c`. These facts prepare a proof of the step formula at `c`. No claim is made here that an arbitrary member of the candidate table has such a pair presentation. ```agda steps : ⟨ γ ⊨ ∀̇∈ (var f) (bothAll i0 stepBody) ⟩ steps q q∈ = bothAll-in i0 stepBody (q ∷ γ) (λ c w s s∈ c∈s w∈s e → let rec : ⟨ pr (fst c) (fst w) ∈ Fv ⟩ rec = subst (λ u → ⟨ u ∈ Fv ⟩) e q∈ c∈ : ⟨ fst c ∈ Bv ⟩ ``` The argument is below the bound by the outward hierarchy reading; ordinality is inherited; and `StepRead.step-in` receives all five hypotheses, including the restricted correctness and completeness and the supply at each smaller argument. ```agda c∈ = hout c w rec .fst oc : IsOrd (fst c) oc = mem-ord {A = Bv} ob (fst c) c∈ in StepRead.step-in i0 i1 (sh 4 f) (sh 4 z) (shN 4 N) (w ∷ c ∷ s ∷ q ∷ γ) tg oc (hout c w rec .snd) (λ d w' d∈ rec' → hout d w' rec' .snd) ``` Below the current argument `c`, completeness comes from `hier-in`: transitivity of the ordinal bound turns `d ∈ c ∈ Bv` into `d ∈ Bv`, where the canonical entry is known to occur. The auxiliary bounds have a different source. They come from the given supply function `sup`, restricted along the same transitivity argument. Thus the hierarchy specification supplies table entries, while `sup` supplies the four bounded coding objects. ```agda (λ d d∈ → hin d (ob .fst {x = fst c} {y = fst d} d∈ c∈)) (λ d od d∈ → sup d od (ob .fst {x = fst c} {y = d} d∈ c∈))) ``` The hierarchy reading has four distinguished slots: the proposed stage `a`, its stage index `p`, the approximation table `f`, and the common witness bound `z`. The tag map interprets the ten numeral positions used by the coding formulas, and the environment supplies carrier elements for all these slots. ```agda module HierRead {m : ℕ} (a p f z : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (tg : Tags γ N) where private Av = fst (lookup a γ) Pv = fst (lookup p γ) Zv = fst (lookup z γ) ``` The soundness theorem for the hierarchy formula says: if the formula holds and the ordinal slot is an ordinal, then the level slot equals the stage at the ordinal slot. The proof reads the approximation and the final step separately. ```agda hier-sound : ⟨ γ ⊨ hierAt a p f z N ⟩ → IsOrd Pv → Av ≡ Lset Pv hier-sound (ha , hs) op = StepRead.step-out a p f z N γ tg hs (ve .fst) (ve .snd) where ve = ApproxRead.approx-out f p z N γ tg ha op ``` The completeness theorem for the hierarchy formula takes ordinality of the index slot, the identification of the level slot with the stage, an actual hierarchy table at the index, and the supply function, and constructs the satisfaction. ```agda hier-complete : (op : IsOrd Pv) → Av ≡ Lset Pv → IsHier Pv (lookup f γ) → ((c : V ℓ) (oc : IsOrd c) → ⟨ c ∈ Pv ⟩ → Supply Zv c oc) → ⟨ γ ⊨ hierAt a p f z N ⟩ hier-complete op aq sp sup = ApproxRead.approx-in f p z N γ tg op sp sup ``` The proof composes the inward approximation from the hierarchy specification with the final step, whose correctness and completeness clauses are read outward from the hierarchy specification at each smaller argument. ```agda , StepRead.step-in a p f z N γ tg op aq (λ c w c∈ rec → hier-out Pv op (lookup f γ) sp c w rec .snd) (hier-in Pv op (lookup f γ) sp) sup ``` ## Reading approximations and the completed hierarchy The inner module seals the formula that will ultimately express the constructible hierarchy inside the object language. ```agda module Inner where ``` The fourteen-slot environment begins with the ten numeral tags. Repeated `weakenFin` embeds each of their indices into `Fin 14` without changing its numerical position, so `N14` occupies slots zero through nine. This agrees with the concrete environment used later, whose first ten entries are the von Neumann numerals. ```agda N14 : Fin 10 → Fin 14 N14 k = weakenFin (weakenFin (weakenFin (weakenFin k))) ``` The four trailing slots complete the mathematical data of the inner formula. Slot ten holds the table `ff`, slot eleven the proposed stage `aa`, slot twelve its stage index `pp`, and slot thirteen the common bound `zz`. Thus the full environment is ordered as ten tags, followed by `f`, `a`, `p`, and `z`. ```agda ff aa pp zz : Fin 14 ff = sh 10 (i0 {3}) aa = sh 11 (i0 {2}) pp = sh 12 (i0 {1}) zz = sh 13 (i0 {0}) ``` The inner formula conjoins two mathematical requirements. `pins N14` fixes the first ten slots as the numeral tags needed by the coding descriptions, while `hierAt aa pp ff zz N14` says that `ff` approximates the hierarchy below `pp` and that `aa` is its next value at `pp`, with all auxiliary data bounded by `zz`. Opacity keeps this large formula behind its proved readings. ```agda opaque inner : Formula S 14 inner = pins N14 ∧̇ hierAt aa pp ff zz N14 ``` To prove boundedness, the checker may unfold `inner` together with the sealed descriptions `satAt` and `defAt`. This scoped unfolding reveals that the large conjunction is built entirely from atoms, connectives, and bounded quantifiers. Outside this proof boundary, the mathematical content is recovered through the read lemmas rather than by normalizing the expanded formula. ```agda opaque unfolding inner satAt defAt ``` After the scoped unfolding, `checkΔ₀ inner tt` supplies the structural `Δ₀` witness: every quantifier occurring in `inner` is bounded. This is a syntactic verification of this particular formula, not a claim that `checkΔ₀` decides boundedness in both directions. The surrounding module and its exported results remain parameterized by `lem : LEM (ℓ-suc ℓ)`. ```agda Δ₀-inner : Δ₀ inner Δ₀-inner = checkΔ₀ inner tt ``` The readings of the sealed formula are exposed through the same unfolding boundary. ```agda opaque unfolding inner ``` The outward reading of the conjunction is the pair of its two conjuncts, since conjunction is a pair of propositions. ```agda inner-out : (γ : S ^ 14) → ⟨ γ ⊨ inner ⟩ → ⟨ γ ⊨ pins N14 ⟩ × ⟨ γ ⊨ hierAt aa pp ff zz N14 ⟩ inner-out γ h = h ``` Conversely, proofs of the pin clauses and of the hierarchy clause form the two components required to satisfy their conjunction. Together with `inner-out`, this gives the two exact directions needed later: one can reason from the large formula through its two mathematical parts, and reconstruct it once both parts have been proved. ```agda inner-in : (γ : S ^ 14) → ⟨ γ ⊨ pins N14 ⟩ → ⟨ γ ⊨ hierAt aa pp ff zz N14 ⟩ → ⟨ γ ⊨ inner ⟩ inner-in γ h1 h2 = h1 , h2 ``` For an outer environment with `suc n` positions, `lastFin` denotes its last position. In every application below, that position contains the common bounding set that supplies the bound for the new existential. The witness introduced by the bounded quantifier occupies the new front position of the body; it is not the position denoted by `lastFin`. ```agda lastFin : {n : ℕ} → Fin (suc n) lastFin {zero} = zero lastFin {suc n} = suc (lastFin {n}) ``` The operation `wrap` existentially binds the front witness position of its body and requires that witness to belong to the set named by the last outer position. Consequently the arity drops by one while boundedness is preserved. Repeating this operation will quantify the ten numeral tags and the table, each as an element of the common bound `z`. ```agda wrap : {n : ℕ} → Formula S (suc (suc n)) → Formula S (suc n) wrap {n} φ = ∃̇∈ (var (lastFin {n})) φ ``` The Δ₀ witness is preserved under wrapping, because bounded existential quantification is itself a bounded construction. ```agda δ-wrap : {n : ℕ} {φ : Formula S (suc (suc n))} → Δ₀ φ → Δ₀ (wrap {n} φ) δ-wrap d = δ-∃∈ d ``` Five wrapping steps consume five of the ten numeral slots, reducing the free positions one at a time from fourteen to nine. ```agda s13 = wrap {12} inner s12 = wrap {11} s13 s11 = wrap {10} s12 s10 = wrap {9} s11 s9 = wrap {8} s10 ``` Five more wrapping steps reduce the free positions from nine to four, leaving only the level, the ordinal index, the table and the witness bound. ```agda s8 = wrap {7} s9 s7 = wrap {6} s8 s6 = wrap {5} s7 s5 = wrap {4} s6 s4 = wrap {3} s5 ``` The eleventh wrap existentially binds the remaining auxiliary slot, the hierarchy table `f`, again with bound `z`. Exactly three free positions remain, in the order `(a,p,z)`: the proposed stage, its stage index, and the common witness bound. Thus `three` has arity three and is not a sentence; the later erasure step will remove its unused constant domain without removing these free variables. ```agda three : Formula S 3 three = wrap {2} s4 ``` The witness formula is wrapped eleven times, once per bounded existential introduced inside the common bound. Each wrap adds one layer of the Δ₀ certificate, so the wrapped formula is bounded throughout. ```agda Δ₀-three : Δ₀ three Δ₀-three = δ-wrap (δ-wrap (δ-wrap (δ-wrap (δ-wrap (δ-wrap (δ-wrap (δ-wrap (δ-wrap (δ-wrap (δ-wrap Δ₀-inner)))))))))) ``` To verify that the wrapped formula contains no constants, the calculation may look through the sealed definitions of `inner`, `satAt`, and `defAt`. This local unfolding exposes enough of their syntax for the occurrence count to reduce, while the large formulas themselves remain hidden behind their read and write lemmas in the surrounding argument. ```agda opaque unfolding inner satAt defAt ``` The constant-occurrence count of `three` is zero. Its three remaining positions are free variables for `a`, `p`, and `z`; they are not constants. Once the sealed components are unfolded for this calculation, the equality reduces definitionally because every term in the formula was built from variables. ```agda count-three : countFo three ≡ 0 count-three = refl ``` Since `three` contains no constants, erasure changes its constant domain from the constructible carrier to the empty type and leaves its variables and quantifier structure intact. The resulting `erased` is therefore parameter-free but still has arity three; embedding it back into the old constant domain recovers `three`. ```agda erased : Formula (⊥* {ℓ-suc ℓ}) 3 erased = Cnt.erase three count-three ``` Erasure also preserves the Δ₀ witness. It changes only the unavailable constant symbols, so every bounded quantifier in `three` remains bounded and the same structural argument proves `erased` to be Δ₀. ```agda Δ₀-erased : Δ₀ erased Δ₀-erased = erase-Δ₀ three count-three Δ₀-three ``` Semantically, one wrapped layer is a propositionally truncated bounded witness. If every member `x` of the bound that satisfies the body yields `P`, then `unwrap` eliminates that truncated existence into `P`. The declaration `P : hProp` supplies precisely the proposition condition required by this elimination. ```agda unwrap : {n : ℕ} (φ : Formula S (suc (suc n))) (γ : S ^ (suc n)) {P : hProp (ℓ-suc ℓ)} → ((x : S) → ⟨ fst x ∈ fst (lookup (lastFin {n}) γ) ⟩ → ⟨ (x ∷ γ) ⊨ φ ⟩ → ⟨ P ⟩) → ⟨ γ ⊨ wrap {n} φ ⟩ → ⟨ P ⟩ unwrap φ γ {P} k h = PT.rec (snd P) (λ { (x , xz , hx) → k x xz hx }) h ``` `wrap-in` builds the bounded existential from a named member and the body's satisfaction at its extension, the introduction rule of the bounded existential quantifier. ```agda wrap-in : {n : ℕ} (φ : Formula S (suc (suc n))) (γ : S ^ (suc n)) (x : S) → ⟨ fst x ∈ fst (lookup (lastFin {n}) γ) ⟩ → ⟨ (x ∷ γ) ⊨ φ ⟩ → ⟨ γ ⊨ wrap {n} φ ⟩ wrap-in φ γ x m h = ∣ x , (m , h) ∣₁ ``` ## A parameter-free formula for constructible levels The visible formula `levelFo` has three free positions `(a,p,z)`. It conjoins the assertion that `p` is an ordinal with the erased hierarchy description bounded by `z`. Thus `z` remains a free input even though the soundness conclusion will mention only `a` and `p`. ```agda levelFo : Formula (⊥* {ℓ-suc ℓ}) 3 levelFo = isOrd-at-p ∧̇ Inner.erased ``` Both conjuncts of `levelFo` are Δ₀, and the Δ₀ class is closed under conjunction. The conjunction constructor therefore combines their two boundedness witnesses into the witness `Δ₀-levelFo` without introducing an unbounded quantifier. ```agda Δ₀-levelFo : Δ₀ levelFo Δ₀-levelFo = δ-∧ Δ₀-isOrd-at-p Inner.Δ₀-erased ``` The reading lemma composes three paths for any constant-free Δ₀ formula: Δ₀ absoluteness from the restricted carrier to the ambient hierarchy, the invariance of satisfaction under embedding the empty constant domain, and the uniqueness of the empty interpretation. The result is an equality of satisfaction propositions. ```agda read : {n : ℕ} {φ : Formula (⊥* {ℓ-suc ℓ}) n} → Δ₀ φ → (δ : S ^ n) → (δ ⊨ embed φ) ≡ (map fst δ ⊨ₚ φ) read {n} {φ} dφ δ = AbsL.abs₀ (mapΔ₀ Empty.rec* dφ) δ ∙ embed-⊨ 𝒮ᵥ {K = S} fst φ (map fst δ) ``` The final equality in this path concerns the interpretation of constants. Because the constant domain is empty, any such interpretation agrees pointwise with empty elimination. Function extensionality identifies it with the canonical empty interpretation, so the preceding embedding comparison ends at the ambient reading of the same parameter-free formula. ```agda ∙ cong (λ ι → SemVᵃ.At._⊨_ (⊥* {ℓ-suc ℓ}) ι (map fst δ) φ) (funExt (λ b → Empty.rec* b)) ``` The outward ordinal reader unpacks the two clauses of the ordinality atom into the transitivity of the underlying set of `p` and the transitivity of each of its members, with every entry lowered through the presentation of `p`. ```agda ord-out : (a p z : S) → ⟨ (a ∷ p ∷ z ∷ []) ⊨ embed isOrd-at-p ⟩ → IsOrd (fst p) ord-out a p z h = ( λ {x} {y} y∈x x∈p → h .fst (down p x x∈p) x∈p (down (down p x x∈p) y y∈x) y∈x ) , ( λ x x∈p {y} {u} u∈y y∈x → h .snd (down p x x∈p) x∈p (down (down p x x∈p) y y∈x) y∈x ``` For the second ordinality clause, take `x ∈ p`, `y ∈ x`, and `u ∈ y`. Lowering all three memberships into the constructible carrier lets the formula's second conjunct conclude `u ∈ x`. This is exactly the transitivity of each member `x` of `p`, and together with the first clause it yields `IsOrd p`. ```agda (down (down (down p x x∈p) y y∈x) u u∈y) u∈y ) ``` The inward ordinal reader builds the two clauses from the ordinality certificate, with every entry packaged as an element of `L`. ```agda ord-in : (a p z : S) → IsOrd (fst p) → ⟨ (a ∷ p ∷ z ∷ []) ⊨ embed isOrd-at-p ⟩ ord-in a p z op = (λ x x∈p y y∈x → op .fst {x = fst x} {y = fst y} y∈x x∈p) , (λ x x∈p y y∈x u u∈y → op .snd (fst x) x∈p {x = fst y} {y = fst u} u∈y y∈x) ``` The soundness argument now works inside the fourteen-slot reading of the hidden formula. Its task is to discard the bounded auxiliary witnesses while retaining their mathematical consequence: the value in slot `a` is the constructible stage indexed by slot `p`. ```agda private module Sound where open Inner ``` The finish lemma separates the two conjuncts of `inner`. The pins reader turns the first into the ten numeral equalities required by the hierarchy reader. From the approximation in the second conjunct, `hier-sound` recovers only `Values × Entries`, which is enough to read the final step as `a = Lset p` once the ordinality of `p` is supplied. This does not assert that the hidden table has no malformed members or entries outside `p`. ```agda finish : (γ : S ^ 14) → ⟨ γ ⊨ inner ⟩ → IsOrd (fst (lookup pp γ)) → fst (lookup aa γ) ≡ Lset (fst (lookup pp γ)) finish γ h op = HierRead.hier-sound aa pp ff zz N14 γ tg (inner-out γ h .snd) op where tg : Tags γ N14 ``` The pinned numerals are read outward by the pins reader, which derives the ten numeral equations from the object-language clauses. ```agda tg = PinsRead.pins-out N14 γ (inner-out γ h .fst) ``` The internal soundness lemma begins with three elements `a`, `p`, and `z` of the constructible carrier and assumes that `embed levelFo` holds there. It first uses the erasure inverse to recover satisfaction of the eleven-times-wrapped formula. The desired conclusion compares the underlying set of `a` with `Lset` at the underlying index `p`. ```agda sound-L : (a p z : S) → ⟨ (a ∷ p ∷ z ∷ []) ⊨ embed levelFo ⟩ → fst a ≡ Lset (fst p) sound-L a p z (ho , hφ) = go (subst (λ ψ → ⟨ (a ∷ p ∷ z ∷ []) ⊨ ψ ⟩) (Cnt.erase-inv three count-three) hφ) where ordp : IsOrd (fst p) ``` The ordinality conjunct produces the ordinality certificate of `p` through the outward ordinal reader, which is the remaining input that the hierarchy reader requires. ```agda ordp = ord-out a p z ho ``` The equality to be retained is made into the proposition `G`. Sets in the cumulative hierarchy form an h-set, so `setIsSet` proves that this equality type is an `hProp`. Consequently each propositionally truncated bounded witness may be eliminated into `G` without exposing a chosen witness. ```agda G : hProp (ℓ-suc ℓ) G = (fst a ≡ Lset (fst p)) , setIsSet (fst a) (Lset (fst p)) ``` Soundness unwraps the eleven bounded existentials one at a time, consuming the truncated witnesses into the propositional equality. The unwrapping order mirrors the binding order of the formula. ```agda go : ⟨ (a ∷ p ∷ z ∷ []) ⊨ three ⟩ → ⟨ G ⟩ go = unwrap s4 (a ∷ p ∷ z ∷ []) {G} λ F mF → unwrap s5 (F ∷ a ∷ p ∷ z ∷ []) {G} λ x9 m9 → unwrap s6 (x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x8 m8 → ``` The next five eliminations recover the numeral witnesses `x7` through `x3`. At every stage the environment grows at the front, while its last slot remains `z`, the common bound from which all eleven witnesses came. ```agda unwrap s7 (x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x7 m7 → unwrap s8 (x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x6 m6 → unwrap s9 (x6 ∷ x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x5 m5 → unwrap s10 (x5 ∷ x6 ∷ x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x4 m4 → unwrap s11 (x4 ∷ x5 ∷ x6 ∷ x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x3 m3 → ``` The innermost witness completes the unwrapping: the fourteen-slot environment is passed to the finish lemma together with the ordinality certificate, producing the equality of the two underlying sets. ```agda unwrap s12 (x3 ∷ x4 ∷ x5 ∷ x6 ∷ x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x2 m2 → unwrap s13 (x2 ∷ x3 ∷ x4 ∷ x5 ∷ x6 ∷ x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x1 m1 → unwrap inner (x1 ∷ x2 ∷ x3 ∷ x4 ∷ x5 ∷ x6 ∷ x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x0 m0 hm → finish (x0 ∷ x1 ∷ x2 ∷ x3 ∷ x4 ∷ x5 ∷ x6 ∷ x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) hm ordp ``` For ambient sets `a`, `p`, and `z` known to be constructible, their constructibility proofs present them as elements of the constructible carrier. Reading Δ₀ absoluteness backwards transfers ambient satisfaction of `levelFo` to satisfaction by those presentations, where the internal soundness argument applies. Projecting back gives `a = Lset p`. Thus constructibility of all three inputs is an explicit hypothesis, not a consequence of the formula. ```agda level-sound : (a p z : V ℓ) → ⟨ isL a ⟩ → ⟨ isL p ⟩ → ⟨ isL z ⟩ → ⟨ (a ∷ p ∷ z ∷ []) ⊨ₚ levelFo ⟩ → a ≡ Lset p level-sound a p z la lp lz h = Sound.sound-L (a , la) (p , lp) (z , lz) (subst ⟨_⟩ (sym (read Δ₀-levelFo ((a , la) ∷ (p , lp) ∷ (z , lz) ∷ []))) h) ``` For completeness, fix `lam` with adequacy data and an ordinal `p ∈ lam`. The ordinality field makes `lam` a stage index, whose corresponding stage is `Lset lam`; the other fields give successor closure, membership of `ω`, and the required coding witnesses below `lam`. The proof will use these facts to show that the particular bound `Lset lam` contains every witness needed to describe the stage `Lset p`. ```agda private module Complete (lam : V ℓ) (ad : Adequate lam) (p : V ℓ) (op : IsOrd p) (p∈λ : ⟨ p ∈ lam ⟩) where open Inner open Adequate lam ad using ( ord; succ; ω∈; wit ) ``` Transitivity of the adequate stage `lam` is extracted from its ordinality: two nested memberships compose into one. ```agda private tr : (x y : V ℓ) → ⟨ x ∈ lam ⟩ → ⟨ y ∈ x ⟩ → ⟨ y ∈ lam ⟩ tr x y x∈ y∈ = ord .fst {x = x} {y = y} y∈ x∈ ``` The empty set belongs to the adequate stage, by transitivity applied to the chain `∅ ∈ ω ∈ lam`. ```agda ∅∈λ : ⟨ ∅ ∈ lam ⟩ ∅∈λ = tr ω ∅ ω∈ (#∈ω zero) ``` The numeral-bound argument specializes to the constructible hierarchy at `lam`. Ordinality, successor closure, and the membership `∅ ∈ lam` imply that the underlying set of every model numeral belongs to `Lset lam`. This supplies the uniform bound later needed for all ten tag numerals. ```agda module B = Bound lam ord succ ∅∈λ using ( num∈λ ) ``` Set `K = Lset lam`. This is the common bounding set represented by the third free input `zS`; the hierarchy table, the ten numerals, and every auxiliary set used to justify a row must all be shown to belong to `K`. ```agda K : V ℓ K = Lset lam ``` If `c ∈ lam`, successor closure gives `sucV c ∈ lam`. The standard successor-stage fact places `Lset c` in `Lset (sucV c)`, and monotonicity along `sucV c ∈ lam` then lifts this membership to `Lset c ∈ K`. Later the same lemma is applied to `sucV c`, using successor closure once more, to put `Lset (sucV c)` in `K`; that is the definable-power-set witness needed for the row at `c`. ```agda Lset∈K : (c : V ℓ) → ⟨ c ∈ lam ⟩ → ⟨ Lset c ∈ K ⟩ Lset∈K c c∈ = Lset-mono {α = lam} {β = sucV c} (succ c c∈) (Lset∈suc c) ``` The numeral-bound theorem first places the underlying set of the model numeral in `K`. The projection equation `numeralL-fst` identifies that set with the ambient von Neumann numeral `# k`, and transport yields `# k ∈ K`. Hence all ten numeral witnesses satisfy the same bound as the hierarchy table. ```agda num∈K : (k : ℕ) → ⟨ # k ∈ K ⟩ num∈K k = subst (λ u → ⟨ u ∈ K ⟩) (numeralL-fst k) (B.num∈λ k) ``` Four sets are named: the level `Lset p`, the ordinal `p`, the stage `Lset lam`, and the hierarchy table at `p`, each in the appropriate carrier. ```agda aS pS zS F : S aS = LsetS p op pS = p , At.cL p op zS = LsetS lam ord F = At.hier p op ``` The environment `E` now records the complete fourteen-slot assignment. From front to back it contains the numerals `0` through `9`, the genuine hierarchy table at `p`, the intended value `Lset p`, the index `p`, and the common bound `Lset lam`. This is exactly the slot order in which `inner` reads its data. ```agda E : S ^ 14 E = nn 0 ∷ nn 1 ∷ nn 2 ∷ nn 3 ∷ nn 4 ∷ nn 5 ∷ nn 6 ∷ nn 7 ∷ nn 8 ∷ nn 9 ∷ F ∷ aS ∷ pS ∷ zS ∷ [] ``` The tag hypothesis identifies each of the first four tag slots with its own numeral, definitionally. ```agda tg : Tags E N14 tg zero = refl tg (suc zero) = refl tg (suc (suc zero)) = refl tg (suc (suc (suc zero))) = refl ``` The next five cases verify the tag slots at indices four through eight. Each lookup reduces to the corresponding entry of `E`, so these slots are definitionally the numerals `4` through `8`. ```agda tg (suc (suc (suc (suc zero)))) = refl tg (suc (suc (suc (suc (suc zero))))) = refl tg (suc (suc (suc (suc (suc (suc zero)))))) = refl tg (suc (suc (suc (suc (suc (suc (suc zero))))))) = refl tg (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) = refl ``` The final case verifies the tenth tag slot, at index nine, as the numeral `9`. All ten equations required by `Tags E N14` are therefore established by computation on the explicit environment. ```agda tg (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))) = refl ``` For each member `c` of the ordinal `p`, the supply lemma places four objects in `K`: the satisfaction graph, the code set, the environment tower, and the next level `Lset (sucV c)`. The chain `c ∈ p ∈ lam` and the transitivity of `lam` first place `c` in `lam`, making the adequacy witnesses available. ```agda sup : (c : V ℓ) (oc : IsOrd c) → ⟨ c ∈ p ⟩ → Supply K c oc sup c oc c∈ = w .snd .snd .fst , ( w .snd .fst , ( w .snd .snd .snd , Lset∈K (sucV c) (succ c c∈λ) )) where c∈λ : ⟨ c ∈ lam ⟩ c∈λ = tr p c p∈λ c∈ ``` The witness for each `c` is read from the adequacy data, closing the supply for every member of the ordinal. ```agda w = wit c c∈λ oc ``` The inner formula now holds at `E`. The pins writer supplies its numeral conjunct. For the hierarchy conjunct, `hier-complete` uses the ordinality of `p`, the reflexive identification of the proposed value with `Lset p`, the exact hierarchy table supplied by `hierL-spec`, and the row-by-row supply derived above from adequacy. No strengthened stage hypothesis is used here. ```agda hm : ⟨ E ⊨ inner ⟩ hm = inner-in E (PinsRead.pins-in N14 E tg) (HierRead.hier-complete aa pp ff zz N14 E tg op refl (hierL-spec p (At.cL p op) op) sup) ``` The adequacy witness at `p` places the underlying set of the genuine hierarchy table `F` in the common bound `K`. This supplies the membership proof needed to introduce `F` as the outermost bounded witness. ```agda FK : ⟨ fst F ∈ K ⟩ FK = wit p p∈λ op .fst ``` It remains to hide the table and numeral data behind the eleven bounded existentials. The outermost introduction uses the genuine hierarchy table `F`, whose membership in `K` was just proved. The next two introductions use the numerals `9` and `8`, each with its membership in the same common bound. ```agda h3 : ⟨ (aS ∷ pS ∷ zS ∷ []) ⊨ three ⟩ h3 = wrap-in s4 (aS ∷ pS ∷ zS ∷ []) F FK ( wrap-in s5 (F ∷ aS ∷ pS ∷ zS ∷ []) (nn 9) (num∈K 9) ( wrap-in s6 (nn 9 ∷ F ∷ aS ∷ pS ∷ zS ∷ []) (nn 8) (num∈K 8) ( ``` The same introduction rule inserts the numerals `7` through `3`. Their membership proofs all come from `num∈K`, so every quantifier is witnessed inside `K = Lset lam`; no witness is taken from an unbounded ambient search. ```agda wrap-in s7 (nn 8 ∷ nn 9 ∷ F ∷ aS ∷ pS ∷ zS ∷ []) (nn 7) (num∈K 7) ( wrap-in s8 (nn 7 ∷ nn 8 ∷ nn 9 ∷ F ∷ aS ∷ pS ∷ zS ∷ []) (nn 6) (num∈K 6) ( wrap-in s9 (nn 6 ∷ nn 7 ∷ nn 8 ∷ nn 9 ∷ F ∷ aS ∷ pS ∷ zS ∷ []) (nn 5) (num∈K 5) ( wrap-in s10 (nn 5 ∷ nn 6 ∷ nn 7 ∷ nn 8 ∷ nn 9 ∷ F ∷ aS ∷ pS ∷ zS ∷ []) (nn 4) (num∈K 4) ( wrap-in s11 (nn 4 ∷ nn 5 ∷ nn 6 ∷ nn 7 ∷ nn 8 ∷ nn 9 ∷ F ∷ aS ∷ pS ∷ zS ∷ []) (nn 3) (num∈K 3) ( ``` Finally the numerals `2`, `1`, and `0` are inserted. After the last introduction, the extended environment is exactly `E`, where `hm` already proves `inner`. The nested introductions therefore establish satisfaction of the eleven-times-wrapped formula at the visible triple `(Lset p,p,Lset lam)`. ```agda wrap-in s12 (nn 3 ∷ nn 4 ∷ nn 5 ∷ nn 6 ∷ nn 7 ∷ nn 8 ∷ nn 9 ∷ F ∷ aS ∷ pS ∷ zS ∷ []) (nn 2) (num∈K 2) ( wrap-in s13 (nn 2 ∷ nn 3 ∷ nn 4 ∷ nn 5 ∷ nn 6 ∷ nn 7 ∷ nn 8 ∷ nn 9 ∷ F ∷ aS ∷ pS ∷ zS ∷ []) (nn 1) (num∈K 1) ( wrap-in inner (nn 1 ∷ nn 2 ∷ nn 3 ∷ nn 4 ∷ nn 5 ∷ nn 6 ∷ nn 7 ∷ nn 8 ∷ nn 9 ∷ F ∷ aS ∷ pS ∷ zS ∷ []) (nn 0) (num∈K 0) hm)))))))))) ``` The erasure inverse says that embedding `erased` into the constructible constant domain recovers `three`. Transporting `h3` along the inverse direction therefore yields satisfaction of `embed erased` at the same three-slot environment. Only the constant domain has changed; the eleven bounded witnesses and their common bound remain the ones already constructed. ```agda hφ : ⟨ (aS ∷ pS ∷ zS ∷ []) ⊨ embed erased ⟩ hφ = subst (λ ψ → ⟨ (aS ∷ pS ∷ zS ∷ []) ⊨ ψ ⟩) (sym (Cnt.erase-inv three count-three)) h3 ``` Completeness is assembled from the two conjuncts: the ordinality atom holds by `ord-in`, and the erased witness formula holds by the transport just proved. The reading lemma transfers both to the ambient satisfaction. ```agda complete : ⟨ (Lset p ∷ p ∷ Lset lam ∷ []) ⊨ₚ levelFo ⟩ complete = subst ⟨_⟩ (read Δ₀-levelFo (aS ∷ pS ∷ zS ∷ [])) (ord-in aS pS zS op , hφ) ``` The completeness theorem states the precise existence direction available here. If `γ` is adequate and contains the ordinal `p`, then the triple `(Lset p,p,Lset γ)` satisfies `levelFo`. Later, `CondensationTransfer` places unbounded existential quantifiers around this Δ₀ core, carries all three coordinates through elementarity, and uses soundness to recognize the transported first coordinate as the corresponding constructible stage. The theorem makes no claim that an arbitrary third coordinate works or is uniquely determined. ```agda level-complete : (γ : V ℓ) → Adequate γ → (p : V ℓ) → IsOrd p → ⟨ p ∈ γ ⟩ → ⟨ (Lset p ∷ p ∷ Lset γ ∷ []) ⊨ₚ levelFo ⟩ level-complete γ ad p op p∈ = Complete.complete γ ad p op p∈ ```