---
title: "从四条内部界装配 GCH"
module: L.GCH.Assembly
lang: zh
site: "Bedrock"
description: "从四条内部界装配 GCH"
stage: "证明 GCH"
reading_order: 97
canonical: https://bedrock.institute/zh/L.GCH.Assembly.html
html: L.GCH.Assembly.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/Assembly.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Semantics, FOL.ZFModel, V.Hierarchy, V.Presentation, L.Constructible, L.Ordinal, L.Ordinal.Linear, L.Ordinal.SquareLaw, L.WellOrder.Base, L.Axioms.Basic, L.Cardinal, L.CardinalAbove, L.DefinableInjection, L.GCH, L.InjectionComposition]
routes: [cardinal-tools]
translations: [https://bedrock.institute/en/L.GCH.Assembly.md, https://bedrock.institute/ja/L.GCH.Assembly.md]
agent_guide: https://bedrock.institute/llms.txt
license: "CC-BY-NC-SA-4.0"
---


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

# 从四条内部界装配 GCH

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

我们把这一假设固定在证明所需的唯一宇宙层级上。因此下文所有构造，包括最小候选者论证，都只依赖同一个显式实例 `LEM (ℓ-suc ℓ)`。

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

```agda
open import FOL.ZFStructure using ( module hPropView )
open import FOL.Syntax using ( var; _∈̇_; _∧̇_ )
import FOL.Semantics
import FOL.ZFModel
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Presentation {ℓ} using ( member; fiber )
open import L.Constructible {ℓ}
  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 ℓ}
  using ( SWO; IsLeast; leastOfFormula; 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 )
open import L.DefinableInjection {ℓ} lem using ( cardinalAt; module CardinalAt )
open import L.GCH {ℓ} lem using ( GCHStatement )
open import L.InjectionComposition {ℓ} lem using ( inclusion-coded; injl-trans )
```

本章完成 `L` 内部所采用的 GCH 陈述。对每个无穷内部序数基数 `κ`，它在最外层的命题截断下证明：存在一个后继基数 `δ`，并有两条编码单射 `𝒫κ ↪ δ` 与 `δ ↪ 𝒫κ`。证明可以在截断的局部分支内使用见证，但最终既不选定一个 `δ`，也不交出任何一张单射图。

装配过程使用的唯一经典原则是排中律。一旦把候选者放进一个小良序中，排中律便可把仅仅非空的候选族化为其唯一最小元。

这里汇合了两个集合论视角。外围累积层级提供成员关系与小呈现，可构造子宇宙提供谓词 `isL` 和各层 `Lset α`；随后由 ZF 模型结构解释内部幂集。

极小化论证使用序数的三项事实：序数中的成员关系具有传递性，任意两个序数满足三分律，并且序数的小呈现上的成员关系次序是良序。这些事实使有界搜索所得的最小候选者能够控制任意竞争基数。

内部大小比较由 `InjL` 表达，即「存在一个编码单射的可构造图」的命题截断。`IsCardinalL` 据此定义内部基数，`SuccCardL` 刻画严格大于给定基数的最小内部序数基数；`CardAboveL` 只在命题截断下提供某个更大的基数。

最终的 GCH 陈述要求：仅仅存在一个后继基数，并有它与模型幂集之间两个方向的编码单射。为构造从幂集出发的比较，证明先把包含关系编码成单射，再与计数可构造层的单射复合。

有界搜索通过序数 `sucV (θ .fst)` 的小呈现变成一个小类型。其索引表示 `sucV (θ .fst)` 的元素，也就是不大于 `θ` 的序数；`ω` 则另用于表达所研究的基数不是有限序数。若两个可构造对的底层集合相等，可构造性的命题性会把这一相等提升为这两个配对的相等。

```agda
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet {ℓ} using ( ω; sucV )
```

三分律将通过余积的三个分支来分析。不可能的分支落入空类型，而命题截断只记录存在而不暴露选定见证；因此下文对它的消去总是以成员关系或另一个截断存在陈述等命题为目标。

记作 `_∈ˢ_` 的成员关系是累积层级中的外围成员关系。逐点包含使用这一关系，特别是「`κ` 的一个可构造子集的每个外围元素也属于 `κ`」这一陈述。

```agda
open hPropView 𝒮ᵥ using ( _∈ˢ_ )
```

记外围的命题值集合论结构为 `SV`。它的载体包含逐点子集前提所量化的全部集合。

```agda
module SV = hPropView 𝒮ᵥ
```

记限制在可构造集合上的相应结构为 `SL`。它的元素把一个外围底层集合与该集合属于 `L` 的证明配成一对。

```agda
module SL = hPropView 𝒮ʟ
```

`SL` 上的 ZF 模型结构提供指定的内部幂集 `𝒫κ`。因此后文提到的幂集都指可构造模型的幂集，而不是整个累积层级中的外围幂集。

```agda
module ModelL = FOL.ZFModel 𝒮ʟ
```

## 四条内部估计

第一个接口陈述「层被计数」的含义：对每对「可构造序数 `δ` 与底层集合恰为层 `Lset δ` 的集合 `Lδ`」，若 `δ` 非有限，则该层单射入该序数。该类型排除有限序数，且只产出编码单射的截断存在。

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

第二个接口陈述有界子集定理。对非有限、序数、内部基数的 `κ`，以及任一「其外围元素都属于 `κ`」的可构造集合 `y`，都仅仅地存在序数 `β`，使 `y` 落在层 `Lset β` 中且 `β` 单射入 `κ`。子集前提量化外围集合，从而覆盖那些自身不带可构造性证明的元素。

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

产出的记录包含 `β` 的序数性、`y` 在层中的落位，以及 `β` 到 `κ` 的编码单射。

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

第三个接口是条件性的反向比较：给定 `κ` 的内部幂集单射入 `κ` 的后继基数 `δ`，它返回 `δ` 到幂集的反向单射。该假设是真正条件性的；仅凭后继基数记录无法调用此接口。

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

第四个接口陈述后继基数的仅仅存在：对每个无穷内部序数基数，存在某个后继基数。结论是截断的，调用者不能从中选定全局代表。

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

## 更大的内部基数存在

约简模块固定严格大于 `κ` 的序数内部基数 `θ`，并证明：在 `θ` 的后继所决定的小搜索空间内，存在 `κ` 之上的最小基数。这是本章的核心：先固定显式上界，再在其内最小化。

<details open class="submodule-fold">
<summary class="submodule-fold-heading">

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

</summary>
<div class="submodule-fold-content">

此前的基数机制提供映射 `up`，把序数 `sucV (θ .fst)` 的小呈现中的索引送到可构造集合。它还提供呈现 `θ` 自身的索引 `self`，以及把 `up self` 的底层集合与 `θ` 认同起来的等式 `self-eq`。因此，已知的基数 `θ` 确实出现在有界搜索的候选者中。

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

搜索空间是序数后继 `sucV (θ .fst)` 的小呈现。这里呈现的是一个序数，而不是可构造层 `Lset (θ .fst)`。

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

序数 `sucV (θ .fst)` 上的成员关系在这一呈现上诱导出严格良序。借助该良序，证明可以在这个小候选族中寻找最小元。

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

对呈现索引 `m` 与 `n`，诱导关系 `m < n` 恰在 `m` 所表示的序数属于 `n` 所表示的序数时成立。因此，在搜索序中更靠前正对应于序数意义下更小。

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

内部基数性是命题。具体说，`IsCardinalL x` 对 `x` 的每个可构造元素 `δ` 断言：任何从 `x` 到 `δ` 的编码单射都会导出空类型；而结论为命题的依值函数类型仍是命题。因此，基数性可作为下文命题值候选谓词的一个分量。

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

候选谓词向索引要求两件事：其呈现的可构造集合是内部基数，并且 `κ` 属于它。谓词无需另存序数性，因为每个被呈现的集合都是序数 `sucV (θ .fst)` 的元素，因而自身就是序数。包 `definedGood` 用 `cardinalAt zero ∧̇ (var one ∈̇ var zero)` 呈现这个合取；其环境把候选者放在 `κ` 之前，而 `CardinalAt` 的两个方向为非原子合取支给出经过检查的读取。

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

  definedGood : FOL.Semantics.FormulaPredicate 𝒮ʟ A SL.S id Good
  definedGood = FOL.Semantics.presented 2
    (cardinalAt zero ∧̇ (var (suc zero) ∈̇ var zero)) (λ b → up b ∷ κ ∷ [])
    (λ b → ⇔toPath
      (λ { (card , mem) → CardinalAt.fill zero (up b ∷ κ ∷ []) card , mem })
      (λ { (sat , mem) → CardinalAt.read zero (up b ∷ κ ∷ []) sat , mem }))
```

呈现 `θ` 自身的索引所呈现的可构造集合，其底层集合就是 `θ`，依据是可构造性的命题性。

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

候选类非空：呈现 `θ` 的索引就是候选，它携带沿该同一视搬运的基数性与成员关系。

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

搜索空间上的面向公式搜索随即产出实际的最小候选及其最小性证明。最小见证的类型是命题，因此非空性的截断可在此消去；经典下降判定的是 `definedGood` 的满足关系，而不是不受限制的宿主回调。

```agda
  least : Σ[ b ∶ A ] IsLeast w Good b
  least = leastOfFormula w definedGood lem nonempty
```

把最小候选所呈现的可构造集合命名为 `δ`。下面将验证：它在有界搜索中的局部最小性足以给出 `SuccCardL δ κ` 的四个条款，包括相对于每个严格大于 `κ` 的竞争内部序数基数的全局最小性。

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

由呈现所附的成员关系记录，`δ` 的底层集合属于序数 `sucV (θ .fst)`。因此这里证明的只是 `δ .fst ∈ sucV (θ .fst)`，即 `δ` 不大于 `θ`；并没有断言 `δ .fst ∈ θ .fst`。

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

`δ` 的底层集是序数，因为它是某序数的序数后继的元素。

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

最小候选是内部基数，由候选记录读出。

```agda
  cδ : IsCardinalL δ
  cδ = ((least .snd) .fst) .fst
```

给定基数位于最小候选之下，这同样由候选记录读出。

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

最小性说：搜索空间中没有任何更早的索引是候选。

```agda
  δ-min : (b : A) → ⟨ Good b ⟩ → let module W = SWO w in (b W.<∙ least .fst → ⊥₀)
  δ-min = (least .snd) .snd
```

全局最小性被陈述为包含：对每个位于 `κ` 之上的序数内部基数 `c`，`δ` 的每个元素都属于 `c`。这正是后继基数记录的最后一个条款；证明比较序数 `δ` 与 `c`。

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

三分法的三种情形被直接处理：若 `δ` 低于 `c`，由 `c` 的传递性给出包含；若二者相等，沿等式搬运包含；若 `c` 低于 `δ`，则由最小性导出矛盾。

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

在余下的情形中有 `c ∈ δ`。由 `δ .fst ∈ sucV (θ .fst)` 及序数 `sucV (θ .fst)` 的传递性，可得 `c .fst ∈ sucV (θ .fst)`。只有这个反证分支才需要把竞争基数拉回有界搜索空间；证明并未预先假设任意竞争者都受 `θ` 限制。

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

恢复出的索引恰呈现 `c`，其呈现的可构造集合即 `c` 自身；该索引的候选谓词由沿此同一视搬运 `c` 的基数性与成员关系得到。

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

于是「`c` 位于 `δ` 之下」的成员关系被转换为搜索空间的严格序，与所选索引的最小性矛盾。

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

</div>
</details>

`CardAboveL` 只在命题截断下给出某个序数内部基数 `θ`，满足 `κ ∈ θ`；它既不提供最小性，也不选定 `θ`。证明把每个局部见证送入 `Reduce`，并在那里于 `sucV (θ .fst)` 的呈现中完成极小化。因此，所得后继基数仍处在命题截断之下。

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

在一个局部分支内，`build` 把选出的 `δ` 与 `SuccCardL δ κ` 的四个条款打包：`δ` 是序数，是内部基数，满足 `κ ∈ δ`，并且包含于每个严格大于 `κ` 的序数内部基数。

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

## 兑现结构性估计

指数为序数的层是可构造的，依据联系层与可构造性的公理。

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

幂集的桥接谓词陈述其内容：对可构造集合 `κ` 与 `y`，其中 `κ` 是序数且 `y` 属于模型幂集 `𝒫κ`，`y` 的每个外围元素 `z` 都可构造、属于 `κ`，且是序数。

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

这座桥依赖所给的 ZF 模型，因为其前提涉及该模型指定的幂集。因此，在整个论证中，`𝒫κ` 始终是 `L` 的内部幂集。

```agda
  where open ModelL.isZFModel zf using ( 𝒫 )
```

这里的细节在于量化域发生了转换。幂集成员关系给出的子集陈述量化可构造集合，而 `z` 起初量化整个外围层级。先用 `L` 的传递性证明 `z` 可构造，才能把内部子集陈述施用于它；随后由 `z ∈ κ` 与 `κ` 的序数性得到 `z` 的序数性。

```agda
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 )
```

`z` 的可构造性由传递性得出：`z` 属于可构造集合 `y`，而 `y` 自身可构造。

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

模型幂集的定义规格把 `y ∈ 𝒫κ` 认同为内部子集关系 `y ⊆ κ`。这一关系量化 `SL` 的元素，因此上一步所得的可构造性不可缺少。

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

内部子集关系随即施加于「`z` 连同其可构造性」的配对，得到 `z` 属于 `κ`。

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

## 每个子集都在后继之前落定

落位引理就模型、有界子集接口与 `κ` 的固定后继基数 `δ` 陈述：模型幂集 `𝒫κ` 的每个元素都落在层 `Lset δ` 中。

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

对每个固定的 `y`，有界子集定理只在命题截断下返回一个合适的层索引 `β`。目标结论 `y ∈ Lset δ` 本身是命题，所以证明可以使用局部的 `β` 推理，而无需为所有 `y` 一致地选择层索引。该定理所需的外围逐点子集前提，正是刚才建立的桥。

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

由 `y ∈ 𝒫κ` 与 `z ∈ y`，最强成员关系引理得到 `z ∈ κ`。其证明先利用 `L` 的传递性认出外围元素 `z` 是可构造的，从而能把幂集成员关系所表达的内部子集关系施用于 `z`。

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

从 `δ` 到 `κ` 的单射不可能存在，因为 `δ` 是内部基数且 `κ` 是 `δ` 的元素。这条反驳是下文排除不可能三歧分支的工具。

```agda
  no-δ↪κ : InjL δ κ → ⊥₀
  no-δ↪κ = cardδ κ κ∈δ
```

对固定的子集 `y`，有界子集估计在命题截断下给出一个序数 `β`，使得 `y ∈ Lset β`，并且存在内部编码单射 `β ↪ κ`。在局部展开这样一个见证后，`place` 用序数三歧性比较 `β` 与 `δ`，并证明 `y` 已属于 `Lset δ`。

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

若 `β` 低于 `δ`，塔的单调性直接把较低层中的元素放进较高层。若 `β` 等于 `δ`，则注入 `β ↪ κ` 会变成注入 `δ ↪ κ`，与 `δ` 的基数性矛盾。

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

在相等分支中，因为可构造性取命题值，底层集合的相等可提升为相应 `L` 元素的相等。在余下的 `δ ∈ β` 分支中，先取包含给出的 `δ ↪ β`，再接上已有的编码单射 `β ↪ κ`，便会产生被排除的编码单射 `δ ↪ κ`。

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

包含是序数 `β` 的传递性施于两条成员关系的结果。

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

## 把幂集编码到后继以下

幂集比较现在来自复合链 `𝒫κ ↪ Lset δ ↪ δ`。第一条箭头来自「内部幂集的每个元素都属于 `Lset δ`」，第二条则用 `δ` 计数这一可构造层。证明没有为 `𝒫κ` 的各个元素一致地选择层索引。

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

逐点包含先由 `inclusion-coded` 转换为编码单射 `𝒫κ ↪ Lset δ`。层计数假设给出 `Lset δ ↪ δ`，再由 `injl-trans` 复合两者。由于两项比较都用 `InjL` 表达，见证它们的图仍处于命题截断之下。

```agda
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 ( 𝒫 )
```

`δ` 处的层通过把层集合与其可构造性证书配对而呈现为 `L` 的元素，证书由 `δ` 的序数性得来。

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

后继基数 `δ` 落在 `ω` 之外：若它在 `ω` 内，则成员关系 `κ ∈ δ` 经 `ω` 的传递性将迫使 `κ ∈ ω`，与假设矛盾。

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

幂集的每个元素由安放引理落入 `Lset δ` 之内，其可构造性经 `L` 的传递性从幂集成员关系供给。

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

## 广义连续统假设

最终定理把两个方向的职责明确分开。层计数与有界子集定理建立 `𝒫κ ↪ δ`。只有取得这条单射之后，独立的条件定理 `SuccIntoPower` 才能把它与后继基数事实一同使用，建立 `δ ↪ 𝒫κ`。

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

定理 `succCardExists` 只给出后继基数 `δ` 的命题截断存在。因此映射在每个局部见证内工作：`step` 保留后继基数证明，用落层论证构造命题截断下的编码单射 `𝒫κ ↪ δ`，再把该结果交给独立的条件接口，得到命题截断下的编码单射 `δ ↪ 𝒫κ`。

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

落层论证给出 `pis : InjL (𝒫 κ) δ`，独立的条件接口再以 `pis` 为前提给出 `InjL δ (𝒫 κ)`。每个 `InjL` 都是「存在可构造单射码」的命题截断，所以结果恰好记录两个相反方向的编码单射存在性；它没有选定任何一张图，也没有构造双射、集合相等或基数算术等式。

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