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.

{-# 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.

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.

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.

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.

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.

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 Δ₀.

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.

  ( 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.

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.

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.

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.

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.

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.

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.

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.

defIn : ∀ {k} → Fin k → Fin k → (Fin  → Fin k) → Formula S ( + k) → Formula S k
defIn w z N body =
  ∃̇∈ (var z) (∃̇∈ (var (sh  z)) (∃̇∈ (var (sh  z)) (∃̇∈ (var (sh  z))
    (satAt i3 (sh  w) i2 i1 (shN  N) ∧̇ (defAt i0 (sh  w) i3 i2 (shN  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.

intoAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin  → Fin m) → Formula S m
intoAt v b f z N =
  ∀̇∈ (var v) (∃̇∈ (var (sh  b)) (∃̇∈ (var (sh  f))
    (sndEx i0 i1 (defIn i0 (sh  z) (shN  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.

overAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin  → Fin m) → Formula S m
overAt v b f z N =
  ∀̇∈ (var b) (∀̇∈ (var (sh  f))
    (sndAll i0 i1 (defIn i0 (sh  z) (shN  N) (∀̇∈ (var i0) (var i0 ∈̇ var (sh  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.

stepAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin  → 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.

approxAt : ∀ {m} → Fin m → Fin m → Fin m → (Fin  → Fin m) → Formula S m
approxAt f b z N =
    ∀̇∈ (var b) (∃̇∈ (var (sh  f)) (sndEx i0 i1 ⊤̇))
  ∧̇ ∀̇∈ (var f) (bothAll i0 (stepAt i0 i1 (sh  f) (sh  z) (shN  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.

hierAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin  → 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.

pins : ∀ {m} → (Fin  → 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.

  ∧̇ ( 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.

module PinsRead {m : ℕ} (N : Fin  → Fin m) (γ : S ^ m) where

Reading the tag clause first shows that the first slot is empty: it has no members.

  pins-out : ⟨ γ ⊨ pins N ⟩ → Tags γ N
  pins-out (h0 , hs) = go
    where
    q0 : fst (lookup (N f0) γ) ≡ # 
    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.

      (λ 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).

    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.

    q1 = up (N f0) (N f1)  (hs .fst) q0
    q2 = up (N f1) (N f2)  (hs .snd .fst) q1
    q3 = up (N f2) (N f3)  (hs .snd .snd .fst) q2
    q4 = up (N f3) (N f4)  (hs .snd .snd .snd .fst) q3
    q5 = up (N f4) (N f5)  (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.

    q6 = up (N f5) (N f6)  (hs .snd .snd .snd .snd .snd .fst) q5
    q7 = up (N f6) (N f7)  (hs .snd .snd .snd .snd .snd .snd .fst) q6
    q8 = up (N f7) (N f8)  (hs .snd .snd .snd .snd .snd .snd .snd .fst) q7
    q9 = up (N f8) (N f9)  (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.

    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.

    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.

    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.

  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.

    , ( st f6 f7 refl , ( st f7 f8 refl , st f8 f9 refl ))))))))
    where
    st : (j k : Fin ) → # (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.

module DefInRead {k : ℕ} (w z : Fin k) (N : Fin  → Fin k) (body : Formula S ( + 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.

  δ4 : (T C E d : S) → S ^ ( + 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.

  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.

      T , C , E , d , ( d∈ , ( def-sound i0 (sh  w) i3 i2 i1 (shN  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.

  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.

    ∣ T , ( T∈ , ∣ C , ( C∈ , ∣ E , ( E∈ , ∣ d , ( d∈ , ( hs
      , ( def-complete i0 (sh  w) i3 i2 i1 (shN  N) (δ4 T C E d) W qw tg hs qd , hb ))) ∣₁ ) ∣₁ ) ∣₁ ) ∣₁
    where
    hs : ⟨ δ4 T C E d ⊨ satAt i3 (sh  w) i2 i1 (shN  N) ⟩
    hs = sat-complete i3 (sh  w) i2 i1 (shN  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).

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.

  × ⟨ 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.

module StepRead {m : ℕ} (v b f z : Fin m) (N : Fin  → 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.

    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.

    intoBody : Formula S ( + m)
    intoBody = defIn i0 (sh  z) (shN  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.

    overBody : Formula S ( + m)
    overBody = defIn i0 (sh  z) (shN  N) (∀̇∈ (var i0) (var i0 ∈̇ var (sh  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.

  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.

      (λ { (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.

        (DefInRead.defIn-out i0 (sh  z) (shN  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.

      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.

    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.

        (λ { (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  z) (shN  N) (∀̇∈ (var i0) (var i0 ∈̇ var (sh  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.

        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.

        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.

  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.

    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  b)) (∃̇∈ (var (sh  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.

      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.

        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 δ).

        w = LsetS δ oδ
        s = sup δ oδ δ∈
        hb : ⟨ (w ∷ container q c w refl .fst ∷ q ∷ c ∷ x ∷ γ) ⊨ intoBody ⟩
        hb = DefInRead.defIn-in i0 (sh  z) (shN  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.

               (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.

    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.

          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  z) (shN  N) (∀̇∈ (var i0) (var i0 ∈̇ var (sh  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.

           (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.

module ApproxRead {m : ℕ} (f b z : Fin m) (N : Fin  → 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.

    stepBody : Formula S ( + m)
    stepBody = stepAt i0 i1 (sh  f) (sh  z) (shN  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.

  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.

    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.

    step : (c : V ℓ) → ((y : V ℓ) → ⟨ y ∈ c ⟩ → P y) → P c
    step c IH c∈ w rec =
      StepRead.step-out i0 i1 (sh  f) (sh  z) (shN  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.

      cS : S
      cS = down (lookup b γ) c c∈
      q : S
      q = down (lookup f γ) (pr c (fst w)) rec
      env : S ^ ( + 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.

      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.

      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.

    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.

    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.

  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.

    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.

    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.

    dom : ⟨ γ ⊨ ∀̇∈ (var b) (∃̇∈ (var (sh  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.

      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.

    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.

          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  f) (sh  z) (shN  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.

           (λ 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.

module HierRead {m : ℕ} (a p f z : Fin m) (N : Fin  → 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.

  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.

  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.

    , 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.

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.

  N14 : Fin  → Fin 
  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.

  ff aa pp zz : Fin 
  ff = sh  (i0 {})
  aa = sh  (i0 {})
  pp = sh  (i0 {})
  zz = sh  (i0 {})

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.

  opaque
    inner : Formula S 
    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.

  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 ℓ).

    Δ₀-inner : Δ₀ inner
    Δ₀-inner = checkΔ₀ inner tt

The readings of the sealed formula are exposed through the same unfolding boundary.

  opaque
    unfolding inner

The outward reading of the conjunction is the pair of its two conjuncts, since conjunction is a pair of propositions.

    inner-out : (γ : S ^ ) → ⟨ γ ⊨ 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.

    inner-in : (γ : S ^ ) → ⟨ γ ⊨ 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.

  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.

  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.

  δ-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.

  s13 = wrap {} inner
  s12 = wrap {} s13
  s11 = wrap {} s12
  s10 = wrap {}  s11
  s9  = wrap {}  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.

  s8  = wrap {}  s9
  s7  = wrap {}  s8
  s6  = wrap {}  s7
  s5  = wrap {}  s6
  s4  = wrap {}  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.

  three : Formula S 
  three = wrap {} 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.

  Δ₀-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.

  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.

    count-three : countFo three ≡ 
    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.

  erased : Formula (⊥* {ℓ-suc ℓ}) 
  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 Δ₀.

  Δ₀-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.

  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.

  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.

levelFo : Formula (⊥* {ℓ-suc ℓ}) 
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.

Δ₀-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.

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.

  ∙ 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.

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.

          (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.

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.

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.

    finish : (γ : S ^ ) → ⟨ γ ⊨ 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.

      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.

    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.

      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.

      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.

      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.

        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.

        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.

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.

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.

    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.

      ∅∈λ : ⟨ ∅ ∈ 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.

      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.

      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.

      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.

      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.

    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.