--- title: "The index of the least constructible stage" module: L.Stage lang: en site: "Bedrock" description: "The index of the least constructible stage" stage: "Constructible stages and the axioms" reading_order: 30 canonical: https://bedrock.institute/en/L.Stage.html html: L.Stage.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Stage.lagda.md prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, V.Hierarchy, L.Constructible, L.Ordinal.Linear] routes: [constructible-axioms] translations: [https://bedrock.institute/zh/L.Stage.md, https://bedrock.institute/ja/L.Stage.md] agent_guide: /llms.txt license: CC-BY-NC-SA-4.0 --- # The index of the least constructible stage Every constructible set x belongs to `Lset α` for at least one ordinal α. This chapter turns that mere existence into a canonical bound: the least ordinal whose stage contains x. The construction first solves a more general problem. For any hProp-valued property P of ordinals, a well-founded descent finds its least witness, while ordinal trichotomy proves that the resulting witness is unique. The descent begins at any ordinal satisfying P. At α it asks whether some smaller ordinal β ∈ α also satisfies P. A positive answer invokes the induction result at β; a negative answer proves α minimal. Membership induction makes this definition well founded. Both the assertion of a smaller witness and the initial witness are propositionally truncated, but `LeastOrd P` is itself a proposition, so each truncation may be eliminated into that complete package. Specializing P σ to x ∈ Lset σ gives `stage x hx`. Its accompanying theorems state that this index is an ordinal, that its stage contains x, and that no smaller ordinal stage contains x. The proof uses excluded middle only to decide the existence of a smaller witness and to compare two candidate ordinals. Work at a fixed universe level ℓ and assume excluded middle at level ℓ-suc ℓ. The assumption will be used in two mathematically distinct ways: `ord-tri` compares ordinal candidates, while the descent decides the hProp asserting that a smaller candidate exists. ```agda {-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import Base.Classical using ( LEM ) module L.Stage {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where ``` Membership supplies both the strict order on ordinals and its well-founded induction principle. Constructibility supplies the predicate IsOrd, the stage family Lset and the assertion isL x that x occurs in some ordinal-indexed stage. Thus the same membership relation controls descent among candidate indices and, after specialization, membership of x in a stage. ```agda open import FOL.ZFStructure using ( module hPropStructure ) open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-induction ) open import L.Constructible {ℓ} using ( IsOrd; isPropIsOrd; Lset; isL ) open import L.Ordinal.Linear {ℓ} lem using ( ord-tri ) open import Cubical.Data.Sum using ( _⊎_; inl; inr ) ``` The assertion that a smaller witness exists is represented by a propositionally truncated existential. It records existence without exposing a chosen β. The eliminator `PT.rec` can use such evidence only when the target is a proposition; the uniqueness proof below supplies exactly this fact for `LeastOrd P`. Products and dependent function spaces preserve propositionhood, which will also show that the evidence attached to a fixed ordinal index is unique. ```agda import Cubical.Data.Empty as Empty import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∣_∣₁; ∥_∥₁ ) open import Cubical.Functions.Logic using ( ∃[∶]-syntax ) open import Cubical.Data.Sigma using ( Σ≡Prop ) ``` A property P is a map into Ω, the type of hProps. Hence `⟨ P α ⟩` is its underlying proposition at α, and `snd (P α)` proves that any two of its witnesses agree. This propositionhood is needed when equality of ordinal indices is lifted to equality of complete least-witness packages. ```agda open import Cubical.Foundations.HLevels using ( isProp×; isPropΠ ) open hPropStructure 𝒮ᵥ ``` ## The least ordinal satisfying a property For a property `P` of ordinals, `LeastOrd P` packages an ordinal α satisfying `P` together with the proof that no smaller ordinal satisfies it. This definition concerns the ordinal index itself; only the later specialization `P σ = (x ∈ Lset σ)` turns such an index into the index of a constructible stage. Uniqueness uses the fact that the property takes values in an `hProp`: the two candidates are compared by trichotomy, each strict direction is refuted by the other's minimality, and the remaining components are propositions, so the equality of the ordinals is the equality of the packages. Leastness is stated as a refutation: `isLeastOrd α` is the assertion, for every set γ, that γ cannot be an ordinal satisfying P with γ ∈ α. Minimality by contradiction is the right shape here because the strict order on ordinals is read off membership; there is no smaller-ordinal value to return, only an impossible situation to derive. The full package `LeastOrd` then bundles an ordinal, its ordinalhood, a proof of P at it, and this minimality clause. ```agda module _ (P : S → hProp (ℓ-suc ℓ)) where isLeastOrd : S → Type (ℓ-suc ℓ) isLeastOrd α = (γ : S) → IsOrd γ → ⟨ P γ ⟩ → ⟨ γ ∈ˢ α ⟩ → Empty.⊥ LeastOrd : Type (ℓ-suc ℓ) LeastOrd = Σ[ α ∈ S ] (IsOrd α × ⟨ P α ⟩ × isLeastOrd α) ``` To prove two such packages equal, compare their ordinal indices first. Trichotomy delivers one of three cases: α ∈ α′, α = α′, or α′ ∈ α. The plan is to eliminate both strict cases by contradiction and keep the equality case; `decide` is the function turning that trichotomy result into a path α ≡ α′. Crucially, this argument shows the indices equal; the packages are dependent pairs over the index, so an equality of packages is not yet obtained from an equality of indices alone. ```agda isPropLeastOrd : isProp LeastOrd isPropLeastOrd (α , ordα , pα , leastα) (α' , ordα' , pα' , leastα') = Σ≡Prop propRest α≡α' where decide : (⟨ α ∈ˢ α' ⟩ ⊎ ((α ≡ α') ⊎ ⟨ α' ∈ˢ α ⟩)) → α ≡ α' ``` Each strict case contradicts minimality, but minimality of the *other* candidate. If α were a member of α′, then α is an ordinal satisfying P that lies strictly below α′, and `leastα'` refutes exactly that; the case α′ ∈ α is symmetric, using `leastα`. The middle case is the path itself. Feeding `ord-tri`'s verdict into `decide` thus yields the path `α≡α'`, and note that no assumption about P beyond its values being propositions was used so far. ```agda decide (inl α∈α') = Empty.rec (leastα' α ordα pα α∈α') decide (inr (inl e)) = e decide (inr (inr α'∈α)) = Empty.rec (leastα α' ordα' pα' α'∈α) α≡α' : α ≡ α' α≡α' = decide (ord-tri α ordα α' ordα') ``` It remains to lift the path of indices to a path of packages, and this uses propositionhood of the dependent remainder. The component that varies with the index is `IsOrd β × ⟨ P β ⟩ × isLeastOrd β`; `IsOrd β` is a proposition by the constructible chapter, `⟨ P β ⟩` is a proposition because P is hProp-valued, and `isLeastOrd β` is a function type into the empty type, hence a proposition by `isPropΠ` iterated. So `propRest β` certifies propositionhood of the whole remainder, and `Σ≡Prop` turns the base path into the required equality of packages: once the index agrees, the dependent remainder cannot disagree. ```agda propRest : (β : S) → isProp (IsOrd β × ⟨ P β ⟩ × isLeastOrd β) propRest β = isProp× (isPropIsOrd β) (isProp× (snd (P β)) (isPropΠ λ _ → isPropΠ λ _ → isPropΠ λ _ → isPropΠ λ _ → Empty.isProp⊥)) ``` ## Descent to the least ordinal Starting from any ordinal satisfying `P`, `leastOrdBelow` asks whether a strictly smaller ordinal also satisfies `P` and recurses when one does. Membership induction defines the result from the results at strictly smaller ordinals, yielding the least ordinal satisfying `P`, before the construction is specialized to constructible stages. The result being a proposition, the starting ordinal may be given truncated, and that is the form the callers have: they know a suitable ordinal exists without having chosen one. The descent is organized as well-founded induction on membership, the principle `∈-induction` from the hierarchy chapter. Its step receives an ordinal α, its ordinalhood, a proof of P at α, and an induction hypothesis valid for every strictly smaller member β: provided β is again an ordinal satisfying P, the globally least P-witness obtained by starting the induction at β is already available. The step's only job is to decide, at α, whether the descent must continue or has arrived. ```agda leastOrdBelow : (α : S) → IsOrd α → ⟨ P α ⟩ → LeastOrd leastOrdBelow = ∈-induction step where step : (α : S) → (∀ β → ⟨ β ∈ˢ α ⟩ → IsOrd β → ⟨ P β ⟩ → LeastOrd) → IsOrd α → ⟨ P α ⟩ → LeastOrd ``` The question to decide is `Smaller`: merely whether there exists a β with β ∈ α, ordinal, and satisfying P, all packaged with conjunctions into a single hProp. Two features matter. First, the existential is truncated: `Smaller` carries no chosen β, only the assertion that one exists. Second, excluded middle at level ℓ-suc ℓ, applied via `lem`, decides this question outright, delivering either an inhabitant of the truncation or a refutation. This is precisely where the classical assumption enters the descent. ```agda step α IH ordα pα = decide (lem Smaller) where Smaller : hProp (ℓ-suc ℓ) Smaller = ∃[ β ∶ S ] ((β ∈ˢ α) ⊓ ((IsOrd β , isPropIsOrd β) ⊓ P β)) decide : (⟨ Smaller ⟩ ⊎ (⟨ Smaller ⟩ → Empty.⊥)) → LeastOrd ``` The two branches of the decision build the answer directly. In the positive branch, the truncated witness cannot be taken apart into data, but `PT.rec` may eliminate it into any proposition, and `LeastOrd` is one: so the witness is converted, without being chosen, into the globally least package supplied by the induction hypothesis at β. In the negative branch there is no smaller witness at all, so α itself is least. Recursion happens only through `∈-induction`'s controlled induction hypothesis. ```agda decide (inl ∃β) = PT.rec isPropLeastOrd (λ { (β , (β∈α , (ordβ , pβ))) → IH β β∈α ordβ pβ }) ∃β decide (inr ¬∃β) = α , ordα , pα , leastProof where leastProof : isLeastOrd α ``` The negative branch's minimality clause is where the refutation earns its keep: given any γ below α that is an ordinal satisfying P, the witness `(γ , γ∈α , ordγ , pγ)` is packaged into the very truncation `Smaller` that was denied, and applying `¬∃β` to it yields the required contradiction. Finally, `leastOrd` handles the form callers actually have: an ordinal satisfying P merely exists. Again the elimination into `LeastOrd` is licensed by its propositionhood, proved in the previous section, so a truncated existence is refined into the canonical least index without eliminating the truncation into an arbitrary data type. ```agda leastProof γ ordγ pγ γ∈α = ¬∃β ∣ γ , (γ∈α , (ordγ , pγ)) ∣₁ leastOrd : ∥ (Σ[ α ∈ S ] (IsOrd α × ⟨ P α ⟩)) ∥₁ → LeastOrd leastOrd = PT.rec isPropLeastOrd (λ { (α , (ordα , pα)) → leastOrdBelow α ordα pα }) ``` ## The stage-index function For `P σ = (x ∈ Lset σ)`, the descent returns the least ordinal index α whose stage `Lset α` contains `x`. The function `stage` selects α, `stage-ord` proves that it is an ordinal, and `stage-mem` and `stage-earliest` relate that index to its stage. The index is exposed through three stable facts rather than its recursive construction: it is an ordinal, its stage contains x, and it is minimal among ordinal indices with that property. Declaring `stage` opaque preserves this abstraction boundary. A constructibility certificate `⟨ isL x ⟩` is exactly the input form `leastOrd` expects: by the class's definition in the constructible chapter, an element of `isL x` is merely a pair of an ordinal σ, its ordinalhood, and a membership `x ∈ˢ Lset σ`. So the property `λ σ → x ∈ˢ Lset σ` satisfies the hypotheses of the descent, and `theEarliest` applies `leastOrd` to this property. Thus constructibility supplies exactly the truncated existence premise needed to obtain a least stage index. ```agda theEarliest : (x : S) → ⟨ isL x ⟩ → LeastOrd (λ σ → x ∈ˢ Lset σ) theEarliest x = leastOrd (λ σ → x ∈ˢ Lset σ) opaque stage : (x : S) → ⟨ isL x ⟩ → S stage x p = theEarliest x p .fst ``` The package `theEarliest x p` contains the least index together with its three proofs. The function `stage` projects the index and keeps its recursive construction opaque, so later arguments use its ordinalhood, membership and minimality. It is an ordinal-valued function of a constructible set and its witness; it is neither a universe level nor the rank function. ```agda opaque unfolding stage stage-ord : (x : S) (p : ⟨ isL x ⟩) → IsOrd (stage x p) stage-ord x p = theEarliest x p .snd .fst stage-mem : (x : S) (p : ⟨ isL x ⟩) → ⟨ x ∈ˢ Lset (stage x p) ⟩ ``` The three theorems are the interface, each a projection of the package. `stage-ord` states that the chosen index is an ordinal, so it can later be compared with other indices. `stage-mem` places `x` in the stage `Lset (stage x p)`, the membership fact established by the descent. `stage-earliest` recovers the minimality clause itself: no smaller ordinal σ has `x ∈ˢ Lset σ`. Together they say that `stage x p` is precisely the least index promised at the head of the chapter, reached by projection rather than by reopening the recursion. ```agda stage-mem x p = theEarliest x p .snd .snd .fst stage-earliest : (x : S) (p : ⟨ isL x ⟩) → isLeastOrd (λ σ → x ∈ˢ Lset σ) (stage x p) stage-earliest x p = theEarliest x p .snd .snd .snd ``` ## Recap `leastOrd` extracts the least ordinal satisfying a property from a truncated existence witness. Its specialization `stage x hx` returns the ordinal index α of the least `Lset α` containing `x`; `stage-ord`, `stage-mem`, and `stage-earliest` state exactly those facts. Later arguments can therefore compare or bound these ordinal indices and then use the corresponding constructible stages.