|
26 | 26 | -- value. (ε₀ is itself the collapse ψ₀(Ω₁) — the first nontrivial data |
27 | 27 | -- point the eventual `denotation` ⟦·⟧ must reproduce.) |
28 | 28 | -- |
29 | | --- This module does NOT prove ε₀ is an ε-number (`ω^^ ε₀ ≡ ε₀`); that |
30 | | --- fixpoint property and the inflationary `α <′ ω^^ α` are follow-on |
31 | | --- rungs. |
| 29 | +-- RUNG 2 (2026-06-18): ε₀ IS an ε-number — `ω^^ ε₀ ≃ ε₀` as `_≤′_` in |
| 30 | +-- BOTH directions (`ω^^-ε₀-≤`, `ε₀-≤-ω^^-ε₀`, packaged `ε₀-ε-number`). |
| 31 | +-- bi-`≤′`, not `≡`, because two `olim`s of different ℕ-indexings of the |
| 32 | +-- same supremum are not definitionally equal. No general inflationary |
| 33 | +-- lemma is needed: `ω^^ ε₀` is definitionally the `olim` of the shifted |
| 34 | +-- tower `n ↦ ε-tower (suc n)`, so each direction reduces to one-step |
| 35 | +-- `f-in-lim′` (+ `ω^^-pos` for the base index). |
| 36 | +-- |
| 37 | +-- The *strict* inflationary `α <′ ω^^ α` is deliberately NOT pursued: it |
| 38 | +-- is FALSE exactly at the ε-numbers (ε₀ = ω^^ ε₀ is the counterexample). |
| 39 | +-- |
| 40 | +-- RUNG 3 (2026-06-18): the NON-strict inflationary `ω^^-infl : α ≤′ ω^^ α` |
| 41 | +-- IS proved below — the engine for enumerating ε-numbers (φ₁) and the |
| 42 | +-- higher Veblen φ hierarchy toward Γ₀. (`α ≤′ ω^^ α` holds everywhere, |
| 43 | +-- with equality exactly at the ε-numbers.) |
32 | 44 |
|
33 | 45 | module Ordinal.Brouwer.OrdinalExp where |
34 | 46 |
|
35 | 47 | open import Data.Nat.Base using (ℕ; zero; suc) |
36 | | -open import Data.Product.Base using (Σ; _,_) |
| 48 | +open import Data.Product.Base using (Σ; _,_; _×_) |
37 | 49 | open import Data.Unit.Base using (tt) |
38 | 50 | open import Relation.Binary.PropositionalEquality using (_≡_; refl) |
39 | 51 |
|
40 | 52 | open import Ordinal.Brouwer using (Ord; oz; osuc; olim) |
41 | | -open import Ordinal.Brouwer.Phase13 using (_≤′_; _<′_; f-in-lim′) |
42 | | -open import Ordinal.Brouwer.OmegaPow using (_·ℕ_; oz<′oz⊕) |
| 53 | +open import Ordinal.Brouwer.Arithmetic using (_⊕_) |
| 54 | +open import Ordinal.Brouwer.Phase13 using (_≤′_; _<′_; f-in-lim′; ≤′-trans; osuc-mono-≤′; ⊕-mono-≤-right) |
| 55 | +open import Ordinal.Brouwer.OmegaPow using (_·ℕ_; oz<′oz⊕; X≤′oz⊕X) |
43 | 56 |
|
44 | 57 | ---------------------------------------------------------------------- |
45 | 58 | -- Ordinal exponentiation base ω |
@@ -83,3 +96,58 @@ open import Ordinal.Brouwer.OmegaPow using (_·ℕ_; oz<′oz⊕) |
83 | 96 |
|
84 | 97 | ε-tower-below-ε₀ : ∀ n → ε-tower n ≤′ ε₀ |
85 | 98 | ε-tower-below-ε₀ n = f-in-lim′ ε-tower n |
| 99 | + |
| 100 | +---------------------------------------------------------------------- |
| 101 | +-- ε₀ is an ε-number: a fixed point of ω-exponentiation (RUNG 2) |
| 102 | +---------------------------------------------------------------------- |
| 103 | + |
| 104 | +-- `ω^^ ε₀ ≃ ε₀`, as `_≤′_` in both directions. `ω^^ ε₀ = ω^^ (olim |
| 105 | +-- ε-tower)` reduces to `olim (n ↦ ω^^ (ε-tower n))`, and each |
| 106 | +-- `ω^^ (ε-tower n)` is definitionally `ε-tower (suc n)` — i.e. `ω^^ ε₀` |
| 107 | +-- is the supremum of the tower SHIFTED by one. A shifted supremum has |
| 108 | +-- the same value, so both inequalities are one-step `f-in-lim′`s. |
| 109 | + |
| 110 | +-- Upper: every element of the shifted tower is below ε₀. |
| 111 | +ω^^-ε₀-≤ : ω^^ ε₀ ≤′ ε₀ |
| 112 | +ω^^-ε₀-≤ n = f-in-lim′ ε-tower (suc n) |
| 113 | + |
| 114 | +-- Lower: every tower element is below the shifted tower's supremum. |
| 115 | +-- The base index ε-tower 0 = 1 sits below ε-tower 1 = ω^^ 1 by `ω^^-pos`; |
| 116 | +-- every successor element ε-tower (suc m) = ω^^ (ε-tower m) IS the m-th |
| 117 | +-- element of the shifted tower, so it is below by `f-in-lim′`. |
| 118 | +ε₀-≤-ω^^-ε₀ : ε₀ ≤′ ω^^ ε₀ |
| 119 | +ε₀-≤-ω^^-ε₀ zero = 0 , ω^^-pos (osuc oz) |
| 120 | +ε₀-≤-ω^^-ε₀ (suc m) = f-in-lim′ (λ k → ω^^ (ε-tower k)) m |
| 121 | + |
| 122 | +-- ε₀ is a fixed point of ω-exponentiation (the defining property of an |
| 123 | +-- ε-number), packaged as bi-`≤′`. |
| 124 | +ε₀-ε-number : (ω^^ ε₀ ≤′ ε₀) × (ε₀ ≤′ ω^^ ε₀) |
| 125 | +ε₀-ε-number = ω^^-ε₀-≤ , ε₀-≤-ω^^-ε₀ |
| 126 | + |
| 127 | +---------------------------------------------------------------------- |
| 128 | +-- ω-exponentiation is inflationary (RUNG 3 prerequisite) |
| 129 | +---------------------------------------------------------------------- |
| 130 | + |
| 131 | +-- `α ≤′ ω^^ α` for every α — the non-strict inflationary law. This is |
| 132 | +-- the engine the Veblen φ-hierarchy needs: "the next ε-number strictly |
| 133 | +-- above β" is a genuine fixed point only because `osuc β ≤′ ω^^ (osuc β)`. |
| 134 | +-- (The strict `α <′ ω^^ α` is FALSE at ε-numbers — ε₀ = ω^^ ε₀.) |
| 135 | +-- |
| 136 | +-- * oz : `oz ≤′ _` is `⊤`. |
| 137 | +-- * osuc β : witness index 2, since `(ω^^ β) ·ℕ 2 ≡ (oz ⊕ ω^^ β) ⊕ ω^^ β`; |
| 138 | +-- chain `osuc β ≤′ osuc (ω^^ β) ≤′ osuc (oz ⊕ ω^^ β) ≤′ (oz ⊕ ω^^ β) ⊕ ω^^ β` |
| 139 | +-- via `osuc-mono-≤′` (IH, then `X≤′oz⊕X`) and right-monotonicity of `_⊕_` |
| 140 | +-- (`⊕-mono-≤-right`, using `osuc oz ≤′ ω^^ β` = `ω^^-pos β` and the |
| 141 | +-- definitional `Y ⊕ osuc oz ≡ osuc Y`). |
| 142 | +-- * olim f : per branch, IH `f n ≤′ ω^^ (f n)` then `f-in-lim′`. |
| 143 | +ω^^-infl : ∀ α → α ≤′ ω^^ α |
| 144 | +ω^^-infl oz = tt |
| 145 | +ω^^-infl (osuc β) = |
| 146 | + 2 , ≤′-trans {osuc β} {osuc (ω^^ β)} {(oz ⊕ ω^^ β) ⊕ ω^^ β} |
| 147 | + (osuc-mono-≤′ {β} {ω^^ β} (ω^^-infl β)) |
| 148 | + (≤′-trans {osuc (ω^^ β)} {osuc (oz ⊕ ω^^ β)} {(oz ⊕ ω^^ β) ⊕ ω^^ β} |
| 149 | + (osuc-mono-≤′ {ω^^ β} {oz ⊕ ω^^ β} (X≤′oz⊕X {ω^^ β})) |
| 150 | + (⊕-mono-≤-right {oz ⊕ ω^^ β} {osuc oz} {ω^^ β} (ω^^-pos β))) |
| 151 | +ω^^-infl (olim f) = |
| 152 | + λ n → ≤′-trans {f n} {ω^^ (f n)} {olim (λ k → ω^^ (f k))} |
| 153 | + (ω^^-infl (f n)) (f-in-lim′ (λ k → ω^^ (f k)) n) |
0 commit comments