|
| 1 | +{-# OPTIONS --safe --without-K #-} |
| 2 | +-- SPDX-License-Identifier: MPL-2.0 |
| 3 | +-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 4 | + |
| 5 | +-- Veblen φ-hierarchy over Brouwer ordinals — RUNG 3 (slice 3): φ₁ is a |
| 6 | +-- NORMAL FUNCTION, and `next-ε β` is the LEAST ε-number above β. Target- |
| 7 | +-- side climb toward ψ₀(Ω_ω) (BH order-type fidelity, open problem |
| 8 | +-- D-2026-06-14). Builds directly on `VeblenPhi` (φ₁ / next-ε defined and |
| 9 | +-- proved ε-valued) and `OrdinalExp` (ω^^). 2026-06-19. |
| 10 | +-- |
| 11 | +-- ## What this slice adds |
| 12 | +-- |
| 13 | +-- The previous slice (`VeblenPhi`) proved that every value of φ₁ IS an |
| 14 | +-- ε-number (`φ₁-ε-number`) and that `next-ε β` is AN ε-number strictly |
| 15 | +-- above β. This slice upgrades that to the two defining properties of an |
| 16 | +-- ε-number ENUMERATION: |
| 17 | +-- |
| 18 | +-- * `next-ε-least` — `next-ε β` is the LEAST ω^^-closed ordinal strictly |
| 19 | +-- above β. This is what makes `next-ε` the genuine "next ε-number" |
| 20 | +-- operator (not merely *an* ε-number above β). Definitional, because |
| 21 | +-- `olim f ≤′ γ` reduces to `∀ n → f n ≤′ γ` (olim is the least upper |
| 22 | +-- bound), so the proof is induction on the ω^^-tower index using |
| 23 | +-- ω^^-monotonicity + the ω^^-closure hypothesis on γ. |
| 24 | +-- * `φ₁` is a NORMAL FUNCTION: |
| 25 | +-- - `φ₁-mono` — monotone (α ≤′ β → φ₁ α ≤′ φ₁ β) |
| 26 | +-- - `φ₁-strict-mono` — strictly monotone (α <′ β → φ₁ α <′ φ₁ β) |
| 27 | +-- - `φ₁-continuous` — continuous at limits (definitional, `refl`) |
| 28 | +-- A normal function is precisely a strictly-monotone, continuous |
| 29 | +-- ordinal function; φ₁ is now mechanically one. |
| 30 | +-- |
| 31 | +-- The one prerequisite the previous slices left open is `ω^^-mono-≤′` |
| 32 | +-- (monotonicity of ω-exponentiation), proved here by structural recursion |
| 33 | +-- on the `_≤′_` shape; it is a pure ω^^ fact and a natural candidate to |
| 34 | +-- migrate into `OrdinalExp` when the binary Veblen rung needs it. |
| 35 | +-- |
| 36 | +-- ## Honest scope (still rung 3 of a LONG climb — do not overclaim) |
| 37 | +-- |
| 38 | +-- φ₁ being a normal function is the standard precondition for taking its |
| 39 | +-- fixed points (the next Veblen level) and ultimately the binary φ_α and |
| 40 | +-- its diagonal → Γ₀. It does NOT reach Γ₀, and ψ₀(Ω_ω) sits far above |
| 41 | +-- even Γ₀ and additionally needs the ordinal-collapsing layer. Order-type |
| 42 | +-- fidelity (ψ₀(Ω_ω)) REMAINS OPEN (D-2026-06-14); this slice neither |
| 43 | +-- reaches Γ₀ nor plugs `Fidelity.AtHeight`. bi-`≤′` (not `≡`) is used for |
| 44 | +-- the fixed-point facts because Brouwer `olim`s of different ℕ-indexings of |
| 45 | +-- one supremum are not definitionally equal; the monotonicity results are |
| 46 | +-- single-`≤′` / single-`<′` and exact. |
| 47 | + |
| 48 | +module Ordinal.Brouwer.VeblenPhiNormal where |
| 49 | + |
| 50 | +open import Data.Nat.Base using (ℕ; zero; suc) |
| 51 | +open import Data.Product.Base using (Σ; _,_) |
| 52 | +open import Data.Empty using (⊥-elim) |
| 53 | +open import Relation.Binary.PropositionalEquality using (_≡_; refl) |
| 54 | + |
| 55 | +open import Ordinal.Brouwer using (Ord; oz; osuc; olim) |
| 56 | +open import Ordinal.Brouwer.Phase13 |
| 57 | + using (_≤′_; _<′_; ≤′-refl; ≤′-trans; ≤′-lim; ≤′-self-osuc) |
| 58 | +open import Ordinal.Brouwer.OmegaPow using (_·ℕ_; ·ℕ-mono-≤-left) |
| 59 | +open import Ordinal.Brouwer.OrdinalExp using (ω^^_; ε₀; ω^^-pos) |
| 60 | +open import Ordinal.Brouwer.VeblenPhi |
| 61 | + using (tower-from; next-ε; φ₁; ω^^-next-ε-≤; β<next-ε) |
| 62 | + |
| 63 | +---------------------------------------------------------------------- |
| 64 | +-- ω-exponentiation is monotone (the one missing prerequisite). |
| 65 | +-- |
| 66 | +-- `α ≤′ β → ω^^ α ≤′ ω^^ β`, by structural recursion on the `_≤′_` shape |
| 67 | +-- of (α, β) — the same descent pattern as `Phase13.≤′-trans`. Uses only |
| 68 | +-- ω^^-positivity (the `oz` base), `·ℕ`-left-monotonicity (the |
| 69 | +-- successor/successor case, where `ω^^ (osuc α) = olim (n ↦ ω^^ α ·ℕ n)`), |
| 70 | +-- and the olim least-upper-bound `≤′-lim`. |
| 71 | +---------------------------------------------------------------------- |
| 72 | + |
| 73 | +ω^^-mono-≤′ : ∀ {α β} → α ≤′ β → ω^^ α ≤′ ω^^ β |
| 74 | +ω^^-mono-≤′ {oz} {β} _ = ω^^-pos β |
| 75 | +ω^^-mono-≤′ {osuc α} {oz} p = ⊥-elim p |
| 76 | +ω^^-mono-≤′ {osuc α} {osuc β} p = |
| 77 | + λ n → ≤′-lim {(ω^^ α) ·ℕ n} (λ m → (ω^^ β) ·ℕ m) n |
| 78 | + (·ℕ-mono-≤-left {ω^^ α} {ω^^ β} n (ω^^-mono-≤′ {α} {β} p)) |
| 79 | +ω^^-mono-≤′ {osuc α} {olim f} (n , q) = |
| 80 | + ≤′-lim {ω^^ (osuc α)} (λ k → ω^^ (f k)) n (ω^^-mono-≤′ {osuc α} {f n} q) |
| 81 | +ω^^-mono-≤′ {olim g} {β} p = |
| 82 | + λ n → ω^^-mono-≤′ {g n} {β} (p n) |
| 83 | + |
| 84 | +---------------------------------------------------------------------- |
| 85 | +-- `next-ε β` is the LEAST ω^^-closed ordinal strictly above β. |
| 86 | +-- |
| 87 | +-- For any γ with `osuc β ≤′ γ` (β strictly below γ) and `ω^^ γ ≤′ γ` |
| 88 | +-- (γ is closed under ω-exponentiation — the direction of the ε-number |
| 89 | +-- property we need), `next-ε β ≤′ γ`. `next-ε β = olim (tower-from |
| 90 | +-- (osuc β))`, and `olim … ≤′ γ` is definitionally "every tower approximant |
| 91 | +-- is ≤′ γ", proved by induction on the tower index n: |
| 92 | +-- * n = 0 : `tower-from (osuc β) 0 = osuc β ≤′ γ` (hypothesis) |
| 93 | +-- * n+1 : `ω^^ (tower-from … n) ≤′ ω^^ γ ≤′ γ` (ω^^-mono + closure) |
| 94 | +---------------------------------------------------------------------- |
| 95 | + |
| 96 | +next-ε-least : ∀ {β γ} → osuc β ≤′ γ → ω^^ γ ≤′ γ → next-ε β ≤′ γ |
| 97 | +next-ε-least {β} {γ} β<γ ω^^γ≤γ = go |
| 98 | + where |
| 99 | + go : ∀ n → tower-from (osuc β) n ≤′ γ |
| 100 | + go zero = β<γ |
| 101 | + go (suc m) = |
| 102 | + ≤′-trans {ω^^ (tower-from (osuc β) m)} {ω^^ γ} {γ} |
| 103 | + (ω^^-mono-≤′ {tower-from (osuc β) m} {γ} (go m)) ω^^γ≤γ |
| 104 | + |
| 105 | +-- Monotonicity of `next-ε`: a larger base gives a larger next ε-number. |
| 106 | +-- By `next-ε-least` with γ := next-ε β (which is ω^^-closed by |
| 107 | +-- `ω^^-next-ε-≤`), since `osuc α ≤′ osuc β ≤′ next-ε β`. |
| 108 | +next-ε-mono : ∀ {α β} → α ≤′ β → next-ε α ≤′ next-ε β |
| 109 | +next-ε-mono {α} {β} p = |
| 110 | + next-ε-least {α} {next-ε β} |
| 111 | + (≤′-trans {osuc α} {osuc β} {next-ε β} p (β<next-ε β)) |
| 112 | + (ω^^-next-ε-≤ β) |
| 113 | + |
| 114 | +---------------------------------------------------------------------- |
| 115 | +-- ε₀ is the least value of φ₁ (φ₁ oz), hence ≤′ every φ₁ value. |
| 116 | +-- The `oz` base case of monotonicity; recursion on β alone. |
| 117 | +---------------------------------------------------------------------- |
| 118 | + |
| 119 | +ε₀-least : ∀ β → ε₀ ≤′ φ₁ β |
| 120 | +ε₀-least oz = ≤′-refl {ε₀} |
| 121 | +ε₀-least (osuc β) = |
| 122 | + ≤′-trans {ε₀} {φ₁ β} {next-ε (φ₁ β)} |
| 123 | + (ε₀-least β) |
| 124 | + (≤′-trans {φ₁ β} {osuc (φ₁ β)} {next-ε (φ₁ β)} |
| 125 | + (≤′-self-osuc (φ₁ β)) (β<next-ε (φ₁ β))) |
| 126 | +ε₀-least (olim f) = ≤′-lim {ε₀} (λ n → φ₁ (f n)) 0 (ε₀-least (f 0)) |
| 127 | + |
| 128 | +---------------------------------------------------------------------- |
| 129 | +-- φ₁ is a NORMAL FUNCTION. |
| 130 | +---------------------------------------------------------------------- |
| 131 | + |
| 132 | +-- Monotone. Structural recursion on the `_≤′_` shape of (α, β): |
| 133 | +-- * oz base reduces to `ε₀-least`; |
| 134 | +-- * successor/successor is `next-ε-mono` of the inductive step; |
| 135 | +-- * the two olim cases thread through `≤′-lim` / the pointwise olim rule. |
| 136 | +φ₁-mono : ∀ {α β} → α ≤′ β → φ₁ α ≤′ φ₁ β |
| 137 | +φ₁-mono {oz} {β} _ = ε₀-least β |
| 138 | +φ₁-mono {osuc α} {oz} p = ⊥-elim p |
| 139 | +φ₁-mono {osuc α} {osuc β} p = next-ε-mono {φ₁ α} {φ₁ β} (φ₁-mono {α} {β} p) |
| 140 | +φ₁-mono {osuc α} {olim f} (n , q) = |
| 141 | + ≤′-lim {φ₁ (osuc α)} (λ k → φ₁ (f k)) n (φ₁-mono {osuc α} {f n} q) |
| 142 | +φ₁-mono {olim g} {β} p = λ n → φ₁-mono {g n} {β} (p n) |
| 143 | + |
| 144 | +-- Strictly increasing at successors: φ₁ α <′ φ₁ (osuc α). Immediate, |
| 145 | +-- since `φ₁ (osuc α) = next-ε (φ₁ α)` and `β<next-ε` places `φ₁ α` strictly |
| 146 | +-- below `next-ε (φ₁ α)`. |
| 147 | +φ₁-lt-succ : ∀ α → φ₁ α <′ φ₁ (osuc α) |
| 148 | +φ₁-lt-succ α = β<next-ε (φ₁ α) |
| 149 | + |
| 150 | +-- Strictly monotone. `α <′ β` is `osuc α ≤′ β`; chain the successor jump |
| 151 | +-- `φ₁ α <′ φ₁ (osuc α)` with `φ₁ (osuc α) ≤′ φ₁ β` (monotonicity). |
| 152 | +φ₁-strict-mono : ∀ {α β} → α <′ β → φ₁ α <′ φ₁ β |
| 153 | +φ₁-strict-mono {α} {β} α<β = |
| 154 | + ≤′-trans {osuc (φ₁ α)} {φ₁ (osuc α)} {φ₁ β} |
| 155 | + (φ₁-lt-succ α) (φ₁-mono {osuc α} {β} α<β) |
| 156 | + |
| 157 | +-- Continuous at limits. φ₁ commutes with `olim` definitionally |
| 158 | +-- (the `olim` clause of φ₁), so continuity is `refl` — exactly the |
| 159 | +-- supremum-preservation a normal function requires. |
| 160 | +φ₁-continuous : ∀ f → φ₁ (olim f) ≡ olim (λ n → φ₁ (f n)) |
| 161 | +φ₁-continuous f = refl |
0 commit comments