Injecting an infinite constructible stage into its index

This chapter proves the stage estimate used in GCH: if δ is a non-finite constructible ordinal, then Lset δ admits an internal coded injection into δ. The conclusion InjL is the propositional truncation of the type of constructible graphs satisfying the injection conditions. Thus it asserts that such a graph exists, without retaining a chosen graph; it asserts neither a host-level function nor a bijection, and it does not assume that δ is itself an internal cardinal.

{-# OPTIONS --cubical --safe --guardedness #-}

The proof repeatedly separates existence from choice. Classical reasoning supplies suitable stages and cardinal representatives, while every exported injection remains under propositional truncation. Local witnesses may therefore be used inside propositional arguments without turning them into canonical global data.

open import Base.Prelude
open import Base.Classical using ( LEM )

The argument is uniform in the universe level and uses only the displayed instance lem : LEM (ℓ-suc ℓ) of excluded middle. In particular, the later passage to an internal cardinal representative does not add a hidden assumption that the original ordinal δ is a cardinal.

module L.GCH.StageInjection {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

To turn the inverse collapse into an injection inside L, its graph must be expressed in the first-order language of the constructible structure. Only variables, constants, membership, and conjunction are needed. Formula renaming will exchange the two argument positions while preserving satisfaction, and the ambient cumulative hierarchy supplies the sets on which the collapse is computed.

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; con; _∈̇_; _∧̇_ )
open import FOL.Manipulation.Renaming using ( renameFo; module Sat )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )

The collapse will be injective because the hull carries the required extensionality. Later, self∈sucV places δ in its set-theoretic successor δ+1, while the constructible-stage lemmas provide transitivity, monotonicity, and the passage between a stage and its layers. Ordinal successors are kept distinct from successor stages throughout this argument.

open import V.Collapse {ℓ} using ( isExt )
open import V.Model {ℓ} using ( self∈sucV )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-mono; Lset-layer; layer-trans )
open import L.Ordinal {ℓ} using ( #∈ω; suc-ord )

Two complementary stage facts will be used. A constructible stage can be packaged as an element of L, and if an ordinal x belongs to the stage Lset α, then rank comparison yields x ∈ α. The target InjL records the mere existence of an internal coded injection, while IsCardinalL will apply only to the cardinal representative introduced later.

open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset→∈ )
open import L.Axioms.Basic {ℓ} using ( LsetS )
open import L.Axioms.Numerals {ℓ} using ( sucʟ; sucʟ-fst )
open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem )
open import L.Cardinal {ℓ} lem using ( InjL; IsCardinalL )

The desired estimate has the interface StageCountedCoded. Its proof first replaces the arbitrary infinite ordinal δ by an internal cardinal representative μ, counts a suitable Skolem hull into μ, and then composes coded injections. To make the inverse collapse participate in this chain, it will be presented as a definable map whose graph is a set of L.

open import L.GCH.Assembly {ℓ} lem using ( StageCountedCoded )
open import L.InjectionComposition {ℓ} lem using ( inclusion-coded; injl-trans )
open import L.GCH.CardinalRepresentative {ℓ} lem using ( cardOf )
open import L.DefinableInjection {ℓ} lem using ( DefinableMap; module Inj )
open import L.GCH.SkolemHull {ℓ} lem

The global comparison will combine three ingredients. Condensation turns a hull into a stage Lset β; the shift for non-finite ordinals and the cardinal representative μ make the starting set injectable into μ; and composition transports these local comparisons back to the desired endpoints. None of these steps changes an internal coded injection into a host-level function.

  using ( module Frame; module HullStage; module HullElemDown )
open import L.GCH.ConstructibleHull {ℓ} lem using ( module PiIn; module Condense′ )
open import L.GCH.CardinalSquareLaw {ℓ} lem using ( ordL; ω⊆; no-fin; module Shift )
open import L.GCH.AdequateStages {ℓ} lem using ( superadequate-above; Superadequate )
open import L.GCH.StageCountingTools {ℓ} lem using ( move )

The hull-count theorem is the quantitative input: once its starting set injects into a non-finite internal cardinal, the generated hull does too. We will also use that every ordinal is contained in its own constructible stage, and that equality of the underlying sets determines equality of elements of the constructible carrier because their constructibility proofs are propositions.

open import L.GCH.HullCounting {ℓ} lem using ( ord⊆Lset; module Count; S≡ )

The inverse collapse will be compared as a map between elements of the constructible carrier S. Such an element includes both an underlying set and a constructibility proof, but the proof component is propositional. Consequently, equality of underlying sets determines equality in S, so the coded graph does not depend on which constructibility evidence presents its values.

open import Cubical.Data.Sigma using ( _×_; Σ≡Prop )
open import Cubical.Foundations.Prelude using ( subst2 )
open import Cubical.Foundations.HLevels using ( isProp× )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ∈∈ₛ )

Non-finiteness enters the later counting argument in two concrete ways. It provides the shift injection δ+1 ↪ δ, and it implies that every finite ordinal, in particular the empty set, lies below δ. The length-two environments used for the inverse-collapse formula are independent of this infinitude argument.

open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet; ∅ )
open InfinitySet {ℓ} using ( ω; sucV )
open import Cubical.Data.Vec using ( _∷_; [] )
import Cubical.Data.Empty as Empty

Propositional truncation appears at two decisive points. It lets the proof use the mere constructibility of the hull when establishing a propositional satisfaction statement, and it is also the outer form of every conclusion InjL. Elimination is therefore always into a proposition.

import Cubical.HITs.PropositionalTruncation as PT
open PT using ( squash₁ )

Membership written _∈ˢ_ is membership in the ambient hierarchy structure 𝒮ᵥ. It is used for statements about the hull, its collapse image, and ordinal indices before those sets are packaged as elements of the constructible structure.

open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )

The type S is the carrier of the constructible structure: an element consists of an ambient set together with a proof that it belongs to L. Domains, codomains, and graph parameters of the internal coded maps below all live in this carrier.

open hPropStructure 𝒮ʟ using ( S )

Satisfaction of an object-language formula in 𝒮ʟ is read through absoluteness as the corresponding proposition about ambient sets. This bridge lets the proof establish the inverse-collapse graph externally and then package the same relation as a definable graph inside L.

open FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using () renaming ( _⊨ᵐ_ to _⊨_ )

There is one small mismatch of conventions to resolve. The collapse formula piFo is read with its value and preimage in the order (v,x), whereas the definable-map graph is evaluated in the order (x,v). Swapping the two free variables and using invariance of satisfaction under renaming expresses the same relation in the required order; no model or formula meaning is changed.

module Ren = Sat 𝒮ʟ id using ( Agrees; ⊨-rename )

Counting the hull at a strengthened adequate stage

We first isolate the geometric part of the argument from its later cardinal estimate. Fix an ordinal lam closed under successors and a starting set X contained in Lset lam; assume also that the index contains the empty set and that the Skolem hull generated from X is elementary in the required sense. No target cardinal is involved at this point.

module Site (lam : V ℓ) (ordλ : IsOrd lam)
  (succλ : (d : V ℓ) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩)
  (X : V ℓ) (X⊆Lλ : (z : V ℓ) → ⟨ z ∈ˢ X ⟩ → ⟨ z ∈ˢ Lset lam ⟩)
  (∅∈λ : ⟨ ∅ ∈ˢ lam ⟩)
  (elem : Frame.A.Elementary lam ordλ succλ X X⊆Lλ ∅∈λ)

Superadequacy of lam supplies the closure and correctness conditions required by condensation. Constructibility of X ensures that the successive finite closure stages used to generate the hull, and hence their union, remain in L. The hull and its collapse image can therefore both be represented inside the constructible structure.

  (sup : Superadequate lam)
  (X-isL : ⟨ isL X ⟩) where

Condensation now identifies the collapse image with Lset β for some ordinal β. Independently, the hull construction proves that the hull M is constructible. These are exactly the two facts needed to regard the inverse collapse as a map from a constructible stage to a constructible hull.

  condenses′ = Condense′.condenses′ lam ordλ succλ X X⊆Lλ ∅∈λ elem sup X-isL
  M-isL = Condense′.M-isL lam ordλ succλ X X⊆Lλ ∅∈λ elem sup X-isL

Write π : M → πX for the collapse and πX for its image. The collapse machinery supplies preimages of points in πX, injectivity on the extensional hull, and the fact that transitive parts of the hull are fixed. The formula piFo represents the graph of π; its adequacy lemmas will connect satisfaction of that formula with the actual collapse value.

  module HS = HullStage lam ordλ succλ X X⊆Lλ ∅∈λ using ( M )
  module HSH = HullStage.H lam ordλ succλ X X⊆Lλ ∅∈λ using ( X⊆M )
  module HSC = HullStage.C lam ordλ succλ X X⊆Lλ ∅∈λ
    using ( πX; π; fixes; πX-intro; πX-member )
  module P = PiIn (HS.M , M-isL) using ( piFo; up; good-at; piFo-val )

The ordinal β measures the height of the collapse image. At this general site there is no ordinal δ to be counted and no target cardinal, so no comparison between β and either of them is available yet.

  β : V ℓ
  β = condenses′ .fst

The accompanying proof that β is an ordinal makes Lset β a genuine ordinal-indexed stage. It will also be essential later when membership of an ordinal in Lset β is converted into an ordinal comparison with β.

  oβ : IsOrd β
  oβ = condenses′ .snd .fst

The equality ext : πX = Lset β is the hinge between collapse theory and the constructible hierarchy. It converts membership in the collapse image into membership in the stage at β; later, once the collapse is shown to fix δ, this is exactly how δ ∈ Lset β will be obtained.

  ext : HSC.πX ≡ Lset β
  ext = condenses′ .snd .snd

Because β is an ordinal, Lset β is constructible and can be packaged as an element Lβ of the carrier S. This packaged stage will be the domain of the inverse-collapse map.

  Lβ : S
  Lβ = LsetS β oβ

The ordinal β itself is also constructible and is packaged as βL. Although the inverse-collapse map uses Lβ, the packaged index will later let the bounded-subset argument compare β with a target cardinal by an internal coded injection.

  βL : S
  βL = ordL β oβ

An internal coded map must have a codomain in the carrier S, not merely an externally described class of hull members. The element hullL supplies that internal presentation of the hull together with its constructibility evidence.

  hullL : S
  hullL = Condense′.hullL lam ordλ succλ X X⊆Lλ ∅∈λ elem sup X-isL

The equality M≡ connects the two presentations of the hull. Collapse theorems speak about the ambient set M, whereas the internal graph speaks about the carrier element hullL; transporting along this equality lets the same membership evidence serve on both sides.

  M≡ : fst hullL ≡ HS.M
  M≡ = Condense′.hullL-spec lam ordλ succλ X X⊆Lλ ∅∈λ elem sup X-isL

The hull frame proves that membership on M is extensional. This is the precise hypothesis needed to deduce that two members of the hull with the same collapse value are equal.

  Mext : isExt HS.M
  Mext = Frame.Mext lam ordλ succλ X X⊆Lλ ∅∈λ

Applying the collapse injectivity theorem to this extensional hull yields π-inj. It will prove both uniqueness of each preimage and injectivity of the inverse-collapse map constructed from those preimages.

  module CI = HullStage.C.InjExt lam ordλ succλ X X⊆Lλ ∅∈λ Mext using ( π-inj )

A preimage of a collapse value v is an element x of the hull whose collapse equals the underlying set of v. The record is an untruncated dependent pair: both the preimage and its membership and its identification are carried explicitly.

  Pre : S → Type (ℓ-suc ℓ)
  Pre v = Σ[ x ∈ V ℓ ] (⟨ x ∈ˢ HS.M ⟩ × (HSC.π x ≡ fst v))

Preimages are unique, because the collapse is injective on the hull: two records with the same value identify their preimages through π-inj, and the remaining components are propositions. This is why the preimage can be recovered without choosing it.

  isPropPre : (v : S) → isProp (Pre v)
  isPropPre v (x , mx , e) (x' , mx' , e') =
    Σ≡Prop (λ x → isProp× (snd (x ∈ˢ HS.M)) (setIsSet _ _)) (CI.π-inj x x' mx mx' (e ∙ sym e'))

The inverse collapse is required only for points of its image, which condensation identifies with Lset β. Accordingly, Mem v is the proposition that the underlying set of v belongs to this stage; this domain evidence is what produces an inhabited preimage type.

  Mem : S → Type (ℓ-suc ℓ)
  Mem v = ⟨ fst v ∈ˢ fst Lβ ⟩

Membership in Lset β gives only the propositionally truncated type of preimages under the collapse. Since Pre v has already been proved to be a proposition, truncation elimination recovers its unique inhabitant. Thus pre uses uniqueness to obtain the inverse value; it makes no arbitrary choice among competing preimages.

  pre : (v : S) → Mem v → Pre v
  pre v m = PT.rec (isPropPre v) (λ w → w)
    (HSC.πX-member (fst v) (subst (λ w → ⟨ fst v ∈ˢ w ⟩) (sym ext) m))

The preimage is packaged as a constructible set: its constructibility is transported from the hull through the identification of the packaged hull with the hull itself. The function is defined only on members of the stage at β, with the hull as its codomain; it is the inverse of the collapse on its image, not a global inverse.

  fn : (v : S) → Mem v → S
  fn v m = pre v m .fst
         , isL-trans {x = fst hullL} {y = pre v m .fst}
             (subst (λ w → ⟨ pre v m .fst ∈ˢ w ⟩) (sym M≡) (pre v m .snd .fst)) (snd hullL)

The renaming swaps the two variable slots: slot zero becomes slot one and conversely.

  ρ : Fin  → Fin 
  ρ zero = suc zero
  ρ (suc zero) = zero

The two environments list the same carrier elements in opposite orders. The proof ag checks at each of the two variable indices that looking up a variable after applying ρ agrees with looking it up in the swapped environment. This pointwise agreement is the hypothesis needed by satisfaction under renaming.

  private
    ag : (x v : S) → Ren.Agrees ρ (x ∷ v ∷ []) (v ∷ x ∷ [])
    ag x v zero = refl
    ag x v (suc zero) = refl

Satisfaction of the renamed formula at the ordered environment equals satisfaction of the original formula at the swapped environment; this is the transport used to arrange the collapse graph's slots.

    rn : (x v : S) → ⟨ (x ∷ v ∷ []) ⊨ renameFo ρ P.piFo ⟩ ≡ ⟨ (v ∷ x ∷ []) ⊨ P.piFo ⟩
    rn x v = cong ⟨_⟩ (Ren.⊨-rename ρ P.piFo (x ∷ v ∷ []) (v ∷ x ∷ []) (ag x v))

The inverse-collapse graph is the conjunction: the preimage belongs to the hull, and the renamed pairing graph holds of the preimage and the value.

  invFo : Formula S 
  invFo = (var zero ∈̇ con hullL) ∧̇ renameFo ρ P.piFo

For a hull member x whose collapse is v, the actual pair (v,x) satisfies piFo. Constructibility of the hull is itself given through a propositional truncation, so the proof eliminates that truncation into the satisfaction statement, which is a proposition, and works at any constructible stage containing the hull.

  π-graph : (x : S) (mx : ⟨ fst x ∈ˢ HS.M ⟩) (v : S) → HSC.π (fst x) ≡ fst v
          → ⟨ (v ∷ x ∷ []) ⊨ P.piFo ⟩
  π-graph x mx v e = PT.rec (snd ((v ∷ x ∷ []) ⊨ P.piFo)) read M-isL
    where
    read : Σ[ α ∈ V ℓ ] (IsOrd α × ⟨ HS.M ∈ˢ Lset α ⟩) → ⟨ (v ∷ x ∷ []) ⊨ P.piFo ⟩

The read statement transports both slots: the collapse value is identified with the underlying set of v, and the hull member is identified with the underlying set of x.

    read (α , oα , M∈Lα) =
      subst2 (λ a b → ⟨ (a ∷ b ∷ []) ⊨ P.piFo ⟩)
        (S≡ {x = HSC.π (fst x) , G .fst} {y = v} e) (S≡ {x = P.up (fst x) mx} {y = x} refl)
        (G .snd mx)
      where

Given a constructible stage Lset α containing the hull, transitivity of the layer places each hull member x in that same stage. The lemma good-at then supplies a constructibility proof for π x together with a proof that the packaged collapse value and the packaged member satisfy piFo.

      G = P.good-at α oα (fst x) mx (layer-trans (Lset-layer α) {x = HS.M} {y = fst x} mx M∈Lα)

The proof defines is the bridge from the actual inverse value to the internal formula. Its first component places that value in the packaged hull, and its second component uses the collapse equation together with renaming to show that invFo relates the value to its image point.

  defines : (v : S) (m : Mem v) → ⟨ (fn v m ∷ v ∷ []) ⊨ invFo ⟩
  defines v m =
      subst (λ w → ⟨ pre v m .fst ∈ˢ w ⟩) (sym M≡) (pre v m .snd .fst)
    , transport (sym (rn (fn v m) v)) (π-graph (fn v m) (pre v m .snd .fst) v (pre v m .snd .snd))

Only the preimage is left to identify: any preimage satisfying the inverse graph has the same collapse value as the packaged preimage, and the injectivity of the collapse returns the equality of the two preimages.

  only : (v : S) (m : Mem v) (x' : S) → ⟨ (x' ∷ v ∷ []) ⊨ invFo ⟩ → x' ≡ fn v m
  only v m x' (hx , hp) = S≡ (CI.π-inj (fst x') (pre v m .fst) mx' (pre v m .snd .fst)
    (sym (P.piFo-val x' mx' v (transport (rn x' v) hp)) ∙ sym (pre v m .snd .snd)))
    where
    mx' : ⟨ fst x' ∈ˢ HS.M ⟩

For an alternative output x' satisfying the graph, the first conjunct says that its underlying set belongs to the packaged hull. Transport along M≡ turns this into membership in the ambient hull M, which is the premise needed to compare x' with the recovered preimage by collapse injectivity.

    mx' = subst (λ w → ⟨ fst x' ∈ˢ w ⟩) M≡ hx

These results internalize the restricted inverse as a single-valued definable map. Every v ∈ Lβ is sent into the hull and satisfies invFo, while only shows that any other output satisfying the same graph is equal to this value. Injectivity is a further property and is proved separately next.

  Dmap : DefinableMap
  Dmap = record
    { dom = Lβ ; cod = hullL ; fn = fn
    ; into = λ v m → subst (λ w → ⟨ pre v m .fst ∈ˢ w ⟩) (sym M≡) (pre v m .snd .fst)
    ; graph = invFo ; defines = defines ; only = only }

Each uniquely determined preimage satisfies π(pre(v)) = v. Hence, if the two values of the inverse-collapse map are equal, applying π to that equality and composing with the two preimage equations gives v = v'. Thus the inverse on the collapse image is injective; this step uses the right-inverse equations rather than injectivity of the collapse.

  inj : (v : S) (m : Mem v) (v' : S) (m' : Mem v') → fst (fn v m) ≡ fst (fn v' m') → fst v ≡ fst v'
  inj v m v' m' q = sym (pre v m .snd .snd) ∙ cong HSC.π q ∙ pre v' m' .snd .snd

The restricted inverse is packaged as a coded injection from Lβ into the hull, completing the first section's construction. The packaging preserves the truncated form, so only the existence of a coded graph is exposed.

  Lβ↪M : InjL Lβ hullL
  Lβ↪M = Inj.injL Dmap inj

Collapsing the hull back to the original stage

The counting module At fixes a non-finite constructible ordinal δL, its ordinality, and its exclusion from ω; an internal cardinal representative μ with the same non-finiteness; and two coded injections between δL and μ in both directions. These are exactly the data needed to count a non-finite stage by a cardinal representative.

module At (δL : S) (oδ : IsOrd (fst δL)) (δ∉ω : ⟨ fst δL ∈ˢ ω ⟩ → Empty.⊥)
          (μ : S) (oμ : IsOrd (fst μ)) (cμ : IsCardinalL μ)
          (μ∉ω : ⟨ fst μ ∈ˢ ω ⟩ → Empty.⊥)
          (δ↪μ : InjL δL μ) (μ↪δ : InjL μ δL) where

It is useful to separate the carrier element δL from its underlying ambient ordinal δ = fst δL. Set-theoretic successor, stage membership, and the collapse act on δ, while internal coded injections retain the packaged endpoint δL.

  δ : V ℓ
  δ = fst δL

The stage of the ordinal δ is the earliest constructible level containing it; here it provides the starting index for finding a sufficiently high superadequate level.

  private
    α₀ : V ℓ
    α₀ = stage δ (snd δL)

The least-stage construction always returns an ordinal index. Applied to the constructible set δ, this gives the ordinality of α₀; the argument does not derive it from the separate hypothesis that δ is an ordinal.

    oα₀ : IsOrd α₀
    oα₀ = stage-ord δ (snd δL)

The ordinal δ belongs to its own stage, which is the membership fact that anchors δ inside the constructible hierarchy.

    δ∈Lα₀ : ⟨ δ ∈ˢ Lset α₀ ⟩
    δ∈Lα₀ = stage-mem δ (snd δL)

A superadequate level above the stage index is obtained; it carries all the closure conditions needed for the Skolem hull construction and for the condensation transfer.

    sa = superadequate-above α₀ oα₀

Choose the strengthened adequate stage supplied above and denote its ordinal index by λ. All subsequent hull and condensation arguments take place at this one sufficiently high stage.

  opaque
    lam : V ℓ
    lam = sa .fst

The chosen high index λ is an ordinal. Its transitivity will first carry δ through the comparison δ ∈ α₀ ∈ λ, and will then place every member of δ+1 below λ.

    ordλ : IsOrd lam
    ordλ = sa .snd .fst

Successor closure is the second property of the index used immediately below: from δ ∈ λ it yields δ+1 ∈ λ. This is a statement about the ordinal index λ; it should not be confused with taking a successor constructible stage.

    succλ : (d : V ℓ) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩
    succλ = sa .snd .snd .snd .fst .snd .fst

Superadequacy says that above every member d of λ there merely exists an adequate stage γ that still belongs to λ. This supply of intermediate adequate stages provides the local reflection and closure used in counting and condensing the hull.

    sup : Superadequate lam
    sup = sa .snd .snd .snd .snd

First, δ ∈ Lset α₀ and the fact that both δ and α₀ are ordinals imply δ ∈ α₀. Since α₀ ∈ λ, transitivity of the ordinal λ then yields δ ∈ λ.

    δ∈λ : ⟨ δ ∈ˢ lam ⟩
    δ∈λ = ordλ .fst (ord∈Lset→∈ α₀ oα₀ δ oδ δ∈Lα₀) (sa .snd .snd .fst)

Take the starting set to be the von Neumann successor X = δ+1. It contains δ together with every smaller ordinal, and, because δ is an ordinal, X is transitive; these are exactly the features needed when the collapse is later shown to fix δ.

  X : V ℓ
  X = sucV δ

Successor closure of the ordinal index now gives X = δ+1 ∈ λ. This is an ordinal comparison. The stronger-looking statement needed by the hull construction, that every member of X lies in Lset λ, is derived separately in the next step.

  sucδ∈λ : ⟨ X ∈ˢ lam ⟩
  sucδ∈λ = succλ δ δ∈λ

If z ∈ X, transitivity of the ordinal λ and X ∈ λ give z ∈ λ. The general inclusion of an ordinal in its own constructible stage then yields z ∈ Lset λ. Hence the required premise is precisely X ⊆ Lset λ.

  X⊆Lλ : (z : V ℓ) → ⟨ z ∈ˢ X ⟩ → ⟨ z ∈ˢ Lset lam ⟩
  X⊆Lλ z hz = ord⊆Lset lam ordλ z (ordλ .fst hz sucδ∈λ)

Because δ is non-finite, every finite ordinal lies below δ; in particular ∅ ∈ δ. Combining this with δ ∈ λ and transitivity of the ordinal λ gives the separate hull premise ∅ ∈ λ.

  ∅∈λ : ⟨ ∅ ∈ˢ lam ⟩
  ∅∈λ = ordλ .fst (ω⊆ δ oδ δ∉ω ∅ (#∈ω zero)) δ∈λ

The starting set is constructible, because the coded successor of a constructible set is constructible, transported along the equation identifying the coded successor with the set-theoretic successor.

  X-isL : ⟨ isL X ⟩
  X-isL = subst (λ w → ⟨ isL w ⟩) (sucʟ-fst δL) (snd (sucʟ δL))

The constructibility proof turns the ambient set X = δ+1 into the carrier element XS. This changes only its presentation: the counting problem remains the problem of injecting the successor of δ into the cardinal representative μ.

  XS : S
  XS = X , X-isL

The start is counted by the chain δ+1 ↪ δ ↪ μ. The first coded injection is the shift available for every non-finite ordinal δ, and the second is the assumed internal injection from δ to its cardinal representative μ. Their composition gives InjL XS μ without assuming that δ itself is a cardinal.

  base : InjL XS μ
  base = injl-trans XS δL μ
    (move (sucʟ δL) XS δL δL (sucʟ-fst δL) refl (Shift.injL δL oδ δ∉ω))
    δ↪μ

The Skolem hull generated from X is elementary in the surrounding stage Lset λ. This elementarity is what lets the counting theorem and the condensation argument transfer the relevant formulas and witnesses between the hull and the stage.

  elem = HullElemDown.elem lam ordλ X X⊆Lλ ∅∈λ

The Skolem hull is counted by the cardinal representative μ, because the starting set already injects into μ and the hull chapter shows that closure preserves the counting.

  hull↪μ = Count.hull↪κ lam ordλ succλ X X⊆Lλ ∅∈λ elem sup X-isL μ oμ cμ μ∉ω base

Apply the general condensation construction to this hull. It supplies an ordinal β whose stage Lβ is the collapse image, presents the hull as a constructible set, and gives the propositionally truncated coded injection Lβ ↪ M obtained from the inverse collapse.

  module St = Site lam ordλ succλ X X⊆Lλ ∅∈λ elem sup X-isL
    using ( β; oβ; ext; Lβ; hullL; Lβ↪M )

For the remaining comparison, use three facts about this hull: its underlying set is M, every member of the start lies in M, and the collapse π maps M onto Lβ while fixing members of any transitive subset of M. Applied to the transitive start δ+1, these facts will place δ in Lβ.

  module HS = HullStage lam ordλ succλ X X⊆Lλ ∅∈λ using ( M )
  module HSH = HullStage.H lam ordλ succλ X X⊆Lλ ∅∈λ using ( X⊆M )
  module HSC = HullStage.C lam ordλ succλ X X⊆Lλ ∅∈λ
    using ( π; fixes; πX-intro )

The ordinal δ belongs to its own successor, which is the starting set for the hull construction.

  δ∈X : ⟨ δ ∈ˢ X ⟩
  δ∈X = self∈sucV δ

The ordinal δ therefore belongs to the hull, because the hull contains every member of the starting set.

  δ∈M : ⟨ δ ∈ˢ HS.M ⟩
  δ∈M = HSH.X⊆M δ δ∈X

The successor X = δ+1 is transitive and is contained in the hull M. The collapse therefore fixes every member of X; since δ ∈ X, it follows in particular that π(δ) = δ.

  πδ : HSC.π δ ≡ δ
  πδ = HSC.fixes X
    (λ a a∈ₛX → ∈∈ₛ {a = a} {b = HS.M} .fst (HSH.X⊆M a (∈∈ₛ {a = a} {b = X} .snd a∈ₛX)))
    (suc-ord oδ .fst) δ δ∈X

The ordinal δ lies inside the collapse level Lβ, because its collapse (which is itself) belongs to the collapse image, and the collapse image equals Lset β.

  δ∈Lβ : ⟨ δ ∈ˢ Lset St.β ⟩
  δ∈Lβ = subst (λ w → ⟨ w ∈ˢ Lset St.β ⟩) πδ
    (subst (λ w → ⟨ HSC.π δ ∈ˢ w ⟩) St.ext (HSC.πX-intro δ δ∈M))

The ordinal-stage bound now applies: when an ordinal δ belongs to Lset β, it must belong to the ordinal index β. Thus δ ∈ β. This is the strict comparison needed for monotonicity, and its direction places Lset δ inside Lset β.

  δ∈β : ⟨ δ ∈ˢ St.β ⟩
  δ∈β = ord∈Lset→∈ St.β St.oβ δ oδ δ∈Lβ

The canonical carrier presentation Lδ has underlying set Lset δ. It is the source used by At.result; the final theorem will later transport this source to any other carrier element whose underlying set is equal to the same stage.

  Lδ : S
  Lδ = LsetS δ oδ

The final comparison follows the chain Lset δ ↪ Lset β ↪ M ↪ μ ↪ δ. Its arrows come respectively from stage monotonicity using δ ∈ β, the inverse collapse, hull counting, and the assumed injection μ ↪ δ. Composing them proves InjL Lδ δL, the propositionally truncated existence of an internally coded injection from the stage at δ into δ.

  result : InjL Lδ δL
  result = injl-trans Lδ St.Lβ δL
    (inclusion-coded Lδ St.Lβ (λ z hz → Lset-mono {α = St.β} {β = δ} δ∈β hz))
    (injl-trans St.Lβ St.hullL δL St.Lβ↪M
      (injl-trans St.hullL μ δL hull↪μ μ↪δ))

For a general non-finite constructible ordinal δ, cardOf provides a cardinal representative only under propositional truncation. The proof works with a local representative μ inside the eliminator and applies At.result. This is legitimate because the target InjL Lδ δ is itself a propositionally truncated existence and hence a proposition. The resulting theorem is the stage-counting interface used later by both the GCH assembly and the bounded-subset argument; it proves only Lset δ ↪ δ, not GCH by itself.

stage-counted : StageCountedCoded
stage-counted δ Lδ oδ δ∉ω q = PT.rec squash₁ build (cardOf δ oδ)
  where
  build : Σ[ μ ∈ S ]
            ( IsOrd (fst μ) × IsCardinalL μ

A local cardOf witness records that μ is an ordinal and an internal cardinal, that its underlying set is contained in δ, and that coded injections exist in both directions. The containment proof is part of the representative package but is not needed by At.result; the construction uses the two injections together with ordinality, cardinality, and non-finiteness. Finally, move transports the source from the canonical LsetS (fst δ) oδ along q : fst Lδ = Lset (fst δ) to the presentation required by StageCountedCoded.

            × ((z : V ℓ) → ⟨ z ∈ˢ fst μ ⟩ → ⟨ z ∈ˢ fst δ ⟩)
            × InjL δ μ × InjL μ δ )
        → InjL Lδ δ
  build (μ , oμ , cμ , μ⊆δ , δ↪μ , μ↪δ) =
    move (LsetS (fst δ) oδ) Lδ δ δ (sym q) refl

It remains to justify the non-finiteness required by the hull-count theorem. If μ ∈ ω, the coded injection δ ↪ μ would inject the non-finite ordinal δ into a finite ordinal, contradicting δ ∉ ω; hence μ ∉ ω. With this last premise, At.result supplies exactly the propositionally truncated coded injection from the chosen presentation of Lset δ into δ.

      (At.result δ oδ δ∉ω μ oμ cμ μ∉ω δ↪μ μ↪δ)
    where
    μ∉ω : ⟨ fst μ ∈ˢ ω ⟩ → Empty.⊥
    μ∉ω h = no-fin δ μ oδ δ∉ω oμ h δ↪μ