This chapter completes the stated form of GCH inside L. For each infinite internal ordinal cardinal κ, it proves, under an outer propositional truncation, that there is a successor cardinal δ together with the two coded injections 𝒫κ ↪ δ and δ ↪ 𝒫κ. The proof may work with witnesses inside a truncated branch, but it exports neither a chosen δ nor either injection graph.

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

The only classical principle used in the assembly is excluded middle. It will turn a merely inhabited family of candidates into its unique least member, once the candidates have been placed in a small well-order.

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

We fix this hypothesis at the single universe level required by the proof. Thus every construction below, including the least-candidate argument, depends on the same explicit instance LEM (ℓ-suc ℓ).

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

Two set-theoretic viewpoints meet here. The ambient cumulative hierarchy supplies membership and small presentations, while the constructible subuniverse supplies the predicate isL and the stages Lset α; the ZF model structure later interprets the internal power set.

open import FOL.ZFStructure using ( module hPropStructure )
import FOL.ZFModel
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Presentation {ℓ} using ( member; fiber )
open import L.Constructible {ℓ}

The minimization argument uses three facts about ordinals: membership in an ordinal is transitive, any two ordinals satisfy trichotomy, and the membership order on the small presentation of an ordinal is a well-order. These facts let a least candidate found in a bounded search control every competing cardinal.

  using ( 𝒮ʟ; IsOrd; Lset; Lset-mono; isL; isL-trans )
open import L.Ordinal {ℓ} using ( mem-ord; suc-ord; ω-ord )
open import L.Ordinal.Linear {ℓ} lem using ( Tri; ord-tri )
open import L.Ordinal.SquareLaw {ℓ} lem using ( ordSWO )
open import L.WellOrder.Base {ℓₚ = ℓ-suc ℓ}

Internal size comparisons are expressed by InjL, the propositional truncation of a constructible graph coding an injection. From these comparisons, IsCardinalL defines internal cardinals and SuccCardL specifies the least internal ordinal cardinal strictly above a given one; CardAboveL supplies only some larger cardinal, still under truncation.

  using ( SWO; IsLeast; leastOf; module SWO )
open import L.Axioms.Basic {ℓ} using ( isL-Lset )
open import L.Cardinal {ℓ} lem
  using ( InjL; SuccCardL; IsCardinalL; module LeastCardInjL )
open import L.CardinalAbove {ℓ} lem using ( CardAboveL )

The final GCH statement asks for a successor cardinal together with coded injections in both directions between it and the model's power set. To construct the forward comparison, inclusions will first be coded as injections and then composed with the injection that counts a constructible stage.

open import L.GCH {ℓ} lem using ( GCHStatement )
open import L.InjectionComposition {ℓ} lem using ( inclusion-coded; injl-trans )

The bounded search is made small by using the presentation of the ordinal sucV (fst θ). Its indices represent the members of sucV (fst θ), hence ordinals no larger than θ; ω is used separately to express that the cardinal under study is not finite. When two constructible pairs have equal underlying sets, propositionhood of constructibility lifts that equality to the pairs themselves.

open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet {ℓ} using ( ω; sucV )
open import Cubical.Data.Sigma using ( _×_; Σ≡Prop )

Trichotomy will be analyzed through three coproduct branches. Impossible branches end in the empty type, while propositional truncation records existence without exposing a chosen witness; its eliminations below therefore always target propositions such as membership or another truncated existence statement.

open import Cubical.Data.Sum using ( inl; inr )
open import Cubical.Foundations.HLevels using ( isPropΠ; isProp× )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁ )

Membership written _∈ˢ_ is ambient membership in the cumulative hierarchy. This is the relation needed for pointwise containments, including the claim that every ambient member of a constructible subset of κ also belongs to κ.

open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )

We write SV for the ambient proposition-valued set-theoretic structure. Its carrier includes every set over which the pointwise subset hypotheses range.

module SV = hPropStructure 𝒮ᵥ

We write SL for the corresponding structure restricted to constructible sets. Its elements pair an underlying ambient set with a proof that the set lies in L.

module SL = hPropStructure 𝒮ʟ

The ZF model structure on SL supplies the specified internal power set 𝒫κ. Hence every later reference to a power set concerns the power set of the constructible model, rather than the ambient power set in the whole cumulative hierarchy.

module ModelL = FOL.ZFModel 𝒮ʟ

Four internal estimates

The first interface says what it means for a stage to be counted: for every pair of a constructible ordinal δ and a set Lδ whose underlying set is the stage Lset δ, if δ is not finite, then the stage injects into the ordinal. The type excludes finite ordinals and produces only the truncated existence of a coded injection.

StageCountedCoded : Type (ℓ-suc ℓ)
StageCountedCoded =
    (δ Lδ : SL.S) → IsOrd (fst δ) → (⟨ fst δ ∈ˢ ω ⟩ → Empty.⊥)
  → fst Lδ ≡ Lset (fst δ) → InjL Lδ δ

The second interface states the bounded-subset theorem. For an ordinal internal cardinal κ that is not finite, and any constructible set y whose ambient members all belong to κ, there is, merely, an ordinal β such that y lies in the stage Lset β and β injects into κ. The subset hypothesis quantifies over ambient sets, which covers members that carry no constructibility proof of their own.

InternalBoundedSubset : Type (ℓ-suc ℓ)
InternalBoundedSubset =
    (κ : SL.S) → IsOrd (fst κ) → IsCardinalL κ → (⟨ fst κ ∈ˢ ω ⟩ → Empty.⊥)
  → (y : SL.S) → ((z : SV.S) → ⟨ z ∈ˢ fst y ⟩ → ⟨ z ∈ˢ fst κ ⟩)
  → ∥ Σ[ β ∈ SL.S ]

The produced record contains the ordinality of β, the landing of y in the stage, and the coded injection of β into κ.

       (IsOrd (fst β) × ⟨ fst y ∈ˢ Lset (fst β) ⟩ × InjL β κ) ∥₁

The third interface is a conditional reverse comparison: given that the internal power set of κ injects into a successor cardinal δ of κ, it returns the reverse injection of δ into the power set. The hypothesis is genuinely conditional; the interface cannot be invoked from the successor-cardinal record alone.

SuccIntoPower : ModelL.isZFModel → Type (ℓ-suc ℓ)
SuccIntoPower zf =
    (κ δ : SL.S) → (⟨ fst κ ∈ˢ ω ⟩ → Empty.⊥) → SuccCardL δ κ
  → InjL (𝒫 κ) δ → InjL δ (𝒫 κ)
  where open ModelL.isZFModel zf using ( 𝒫 )

The fourth interface states the mere existence of a successor cardinal: for every infinite internal ordinal cardinal, some successor cardinal exists. The conclusion is truncated, so a caller cannot select a global representative from it.

SuccCardExists : Type (ℓ-suc ℓ)
SuccCardExists =
    (κ : SL.S) → IsOrd (fst κ) → IsCardinalL κ
  → (⟨ fst κ ∈ˢ ω ⟩ → Empty.⊥)
  → ∥ Σ[ δ ∈ SL.S ] SuccCardL δ κ ∥₁

Larger internal cardinals exist

The reduction module fixes an ordinal internal cardinal θ strictly above κ and proves that, within the small search space determined by the successor of θ, a least cardinal above κ exists. This is the heart of the chapter: first fix an explicit upper bound, then minimize inside it.

module Reduce (κ : SL.S) (oκ : IsOrd (fst κ))
              (θ : SL.S) (oθ : IsOrd (fst θ))
              (cθ : IsCardinalL θ) (κ∈θ : ⟨ fst κ ∈ˢ fst θ ⟩) where

The earlier cardinal machinery supplies a map up from indices in the small presentation of the ordinal sucV (fst θ) to constructible sets. It also supplies an index self that presents θ itself and an equation self-eq identifying the underlying set of up self with θ. Thus the known cardinal θ occurs among the candidates of the bounded search.

  open LeastCardInjL θ oθ using ( up; self; self-eq )

The search space is the small presentation of the ordinal successor sucV (fst θ). It is a presentation of an ordinal, not a constructible stage Lset (fst θ).

  A : Type ℓ
  A = ⟪ sucV (fst θ) ⟫

Membership on the ordinal sucV (fst θ) induces a strict well-order on this presentation. That well-order makes it possible to search the small candidate family for a least member.

  opaque
    w : SWO A
    w = ordSWO (sucV (fst θ)) (suc-ord oθ)

For presentation indices m and n, the induced relation m < n holds exactly when the ordinal represented by m belongs to the ordinal represented by n. Consequently, being earlier in the search order has the intended mathematical meaning of being a smaller ordinal.

  opaque
    unfolding w
    w-lt : (m n : A) → SWO._<∙_ w m n
         ≡ ⟨ ⟪ sucV (fst θ) ⟫↪ m ∈ˢ ⟪ sucV (fst θ) ⟫↪ n ⟩
    w-lt m n = refl

Internal cardinality is a proposition. Indeed, IsCardinalL x says, for every constructible member δ of x, that any coded injection from x into δ leads to the empty type; dependent function types with proposition-valued conclusions remain propositions. This allows cardinality to form one component of the proposition-valued candidate predicate below.

  isPropIsCardinalL : (x : SL.S) → isProp (IsCardinalL x)
  isPropIsCardinalL x =
    isPropΠ (λ _ → isPropΠ (λ _ → isPropΠ (λ _ → Empty.isProp⊥)))

The candidate predicate asks two things of an index: the constructible set it presents is an internal cardinal, and κ belongs to it. Ordinality need not be stored in the predicate, because every presented set is a member of the ordinal sucV (fst θ) and is therefore itself an ordinal.

  Good : A → hProp (ℓ-suc ℓ)
  Good b = (IsCardinalL (up b) × ⟨ fst κ ∈ˢ fst (up b) ⟩)
         , isProp× (isPropIsCardinalL (up b)) (snd (fst κ ∈ˢ fst (up b)))

The index presenting θ itself presents a constructible set whose underlying set is θ, by the propositionhood of constructibility.

  upSelf : up self ≡ θ
  upSelf = Σ≡Prop (λ x → snd (isL x)) self-eq

The candidate class is nonempty: the index presenting θ is a candidate, carrying the cardinality and the membership transported along that identification.

  nonempty : ∥ Σ[ b ∈ A ] ⟨ Good b ⟩ ∥₁
  nonempty = ∣ self
            , subst (λ z → IsCardinalL z × ⟨ fst κ ∈ˢ fst z ⟩)
                (sym upSelf) (cθ , κ∈θ) ∣₁

The well order of the search space then produces an actual least candidate, with its leastness proof. The least-witness type is a proposition, so the truncation of nonemptiness can be eliminated here; the search itself uses excluded middle.

  least : Σ[ b ∈ A ] IsLeast w Good b
  least = leastOf w lem Good nonempty

Name the constructible set presented by the least candidate δ. The following argument verifies that its local leastness in the bounded search gives all four clauses of SuccCardL δ κ, including leastness against every competing internal ordinal cardinal above κ.

  δ : SL.S
  δ = up (fst least)

By the presentation's membership record, the underlying set of δ belongs to the ordinal sucV (fst θ). Thus the construction proves only fst δ ∈ sucV (fst θ), which places δ at or below θ; it does not assert fst δ ∈ fst θ.

  δ∈sθ : ⟨ fst δ ∈ˢ sucV (fst θ) ⟩
  δ∈sθ = member (sucV (fst θ)) (fst least)

The underlying set of δ is an ordinal, because it is a member of the ordinal successor of an ordinal.

  oδ : IsOrd (fst δ)
  oδ = mem-ord {A = sucV (fst θ)} (suc-ord oθ) (fst δ) δ∈sθ

The least candidate is an internal cardinal, read off the candidate record.

  cδ : IsCardinalL δ
  cδ = fst (fst (snd least))

The given cardinal lies below the least candidate, also read off the candidate record.

  κ∈δ : ⟨ fst κ ∈ˢ fst δ ⟩
  κ∈δ = snd (fst (snd least))

Leastness says that no earlier index of the search space is a candidate.

  δ-min : (b : A) → ⟨ Good b ⟩ → (SWO._<∙_ w b (fst least) → Empty.⊥)
  δ-min = snd (snd least)

Global leastness is stated as a containment: for every ordinal internal cardinal c above κ, every member of δ belongs to c. This is exactly the last clause of the successor-cardinal record, and the proof compares the ordinals δ and c.

  leastness : (c : SL.S) → IsOrd (fst c) → IsCardinalL c
            → ⟨ fst κ ∈ˢ fst c ⟩
            → (x : SL.S) → ⟨ fst x ∈ˢ fst δ ⟩ → ⟨ fst x ∈ˢ fst c ⟩
  leastness c oc cc κ∈c = go (ord-tri (fst δ) oδ (fst c) oc)
    where

The three trichotomy cases are handled directly: if δ lies below c, the transitivity of c gives the containment; if they are equal, the equation transports the containment; if c lies below δ, a contradiction is derived from the leastness.

    go : Tri (fst δ) (fst c)
       → (x : SL.S) → ⟨ fst x ∈ˢ fst δ ⟩ → ⟨ fst x ∈ˢ fst c ⟩
    go (inl δ∈c)       x x∈δ = oc .fst x∈δ δ∈c
    go (inr (inl e))   x x∈δ = subst (λ v → ⟨ fst x ∈ˢ v ⟩) e x∈δ
    go (inr (inr c∈δ)) x x∈δ = Empty.rec (δ-min b bGood b<δ)

In the remaining case, c ∈ δ. Since fst δ ∈ sucV (fst θ) and the ordinal sucV (fst θ) is transitive, it follows that fst c ∈ sucV (fst θ). Only this contradictory branch needs to pull the competing cardinal back into the bounded search space; no prior bound on an arbitrary competitor was assumed.

      where
      c∈sθ : ⟨ fst c ∈ˢ sucV (fst θ) ⟩
      c∈sθ = suc-ord oθ .fst c∈δ δ∈sθ
      b : A
      b = fiber (sucV (fst θ)) c∈sθ .fst

The recovered index presents exactly c, and the constructible set it presents is therefore c itself; the candidate predicate for this index is obtained by transporting the cardinality and the membership of c along that identification.

      be : ⟪ sucV (fst θ) ⟫↪ b ≡ fst c
      be = fiber (sucV (fst θ)) c∈sθ .snd
      upb : up b ≡ c
      upb = Σ≡Prop (λ v → snd (isL v)) be
      bGood : ⟨ Good b ⟩

The membership of c below δ is then converted into the strict order of the search space, contradicting the leastness of the selected index.

      bGood = subst (λ z → IsCardinalL z × ⟨ fst κ ∈ˢ fst z ⟩)
                (sym upb) (cc , κ∈c)
      b<δ : SWO._<∙_ w b (fst least)
      b<δ = transport (λ i → sym (w-lt b (fst least)) i)
              (subst (λ v → ⟨ v ∈ˢ fst δ ⟩) (sym be) c∈δ)

CardAboveL supplies only the propositionally truncated existence of some ordinal internal cardinal θ with κ ∈ θ; it supplies no leastness and does not select θ. The proof maps each local witness through Reduce, where minimization occurs inside the presentation of sucV (fst θ). The resulting successor cardinal therefore remains under propositional truncation.

succCardExists : SuccCardExists
succCardExists κ oκ cκ κ∉ω = PT.map build (CardAboveL κ oκ cκ κ∉ω)
  where
  build : Σ[ θ ∈ SL.S ]
            (IsOrd (fst θ) × IsCardinalL θ × ⟨ fst κ ∈ˢ fst θ ⟩)

Within one local branch, build packages the chosen δ with the four clauses of SuccCardL δ κ: δ is an ordinal, it is an internal cardinal, κ ∈ δ, and δ is contained in every ordinal internal cardinal lying above κ.

        → Σ[ δ ∈ SL.S ] SuccCardL δ κ
  build (θ , oθ , cθ , κ∈θ) = R.δ , R.oδ , R.cδ , R.κ∈δ , R.leastness
    where module R = Reduce κ oκ θ oθ cθ κ∈θ

Discharging the structural estimates

A stage whose index is an ordinal is constructible, by the axiom relating stages and constructibility.

stage-is-L : (δ : SL.S) → IsOrd (fst δ) → ⟨ isL (Lset (fst δ)) ⟩
stage-is-L δ ordδ = isL-Lset (fst δ) ordδ

The bridging predicate for the power set states its content: for two constructible sets κ and y, with κ an ordinal and y a member of the model's power set of κ, every ambient member z of y is constructible, belongs to κ, and is an ordinal.

zStrongest : ModelL.isZFModel → Type (ℓ-suc ℓ)
zStrongest zf =
    (κ y : SL.S) → IsOrd (fst κ) → ⟨ fst y ∈ˢ fst (𝒫 κ) ⟩
  → (z : SV.S) → ⟨ z ∈ˢ fst y ⟩
  → (⟨ isL z ⟩ × ⟨ z ∈ˢ fst κ ⟩ × IsOrd z)

The bridge depends on the chosen ZF model because its premise refers to that model's specified power set. Thus 𝒫κ here remains the internal power set of L throughout the argument.

  where open ModelL.isZFModel zf using ( 𝒫 )

The subtle point is a change of domains. Power-set membership yields a subset statement quantified over constructible sets, whereas z initially ranges over the ambient hierarchy. Transitivity of L first makes z available as a constructible set; only then can the internal subset statement be applied, after which ordinality follows from z ∈ κ and the ordinality of κ.

z-strongest : (zf : ModelL.isZFModel) → zStrongest zf
z-strongest zf κ y ordκ y∈𝒫κ z z∈y = isLz , z∈κ , mem-ord {A = fst κ} ordκ z z∈κ
  where
  open ModelL.isZFModel zf using ( 𝒫; hasPower )

The constructibility of z follows by transitivity: z belongs to the constructible set y, which is itself constructible.

  isLz : ⟨ isL z ⟩
  isLz = isL-trans z∈y (snd y)

The defining specification of the model's power set identifies y ∈ 𝒫κ with the internal subset relation y ⊆ κ. This relation quantifies over elements of SL, so the constructibility established in the preceding step is essential.

  y⊆κ : ⟨ y ModelL.⊆ˢ κ ⟩
  y⊆κ = subst ⟨_⟩ (ModelL.℩-spec (hasPower κ) y) y∈𝒫κ

The internal subset relation is then applied to the pair of z and its constructibility, yielding membership of z in κ.

  z∈κ : ⟨ z ∈ˢ fst κ ⟩
  z∈κ = y⊆κ (z , isLz) z∈y

Every subset lands before the successor

The landing lemma is stated for the model, the bounded-subset interface, and a fixed successor cardinal δ of κ: every member of the model's power set of κ lies in the stage Lset δ.

stage-landing :
    (zf : ModelL.isZFModel) → InternalBoundedSubset
  → (κ : SL.S) → IsOrd (fst κ) → IsCardinalL κ → (⟨ fst κ ∈ˢ ω ⟩ → Empty.⊥)
  → (δ : SL.S) → SuccCardL δ κ
  → (y : SL.S) → ⟨ fst y ∈ˢ fst (ModelL.isZFModel.𝒫 zf κ) ⟩

For each fixed y, the bounded-subset theorem returns a suitable stage index β only under propositional truncation. The desired conclusion y ∈ Lset δ is itself a proposition, so the proof may reason with a local β without choosing such indices uniformly. The ambient pointwise subset hypothesis required by that theorem is exactly the bridge just established.

  → ⟨ fst y ∈ˢ Lset (fst δ) ⟩
stage-landing zf ibs κ ordκ cardκ κ∉ω δ (ordδ , cardδ , κ∈δ , _) y y∈𝒫κ =
  PT.rec (snd (fst y ∈ˢ Lset (fst δ))) place (ibs κ ordκ cardκ κ∉ω y y⊆κ)
  where
  y⊆κ : (z : SV.S) → ⟨ z ∈ˢ fst y ⟩ → ⟨ z ∈ˢ fst κ ⟩

From y ∈ 𝒫κ and z ∈ y, the strongest-member lemma yields z ∈ κ. Its proof first uses the transitivity of L to recognize the ambient member z as constructible, so that the internal subset relation expressed by power-set membership can be applied to it.

  y⊆κ z z∈y = z-strongest zf κ y ordκ y∈𝒫κ z z∈y .snd .fst

No injection from δ into κ can exist, because δ is an internal cardinal and κ is a member of δ. This refutation is the tool used to eliminate the impossible trichotomy branches below.

  no-δ↪κ : InjL δ κ → Empty.⊥
  no-δ↪κ = cardδ κ κ∈δ

For the fixed subset y, the bounded-subset estimate supplies, under propositional truncation, an ordinal β such that y ∈ Lset β and there is an internal coded injection β ↪ κ. Once such a witness is exposed locally, place compares β with δ by ordinal trichotomy and proves that y already belongs to Lset δ.

  place : Σ[ β ∈ SL.S ]
            (IsOrd (fst β) × ⟨ fst y ∈ˢ Lset (fst β) ⟩ × InjL β κ)
        → ⟨ fst y ∈ˢ Lset (fst δ) ⟩
  place (β , ordβ , y∈Lβ , β↪κ) = go (ord-tri (fst β) ordβ (fst δ) ordδ)
    where

If β lies below δ, monotonicity of the tower directly places the member at the lower stage inside the higher stage. If β equals δ, the injection β ↪ κ would become an injection δ ↪ κ, contradicting the cardinality of δ.

    go : Tri (fst β) (fst δ) → ⟨ fst y ∈ˢ Lset (fst δ) ⟩
    go (inl β∈δ)       = Lset-mono β∈δ y∈Lβ
    go (inr (inl e))   = Empty.rec (no-δ↪κ (subst (λ b → InjL b κ) β≡δ β↪κ))
      where
      β≡δ : β ≡ δ

In the equality branch, equality of the underlying sets lifts to equality of the corresponding elements of L because constructibility is proposition-valued. In the remaining branch, where δ ∈ β, the inclusion δ ↪ β followed by the given coded injection β ↪ κ would produce the forbidden coded injection δ ↪ κ.

      β≡δ = Σ≡Prop (λ x → snd (isL x)) e
    go (inr (inr δ∈β)) = Empty.rec (no-δ↪κ
      (injl-trans δ β κ (inclusion-coded δ β δ⊆β) β↪κ))
      where
      δ⊆β : (z : SV.S) → ⟨ z ∈ˢ fst δ ⟩ → ⟨ z ∈ˢ fst β ⟩

The inclusion is the transitivity of the ordinal β applied to the two memberships.

      δ⊆β z z∈δ = ordβ .fst z∈δ δ∈β

Coding the power set below the successor

The power-set comparison now follows from the chain 𝒫κ ↪ Lset δ ↪ δ. The first arrow comes from the fact that every member of the internal power set lies in Lset δ, and the second counts that constructible stage by δ. No stage index is chosen uniformly for the members of 𝒫κ.

power-into-succ :
    (zf : ModelL.isZFModel) → StageCountedCoded → InternalBoundedSubset
  → (κ : SL.S) → IsOrd (fst κ) → IsCardinalL κ → (⟨ fst κ ∈ˢ ω ⟩ → Empty.⊥)
  → (δ : SL.S) → SuccCardL δ κ
  → InjL (ModelL.isZFModel.𝒫 zf κ) δ

Pointwise containment is first converted by inclusion-coded into the coded injection 𝒫κ ↪ Lset δ. The stage-counting hypothesis supplies Lset δ ↪ δ, and injl-trans composes the two. Since both comparisons are expressed by InjL, their witnessing graphs remain propositionally truncated.

power-into-succ zf scc ibs κ ordκ cardκ κ∉ω δ sc@(ordδ , _ , κ∈δ , _) =
  injl-trans (𝒫 κ) Lδ δ (inclusion-coded (𝒫 κ) Lδ into)
    (scc δ Lδ ordδ δ∉ω refl)
  where
  open ModelL.isZFModel zf using ( 𝒫 )

The stage at δ is presented as an element of L by pairing the stage set with its constructibility certificate, obtained from the ordinality of δ.

  Lδ : SL.S
  Lδ = Lset (fst δ) , stage-is-L δ ordδ

The successor cardinal δ lies outside ω: if it were inside, the membership κ ∈ δ would force κ ∈ ω by transitivity of ω, contradicting the hypothesis.

  δ∉ω : ⟨ fst δ ∈ˢ ω ⟩ → Empty.⊥
  δ∉ω δ∈ω = κ∉ω (ω-ord .fst {x = fst δ} {y = fst κ} κ∈δ δ∈ω)

Every member of the power set is landed inside Lset δ by the landing lemma, with its constructibility supplied through the transitivity of L from the power-set membership.

  into : (z : SV.S) → ⟨ z ∈ˢ fst (𝒫 κ) ⟩ → ⟨ z ∈ˢ fst Lδ ⟩
  into z z∈ =
    stage-landing zf ibs κ ordκ cardκ κ∉ω δ sc (z , isL-trans z∈ (snd (𝒫 κ))) z∈

The generalized continuum hypothesis

The final theorem keeps the two directions logically separate. Stage counting and the bounded-subset theorem establish 𝒫κ ↪ δ. Only after that injection has been obtained does the independent conditional theorem SuccIntoPower apply, using it together with the successor-cardinal facts to establish δ ↪ 𝒫κ.

gch-from-internal-bill :
    (zf : ModelL.isZFModel)
  → StageCountedCoded → InternalBoundedSubset → SuccIntoPower zf
  → GCHStatement zf
gch-from-internal-bill zf scc ibs sip κ ordκ cardκ κ∉ω =

The theorem succCardExists gives only the propositionally truncated existence of a successor cardinal δ. The map therefore works inside each local witness: step keeps the successor-cardinal proof, constructs the truncated coded injection 𝒫κ ↪ δ by the landing argument, and passes that result to the independent conditional interface to obtain the truncated coded injection δ ↪ 𝒫κ.

  PT.map step (succCardExists κ ordκ cardκ κ∉ω)
  where
  open ModelL.isZFModel zf using ( 𝒫 )
  step : Σ[ δ ∈ SL.S ] SuccCardL δ κ
       → Σ[ δ ∈ SL.S ] (SuccCardL δ κ × InjL (𝒫 κ) δ × InjL δ (𝒫 κ))

The landing argument supplies pis : InjL (𝒫 κ) δ, and the independent conditional interface uses pis to supply InjL δ (𝒫 κ). Each InjL is the propositional truncation of the existence of a constructible injection code, so the result records exactly two opposite coded-injection existences; it does not select either graph or construct a bijection, a set equality, or a cardinal-arithmetic equality.

  step (δ , sc) = δ , sc , pis , sip κ δ κ∉ω sc pis
    where
    pis : InjL (𝒫 κ) δ
    pis = power-into-succ zf scc ibs κ ordκ cardκ κ∉ω δ sc