Bedrock有界子集落在受控层
可以直接阅读本章，也可以通过阅读指南和依赖地图选择其他路线。
阅读指南 · 依赖地图有界子集定理从如下数据出发：内部基数 κ 的底层集合是序数且不属于 ω，任意可构造集合 y 的每个外围成员都属于 κ。定理在命题截断下给出可构造序数 β，使 y ∈ Lset β，并存在编码单射 β ↪ κ。这里不假设 y 由某个公式定义，不选取最小层，也不随 y 统一选取 β。
{-# OPTIONS --cubical --safe --guardedness #-}
本证明的经典性只来自这里显式给出的排中律实例。该假设支撑本章所用的层、壳与编码映射等先前构造；它不会把最终的截断存在变成一族已选定的见证。
open import Base.Prelude open import Base.Classical using ( LEM )
固定宇宙层级 ℓ，并假设层级 ℓ-suc ℓ 上的排中律。下文全部构造，包括最终的有界子集定理，都只依赖这一项经典假设，而不依赖任何选择原理。
module L.GCH.BoundedSubset {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
整个论证必须始终区分两类对象。κ、α₀、lam 以及后文的 β 等符号表示外围累积层级中的集合，其中一些会被证明为序数；Lset κ、Lset α₀、Lset lam 与 Lset β 则表示相应的可构造层。属于层索引与属于该索引所确定的层是两个不同的断言。
open import FOL.ZFStructure using ( module hPropStructure ) open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV; regularityV ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-mono; Lset-layer; layer-trans ) open import L.Ordinal {ℓ} using ( #∈ω )
第一项任务是把 κ 与 y 一同放进某个足够高的可构造层。由于 y 已作为可构造集合给出，可以直接取得它的某个出现层；这一构造不使用定义 y 的公式，也不使用任何有限的定义参数表。
open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset→∈ ) open import L.Axioms.Basic {ℓ} using ( LsetS ) open import L.Axioms.Numerals {ℓ} using ( pairʟ ) open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem ) open import L.Cardinal {ℓ} lem using ( InjL; IsCardinalL )
核心策略是把单点 y 添入 Lset κ，从这个传递起始集生成初等 Skolem 壳，再应用凝聚。先用 κ 计数起始集，便可进一步用 κ 计数整个壳；凝聚随后把塌缩后的壳识别为某个层 Lset β。
open import L.GCH.Assembly {ℓ} lem using ( InternalBoundedSubset ) open import L.InjectionComposition {ℓ} lem using ( inclusion-coded; injl-trans ) open import L.GCH.SkolemHull {ℓ} lem using ( module UnionKit; module HullStage; module HullElemDown ) open import L.GCH.CardinalSquareLaw {ℓ} lem using ( prodL; ω⊆; Goal; module Step )
这条路线需要两种不同的控制。一个具有充分闭包性质的序数 lam 提供环境层，使壳与凝聚论证能在其中进行。编码单射则控制大小：先得到 X ↪ κ，再得到 M ↪ κ，最终得到 β ↪ κ。
open import L.GCH.AdequateStages {ℓ} lem using ( superadequate-above; Superadequate ) open import L.GCH.StageCountingTools {ℓ} lem using ( move ) open import L.GCH.StageInjection {ℓ} lem using ( stage-counted; module Site ) open import L.GCH.OmegaRecursion {ℓ} lem using ( pairʟ-in ) open import L.GCH.HullCounting {ℓ} lem
大小估计从两个简单部分开始。层 Lset κ 可以编码单射入 κ，单点集也可以编码单射入 κ。有限标签使两部分的像保持分离，而无穷内部基数 κ 的平方律把所得乘积重新吸收到 κ 中。
using ( ord⊆Lset; module Union2; tag-union; module Point; module Count )
下文若干相等通过双向比较成员关系来证明。并集隶属给出的分支带有命题截断，但每个目标隶属陈述本身都是命题，因此可以局部使用这些分支，而不必选定并保留某个分支。
open import Cubical.Data.Sigma using ( _×_ ) open import Cubical.Data.Sum using ( _⊎_; inl; inr ) open import Cubical.Functions.Logic using ( ⇔toPath ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ ) open import Cubical.HITs.CumulativeHierarchy.Properties using ( ∈∈ₛ )
有限 von Neumann 数码提供并集编码所需的标签，序数后继闭包则是壳所需环境的一部分。良基性支撑平方律。命题截断记录编码单射的存在，却不暴露一张选定的图。
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet; ⁅_⁆s ) open InfinitySet {ℓ} using ( #_; ω; sucV ) import Cubical.Induction.WellFounded as WF import Cubical.Data.Empty as Empty import Cubical.HITs.PropositionalTruncation as PT
凡是通过 InjL 断言单射时，其图都只在命题截断下存在。证明可以在命题内部复合这些存在性，却不会得到一条能在截断之外作为计算数据使用的指定单射。
open PT using ( ∣_∣₁ )
子集前提刻意用外围隶属来陈述。因此可以对任意外围集合 z 检验它属于 y，继而推出它属于 κ；并不要求 z 一开始就附带自身的可构造性证明。
open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )
与之相对，κ 与 y 是可构造载体 S 的元素：二者都把外围集合与其属于 L 的证据打包在一起。最终见证也以同样方式打包，因此定理给出的是可构造序数，而不是任意外围序数。
open hPropStructure 𝒮ʟ using ( S )
为基数的可构造子集取界
固定可构造集合 κ，假设其底层集合是序数、是内部基数且不属于 ω。再固定任意可构造集合 y，并逐点假设 y 的每个外围成员都属于 κ。这些就是全部前提；特别地，不假设 y 由公式或有限多个参数定义。
module At (κ : S) (oκ : IsOrd (fst κ)) (cκ : IsCardinalL κ) (κ∉ω : ⟨ fst κ ∈ˢ ω ⟩ → Empty.⊥) (y : S) (y⊆κ : (z : V ℓ) → ⟨ z ∈ˢ fst y ⟩ → ⟨ z ∈ˢ fst κ ⟩) where
由 κ 的序数性与 κ ∉ ω 可得 ω ⊆ κ。每个有限 von Neumann 数码 # k 都属于 ω，所以对每个 k 都有 # k ∈ κ。这些元素将充当并集编码中的有限标签。
num∈κ : (k : ℕ) → ⟨ # k ∈ fst κ ⟩ num∈κ k = ω⊆ (fst κ) oκ κ∉ω (# k) (#∈ω k)
序数 κ 与以它为指标的可构造层是两个不同的集合。因此把 Lset κ 打包为内部集合 Lκ；该层将构成起始集的主要部分，而 κ 自身仍是起始集所要编码单射入的基数。
Lκ : S Lκ = LsetS (fst κ) oκ
为了把 κ 与 y 放进同一个层，先在 L 内形成二者的无序对。任何包含该对的传递层都会包含它的两个成员，因此只需一次出现层构造便能同时处理这两个对象。
private P₀ : S P₀ = pairʟ κ y
选取序数层索引 α₀，使该无序对出现在其所索引的层中。这只是由可构造性给出的一个方便的出现索引；这里没有断言 α₀ 是该对最早出现的层。
α₀ : V ℓ α₀ = stage (fst P₀) (snd P₀)
所选层索引 α₀ 是序数。这一点很关键：下一步要取得严格高于它的超充分序数，稍后还要用序数的传递性把 κ 从 α₀ 以下继续送入 lam。
oα₀ : IsOrd α₀ oα₀ = stage-ord (fst P₀) (snd P₀)
基数 κ 属于 Lset α₀。这是因为 κ 是无序对的成员，该无序对属于 Lset α₀，而这一层是传递集。这里得到的是层隶属，尚不是后文所用的序数隶属 κ ∈ α₀。
κ∈Lα₀ : ⟨ fst κ ∈ˢ Lset α₀ ⟩ κ∈Lα₀ = layer-trans (Lset-layer α₀) {x = fst P₀} {y = fst κ} (pairʟ-in κ y κ (inl refl)) (stage-mem (fst P₀) (snd P₀))
同一个传递性论证经无序对的另一成员把 y 放进 Lset α₀。与 κ 不同，并未假设 y 是序数，所以后文会用层的单调性把这一事实搬到 Lset lam，而不会把它转换成 y ∈ α₀。
y∈Lα₀ : ⟨ fst y ∈ˢ Lset α₀ ⟩ y∈Lα₀ = layer-trans (Lset-layer α₀) {x = fst P₀} {y = fst y} (pairʟ-in κ y y (inr refl)) (stage-mem (fst P₀) (snd P₀))
现在显式选取超充分序数 lam，满足 α₀ ∈ lam。这个严格扩张提供后续壳与凝聚论证所需的闭包性质。lam 自身虽是显式数据，但其超充分性所保证的局部充分指标仍处于命题截断下。
sa = superadequate-above α₀ oα₀
把这个高序数在代码中记作 lam，正文中记作 λ。它的具体构造后文不再起作用；证明只使用其序数性、后继闭包、超充分性以及它高于 α₀ 这一事实。
opaque lam : V ℓ lam = sa .fst
首先保留的事实是 lam 为序数。因此它是传递集，这使得 lam 以下的序数隶属可以继续向上传递。
ordλ : IsOrd lam ordλ = sa .snd .fst
其次保留对序数后继的闭包：只要 d ∈ lam，便有 sucV d ∈ lam。这项闭包是保证有限 Skolem 构造留在 lam 所索引层内的结构前提之一。
succλ : (d : V ℓ) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩ succλ = sa .snd .snd .snd .fst .snd .fst
超充分性表示：对每个 d ∈ lam，都仅仅存在充分序数 γ，满足 d ∈ γ ∈ lam。它在 lam 以下提供局部的充分空间，却不选取最小的 γ，也不选取这样一族 γ。
sup : Superadequate lam sup = sa .snd .snd .snd .snd
基数 κ 属于序数索引 lam。由于 κ 与 α₀ 都是序数，先由 κ ∈ Lset α₀ 得到 κ ∈ α₀；再结合 α₀ ∈ lam 与序数 lam 的传递性，得到 κ ∈ lam。这个结论说的是属于索引 lam，而不是属于层 Lset lam。
κ∈λ : ⟨ fst κ ∈ˢ lam ⟩ κ∈λ = ordλ .fst (ord∈Lset→∈ α₀ oα₀ (fst κ) oκ κ∈Lα₀) (sa .snd .snd .fst)
对 y，所需结论则是它属于层 Lset lam。由 α₀ ∈ lam，层的单调性给出 Lset α₀ ⊆ Lset lam；把它用于先前的 y ∈ Lset α₀，便得到 y ∈ Lset lam。这里不需要假设 y 是序数。
y∈Lλ : ⟨ fst y ∈ˢ Lset lam ⟩ y∈Lλ = Lset-mono {α = lam} {β = α₀} (sa .snd .snd .fst) y∈Lα₀
y 的每个外围成员都属于 Lset κ。子集前提先把 z ∈ y 送到 z ∈ κ；由于 κ 是序数，这样的 z 本身也是序数，属于自己的后继层，再由累积性得到 z ∈ Lset κ。因此，y ⊆ κ 给出了使起始集成为传递集所需的层包含关系。
y⊆Lκ : (z : V ℓ) → ⟨ z ∈ˢ fst y ⟩ → ⟨ z ∈ˢ Lset (fst κ) ⟩ y⊆Lκ z hz = ord⊆Lset (fst κ) oκ z (y⊆κ z hz)
在 Lset lam 内形成起始集 X = Lset κ ∪ {y}。它包含 y，并且是传递集：来自 Lset κ 的元素仍留在这个传递层中；来自 y 的元素则由假设属于 κ，因而属于 Lset κ。这项传递性正是后文使塌缩固定 y 的原因。
module UK = UnionKit (fst κ) lam (fst y) oκ ordλ κ∈λ y⊆Lκ y∈Lλ κ∉ω using ( X; X⊆Lλ; ∅∈λ; Lα∈X; x∈X; X-mem; sgl≡; Xtr )
下文用 X 表示这个由 Lset κ 扩张而成的传递集。需要保留的两项性质彼此配合：y ∈ X 保证壳包含待定位的集合，传递性则保证塌缩不会改变它。
X : V ℓ X = UK.X
为了计数，在内部构造单点集 {y} 及其到 κ 的编码单射，其中使用标签 0 ∈ κ，再把它与 Lκ 作内部并。这样得到同一集合 Lset κ ∪ {y} 的编码呈现，其两个部分已经分别带有带标签并集论证所需的单射。
module Pt = Point κ (num∈κ 0) y using ( Y; Y-out; Y-in; injL ) module U = Union2 Lκ Pt.Y using ( D; out; in₁; in₂ )
把这个内部构造的并记作 Xʟ。它与 X 表示同一个数学并集，但其构造附带了证明它编码单射入 κ 所需的内部数据。
Xʟ : S Xʟ = U.D
为了把 Xʟ 与 X 识别起来，双向比较二者的成员。正向中，属于内部编码并意味着在命题截断下分成两种情形：属于 Lset κ，或属于编码单点集；两种情形都推出属于 X。由于属于 X 是命题，这次消去是合法的。
Xʟ-eq : fst Xʟ ≡ X Xʟ-eq = extensionalV {a = fst Xʟ} {b = X} (λ z → ⇔toPath (fwd z) (bwd z)) where fwd : (z : V ℓ) → ⟨ z ∈ˢ fst Xʟ ⟩ → ⟨ z ∈ˢ X ⟩ fwd z h = PT.rec (snd (z ∈ˢ X)) go (U.out zS h)
在层这一分支中，左侧包含把该成员放入 X。把 z 暂时打包为可构造集合是由 L 的传递性保证的：既然 z 属于可构造集合 Xʟ，它自身也可构造。
where zS : S zS = z , isL-trans {x = fst Xʟ} {y = z} h (snd Xʟ) go : ⟨ z ∈ˢ Lset (fst κ) ⟩ ⊎ ⟨ z ∈ˢ fst Pt.Y ⟩ → ⟨ z ∈ˢ X ⟩ go (inl hz) = UK.Lα∈X z hz
在单点分支中，编码成员等于已知属于 X 的 y。反向中，属于 X 同样只在命题截断下拆分为 Lset κ 一侧与单点一侧；目标「属于 Xʟ」是命题，因此第二次消去同样合法。
go (inr hz) = subst (λ w → ⟨ w ∈ˢ X ⟩) (sym (Pt.Y-out zS hz)) UK.x∈X bwd : (z : V ℓ) → ⟨ z ∈ˢ X ⟩ → ⟨ z ∈ˢ fst Xʟ ⟩ bwd z h = PT.rec (snd (z ∈ˢ fst Xʟ)) go (UK.X-mem z h) where go : ⟨ z ∈ˢ Lset (fst κ) ⟩ ⊎ ⟨ z ∈ˢ ⁅ fst y ⁆s ⟩ → ⟨ z ∈ˢ fst Xʟ ⟩
反向的两个分支分别进入 Xʟ 的两个并项。Lset κ 的成员从左侧进入，其可构造性由该层继承；{y} 的成员先与 y 识别，再从编码单点集一侧进入。因此外延性给出 fst Xʟ ≡ X，而不保留任何一次截断的分支选择。
go (inl hz) = U.in₁ (z , isL-trans {x = Lset (fst κ)} {y = z} hz (snd Lκ)) hz go (inr hz) = subst (λ w → ⟨ w ∈ˢ fst Xʟ ⟩) (sym (UK.sgl≡ z hz)) (U.in₂ y Pt.Y-in)
起始集合可构造，因为内部副本可构造且两副本底层集合相等。
X-isL : ⟨ isL X ⟩ X-isL = subst (λ w → ⟨ isL w ⟩) Xʟ-eq (snd Xʟ)
把 X 连同这份可构造性证明打包为 XS : S。它的底层外围集合仍恰好是 X；这项打包只提供 InjL 所要求的内部定义域。
XS : S XS = X , X-isL
无穷基数平方律给出编码单射 κ × κ ↪ κ 的命题截断存在。它所需的前提正是开头固定的事实：κ 是序数、内部基数且不属于 ω。这里既不产生双射，也不产生一张选定的单射图。
pairκ : InjL (prodL κ) κ pairκ = WF.WFI.induction regularityV {P = Goal} Step.result (fst κ) (snd κ) oκ cκ κ∉ω
两条分量单射输入带标签并的构造，得到编码单射 Xʟ ↪ κ × κ：标签 #0 与 #1 区分层部分和单点集部分。再与平方律给出的单射复合，得到 Xʟ ↪ κ；最后沿 fst Xʟ ≡ X 搬运定义域，把它换成可构造包装 XS。所得正是需要的编码单射 X ↪ κ，并且仍处于命题截断下。
base : InjL XS κ base = move Xʟ XS κ κ Xʟ-eq refl (injl-trans Xʟ (prodL κ) κ (tag-union κ (num∈κ 0) (num∈κ 1) Lκ Pt.Y (stage-counted κ Lκ oκ κ∉ω refl) Pt.injL) pairκ)
令 M 为 X 在 Lset lam 内生成的 Skolem 壳。适用于这个壳的 Tarski-Vaught 定理表明，M 具有凝聚所需的初等性。整个传递集 X 就是起始集，因此这正是包含 y、且其塌缩稍后将固定 y 的同一个壳。
elem = HullElemDown.elem lam ordλ X UK.X⊆Lλ UK.∅∈λ
壳计数定理把 X ↪ κ 依次传过 Skolem 闭包的有限阶段及这些阶段的并，得到编码单射 M ↪ κ 在命题截断下的存在性。于是，这个壳既具有应用凝聚所需的初等性，其大小又仍受 κ 控制。
hull↪κ = Count.hull↪κ lam ordλ succλ X UK.X⊆Lλ UK.∅∈λ elem sup X-isL κ oκ cκ κ∉ω base
凝聚给出显式序数 β，并把 M 的塌缩像识别为 Lset β。它还把 Lset β 与 M 打包为可构造集合，并通过逆塌缩给出编码单射 Lset β ↪ M 的命题截断存在。这里 β 是层索引，Lset β 才是它所索引的层。
module St = Site lam ordλ succλ X UK.X⊆Lλ UK.∅∈λ elem sup X-isL using ( β; oβ; ext; Lβ; βL; hullL; Lβ↪M )
下面使用同一个壳构造的三个方面：壳 M、包含关系 X ⊆ M，以及像为 πX 的塌缩映射 π。相应的不动点定理适用于 M 的传递子集。这些事实将先证明塌缩不改变 y，再把同一个 y 放入凝聚所识别出的层中。
module HS = HullStage lam ordλ succλ X UK.X⊆Lλ UK.∅∈λ using ( M ) module HSH = HullStage.H lam ordλ succλ X UK.X⊆Lλ UK.∅∈λ using ( X⊆M ) module HSC = HullStage.C lam ordλ succλ X UK.X⊆Lλ UK.∅∈λ using ( πX; π; fixes; πX-intro )
集合 y 属于 Skolem 壳 M：它已被放入起点集 X，而 X 的每个成员都属于由 X 生成的壳。
y∈M : ⟨ fst y ∈ˢ HS.M ⟩ y∈M = HSH.X⊆M (fst y) UK.x∈X
塌缩固定 y：因为起点集 X 传递且包含于壳中，塌缩映射在 X 的每个成员上恒等，而 y 即为其中之一。
πy : HSC.π (fst y) ≡ fst y πy = HSC.fixes X (λ a a∈ₛX → ∈∈ₛ {a = a} {b = HS.M} .fst (HSH.X⊆M a (∈∈ₛ {a = a} {b = X} .snd a∈ₛX))) UK.Xtr (fst y) UK.x∈X
由于 y 属于壳，塌缩像包含 π(y)。凝聚把这个像认同为可构造层 Lset β，再由不动点等式 π(y) = y 得到 y ∈ Lset β。关键在于，塌缩没有用另一个集合替换 y，而是把原来的 y 定位在一个受控的可构造层中。
y∈Lβ : ⟨ fst y ∈ˢ Lset St.β ⟩ y∈Lβ = subst (λ w → ⟨ w ∈ˢ Lset St.β ⟩) πy (subst (λ w → ⟨ HSC.π (fst y) ∈ˢ w ⟩) St.ext (HSC.πX-intro (fst y) y∈M))
序数 β 经三条编码单射的链注入 κ：由序数隶属从 β 到层 Lset β 的包含、由受限逆塌缩从 Lset β 到壳 M 的单射、以及由壳计数从 M 到 κ 的单射。这条链给出的是编码单射，而非裸序数比较。
β↪κ : InjL St.βL κ β↪κ = injl-trans St.βL St.Lβ κ (inclusion-coded St.βL St.Lβ (λ z hz → ord⊆Lset St.β St.oβ z hz)) (injl-trans St.Lβ St.hullL κ St.Lβ↪M hull↪κ)
局部见证现把可构造序数 β、它的序数性、y 属于层 Lset β 的事实，以及编码单射 β ↪ κ 打包在一起。这里返回的是层指标 β，而 Lset β 是已经容纳 y 的可构造层；二者不可混同。
result : Σ[ b ∈ S ] (IsOrd (fst b) × ⟨ fst y ∈ˢ Lset (fst b) ⟩ × InjL b κ) result = St.βL , St.oβ , y∈Lβ , β↪κ
最后，∣_∣₁ 把整个局部见证置于命题截断下。因此，最终定理只保留如下存在性：某个可构造序数 β 满足 y ∈ Lset β，并存在编码单射 β ↪ κ。它既不提供最小或规范的 β，也不随 y 统一选取见证。
internal-bounded-subset : InternalBoundedSubset internal-bounded-subset κ oκ cκ κ∉ω y y⊆κ = ∣ At.result κ oκ cκ κ∉ω y y⊆κ ∣₁