---
title: "四つの内部上界から GCH を組み立てる"
module: L.GCH.Assembly
lang: ja
site: "Bedrock"
description: "四つの内部上界から GCH を組み立てる"
stage: "GCH の証明"
reading_order: 97
canonical: https://bedrock.institute/ja/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.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.GCH, L.InjectionComposition]
routes: [cardinal-tools]
translations: [https://bedrock.institute/en/L.GCH.Assembly.md, https://bedrock.institute/zh/L.GCH.Assembly.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
本章では、`L` の内部で採用する形の GCH を完成させます。無限な内部順序数基数 `κ` ごとに、外側の命題的切り詰めのもとで、後続基数 `δ` と二つの符号化された単射 `𝒫κ ↪ δ` および `δ ↪ 𝒫κ` が存在することを示します。証明では切り詰められた枝の内部で証人を使えますが、特定の `δ` も、どちらの単射のグラフも外へ取り出しません。

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

組み立てで用いる古典的原理は排中律だけです。候補を小さな整列順序の中に置いた後、単に要素をもつ候補族から一意な最小元を得るために使います。

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

この仮定を、証明に必要なただ一つの宇宙レベルで固定します。したがって、最小候補の議論を含む以下の構成は、すべて同じ明示的な実例 `LEM (ℓ-suc ℓ)` だけに依存します。

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

ここでは、集合論に関する二つの見方を結び付けます。周囲の累積階層は所属と小さな提示を与え、構成可能な部分宇宙は述語 `isL` と各段階 `Lset α` を与えます。内部の冪集合は、後で ZF モデルの構造によって解釈されます。

```agda
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 {ℓ}
```

最小化の議論では、順序数について三つの事実を使います。順序数の所属は推移的であり、任意の二つの順序数には三岐性が成り立ち、順序数の小さな提示上の所属順序は整列順序です。これにより、有界な探索で得た最小候補が、任意の競合する基数を制御できます。

```agda
  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 ℓ}
```

内部の大きさの比較は `InjL` で表します。これは、単射を符号化する構成可能なグラフが存在するという命題的切り詰めです。`IsCardinalL` はこの比較から内部の基数を定義し、`SuccCardL` は与えられた基数より真に大きい最小の内部順序数基数を指定します。一方、`CardAboveL` が与えるのは、切り詰めの内側にある何らかのより大きい基数だけです。

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

最終的な GCH の主張は、後続基数が単に存在し、それとモデルの冪集合との間に両方向の符号化された単射があることを要求します。冪集合から出る向きの比較を構成するため、まず包含を単射として符号化し、次に構成可能な段階を数える単射と合成します。

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

有界探索には、順序数 `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 )
open import Cubical.Data.Sigma using ( _×_; Σ≡Prop )
```

三岐性は、直和の三つの分岐に分けて調べます。不可能な分岐は空型に帰着し、命題的切り詰めは選ばれた証人を外へ出さずに存在だけを記録します。したがって、以下での消去先は、所属や別の切り詰められた存在命題のような命題に限られます。

```agda
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 ( ∥_∥₁; ∣_∣₁ )
```

`_∈ˢ_` と書く所属は、累積階層における周囲の所属です。点ごとの包含、特に「`κ` の構成可能な部分集合の各周囲要素が `κ` にも属する」という主張には、この関係を使います。

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

周囲の命題値の集合論的構造を `SV` と書きます。その台は、点ごとの部分集合の仮定が量化するすべての集合を含みます。

```agda
module SV = hPropStructure 𝒮ᵥ
```

構成可能な集合に制限した対応する構造を `SL` と書きます。その要素は、周囲の底の集合と、その集合が `L` に属することの証明との対です。

```agda
module SL = hPropStructure 𝒮ʟ
```

`SL` 上の ZF モデルの構造は、指定された内部の冪集合 `𝒫κ` を与えます。したがって、以下でいう冪集合はすべて構成可能モデルの冪集合であり、累積階層全体における周囲の冪集合ではありません。

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

## 四つの内部評価

最初のインターフェースは、段階が数え上げられるとは何を意味するかを述べます。構成可能な順序数 `δ` と、底の集合が段階 `Lset δ` と等しい集合 `Lδ` の対に対して、`δ` が有限でなければ、段階から順序数への単射が存在する、というものです。この型は有限の順序数を排除し、符号化された単射の切り詰められた存在だけを産み出します。

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

第二のインターフェースは、有界部分集合の定理を述べます。有限ではなく順序数であり内部の基数である `κ` と、その周囲の要素がすべて `κ` に属する構成可能な集合 `y` に対して、単に、順序数 `β` が存在し、`y` が段階 `Lset β` の中にあり、`β` が `κ` へ単射します。部分集合の仮定は周囲の集合の上で量化するので、自分自身の構成可能性の証明をもたない要素も覆います。

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

産み出される記録には、`β` の順序数性、`y` の段階への着地、そして `β` から `κ` への符号化された単射が含まれます。

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

第三のインターフェースは条件つきの逆向きの比較です。`κ` の内部の冪集合が `κ` の後続基数 `δ` へ単射することが与えられたとき、`δ` から冪集合への単射を返します。仮定は本当に条件つきであり、後続基数の記録だけから呼び出すことはできません。

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

第四のインターフェースは、後続基数の単なる存在を述べます。無限の内部順序数基数ごとに、ある後続基数が存在します。結論は切り詰められており、呼び出し側がそこから大域的な代表を選ぶことはできません。

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

## より大きな内部基数の存在

約簡のモジュールは、`κ` より真に大きい順序数の内部基数 `θ` を固定し、`θ` の後続が決める小さな探索空間の中で、`κ` より上の最小の基数が存在することを示します。これがこの章の中心です。まず明示的な上界を固定し、その中で最小化するのです。

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

先の基数の仕組みは、順序数 `sucV (fst θ)` の小さな提示の添字から構成可能な集合への写像 `up` を与えます。さらに、`θ` 自身を提示する添字 `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) → SWO._<∙_ w m 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Π (λ _ → Empty.isProp⊥)))
```

候補述語は、添字に二つの条件を課します。その添字が提示する構成可能な集合が内部基数であることと、`κ` がその集合に属することです。順序数性を述語に別途保存する必要はありません。提示される各集合は順序数 `sucV (fst θ)` の要素なので、それ自身も順序数だからです。

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

`θ` 自身を提示する索引が提示する構成可能な集合の底の集合は、構成可能性の命題性によって、`θ` になります。

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

候補の類は空ではありません。`θ` を提示する索引が候補であり、その同一視に沿って運ばれた基数性と所属を運びます。

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

探索空間の整列順序は、実際の最小の候補とその最小性の証明を産み出します。最小の証人の型は命題なので、非空性の切り詰めはここで消去できます。探索そのものは排中律を使います。

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

最小候補が提示する構成可能な集合を `δ` と名付けます。以下では、有界探索における局所的な最小性から `SuccCardL δ κ` の四つの条件がすべて従うことを確かめます。その中には、`κ` より大きい任意の競合する内部順序数基数に対する大域的な最小性も含まれます。

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

提示に付随する所属の記録により、`δ` の底の集合は順序数 `sucV (fst θ)` に属します。したがって、ここで示されるのは `fst δ ∈ sucV (fst θ)`、すなわち `δ` が `θ` 以下であることだけであり、`fst δ ∈ fst θ` を主張してはいません。

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

`δ` の底の集合は順序数です。順序数の順序数としての後続の要素だからです。

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

最小の候補は内部の基数です。候補の記録から読み取られます。

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

与えられた基数は、最小の候補の下にあります。これも候補の記録から読み取られます。

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

最小性は、探索空間のそれより早い索引が候補ではないことを言います。

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

大域的な最小性は、包含として述べられます。`κ` より上にある順序数の内部基数 `c` ごとに、`δ` のすべての要素は `c` に属します。これは、後続基数の記録の最後の条項そのものであり、証明は順序数 `δ` と `c` を比較します。

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

三岐性の三つの場合は直接扱われます。`δ` が `c` より下なら、`c` の推移性が包含を与えます。等しいなら、等式に沿って包含を運びます。`c` が `δ` より下なら、最小性から矛盾を導きます。

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

残る場合には `c ∈ δ` です。`fst δ ∈ sucV (fst θ)` であり、順序数 `sucV (fst θ)` は推移的なので、`fst c ∈ sucV (fst θ)` が従います。競合する基数を有界探索へ引き戻す必要があるのは、この矛盾を導く枝だけです。任意の競合者があらかじめ `θ` で抑えられているとは仮定していません。

```agda
      where
      c∈sθ : ⟨ fst c ∈ˢ 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 ≡ fst c
      be = fiber (sucV (fst θ)) c∈sθ .snd
      upb : up b ≡ c
      upb = Σ≡Prop (λ v → snd (isL v)) be
      bGood : ⟨ Good b ⟩
```

そして、`c` が `δ` より下にあるという所属は、探索空間の厳格な順序に変換され、選ばれた索引の最小性と矛盾します。

```agda
      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` が与えるのは、`κ ∈ θ` を満たす何らかの内部順序数基数 `θ` の命題的に切り詰められた存在だけです。最小性は与えず、`θ` も選びません。証明は各局所的な証人を `Reduce` へ写し、そこで `sucV (fst θ)` の提示の内部における最小化を行います。したがって、得られる後続基数も命題的切り詰めの内側に留まります。

```agda
succCardExists : SuccCardExists
succCardExists κ oκ cκ κ∉ω = PT.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 κ) → ⟨ fst y ∈ˢ fst (𝒫 κ) ⟩
  → (z : SV.S) → ⟨ z ∈ˢ fst y ⟩
  → (⟨ 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 (snd y)
```

モデルの冪集合の定義仕様は、`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 κ ∈ˢ ω ⟩ → Empty.⊥)
  → (δ : SL.S) → SuccCardL δ κ
  → (y : SL.S) → ⟨ fst y ∈ˢ fst (ModelL.isZFModel.𝒫 zf κ) ⟩
```

固定した各 `y` に対して、有界部分集合定理が適切な段階の添字 `β` を返すのは命題的切り詰めの内側だけです。目標である `y ∈ Lset δ` 自体が命題なので、すべての `y` に対して添字を一様に選ぶことなく、局所的な `β` を用いて議論できます。この定理が要求する周囲の点ごとの部分集合の仮定は、直前に確立した橋渡しそのものです。

```agda
  → ⟨ 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 κ ⟩
```

`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 δ κ → Empty.⊥
  no-δ↪κ = cardδ κ κ∈δ
```

固定した部分集合 `y` に対し、有界部分集合の評価は命題的切り詰めのもとで、`y ∈ Lset β` を満たし、内部の符号化された単射 `β ↪ κ` をもつ順序数 `β` を与えます。その証人を局所的に取り出すと、`place` は順序数の三分法によって `β` と `δ` を比較し、`y` がすでに `Lset δ` に属することを示します。

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

`β` が `δ` より下なら、塔の単調性が、低い段階の要素を高い段階の中に直接置きます。`β` が `δ` に等しいなら、注入 `β ↪ κ` は `δ ↪ κ` になり、`δ` の基数性と矛盾します。

```agda
    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
      β≡δ : β ≡ δ
```

等しい場合には、構成可能性が命題値なので、基礎となる集合の等しさを対応する `L` の要素の等しさへ持ち上げられます。残る `δ ∈ β` の場合には、包含から得る `δ ↪ β` に、与えられた符号化された単射 `β ↪ κ` を続けると、存在し得ない符号化された単射 `δ ↪ κ` が生じます。

```agda
      β≡δ = Σ≡Prop (λ x → snd (isL x)) e
    go (inr (inr δ∈β)) = Empty.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 κ ∈ˢ ω ⟩ → Empty.⊥)
  → (δ : 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 δ ∈ˢ ω ⟩ → Empty.⊥
  δ∉ω δ∈ω = κ∉ω (ω-ord .fst {x = fst δ} {y = fst κ} κ∈δ δ∈ω)
```

冪集合のすべての要素は、着地の補題によって `Lset δ` の中に落ちます。その構成可能性は、冪集合への所属から、`L` の推移性を通して供給されます。

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

## 一般連続体仮説

最後の定理では、二つの向きの役割を明確に分けます。段階計数と有界部分集合定理が `𝒫κ ↪ δ` を確立します。この単射を得た後で初めて、独立した条件付き定理 `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
  PT.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
```