---
title: "可构造层级的 Δ₀ 描述"
module: L.GCH.HierarchyDescription
lang: zh
site: "Bedrock"
description: "可构造层级的 Δ₀ 描述"
stage: "证明 GCH"
reading_order: 106
canonical: https://bedrock.institute/zh/L.GCH.HierarchyDescription.html
html: L.GCH.HierarchyDescription.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/HierarchyDescription.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.LevyHierarchy, FOL.Manipulation.ConstantOccurrences, FOL.Manipulation.ConstantMapping, FOL.Manipulation.Relabelling, FOL.Absoluteness, FOL.Semantics, V.Hierarchy, V.Coding, L.Constructible, L.Ordinal, L.Axioms.Basic, L.Axioms.Numerals, L.Coding.Expressions, L.Coding.NumeralBound, L.Coding.CodeSet, L.Coding.Model, L.Coding.Quantification, L.Coding.CodeDomain, L.Coding.EnvironmentTower, L.Hierarchy, L.GCH.SkolemHull, L.Coding.SatisfactionGraphSet, L.GCH.SatisfactionDescription, L.GCH.DefinablePowerSetDescription, L.GCH.AdequateStages]
routes: [gch-descriptions, hulls-and-counting]
translations: [https://bedrock.institute/en/L.GCH.HierarchyDescription.md, https://bedrock.institute/ja/L.GCH.HierarchyDescription.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
后续的凝聚论证需要搬运「某集合是给定序数处的可构造层」这一断言。初等性搬运的是公式，而不是外围定义的运算 `Lset`，所以本章构造一条有界的对象语言公式来识别同一个层关系，并以第三个集合作为全部辅助见证的公共界。

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

这一构造的经典性只来自一个固定的排中律实例。不过，有界存在公式仍被读作命题截断的存在，因此经典背景并不会把隐藏的诸表变成全局选定的数据。

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

固定宇宙层级 `ℓ`，并假设层级 `ℓ-suc ℓ` 上命题的排中律。本章的每条公式、读引理与最终正确性定理都相对于这一个显式经典假设陈述。

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

这里的对象语言只需要隶属、合取、真、假与有界量词；这些构造子都具有结构性的 Δ₀ 见证。稍后证明公式不含常元，便可把常元域改为空字母表，使最终的三变元公式成为无参公式，同时保留其自由变元。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; _∈̇_; _∧̇_; ⊤̇; ⊥̇; ∃̇∈; ∀̇∈ )
open import FOL.LevyHierarchy using ( Δ₀; checkΔ₀; δ-∧; δ-∃∈ )
open import FOL.Manipulation.ConstantOccurrences using ( countFo )
open import FOL.Manipulation.ConstantMapping using ( embed )
```

同一条有界公式既可在可构造载体内部读取，也可在外围累积层级中读取；Δ₀ 绝对性认同这两种读法。隶属归纳将由更低的表行验证当前表行，外延性则把由此得到的两个隶属蕴含化为层的相等。

```agda
open import FOL.Manipulation.Relabelling using ( embed-⊨; mapΔ₀ )
import FOL.Absoluteness
import FOL.Semantics
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-induction; extensionalV )
open import V.Coding {ℓ} using ( pr )
```

层 `Lset b` 由此前各层的可定义幂集组装而成：它的每个成员都来自某个满足 `c ∈ b` 的 `𝒟ₒ (Lset c)`，而每一份这样的贡献都属于 `Lset b`。向内与向外的隶属规则表达这两个方向；序数事实则保证后文使用的索引确实是层索引。

```agda
open import L.Constructible {ℓ} using
  ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-in; Lset-out; Lset-mono; 𝒟ₒ )
open import L.Ordinal {ℓ} using ( mem-ord; suc-ord; #∈ω )
open import L.Axioms.Basic {ℓ} using ( LsetS; Lset-suc )
open import L.Axioms.Numerals {ℓ} using ( numeralL-fst )
```

在模型内部识别一个可定义幂集，需要公式码、满足关系表与环境塔；有序对编码再把每个层索引同其记录值连接起来。这些辅助集合都将由同一个见证集 `z` 界住，从而使完整描述保持在 Δ₀ 中。

```agda
open import L.Coding.Expressions {ℓ} using ( sucAtL )
open import L.Coding.NumeralBound {ℓ} lem using ( module Bound )
open import L.Coding.CodeSet {ℓ} lem using ( AllCodes )
open import L.Coding.Model {ℓ} using ( container )
open import L.Coding.Quantification {ℓ} using
```

在对象语言内部，不能用无界运算投影集合编码的有序对分量。这里改用有界的分量公式，在一个小容器中遍历并读取或填入该有序对。十个具名槽位保存编码描述所用的数码标签；每次新见证扩展环境时，对这些名称作移位便能保持槽位对齐。

```agda
  ( sh; i0; i1; i2; i3; i8; f0; f1; f2; f3; f4; f5; f6; f7; f8; f9
  ; down; suc-out; suc-in; sndEx; sndAll; bothAll
  ; sndEx-out; sndAll-in; bothAll-in; fillSnd; useSnd; useBoth; sndS )
open import L.Coding.CodeDomain {ℓ} using ( Tags; shN )
open import L.Coding.EnvironmentTower {ℓ} lem using ( nn; module Tower )
```

这里汇合了三类语义规格。层级表在一个界以下记录形如 `(c,Lset c)` 的有序对；满足描述识别一层上的真实码、环境与满足关系数据；可定义幂集描述则识别集合 `𝒟ₒ (Lset c)`。可靠性只会恢复表性质 `Values` 与 `Entries`，完备性则从精确规格 `IsHier` 出发。

```agda
open import L.Hierarchy {ℓ} lem using ( hierL-spec; IsHier; hier-out; hier-in; Values; Entries )
open import L.GCH.SkolemHull {ℓ} lem using ( module Cnt; erase-Δ₀; isOrd-at-p; Δ₀-isOrd-at-p; _⊨ₚ_ )
open import L.Coding.SatisfactionGraphSet {ℓ} lem using ( module SatGraph )
open import L.GCH.SatisfactionDescription {ℓ} lem using ( satAt; sat-complete )
open import L.GCH.DefinablePowerSetDescription {ℓ} lem using ( defAt; def-sound; def-complete )
```

完备性需要一个包含全部辅助见证的公共层。若 `γ` 充分且 `c ∈ γ`，则 `Lset γ` 含有在 `c` 处所需的层级表、码集、满足关系表与环境塔；后继封闭还把下一层放入其中，而 `ω ∈ γ` 则供给全部十个有限数码标签。

```agda
open import L.GCH.AdequateStages {ℓ} lem using ( Adequate; module Adequate; module At; Lset∈suc )
```

环境是可构造集合组成的有限向量。引入一个有界见证时，它被放到向量前端，原有每个槽位都后移一位；有限索引把这些移位显式记录下来。正因如此，同一组层、表与界的名称才能穿过多层嵌套量词而保持不变。

```agda
open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Data.Vec using ( _∷_; []; map; lookup )
open import Cubical.Data.Sigma using ( _×_ )
open import Cubical.Data.Unit using ( tt )
open import Cubical.Data.FinData using ( toℕ; weakenFin )
```

存在公式的满足只保留命题截断：它记录合适的数据存在，却忘去具体用了哪一份数据。因此后文每次消去都以命题为目标。这里隶属取命题值，而累积层级中集合的相等也是命题，所以证明所需的这两类结论都可作为合法目标。

```agda
open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
```

十个有限标签由层级内部的 von Neumann 数码表示。零是空集，之后每个标签由集合论后继得到，而且十个数码都属于 `ω`。隶属读式把这些外围集合与它们作为可构造载体元素的呈现连接起来。

```agda
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ∈∈ₛ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( ∅; ∅-empty; module InfinitySet )
open InfinitySet {ℓ} using ( #_; sucV; ω )
```

以 `S` 表示可构造模型的载体。它的元素由外围集合及其可构造性证明组成。所有隐藏的表与见证都在这一载体上量化；最终保留的可见槽位也分别呈现取值 `a`、层索引 `p` 与公共界 `z`。

```agda
open hPropStructure 𝒮ʟ using ( S )
```

`L` 内部的满足关系与外围层级中的满足关系使用不同结构，但当 Δ₀ 公式的参数来自 `L` 时，两种读法一致。引理 `abs₀` 正是二者之间的桥。借助它，完备性可以在内部构造公式的满足，而可靠性可以把搬运后的公式读回外围的层相等。

```agda
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using ( _^_; _⊨ᵐ_; abs₀ )
open AbsL using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ )
module SemVᵃ = FOL.Semantics 𝒮ᵥ
```

公式 `defIn w z N body` 用四层嵌套的有界存在量词，把满足关系表 `T`、码集 `C`、环境塔 `E` 与取值 `d` 放入 `z`。满足描述验证 `w` 处取值上的 `T`、`C`、`E`，可定义幂集描述把 `d` 认同为该取值的可定义幂集，而 `body` 则陈述对 `d` 的进一步要求。满足关系只保留这些见证的命题截断，并且该公式并不唯一刻画 `z`。

```agda
defIn : ∀ {k} → Fin k → Fin k → (Fin 10 → Fin k) → Formula S (4 + k) → Formula S k
defIn w z N body =
  ∃̇∈ (var z) (∃̇∈ (var (sh 1 z)) (∃̇∈ (var (sh 2 z)) (∃̇∈ (var (sh 3 z))
    (satAt i3 (sh 4 w) i2 i1 (shN 4 N) ∧̇ (defAt i0 (sh 4 w) i3 i2 (shN 4 N) ∧̇ body)))))
```

内向包含式 `intoAt` 说，每个 `x ∈ v` 都由某个更早的层索引 `c ∈ b` 说明：`f` 中有一个有序对形的成员在 `c` 处记录取值 `w`，而 `x` 属于 `w` 的可定义幂集。其外层有界形状是 `∀[ x ∈ v ] ∃[ c ∈ b ] ...`；余下的有界见证展开该表行以及识别这个幂集所需的数据。

```agda
intoAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m
intoAt v b f z N =
  ∀̇∈ (var v) (∃̇∈ (var (sh 1 b)) (∃̇∈ (var (sh 2 f))
    (sndEx i0 i1 (defIn i0 (sh 5 z) (shN 5 N) (var i8 ∈̇ var i0)))))
```

反向包含式 `overAt` 遍历 `c ∈ b`，并遍历 `f` 中可呈现为有序对 `(c,w)` 的成员。对每个这样的呈现，`w` 的可定义幂集的每个成员都必须属于 `v`。该子句不讨论 `f` 中无法如此呈现的成员，因此不能把它读成从整个候选表中排除了任意垃圾成员。

```agda
overAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m
overAt v b f z N =
  ∀̇∈ (var b) (∀̇∈ (var (sh 1 f))
    (sndAll i0 i1 (defIn i0 (sh 4 z) (shN 4 N) (∀̇∈ (var i0) (var i0 ∈̇ var (sh 9 v))))))
```

合取式 `stepAt` 合并这两个包含。相对于 `b` 以下记录的有序对表行，`intoAt` 说明 `v` 没有额外成员，`overAt` 则说明可定义幂集的贡献一项不缺。表中取值的正确性是后续读引理另行要求的假设。

```agda
stepAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m
stepAt v b f z N = intoAt v b f z N ∧̇ overAt v b f z N
```

`approxAt` 的前半给出覆盖性：每个 `c ∈ b` 在 `f` 中都有某个有序对形的表项。后半则在 `f` 的一个成员被呈现为 `(c,w)` 时检验 `stepAt w c f z N`。它并未断言 `f` 的每个成员都是有序对，也未断言每个被记录的第一分量都低于 `b`。因此，`approx-out` 恰好恢复 `Values f b × Entries f b`，既不恢复与整个层级图的相等，也不恢复全局的无垃圾性质。

```agda
approxAt : ∀ {m} → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m
approxAt f b z N =
    ∀̇∈ (var b) (∃̇∈ (var (sh 1 f)) (sndEx i0 i1 ⊤̇))
  ∧̇ ∀̇∈ (var f) (bothAll i0 (stepAt i0 i1 (sh 4 f) (sh 4 z) (shN 4 N)))
```

子句 `hierAt a p f z N` 把 `p` 以下的逼近与 `p` 处的最后一步连接起来。若逼近给出 `Values` 与 `Entries`，最后一步便把 `a` 认同为 `Lset p`；反过来，精确的层级表 `IsHier p f` 与充分的见证供应可以填入两个合取支。这就是最终三变元公式将在有界见证之后隐藏的局部层关系。

```agda
hierAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m
hierAt a p f z N = approxAt f p z N ∧̇ stepAt a p f z N
```

标签子句把十个槽位钉在数码上：第一个槽位没有成员，故它是空集。

```agda
pins : ∀ {m} → (Fin 10 → Fin m) → Formula S m
pins N =
    ∀̇∈ (var (N f0)) ⊥̇
  ∧̇ ( sucAtL (N f0) (N f1) ∧̇ ( sucAtL (N f1) (N f2) ∧̇ ( sucAtL (N f2) (N f3)
  ∧̇ ( sucAtL (N f3) (N f4) ∧̇ ( sucAtL (N f4) (N f5) ∧̇ ( sucAtL (N f5) (N f6)
```

其余九个槽位由九条后继断言串联，于是十个槽位恰是数码零至九。

```agda
  ∧̇ ( sucAtL (N f6) (N f7) ∧̇ ( sucAtL (N f7) (N f8) ∧̇ sucAtL (N f8) (N f9) ))))))))
```

## 层级表的有界子句

为了在后续描述中使用这十个标签，对象语言中的固定条件必须与语义记录 `Tags γ N` 一致。接下来的两个引理证明两个方向：一个从 `pins` 读出数码等式，另一个由这些等式重建 `pins`。

```agda
module PinsRead {m : ℕ} (N : Fin 10 → Fin m) (γ : S ^ m) where
```

读取标签子句先证第一个槽位为空：它没有成员。

```agda
  pins-out : ⟨ γ ⊨ pins N ⟩ → Tags γ N
  pins-out (h0 , hs) = go
    where
    q0 : fst (lookup (N f0) γ) ≡ # 0
    q0 = extensionalV (λ y → ⇔toPath
```

空性是双向的外延性论证：第一个槽位的任何成员都会与假值子句矛盾，而空集本无成员。

```agda
      (λ y∈ → Empty.rec* (h0 (down (lookup (N f0) γ) y y∈) y∈))
      (λ y∈ → Empty.rec (∅-empty y (∈∈ₛ {a = y} {b = ∅} .fst y∈))))
```

辅助引理 `up` 沿数码链前进一步。若槽位 `i` 表示 `# k` 且 `sucAtL i j` 成立，则其可靠读法把槽位 `j` 认同为 `sucV (# k)`，因而认同为数码 `# (suc k)`。

```agda
    up : (i j : Fin m) (k : ℕ) → ⟨ γ ⊨ sucAtL i j ⟩ → fst (lookup i γ) ≡ # k
       → fst (lookup j γ) ≡ # (suc k)
    up i j k h q = suc-out i j γ h ∙ cong sucV q
```

从零的等式出发，前五条后继子句依次给出 `q1` 至 `q5`。因此，由 `f1` 至 `f5` 命名的槽位分别被认同为数码一至五。

```agda
    q1 = up (N f0) (N f1) 0 (hs .fst) q0
    q2 = up (N f1) (N f2) 1 (hs .snd .fst) q1
    q3 = up (N f2) (N f3) 2 (hs .snd .snd .fst) q2
    q4 = up (N f3) (N f4) 3 (hs .snd .snd .snd .fst) q3
    q5 = up (N f4) (N f5) 4 (hs .snd .snd .snd .snd .fst) q4
```

余下四条后继子句延续同一条链，给出 `q6` 至 `q9`。由此，槽位 `f6` 至 `f9` 分别被认同为数码六至九，数码读取也随之完成。

```agda
    q6 = up (N f5) (N f6) 5 (hs .snd .snd .snd .snd .snd .fst) q5
    q7 = up (N f6) (N f7) 6 (hs .snd .snd .snd .snd .snd .snd .fst) q6
    q8 = up (N f7) (N f8) 7 (hs .snd .snd .snd .snd .snd .snd .snd .fst) q7
    q9 = up (N f8) (N f9) 8 (hs .snd .snd .snd .snd .snd .snd .snd .snd) q8
```

记录 `Tags γ N` 要求对 `Fin 10` 的每个元素给出相应的数码等式。前四个情形返回 `q0`、`q1`、`q2` 与 `q3`，分别对应标签零至三。

```agda
    go : Tags γ N
    go zero = q0
    go (suc zero) = q1
    go (suc (suc zero)) = q2
    go (suc (suc (suc zero))) = q3
```

`go` 接下来的五个情形返回 `q4` 至 `q8`。这些模式写成嵌套后继，直接穷尽标签四至八，无须再引入算术论证。

```agda
    go (suc (suc (suc (suc zero)))) = q4
    go (suc (suc (suc (suc (suc zero))))) = q5
    go (suc (suc (suc (suc (suc (suc zero)))))) = q6
    go (suc (suc (suc (suc (suc (suc (suc zero))))))) = q7
    go (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) = q8
```

`Fin 10` 唯一剩余的情形是零的第九次后继，它返回 `q9`。至此，分类讨论供给了 `Tags γ N` 所需的全部十条数码等式。

```agda
    go (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))) = q9
```

反过来，设这些槽位已经满足 `Tags γ N`。零槽位的任意假定成员都可沿标签等式搬运为空集的成员，因而不可能存在；同一组标签等式随后供给填入九条后继子句所需的数据。

```agda
  pins-in : Tags γ N → ⟨ γ ⊨ pins N ⟩
  pins-in tg =
      (λ x x∈ → Empty.rec (∅-empty (fst x) (∈∈ₛ {a = fst x} {b = ∅} .fst
                  (subst (λ u → ⟨ fst x ∈ u ⟩) (tg f0) x∈))))
    , ( st f0 f1 refl , ( st f1 f2 refl , ( st f2 f3 refl , ( st f3 f4 refl , ( st f4 f5 refl , ( st f5 f6 refl
```

每条后继子句都先沿相应的数码等式改写两个标签槽，再应用后继公式的向内读法来重建。

```agda
    , ( st f6 f7 refl , ( st f7 f8 refl , st f8 f9 refl ))))))))
    where
    st : (j k : Fin 10) → # (toℕ k) ≡ sucV (# (toℕ j)) → ⟨ γ ⊨ sucAtL (N j) (N k) ⟩
    st j k e = suc-in (N j) (N k) γ (tg k ∙ e ∙ cong sucV (sym (tg j)))
```

固定一个环境 `δ`，其中十个具名槽位都具有所要求的数码值。以 `Wv` 表示 `w` 处的底层集合，以 `Zv` 表示 `z` 处的底层集合。前者是解释可定义性的层，后者则是必须容纳四个见证的公共界。

```agda
module DefInRead {k : ℕ} (w z : Fin k) (N : Fin 10 → Fin k) (body : Formula S (4 + k))
  (δ : S ^ k) (tg : Tags δ N) where
  private
    Wv = fst (lookup w δ)
    Zv = fst (lookup z δ)
```

四个见证依次绑定为 `T`、`C`、`E` 与 `d`。由于每个新约束子都从环境前端扩展，主体在 `d ∷ E ∷ C ∷ T ∷ δ` 上求值。因此，其前四个槽位依次指向可定义幂集的取值、环境塔、码集与满足关系表。

```agda
  δ4 : (T C E d : S) → S ^ (4 + k)
  δ4 T C E d = d ∷ E ∷ C ∷ T ∷ δ
```

读取 `defIn` 时，四个见证 `T`、`C`、`E`、`d` 外面的命题截断保持不变。其结论有意只保留 `d ∈ z`、`d = 𝒟ₒ Wv`，以及主体在扩展环境中成立。`T`、`C`、`E` 属于 `z` 的证明，以及内部的满足描述与幂集描述证明，都在导出这条较弱陈述时被消耗。

```agda
  defIn-out : ⟨ δ ⊨ defIn w z N body ⟩
            → ∥ Σ[ T ∈ S ] Σ[ C ∈ S ] Σ[ E ∈ S ] Σ[ d ∈ S ]
                (⟨ fst d ∈ Zv ⟩ × ((fst d ≡ 𝒟ₒ Wv) × ⟨ δ4 T C E d ⊨ body ⟩)) ∥₁
  defIn-out = PT.rec squash₁ (λ { (T , (T∈ , h1)) → PT.rec squash₁ (λ { (C , (C∈ , h2)) →
    PT.rec squash₁ (λ { (E , (E∈ , h3)) → PT.map (λ { (d , (d∈ , (hs , (hd , hb)))) →
```

四层嵌套截断暴露见证之后，`def-sound` 把满足描述 `hs` 与可定义幂集描述 `hd` 合并起来。这里保留的唯一等式正是其结论 `d = 𝒟ₒ Wv`；主体的证明则原样继续传递。

```agda
      T , C , E , d , ( d∈ , ( def-sound i0 (sh 4 w) i3 i2 i1 (shN 4 N) (δ4 T C E d) (lookup w δ) refl tg hs hd
                             , hb )) })
      h3 }) h2 }) h1 })
```

反过来，要从语义数据证明 `defIn`，就必须显式给出真实见证：由 `w` 表示的可构造载体 `W`、四个集合及其属于 `z` 的证明、它们分别与真实满足关系表、码集、环境塔和可定义幂集的同一视，以及主体的证明。因此，这个方向所假设的数据多于向外读取有意保留的数据。

```agda
  defIn-in : (W : S) → Wv ≡ fst W → (T C E d : S)
           → ⟨ fst T ∈ Zv ⟩ → ⟨ fst C ∈ Zv ⟩ → ⟨ fst E ∈ Zv ⟩ → ⟨ fst d ∈ Zv ⟩
           → fst T ≡ fst (SatGraph.pairs W) → fst C ≡ fst (AllCodes W) → fst E ≡ fst (Tower.tower W)
           → fst d ≡ 𝒟ₒ (fst W) → ⟨ δ4 T C E d ⊨ body ⟩ → ⟨ δ ⊨ defIn w z N body ⟩
  defIn-in W qw T C E d T∈ C∈ E∈ d∈ qT qC qE qd hb =
```

在向内读法中，`sat-complete` 先证明真实的满足关系表、码集与环境塔满足 `satAt`。`def-complete` 再使用这一证明和给定的 `d` 的等式，证明可定义幂集子句。给定的主体证明补全合取，随后四个见证及其隶属证明被依次引入嵌套的命题截断中。

```agda
    ∣ T , ( T∈ , ∣ C , ( C∈ , ∣ E , ( E∈ , ∣ d , ( d∈ , ( hs
      , ( def-complete i0 (sh 4 w) i3 i2 i1 (shN 4 N) (δ4 T C E d) W qw tg hs qd , hb ))) ∣₁ ) ∣₁ ) ∣₁ ) ∣₁
    where
    hs : ⟨ δ4 T C E d ⊨ satAt i3 (sh 4 w) i2 i1 (shN 4 N) ⟩
    hs = sat-complete i3 (sh 4 w) i2 i1 (shN 4 N) (δ4 T C E d) W qw qT qC qE tg
```

谓词 `Supply` 说：对序数 `c`，`defIn` 所需的四个见证都已在公共界之内，即层 `Lset c` 的满足图、码集与环境塔，以及下一层 `Lset (sucV c)`。

```agda
Supply : (Zv : V ℓ) (c : V ℓ) → IsOrd c → Type (ℓ-suc ℓ)
Supply Zv c oc =
    ⟨ fst (SatGraph.pairs (LsetS c oc)) ∈ Zv ⟩
  × ( ⟨ fst (AllCodes (LsetS c oc)) ∈ Zv ⟩
  × ( ⟨ fst (Tower.tower (LsetS c oc)) ∈ Zv ⟩
```

第四分量是下一层，正是逼近的后继一步所需的。

```agda
  × ⟨ Lset (sucV c) ∈ Zv ⟩ ))
```

现固定环境 `γ` 中一个拟议的层级步骤。以 `Vv` 表示拟议结果，以 `Bv` 表示此前索引组成的集合，以 `Fv` 表示候选表的底层集合。要问的是：一旦知道 `Fv` 中相关表行取值正确且确实存在，这两个有界包含是否迫使 `Vv` 等于 `Lset Bv`。

```agda
module StepRead {m : ℕ} (v b f z : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (tg : Tags γ N) where
  private
    Vv = fst (lookup v γ)
    Bv = fst (lookup b γ)
    Fv = fst (lookup f γ)
```

以 `Zv` 表示公共界的底层集合。它控制可在何处找到辅助的满足关系、码、环境塔与可定义幂集见证。单步所求的等式本身不提及 `Zv`；这个界使描述能够成立，却不成为所得层取值的一部分。

```agda
    Zv = fst (lookup z γ)
```

在内向主体中，`d` 是由 `defIn` 识别的可定义幂集，而 `x` 是外层对 `v` 的有界全称量词引入的成员。原子主体陈述 `x ∈ d`。一旦把记录值 `w` 认同为 `Lset c`，这就成为对某个 `c ∈ b` 的 `𝒟ₒ (Lset c)` 的隶属。

```agda
    intoBody : Formula S (5 + m)
    intoBody = defIn i0 (sh 5 z) (shN 5 N) (var i8 ∈̇ var i0)
```

`over` 主体是一条可定义幂集描述，其内层公式断言，被描述集合的每个成员都属于拟议的下一取值。这给出并集等式所需的反向包含。

```agda
    overBody : Formula S (4 + m)
    overBody = defIn i0 (sh 4 z) (shN 4 N) (∀̇∈ (var i0) (var i0 ∈̇ var (sh 9 v)))
```

单步读引理另行假设：`Bv` 以下每条有序对表行都具有正确取值 (`Values`)，并且 `Bv` 以下每个索引都有其正準表行 (`Entries`)。恰在这两个假设下，`stepAt` 的两半给出相反方向的隶属蕴含，外延性遂得到 `Vv = Lset Bv`。这些假设只约束相关的有序对表行，并不排除候选表中无关的成员。

```agda
  step-out : ⟨ γ ⊨ stepAt v b f z N ⟩ → Values (lookup f γ) Bv → Entries (lookup f γ) Bv → Vv ≡ Lset Bv
  step-out (hi , ho) vals ents = extensionalV (λ x → ⇔toPath (fwd x) (bwd x))
    where
    fwd : (x : V ℓ) → ⟨ x ∈ Vv ⟩ → ⟨ x ∈ Lset Bv ⟩
    fwd x x∈ = PT.rec (snd (x ∈ Lset Bv)) (λ { (c , (c∈ , h1)) → PT.rec (snd (x ∈ Lset Bv))
```

对正向包含，`intoAt` 给出层索引 `c ∈ Bv`、表中的有序对表行 `(c,w)`，以及包含 `x` 的可定义幂集值 `d`。假设 `Values` 把 `w` 认同为 `Lset c`，故 `d = 𝒟ₒ (Lset c)`；层的向内规则 `Lset-in` 随即把 `x` 从这一份贡献送入 `Lset Bv`。

```agda
      (λ { (q , (q∈ , h2)) → PT.rec (snd (x ∈ Lset Bv)) (λ { (w , s , (eq , h3)) →
        PT.rec (snd (x ∈ Lset Bv)) (λ { (T , C , E , d , (d∈ , (qd , hx))) →
          Lset-in Bv (fst c) x c∈
            (subst (λ u → ⟨ x ∈ u ⟩)
              (qd ∙ cong 𝒟ₒ (vals c w c∈ (subst (λ u → ⟨ u ∈ Fv ⟩) eq q∈))) hx) })
```

嵌套存在式的各层读取都保持命题截断。`sndEx-out` 先从有序对形的表项中仅仅恢复第二分量 `w`，`defIn-out` 再仅仅恢复辅助数据，以及把 `d` 认同为 `w` 的可定义幂集的等式。每一层截断都直接消去到隶属命题 `x ∈ Lset Bv`。

```agda
        (DefInRead.defIn-out i0 (sh 5 z) (shN 5 N) (var i8 ∈̇ var i0) (w ∷ s ∷ q ∷ c ∷ xS ∷ γ) tg h3) })
        (sndEx-out i0 i1 intoBody (q ∷ c ∷ xS ∷ γ) h2) })
      h1 })
      (hi xS x∈)
      where
```

证明从外围成员 `x ∈ Vv` 出发，但公式是在可构造载体 `S` 上解释的。运算 `down` 利用这一隶属证明把 `x` 呈现为载体元素 `xS`；再把 `xS` 放到环境前端，便使新约束的槽位表示同一个底层集合 `x`。

```agda
      xS : S
      xS = down (lookup v γ) x x∈
```

`step-out` 的反向包含把真实层 `Lset Bv` 的成员送入拟议取值 `Vv`。它消去 `Lset Bv` 的截断层分解，把目标化归为更早层 `δ`，其中 `x` 属于该层的可定义幂集。

```agda
    bwd : (x : V ℓ) → ⟨ x ∈ Lset Bv ⟩ → ⟨ x ∈ Vv ⟩
    bwd x x∈ = PT.rec (snd (x ∈ Vv)) put (Lset-out Bv x x∈)
      where
      put : Σ[ δ ∈ V ℓ ] (⟨ δ ∈ Bv ⟩ × ⟨ x ∈ 𝒟ₒ (Lset δ) ⟩) → ⟨ x ∈ Vv ⟩
      put (δ , (δ∈ , xD)) = PT.rec (snd (x ∈ Vv))
```

`Lset-out` 给出更早的索引 `δ` 后，完备性提供典范表条目 `(δ, Lset δ)`。`over` 子句施用于这条目，`defIn-out` 再把其中的有界集合 `d` 同认于 `𝒟ₒ (Lset δ)`。因此，其全称体把给定的 `x` 放入拟议取值 `Vv`。这个方向使用 `Entries` 提供的典范条目，无须另行诉诸 `Values`。

```agda
        (λ { (T , C , E , d , (d∈ , (qd , hsub))) →
          hsub (down d x (subst (λ u → ⟨ x ∈ u ⟩) (sym qd) xD)) (subst (λ u → ⟨ x ∈ u ⟩) (sym qd) xD) })
        (DefInRead.defIn-out i0 (sh 4 z) (shN 4 N) (∀̇∈ (var i0) (var i0 ∈̇ var (sh 9 v)))
          (w ∷ container q c w refl .fst ∷ q ∷ c ∷ γ) tg
          (useSnd i0 (q ∷ c ∷ γ) c w refl overBody i1 refl (ho c δ∈ q (ents c δ∈))))
```

两个被命名的对象是编码实参与编码对：二者都沿其隶属证明下降而呈现为载体元素。

```agda
        where
        c : S
        c = down (lookup b γ) δ δ∈
        q : S
        q = down (lookup f γ) (pr δ (Lset δ)) (ents c δ∈)
```

该行的取值 `w` 从对呈现中读取，正是体的满足所消耗的分量。

```agda
        w : S
        w = sndS q δ (Lset δ) refl
```

步进子句的向内方向需要五条假设：界的序数性、拟议取值与界处层的等同、表在界处的正确性与完备性，以及把界的每个成员所需的辅助见证放进见证界的供给函数。证明分为两个合取项。

```agda
  step-in : (ob : IsOrd Bv) → Vv ≡ Lset Bv → Values (lookup f γ) Bv → Entries (lookup f γ) Bv
          → ((c : V ℓ) (oc : IsOrd c) → ⟨ c ∈ Bv ⟩ → Supply Zv c oc)
          → ⟨ γ ⊨ stepAt v b f z N ⟩
  step-in ob vq vals ents sup = into , over
    where
```

`into` 合取项从拟议取值的成员 `x` 向外读取：界处层的截断分解名指更早序数与可定义幂集隶属，存在引入把它们填入两个有界量词。

```agda
    into : ⟨ γ ⊨ intoAt v b f z N ⟩
    into x x∈ = PT.rec squash₁ put (Lset-out Bv (fst x) (subst (λ u → ⟨ fst x ∈ u ⟩) vq x∈))
      where
      put : Σ[ δ ∈ V ℓ ] (⟨ δ ∈ Bv ⟩ × ⟨ fst x ∈ 𝒟ₒ (Lset δ) ⟩)
          → ⟨ (x ∷ γ) ⊨ ∃̇∈ (var (sh 1 b)) (∃̇∈ (var (sh 2 f)) (sndEx i0 i1 intoBody)) ⟩
```

这些嵌套有界存在量词的填充并不从命题截断中取出数据。证明把 `δ` 呈现为载体元素 `c`，用 `Entries` 把典范对呈现为 `q`，再由 `fillSnd` 提供有序对分解；余下的公式体就是 `hb`。每次构造都保留 `∃[]-syntax` 内含的命题截断，因为满足关系本身是命题。

```agda
      put (δ , (δ∈ , xD)) =
        ∣ c , ( δ∈ , ∣ q , ( ents c δ∈ , fillSnd i0 (q ∷ c ∷ x ∷ γ) c w refl intoBody hb i1 refl ) ∣₁ ) ∣₁
        where
        oδ : IsOrd δ
        oδ = mem-ord {A = Bv} ob δ δ∈
```

三个载体元素有不同的来源。隶属 `δ ∈ Bv` 把更早的索引呈现为 `c`；典范对属于表的证明把该对呈现为 `q`；而 `δ` 的序数性使 `LsetS` 能把层 `Lset δ` 呈现为 `w`。组装有界见证时，必须区分这三种来源。

```agda
        c : S
        c = down (lookup b γ) δ δ∈
        q : S
        q = down (lookup f γ) (pr δ (Lset δ)) (ents c δ∈)
        w : S
```

这里的 `w` 是可构造载体中的真实层 `Lset δ`。在 `δ` 处应用供给假设，得到满足关系表、码集、环境塔与后继层都属于 `Zv` 的证明。有了这四个界及其定义等式，`defIn-in` 把余下义务归结为数学事实 `x ∈ 𝒟ₒ (Lset δ)`。

```agda
        w = LsetS δ oδ
        s = sup δ oδ δ∈
        hb : ⟨ (w ∷ container q c w refl .fst ∷ q ∷ c ∷ x ∷ γ) ⊨ intoBody ⟩
        hb = DefInRead.defIn-in i0 (sh 5 z) (shN 5 N) (var i8 ∈̇ var i0)
               (w ∷ container q c w refl .fst ∷ q ∷ c ∷ x ∷ γ) tg w refl
```

四个有界对象分别是真实的满足关系表、码集、环境塔与 `Lset (sucV δ)`。供给假设证明它们都属于 `Zv`，前三个对象则由自反等式同描述所要求的结构对齐。最后，`Lset-suc δ` 把第四个对象同认于 `𝒟ₒ (Lset δ)`，于是 `x` 原有的隶属可被运输到公式体中。

```agda
               (SatGraph.pairs w) (AllCodes w) (Tower.tower w) (LsetS (sucV δ) (suc-ord oδ))
               (s .fst) (s .snd .fst) (s .snd .snd .fst) (s .snd .snd .snd) refl refl refl (Lset-suc δ)
               (subst (λ u → ⟨ fst x ∈ u ⟩) (sym (Lset-suc δ)) xD)
```

证明 `over` 合取项时，固定 `c ∈ Bv`、表的成员 `q`，以及把 `q` 呈现为有序对 `(c,w)` 的方式。正确性随即把 `w` 同认于 `Lset c`。余下目标对 `y` 一致：每个 `y ∈ 𝒟ₒ w` 都必须属于拟议取值 `Vv`。这正是把拟议取值同认于 `Bv` 处层所需的第二个包含关系。

```agda
    over : ⟨ γ ⊨ overAt v b f z N ⟩
    over c c∈ q q∈ = sndAll-in i0 i1 overBody (q ∷ c ∷ γ) (λ w s s∈ w∈ e →
      let wq : fst w ≡ Lset (fst c)
          wq = vals c w c∈ (subst (λ u → ⟨ u ∈ Fv ⟩) e q∈)
          oc : IsOrd (fst c)
```

`c` 的序数性承继自界；层被呈现为载体元素；供给函数在 `c` 处产出四个见证。

```agda
          oc = mem-ord {A = Bv} ob (fst c) c∈
          W : S
          W = LsetS (fst c) oc
          s' = sup (fst c) oc c∈
      in DefInRead.defIn-in i0 (sh 4 z) (shN 4 N) (∀̇∈ (var i0) (var i0 ∈̇ var (sh 9 v)))
```

`c` 处的供给把真实的满足关系表、码集、环境塔与后继层都界定在 `Zv` 内，因此 `defIn-in` 可以建立可定义幂集描述。若 `y` 属于那里描述的集合，`Lset-suc c` 先把它化为 `y ∈ 𝒟ₒ (Lset c)`，再由 `c ∈ Bv` 通过 `Lset-in` 得到 `y ∈ Lset Bv`。最后沿 `Vv ≡ Lset Bv` 运输，便得到 `y` 属于拟议取值。

```agda
           (w ∷ s ∷ q ∷ c ∷ γ) tg W wq
           (SatGraph.pairs W) (AllCodes W) (Tower.tower W) (LsetS (sucV (fst c)) (suc-ord oc))
           (s' .fst) (s' .snd .fst) (s' .snd .snd .fst) (s' .snd .snd .snd) refl refl refl (Lset-suc (fst c))
           (λ y y∈d → subst (λ u → ⟨ fst y ∈ u ⟩) (sym vq)
             (Lset-in Bv (fst c) (fst y) c∈ (subst (λ u → ⟨ fst y ∈ u ⟩) (Lset-suc (fst c)) y∈d))))
```

逼近读取器以表、界、见证界、标签映射与环境为参数。三个底层集合一次性命名。

```agda
module ApproxRead {m : ℕ} (f b z : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (tg : Tags γ N) where
  private
    Fv = fst (lookup f γ)
    Bv = fst (lookup b γ)
    Zv = fst (lookup z γ)
```

步进体是在四个平移槽位处的步进子句。

```agda
    stepBody : Formula S (4 + m)
    stepBody = stepAt i0 i1 (sh 4 f) (sh 4 z) (shN 4 N)
```

逼近子句的向外读法产出表在界处的正确性与完备性。谓词 `P` 记录对每个实参须证之事：其被记录取值是该实参处的层。请仔细注意所证与所未证：结果恰为 `Values` 与 `Entries`；它不说表中没有非对成员、也没有第一分量落在界外的条目。

```agda
  approx-out : ⟨ γ ⊨ approxAt f b z N ⟩ → IsOrd Bv → Values (lookup f γ) Bv × Entries (lookup f γ) Bv
  approx-out (hd , hs) ob = vals , ents
    where
    P : V ℓ → Type (ℓ-suc ℓ)
    P c = ⟨ c ∈ Bv ⟩ → (w : S) → ⟨ pr c (fst w) ∈ Fv ⟩ → fst w ≡ Lset c
```

覆盖子句说：对每个 `c ∈ Bv`，仅命题截断地存在一个表成员，它呈现为第一分量是 `c` 的有序对。读取这个对会显出取值 `w`，并把原隶属证明运输到典范记号 `pr c w` 上。结果仍受命题截断，因此 `entryOf` 只为后续命题推理提供存在性，并不在全局选出一个取值。

```agda
    entryOf : (c : S) → ⟨ fst c ∈ Bv ⟩ → ∥ Σ[ w ∈ S ] ⟨ pr (fst c) (fst w) ∈ Fv ⟩ ∥₁
    entryOf c c∈ = PT.rec squash₁
      (λ { (q , (q∈ , h)) → PT.map (λ { (w , s , (e , _)) → w , subst (λ u → ⟨ u ∈ Fv ⟩) e q∈ })
                              (sndEx-out i0 i1 ⊤̇ (q ∷ c ∷ γ) h) })
      (hd c c∈)
```

归纳步验证任意一条满足 `c ∈ Bv` 的被记录对 `(c,w)`。它的隶属证明使逼近的第二子句给出 `stepAt w c`；归纳假设提供 `c` 以下每个实参处的正确性，覆盖子句则将在这些位置提供相应的典范条目。于是 `StepRead.step-out` 可断定，被记录取值恰为 `Lset c`。

```agda
    step : (c : V ℓ) → ((y : V ℓ) → ⟨ y ∈ c ⟩ → P y) → P c
    step c IH c∈ w rec =
      StepRead.step-out i0 i1 (sh 4 f) (sh 4 z) (shN 4 N) env tg
        (useBoth i0 (q ∷ γ) cS w refl stepBody (hs q rec)) vals' ents'
      where
```

证明现在把有关集合呈现在可构造载体中。隶属 `c ∈ Bv` 给出载体元素 `cS`，而 `pr c (fst w)` 属于表的假设给出 `q`。取值 `w` 已经是归纳谓词所接收的载体元素；接下来的环境把这三个呈现放入步进公式所要求的槽位。

```agda
      cS : S
      cS = down (lookup b γ) c c∈
      q : S
      q = down (lookup f γ) (pr c (fst w)) rec
      env : S ^ (4 + m)
```

扩展环境为步进读法装配四个槽位。界的序数性把更小的实参限制到界以下，而更小实参处的正确性读取即归纳假设的限制。

```agda
      env = w ∷ cS ∷ container q cS w refl .fst ∷ q ∷ γ
      in' : (y : S) → ⟨ fst y ∈ c ⟩ → ⟨ fst y ∈ Bv ⟩
      in' y y∈ = ob .fst {x = c} {y = fst y} y∈ c∈
      vals' : Values (lookup f γ) c
      vals' y w' y∈ rec' = IH (fst y) y∈ (in' y y∈) w' rec'
```

更小实参处的完备性以同一限制恢复：对每个更小实参，消耗其截断条目，而归纳假设的取值等式把典范条目运到位。

```agda
      ents' : Entries (lookup f γ) c
      ents' y y∈ = PT.rec (snd (pr (fst y) (Lset (fst y)) ∈ Fv))
        (λ { (w' , rec') → subst (λ u → ⟨ pr (fst y) u ∈ Fv ⟩) (IH (fst y) y∈ (in' y y∈) w' rec') rec' })
        (entryOf y (in' y y∈))
```

`Bv` 以下的正确性通过在外围累积层级中对底层实参 `c` 作隶属归纳而得。谓词 `P c` 以 `c ∈ Bv` 为条件；这项隶属既把定理限制在所需界内，又借助 `Bv` 的序数性，使每个更小实参都可使用归纳假设。把归纳结论施于任意被记录取值，便得到 `Values`。

```agda
    vals : Values (lookup f γ) Bv
    vals c w c∈ rec = ∈-induction {P = P} step (fst c) c∈ w rec
```

界处的完备性复合截断条目与刚证的正确性：取值等式把被记录条目运成典范条目。

```agda
    ents : Entries (lookup f γ) Bv
    ents c c∈ = PT.rec (snd (pr (fst c) (Lset (fst c)) ∈ Fv))
      (λ { (w , rec) → subst (λ u → ⟨ pr (fst c) u ∈ Fv ⟩) (vals c w c∈ rec) rec })
      (entryOf c c∈)
```

逼近子句的向内方向从更强的语义假设出发：表在界处实现层级。这一不对称是有意的：向外方向只证两条表条件，而向内方向消耗完整的层级规格。

```agda
  approx-in : (ob : IsOrd Bv) → IsHier Bv (lookup f γ)
            → ((c : V ℓ) (oc : IsOrd c) → ⟨ c ∈ Bv ⟩ → Supply Zv c oc)
            → ⟨ γ ⊨ approxAt f b z N ⟩
  approx-in ob sp sup = dom , steps
    where
```

层级规格的向外读法说：每条被记录对的实参低于界，其取值等于该处的层。

```agda
    hout : (c w : S) → ⟨ pr (fst c) (fst w) ∈ Fv ⟩ → ⟨ fst c ∈ Bv ⟩ × (fst w ≡ Lset (fst c))
    hout = hier-out Bv ob (lookup f γ) sp
```

向内读法说：界以下每条典范对都被记录。

```agda
    hin : (c : S) → ⟨ fst c ∈ Bv ⟩ → ⟨ pr (fst c) (Lset (fst c)) ∈ Fv ⟩
    hin = hier-in Bv ob (lookup f γ) sp
```

定义域合取项的证明：对界以下每个实参呈现其层，并把典范对注入表。

```agda
    dom : ⟨ γ ⊨ ∀̇∈ (var b) (∃̇∈ (var (sh 1 f)) (sndEx i0 i1 ⊤̇)) ⟩
    dom c c∈ = ∣ q , ( hin c c∈ , fillSnd i0 (q ∷ c ∷ γ) c w refl ⊤̇ (λ z → z) i1 refl ) ∣₁
      where
      w : S
      w = LsetS (fst c) (mem-ord {A = Bv} ob (fst c) c∈)
```

正準对沿其隶属证明下降而呈现为载体元素。

```agda
      q : S
      q = down (lookup f γ) (pr (fst c) (Lset (fst c))) (hin c c∈)
```

逼近的第二合取项须对表的每个成员 `q`，以及把 `q` 呈现为有序对 `(c,w)` 的每种方式成立。在这样的呈现下，精确的层级规格同时给出 `c ∈ Bv` 与 `w ≡ Lset c`，从而可在 `c` 处证明步进公式。这里并未断言候选表的任意成员都具有这种有序对呈现。

```agda
    steps : ⟨ γ ⊨ ∀̇∈ (var f) (bothAll i0 stepBody) ⟩
    steps q q∈ = bothAll-in i0 stepBody (q ∷ γ) (λ c w s s∈ c∈s w∈s e →
      let rec : ⟨ pr (fst c) (fst w) ∈ Fv ⟩
          rec = subst (λ u → ⟨ u ∈ Fv ⟩) e q∈
          c∈ : ⟨ fst c ∈ Bv ⟩
```

实参由层级向外读法低于界；序数性被承继；`StepRead.step-in` 接收全部五条假设，包括限制后的正确性与完备性及每个更小实参处的供给。

```agda
          c∈ = hout c w rec .fst
          oc : IsOrd (fst c)
          oc = mem-ord {A = Bv} ob (fst c) c∈
      in StepRead.step-in i0 i1 (sh 4 f) (sh 4 z) (shN 4 N) (w ∷ c ∷ s ∷ q ∷ γ) tg oc (hout c w rec .snd)
           (λ d w' d∈ rec' → hout d w' rec' .snd)
```

在当前实参 `c` 以下，完备性来自 `hier-in`：序数界的传递性把 `d ∈ c ∈ Bv` 化为 `d ∈ Bv`，于是典范条目确实存在。辅助界有不同的来源：它们来自给定的供给函数 `sup`，并沿同一传递性论证限制到 `c` 以下。因此，层级规格提供表条目，而 `sup` 提供四个有界编码对象。

```agda
           (λ d d∈ → hin d (ob .fst {x = fst c} {y = fst d} d∈ c∈))
           (λ d od d∈ → sup d od (ob .fst {x = fst c} {y = d} d∈ c∈)))
```

层级读法有四个特殊槽位：拟议层 `a`、它的层索引 `p`、逼近表 `f` 与公共见证界 `z`。标签映射解释编码公式所用的十个数码位置，环境则为所有这些槽位提供载体元素。

```agda
module HierRead {m : ℕ} (a p f z : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (tg : Tags γ N) where
  private
    Av = fst (lookup a γ)
    Pv = fst (lookup p γ)
    Zv = fst (lookup z γ)
```

层级公式的可靠性定理说：若公式成立且序数槽是序数，则层槽等于序数槽处的层。证明分别读取逼近与最后一步。

```agda
  hier-sound : ⟨ γ ⊨ hierAt a p f z N ⟩ → IsOrd Pv → Av ≡ Lset Pv
  hier-sound (ha , hs) op = StepRead.step-out a p f z N γ tg hs (ve .fst) (ve .snd)
    where
    ve = ApproxRead.approx-out f p z N γ tg ha op
```

层级公式的完备性定理取索引槽的序数性、层槽与层的等同、索引处的真实层级表与供给函数，构造满足。

```agda
  hier-complete : (op : IsOrd Pv) → Av ≡ Lset Pv → IsHier Pv (lookup f γ)
                → ((c : V ℓ) (oc : IsOrd c) → ⟨ c ∈ Pv ⟩ → Supply Zv c oc)
                → ⟨ γ ⊨ hierAt a p f z N ⟩
  hier-complete op aq sp sup =
      ApproxRead.approx-in f p z N γ tg op sp sup
```

证明把层级规格的向内逼近与最后一步复合，后者的正确性与完备性子句在每个更小实参处由层级规格向外读取。

```agda
    , StepRead.step-in a p f z N γ tg op aq
        (λ c w c∈ rec → hier-out Pv op (lookup f γ) sp c w rec .snd)
        (hier-in Pv op (lookup f γ) sp) sup
```

## 读取逼近与完整层级

内部模块封存最终将在对象语言内表达可构造层级的公式。

```agda
module Inner where
```

十四槽环境以前十个数码标签开头。反复使用 `weakenFin` 会把各索引嵌入 `Fin 14` 而不改变其数值位置，因此 `N14` 占据零至九号槽。这与后文使用的具体环境一致，其中前十项正是冯·诺伊曼数码。

```agda
  N14 : Fin 10 → Fin 14
  N14 k = weakenFin (weakenFin (weakenFin (weakenFin k)))
```

末尾四个槽位补全内部公式的数学数据：十号槽存放表 `ff`，十一号槽存放拟议层 `aa`，十二号槽存放其层索引 `pp`，十三号槽存放公共界 `zz`。因此，完整环境的顺序是十个标签，随后依次为 `f`、`a`、`p` 与 `z`。

```agda
  ff aa pp zz : Fin 14
  ff = sh 10 (i0 {3})
  aa = sh 11 (i0 {2})
  pp = sh 12 (i0 {1})
  zz = sh 13 (i0 {0})
```

内部公式合取两项数学要求。`pins N14` 把前十个槽位固定为编码描述所需的数码标签；`hierAt aa pp ff zz N14` 则说 `ff` 逼近 `pp` 以下的层级，而 `aa` 是它在 `pp` 处的下一取值，所有辅助数据均由 `zz` 界定。不透明性把这条大型公式保留在已经证明的读引理之后。

```agda
  opaque
    inner : Formula S 14
    inner = pins N14 ∧̇ hierAt aa pp ff zz N14
```

为证明有界性，检查器可以在此局部展开 `inner`，连同封存的描述 `satAt` 与 `defAt`。这一受限展开表明，大型合取只由原子式、联结词与有界量词构成。在这道证明边界之外，公式的数学内容通过读引理恢复，而不靠归约展开后的公式。

```agda
  opaque
    unfolding inner satAt defAt
```

经过局部展开，`checkΔ₀ inner tt` 给出结构性的 `Δ₀` 见证：`inner` 中出现的每个量词都有界。这是对这条特定公式的句法核验，并不声称 `checkΔ₀` 在两个方向上判定有界性。外围模块及其导出结果仍以 `lem : LEM (ℓ-suc ℓ)` 为参数。

```agda
    Δ₀-inner : Δ₀ inner
    Δ₀-inner = checkΔ₀ inner tt
```

封存公式的读法经由同一边界暴露。

```agda
  opaque
    unfolding inner
```

合取的向外读法是其两个合取项组成的对，因为合取就是一对命题。

```agda
    inner-out : (γ : S ^ 14) → ⟨ γ ⊨ inner ⟩ → ⟨ γ ⊨ pins N14 ⟩ × ⟨ γ ⊨ hierAt aa pp ff zz N14 ⟩
    inner-out γ h = h
```

反过来，pin 子句与层级子句的证明正好构成满足其合取所需的两个分量。它与 `inner-out` 合在一起，给出后文所需的两个精确方向：既可从大型公式推出两个数学部分，也可在两部分均已证明时重新构造该公式。

```agda
    inner-in : (γ : S ^ 14) → ⟨ γ ⊨ pins N14 ⟩ → ⟨ γ ⊨ hierAt aa pp ff zz N14 ⟩ → ⟨ γ ⊨ inner ⟩
    inner-in γ h1 h2 = h1 , h2
```

对具有 `suc n` 个位置的外层环境，`lastFin` 表示其最后一个位置。在下文每次应用中，该位置都存放为新存在量词提供界的公共界集。有界量词引入的见证占据公式体中新添的最前位置，并不是 `lastFin` 所指的位置。

```agda
  lastFin : {n : ℕ} → Fin (suc n)
  lastFin {zero} = zero
  lastFin {suc n} = suc (lastFin {n})
```

操作 `wrap` 以存在量词约束公式体最前的见证位置，并要求该见证属于外层最后位置所命名的集合。因此，公式的元数减少一，而有界性保持。反复施用这一操作，会把十个数码标签与表逐个量化，并要求它们都属于公共界 `z`。

```agda
  wrap : {n : ℕ} → Formula S (suc (suc n)) → Formula S (suc n)
  wrap {n} φ = ∃̇∈ (var (lastFin {n})) φ
```

Δ₀ 见证在包裹下保持，因为有界存在量化本身就是有界构造。

```agda
  δ-wrap : {n : ℕ} {φ : Formula S (suc (suc n))} → Δ₀ φ → Δ₀ (wrap {n} φ)
  δ-wrap d = δ-∃∈ d
```

五步包裹消耗十个数码槽中的五个，把自由位置从十四逐次减到九。

```agda
  s13 = wrap {12} inner
  s12 = wrap {11} s13
  s11 = wrap {10} s12
  s10 = wrap {9}  s11
  s9  = wrap {8}  s10
```

再五步包裹把自由位置从九减到四，只余层、序数索引、表与见证界。

```agda
  s8  = wrap {7}  s9
  s7  = wrap {6}  s8
  s6  = wrap {5}  s7
  s5  = wrap {4}  s6
  s4  = wrap {3}  s5
```

第十一次包裹再次以 `z` 为界，用存在量词约束最后的辅助槽，即层级表 `f`。此时恰余三个自由位置，顺序为 `(a,p,z)`：拟议层、它的层索引与公共见证界。因此，`three` 是三元公式而不是句子；后续擦除步骤会移除其未使用的常元域，但不会移除这三个自由变元。

```agda
  three : Formula S 3
  three = wrap {2} s4
```

见证公式被包裹十一次，对应公共界内部引入的十一个有界存在量词。每次包裹增加一层 Δ₀ 见证，因此包裹后的公式始终有界。

```agda
  Δ₀-three : Δ₀ three
  Δ₀-three =
    δ-wrap (δ-wrap (δ-wrap (δ-wrap (δ-wrap (δ-wrap (δ-wrap
      (δ-wrap (δ-wrap (δ-wrap (δ-wrap Δ₀-inner))))))))))
```

为了验证包裹后的公式不含常元，这项计算可以查看已密封的 `inner`、`satAt` 与 `defAt` 的定义。这样的局部展开只暴露化简出现次数所需的语法；在外围论证中，这些大型公式本身仍由各自的读引理与写引理来使用。

```agda
  opaque
    unfolding inner satAt defAt
```

`three` 的常元出现次数为零。它留下的三个位置是供 `a`、`p` 与 `z` 使用的自由变元，并非常元。为这项计算展开密封成分后，该等式按定义化简，因为公式中的每个词项都由变元构成。

```agda
    count-three : countFo three ≡ 0
    count-three = refl
```

由于 `three` 不含常元，擦除把它的常元域从可构造载体改为空类型，同时保持其变元与量词结构。所得 `erased` 因而是无参公式，但元数仍为三；把它嵌回原常元域便恢复 `three`。

```agda
  erased : Formula (⊥* {ℓ-suc ℓ}) 3
  erased = Cnt.erase three count-three
```

擦除也保持 Δ₀ 见证。它只改变已经不出现的常元符号，所以 `three` 中的每个有界量词仍然有界；同一项结构论证由此证明 `erased` 是 Δ₀ 公式。

```agda
  Δ₀-erased : Δ₀ erased
  Δ₀-erased = erase-Δ₀ three count-three Δ₀-three
```

在语义上，一层包裹是一份受命题截断的有界见证。若界中的每个成员 `x` 只要满足主体就能推出 `P`，则 `unwrap` 可把这项受截断的存在消去到 `P` 中。声明 `P : hProp` 恰好提供这种消去所要求的命题条件。

```agda
  unwrap : {n : ℕ} (φ : Formula S (suc (suc n))) (γ : S ^ (suc n)) {P : hProp (ℓ-suc ℓ)}
         → ((x : S) → ⟨ fst x ∈ fst (lookup (lastFin {n}) γ) ⟩ → ⟨ (x ∷ γ) ⊨ φ ⟩ → ⟨ P ⟩)
         → ⟨ γ ⊨ wrap {n} φ ⟩ → ⟨ P ⟩
  unwrap φ γ {P} k h = PT.rec (snd P) (λ { (x , xz , hx) → k x xz hx }) h
```

`wrap-in` 由一个被点名的成员及其扩展处的主体满足构造有界存在，即有界存在量词的引入规则。

```agda
  wrap-in : {n : ℕ} (φ : Formula S (suc (suc n))) (γ : S ^ (suc n)) (x : S)
          → ⟨ fst x ∈ fst (lookup (lastFin {n}) γ) ⟩ → ⟨ (x ∷ γ) ⊨ φ ⟩ → ⟨ γ ⊨ wrap {n} φ ⟩
  wrap-in φ γ x m h = ∣ x , (m , h) ∣₁
```

## 描述可构造层的无参公式

可见公式 `levelFo` 有三个自由位置 `(a,p,z)`。它把「`p` 是序数」与「由 `z` 限界的已擦除层级描述」合取起来。因此，尽管可靠性的结论只提及 `a` 与 `p`，`z` 仍是一个自由输入。

```agda
levelFo : Formula (⊥* {ℓ-suc ℓ}) 3
levelFo = isOrd-at-p ∧̇ Inner.erased
```

`levelFo` 的两个合取项都是 Δ₀ 公式，而 Δ₀ 类对合取封闭。因此，合取构造子把两份 Δ₀ 见证合成 `Δ₀-levelFo`，并未引入无界量词。

```agda
Δ₀-levelFo : Δ₀ levelFo
Δ₀-levelFo = δ-∧ Δ₀-isOrd-at-p Inner.Δ₀-erased
```

读取引理对任何无常元 Δ₀ 公式复合三条路径：从限制载体到外围层级的 Δ₀ 绝对性、空常元域嵌入下满足的不变性、以及空解释的唯一性。结果是两个满足命题的等式。

```agda
read : {n : ℕ} {φ : Formula (⊥* {ℓ-suc ℓ}) n} → Δ₀ φ → (δ : S ^ n)
     → (δ ⊨ embed φ) ≡ (map fst δ ⊨ₚ φ)
read {n} {φ} dφ δ =
    AbsL.abs₀ (mapΔ₀ Empty.rec* dφ) δ
  ∙ embed-⊨ 𝒮ᵥ {K = S} fst φ (map fst δ)
```

这条路径的最后一项等式处理常元解释。由于常元域为空，任何这类解释都逐点等于空类型消去给出的解释。函数外延性把它认同于典范的空解释，于是前一步的嵌入比较最终到达同一无参公式的外围读法。

```agda
  ∙ cong (λ ι → SemVᵃ.At._⊨_ (⊥* {ℓ-suc ℓ}) ι (map fst δ) φ)
         (funExt (λ b → Empty.rec* b))
```

向外序数读取把序数性原子的两个子句展开为：`p` 的底层集合的传递性，以及其每个成员的传递性；所有条目都经 `p` 的呈现降下。

```agda
ord-out : (a p z : S) → ⟨ (a ∷ p ∷ z ∷ []) ⊨ embed isOrd-at-p ⟩ → IsOrd (fst p)
ord-out a p z h =
    ( λ {x} {y} y∈x x∈p → h .fst (down p x x∈p) x∈p (down (down p x x∈p) y y∈x) y∈x )
  , ( λ x x∈p {y} {u} u∈y y∈x →
        h .snd (down p x x∈p) x∈p (down (down p x x∈p) y y∈x) y∈x
```

对序数性的第二个子句，取 `x ∈ p`、`y ∈ x` 与 `u ∈ y`。把这三层隶属都降入可构造载体后，公式的第二个合取项推出 `u ∈ x`。这恰是 `p` 的每个成员 `x` 的传递性；连同第一个子句便得到 `IsOrd p`。

```agda
          (down (down (down p x x∈p) y y∈x) u u∈y) u∈y )
```

向内序数读取由序数性证明构造两个子句，所有条目都打包为 `L` 的元素。

```agda
ord-in : (a p z : S) → IsOrd (fst p) → ⟨ (a ∷ p ∷ z ∷ []) ⊨ embed isOrd-at-p ⟩
ord-in a p z op =
    (λ x x∈p y y∈x → op .fst {x = fst x} {y = fst y} y∈x x∈p)
  , (λ x x∈p y y∈x u u∈y → op .snd (fst x) x∈p {x = fst y} {y = fst u} u∈y y∈x)
```

可靠性论证现在转入隐藏公式的十四槽位读法。它要丢弃受限界的辅助见证，同时保留这些见证的数学后果：槽位 `a` 中的值就是由槽位 `p` 索引的可构造层。

```agda
private
  module Sound where
    open Inner
```

`finish` 引理分开读取 `inner` 的两个合取项。pins 读引理把第一项化为层级读引理所需的十条数码等式。对于第二项中的逼近，`hier-sound` 只恢复 `Values × Entries`；再给出 `p` 的序数性后，这已足以把最后一步读成 `a = Lset p`。这里并未断言隐藏表不含畸形成员，也未断言其中没有基点落在 `p` 之外的条目。

```agda
    finish : (γ : S ^ 14) → ⟨ γ ⊨ inner ⟩ → IsOrd (fst (lookup pp γ))
           → fst (lookup aa γ) ≡ Lset (fst (lookup pp γ))
    finish γ h op = HierRead.hier-sound aa pp ff zz N14 γ tg (inner-out γ h .snd) op
      where
      tg : Tags γ N14
```

被固定的数码由 pins 读式向外读取，从对象语言子句推导出十条数码等式。

```agda
      tg = PinsRead.pins-out N14 γ (inner-out γ h .fst)
```

内部可靠性引理从可构造载体的三个元素 `a`、`p` 与 `z` 出发，并假设 `embed levelFo` 在其上成立。它先用擦除逆等式恢复十一重包裹公式的满足。所求结论把 `a` 的底层集合与 `p` 的底层索引处的 `Lset` 相比较。

```agda
    sound-L : (a p z : S) → ⟨ (a ∷ p ∷ z ∷ []) ⊨ embed levelFo ⟩ → fst a ≡ Lset (fst p)
    sound-L a p z (ho , hφ) =
      go (subst (λ ψ → ⟨ (a ∷ p ∷ z ∷ []) ⊨ ψ ⟩) (Cnt.erase-inv three count-three) hφ)
      where
      ordp : IsOrd (fst p)
```

序数性合取项经向外序数读取产生 `p` 的序数性证明，这是层级读式所需的剩余输入。

```agda
      ordp = ord-out a p z ho
```

需要保留的等式被组成命题 `G`。累积层级中的集合构成 h-集合，因此 `setIsSet` 证明该等式类型是 `hProp`。由此，每份受命题截断的有界见证都可被消去到 `G` 中，而不会暴露一个选定见证。

```agda
      G : hProp (ℓ-suc ℓ)
      G = (fst a ≡ Lset (fst p)) , setIsSet (fst a) (Lset (fst p))
```

可靠性逐一消去十一个有界存在，把截断的见证消耗为命题等式。消去的顺序镜像公式的绑定顺序。

```agda
      go : ⟨ (a ∷ p ∷ z ∷ []) ⊨ three ⟩ → ⟨ G ⟩
      go =
        unwrap s4 (a ∷ p ∷ z ∷ []) {G} λ F mF →
        unwrap s5 (F ∷ a ∷ p ∷ z ∷ []) {G} λ x9 m9 →
        unwrap s6 (x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x8 m8 →
```

接下来的五次消去恢复数码见证 `x7` 至 `x3`。每一步都在环境前端加入一个元素，而最后一个槽位始终是 `z`，也就是十一份见证共同来自的界。

```agda
        unwrap s7 (x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x7 m7 →
        unwrap s8 (x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x6 m6 →
        unwrap s9 (x6 ∷ x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x5 m5 →
        unwrap s10 (x5 ∷ x6 ∷ x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x4 m4 →
        unwrap s11 (x4 ∷ x5 ∷ x6 ∷ x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x3 m3 →
```

最内层见证完成消去：十四槽位环境连同序数性证明一起交给 finish 引理，产出两个底层集合的等式。

```agda
        unwrap s12 (x3 ∷ x4 ∷ x5 ∷ x6 ∷ x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x2 m2 →
        unwrap s13 (x2 ∷ x3 ∷ x4 ∷ x5 ∷ x6 ∷ x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x1 m1 →
        unwrap inner (x1 ∷ x2 ∷ x3 ∷ x4 ∷ x5 ∷ x6 ∷ x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G}
          λ x0 m0 hm →
            finish (x0 ∷ x1 ∷ x2 ∷ x3 ∷ x4 ∷ x5 ∷ x6 ∷ x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) hm ordp
```

对于已知可构造的周遭集合 `a`、`p` 与 `z`，各自的可构造性证明把它们呈现为可构造载体的元素。反向读取 Δ₀ 绝对性，便把 `levelFo` 的周遭满足搬到这些呈现上的满足，从而可应用内部可靠性论证。投影回去后得到 `a = Lset p`。因此，三个输入全都可构造是显式假设，并非公式自身的结论。

```agda
level-sound : (a p z : V ℓ) → ⟨ isL a ⟩ → ⟨ isL p ⟩ → ⟨ isL z ⟩
            → ⟨ (a ∷ p ∷ z ∷ []) ⊨ₚ levelFo ⟩ → a ≡ Lset p
level-sound a p z la lp lz h =
  Sound.sound-L (a , la) (p , lp) (z , lz)
    (subst ⟨_⟩ (sym (read Δ₀-levelFo ((a , la) ∷ (p , lp) ∷ (z , lz) ∷ []))) h)
```

为证明完备性，固定带有充分性数据的 `lam` 以及序数 `p ∈ lam`。序数性字段使 `lam` 成为层索引，其对应的层是 `Lset lam`；其余字段给出后继封闭、包含 `ω`，以及 `lam` 以下各处所需的编码见证。证明将用这些性质说明，特定的界 `Lset lam` 包含描述层 `Lset p` 所需的每份见证。

```agda
private
  module Complete (lam : V ℓ) (ad : Adequate lam) (p : V ℓ) (op : IsOrd p) (p∈λ : ⟨ p ∈ lam ⟩) where
    open Inner
    open Adequate lam ad using ( ord; succ; ω∈; wit )
```

充分层 `lam` 的传递性由其序数性提取：两个嵌套的隶属复合为一个。

```agda
    private
      tr : (x y : V ℓ) → ⟨ x ∈ lam ⟩ → ⟨ y ∈ x ⟩ → ⟨ y ∈ lam ⟩
      tr x y x∈ y∈ = ord .fst {x = x} {y = y} y∈ x∈
```

空集属于充分层，依据是对链 `∅ ∈ ω ∈ lam` 施用的传递性。

```agda
      ∅∈λ : ⟨ ∅ ∈ lam ⟩
      ∅∈λ = tr ω ∅ ω∈ (#∈ω zero)
```

数码限界论证在 `lam` 处特化到可构造层级。由序数性、后继封闭与 `∅ ∈ lam` 可得，每个模型数码的底层集合都属于 `Lset lam`。这给出稍后十个标签数码共同需要的界。

```agda
      module B = Bound lam ord succ ∅∈λ using ( num∈λ )
```

令 `K = Lset lam`。这是第三个自由输入 `zS` 所呈现的公共界集；层级表、十个数码，以及论证每一行所用的全部辅助集合，都必须证明属于 `K`。

```agda
      K : V ℓ
      K = Lset lam
```

若 `c ∈ lam`，后继封闭给出 `sucV c ∈ lam`。标准的后继层事实把 `Lset c` 放入 `Lset (sucV c)`，再沿 `sucV c ∈ lam` 使用单调性，便把这条隶属提升为 `Lset c ∈ K`。稍后把同一引理应用于 `sucV c`，并再用一次后继封闭，即可得到 `Lset (sucV c) ∈ K`；这才是在 `c` 行所需的可定义幂集见证。

```agda
      Lset∈K : (c : V ℓ) → ⟨ c ∈ lam ⟩ → ⟨ Lset c ∈ K ⟩
      Lset∈K c c∈ = Lset-mono {α = lam} {β = sucV c} (succ c c∈) (Lset∈suc c)
```

数码限界定理先把模型数码的底层集合放入 `K`。投影等式 `numeralL-fst` 把该集合认同于周遭的 von Neumann 数码 `# k`，沿此搬运便得 `# k ∈ K`。因此，十个数码见证与层级表满足同一个界。

```agda
      num∈K : (k : ℕ) → ⟨ # k ∈ K ⟩
      num∈K k = subst (λ u → ⟨ u ∈ K ⟩) (numeralL-fst k) (B.num∈λ k)
```

四个集合被命名：层 `Lset p`、序数 `p`、层 `Lset lam`、以及 `p` 处的层级表，各处于相应的载体中。

```agda
    aS pS zS F : S
    aS = LsetS p op
    pS = p , At.cL p op
    zS = LsetS lam ord
    F = At.hier p op
```

环境 `E` 现在记录完整的十四槽位赋值。从前到后依次是数码 `0` 至 `9`、`p` 处的真实层级表、预定值 `Lset p`、索引 `p`，以及公共界 `Lset lam`。这恰是 `inner` 读取数据的槽位次序。

```agda
    E : S ^ 14
    E = nn 0 ∷ nn 1 ∷ nn 2 ∷ nn 3 ∷ nn 4 ∷ nn 5 ∷ nn 6 ∷ nn 7 ∷ nn 8 ∷ nn 9
      ∷ F ∷ aS ∷ pS ∷ zS ∷ []
```

标签假设定义性地把前四个标签槽位各自等同于自己的数码。

```agda
    tg : Tags E N14
    tg zero = refl
    tg (suc zero) = refl
    tg (suc (suc zero)) = refl
    tg (suc (suc (suc zero))) = refl
```

接下来的五个情形验证索引四至八处的标签槽位。每次查找都化简为 `E` 中相应的条目，因此这些槽位按定义分别是数码 `4` 至 `8`。

```agda
    tg (suc (suc (suc (suc zero)))) = refl
    tg (suc (suc (suc (suc (suc zero))))) = refl
    tg (suc (suc (suc (suc (suc (suc zero)))))) = refl
    tg (suc (suc (suc (suc (suc (suc (suc zero))))))) = refl
    tg (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) = refl
```

最后一个情形验证第十个标签槽位，也就是索引九处的槽位，为数码 `9`。由此，`Tags E N14` 要求的十条等式全都由显式环境上的计算得到。

```agda
    tg (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))) = refl
```

对序数 `p` 的每个成员 `c`，供给引理把四个对象放入 `K`：满足图、码集、环境塔与下一层 `Lset (sucV c)`。链 `c ∈ p ∈ lam` 与 `lam` 的传递性先把 `c` 放入 `lam`，从而使充分性见证可用。

```agda
    sup : (c : V ℓ) (oc : IsOrd c) → ⟨ c ∈ p ⟩ → Supply K c oc
    sup c oc c∈ = w .snd .snd .fst , ( w .snd .fst , ( w .snd .snd .snd , Lset∈K (sucV c) (succ c c∈λ) ))
      where
      c∈λ : ⟨ c ∈ lam ⟩
      c∈λ = tr p c p∈λ c∈
```

每个 `c` 的见证从充分性数据读取，为该序数的每个成员完成供给。

```agda
      w = wit c c∈λ oc
```

内层公式现在在 `E` 处成立。pins 写引理给出其中的数码合取项。对于层级合取项，`hier-complete` 使用 `p` 的序数性、候选值与 `Lset p` 的自反等同、`hierL-spec` 给出的精确层级表，以及上文从充分性逐行导出的供给。这里没有使用任何加强的层假设。

```agda
    hm : ⟨ E ⊨ inner ⟩
    hm = inner-in E (PinsRead.pins-in N14 E tg)
           (HierRead.hier-complete aa pp ff zz N14 E tg op refl (hierL-spec p (At.cL p op) op) sup)
```

`p` 处的充分性见证把真实层级表 `F` 的底层集合放入公共界集 `K`。这给出把 `F` 引入为最外层有界见证所需的隶属证明。

```agda
    FK : ⟨ fst F ∈ K ⟩
    FK = wit p p∈λ op .fst
```

还需把层级表与数码数据隐藏在十一个有界存在量词之后。最外层的引入使用真实层级表 `F`，其属于 `K` 已在上一步证明。接下来的两次引入使用数码 `9` 与 `8`，并各自附上属于同一公共界的证明。

```agda
    h3 : ⟨ (aS ∷ pS ∷ zS ∷ []) ⊨ three ⟩
    h3 =
      wrap-in s4 (aS ∷ pS ∷ zS ∷ []) F FK (
      wrap-in s5 (F ∷ aS ∷ pS ∷ zS ∷ []) (nn 9) (num∈K 9) (
      wrap-in s6 (nn 9 ∷ F ∷ aS ∷ pS ∷ zS ∷ []) (nn 8) (num∈K 8) (
```

同一条引入规则继续插入数码 `7` 至 `3`。它们的隶属证明全都来自 `num∈K`，所以每个量词的见证都位于 `K = Lset lam` 内；这里没有从无界的周遭搜索中取得见证。

```agda
      wrap-in s7 (nn 8 ∷ nn 9 ∷ F ∷ aS ∷ pS ∷ zS ∷ []) (nn 7) (num∈K 7) (
      wrap-in s8 (nn 7 ∷ nn 8 ∷ nn 9 ∷ F ∷ aS ∷ pS ∷ zS ∷ []) (nn 6) (num∈K 6) (
      wrap-in s9 (nn 6 ∷ nn 7 ∷ nn 8 ∷ nn 9 ∷ F ∷ aS ∷ pS ∷ zS ∷ []) (nn 5) (num∈K 5) (
      wrap-in s10 (nn 5 ∷ nn 6 ∷ nn 7 ∷ nn 8 ∷ nn 9 ∷ F ∷ aS ∷ pS ∷ zS ∷ []) (nn 4) (num∈K 4) (
      wrap-in s11 (nn 4 ∷ nn 5 ∷ nn 6 ∷ nn 7 ∷ nn 8 ∷ nn 9 ∷ F ∷ aS ∷ pS ∷ zS ∷ []) (nn 3) (num∈K 3) (
```

最后插入数码 `2`、`1` 与 `0`。末次引入后的扩展环境恰好是 `E`，而 `hm` 已证明 `inner` 在该环境中成立。因此，这串嵌套引入证明十一重包裹公式在可见三元组 `(Lset p,p,Lset lam)` 处得到满足。

```agda
      wrap-in s12 (nn 3 ∷ nn 4 ∷ nn 5 ∷ nn 6 ∷ nn 7 ∷ nn 8 ∷ nn 9 ∷ F ∷ aS ∷ pS ∷ zS ∷ []) (nn 2) (num∈K 2) (
      wrap-in s13 (nn 2 ∷ nn 3 ∷ nn 4 ∷ nn 5 ∷ nn 6 ∷ nn 7 ∷ nn 8 ∷ nn 9 ∷ F ∷ aS ∷ pS ∷ zS ∷ []) (nn 1) (num∈K 1) (
      wrap-in inner (nn 1 ∷ nn 2 ∷ nn 3 ∷ nn 4 ∷ nn 5 ∷ nn 6 ∷ nn 7 ∷ nn 8 ∷ nn 9 ∷ F ∷ aS ∷ pS ∷ zS ∷ []) (nn 0) (num∈K 0)
        hm))))))))))
```

擦除逆等式说明，把 `erased` 嵌入可构造常元域便恢复 `three`。因此，沿该等式的反向搬运 `h3`，可得 `embed erased` 在同一三槽位环境中的满足。改变的只有常元域；十一个有界见证及其公共界仍是刚才构造的那些。

```agda
    hφ : ⟨ (aS ∷ pS ∷ zS ∷ []) ⊨ embed erased ⟩
    hφ = subst (λ ψ → ⟨ (aS ∷ pS ∷ zS ∷ []) ⊨ ψ ⟩) (sym (Cnt.erase-inv three count-three)) h3
```

完备性由两个合取项组装：序数性原子由 `ord-in` 成立，擦除后的见证公式由刚才的传输成立。读取引理把二者传入外围满足。

```agda
    complete : ⟨ (Lset p ∷ p ∷ Lset lam ∷ []) ⊨ₚ levelFo ⟩
    complete = subst ⟨_⟩ (read Δ₀-levelFo (aS ∷ pS ∷ zS ∷ [])) (ord-in aS pS zS op , hφ)
```

完备性定理给出这里能够证明的精确存在方向。若 `γ` 充分并含有序数 `p`，则三元组 `(Lset p,p,Lset γ)` 满足 `levelFo`。后续的 `CondensationTransfer` 在这个 Δ₀ 核心之外加入无界存在量词，经初等性搬运三个坐标，再用可靠性把搬运后的第一坐标识别为相应的可构造层。该定理并未断言任意第三坐标都可使用，也未断言第三坐标由公式唯一确定。

```agda
level-complete : (γ : V ℓ) → Adequate γ → (p : V ℓ) → IsOrd p → ⟨ p ∈ γ ⟩
               → ⟨ (Lset p ∷ p ∷ Lset γ ∷ []) ⊨ₚ levelFo ⟩
level-complete γ ad p op p∈ = Complete.complete γ ad p op p∈
```