|
| 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 | +-- Binary Veblen φ_α(β) + the diagonal Γ₀ over Brouwer ordinals — RUNG 4 |
| 6 | +-- of the target-side climb toward ψ₀(Ω_ω) (BH order-type fidelity, open |
| 7 | +-- problem D-2026-06-14). Builds on `OrdinalExp` (ω^^ = φ₀), |
| 8 | +-- `VeblenPhi` / `VeblenPhiNormal` (φ₁ = the ε-number enumeration, now a |
| 9 | +-- normal function). 2026-06-20. |
| 10 | +-- |
| 11 | +-- ## The construction (the load-bearing tractability move) |
| 12 | +-- |
| 13 | +-- The two-argument Veblen function is defined by STRUCTURAL RECURSION ON |
| 14 | +-- THE FIRST ARGUMENT, returning a function `Ord → Ord`: |
| 15 | +-- |
| 16 | +-- φ oz = ω^^_ (φ₀ = ω-exponentiation) |
| 17 | +-- φ (osuc α) = deriv (φ α) (enumerate fixed points of φ_α) |
| 18 | +-- φ (olim f) = deriv (commonStep (n ↦ φ (f n))) (common fixed points) |
| 19 | +-- |
| 20 | +-- The SECOND-argument recursion lives entirely inside the generic |
| 21 | +-- fixed-point enumerator `deriv` (independent of φ), so φ's own recursion |
| 22 | +-- is purely first-argument-structural and Agda accepts its termination |
| 23 | +-- WITHOUT a `TERMINATING` pragma. This is the move that makes binary |
| 24 | +-- Veblen tractable here: |
| 25 | +-- |
| 26 | +-- * `deriv g` enumerates the fixed points of a (continuous) `g`, by |
| 27 | +-- recursion on its own argument — `deriv g (osuc β) = nextFix g |
| 28 | +-- (deriv g β)`, `deriv g (olim h) = olim (deriv g ∘ h)`; |
| 29 | +-- * `nextFix g x = olim (g-tower g (osuc x))` is the least fixed point |
| 30 | +-- of `g` strictly above `x` (sup of the `g`-iteration tower from |
| 31 | +-- `osuc x`) — the exact generalisation of `next-ε` from `VeblenPhi`; |
| 32 | +-- * `commonStep F x = olim (n ↦ F n x)` packages a countable family of |
| 33 | +-- normal functions into one whose fixed points are the COMMON fixed |
| 34 | +-- points of the family — the limit case. |
| 35 | +-- |
| 36 | +-- Γ₀ (the Feferman–Schütte ordinal) is the diagonal: |
| 37 | +-- Γ₀ = sup { 0, φ_0(0), φ_{φ_0(0)}(0), … } = olim Γ-tower. |
| 38 | +-- |
| 39 | +-- ## What is proved here |
| 40 | +-- |
| 41 | +-- * the recurrences (`φ-oz`, `φ-osuc`, `φ-olim`) — definitional; |
| 42 | +-- * φ is CONTINUOUS in its second argument (`φ-cont`) — a normal- |
| 43 | +-- function property, definitional from `deriv`'s `olim` clause; |
| 44 | +-- * the generic fixed-point engine is CORRECT: for continuous monotone |
| 45 | +-- inflationary `g`, `nextFix g x` is a fixed point of `g` (bi-`≤′`, |
| 46 | +-- `nextFix-fixed-≤` / `nextFix-fixed-≥`) and lies strictly above `x` |
| 47 | +-- (`nextFix-above`); |
| 48 | +-- * the engine SUBSUMES the ε-number story: instantiated at ω^^ it |
| 49 | +-- reproves `ω^^ (nextFix ω^^ x) ≃ nextFix ω^^ x` (`ω^^-nextFix-fixed-{≤,≥}`); |
| 50 | +-- * Γ₀ is defined, positive (`Γ₀-pos`), an upper bound of its diagonal |
| 51 | +-- approximants (`Γ-tower-below-Γ₀`, `φ-diagonal-step`). |
| 52 | +-- |
| 53 | +-- ## Honest scope (rung 4 of a LONG climb — do not overclaim) |
| 54 | +-- |
| 55 | +-- Γ₀ is DEFINED and given basic properties; the full theorem that Γ₀ is |
| 56 | +-- the LEAST fixed point of the diagonal α ↦ φ_α(0) (the proper |
| 57 | +-- characterisation of the Feferman–Schütte ordinal) is NOT proved here — |
| 58 | +-- it needs the common-fixed-point correctness of `commonStep` plus |
| 59 | +-- monotonicity/inflationarity of every φ level, and is the next slice. |
| 60 | +-- ψ₀(Ω_ω) sits FAR above Γ₀ and additionally needs the ordinal-collapsing |
| 61 | +-- layer; order-type fidelity (ψ₀(Ω_ω)) therefore REMAINS OPEN |
| 62 | +-- (D-2026-06-14). This slice neither characterises Γ₀ as least nor plugs |
| 63 | +-- `Fidelity.AtHeight`, and closes NO postulate. bi-`≤′` (not `≡`) is used |
| 64 | +-- for fixed-point facts (Brouwer `olim`s of different ℕ-indexings of one |
| 65 | +-- supremum are not definitionally equal). |
| 66 | + |
| 67 | +module Ordinal.Brouwer.VeblenBinary where |
| 68 | + |
| 69 | +open import Data.Nat.Base using (ℕ; zero; suc) |
| 70 | +open import Data.Product.Base using (Σ; _,_) |
| 71 | +open import Relation.Binary.PropositionalEquality using (_≡_; refl) |
| 72 | + |
| 73 | +open import Ordinal.Brouwer using (Ord; oz; osuc; olim) |
| 74 | +open import Ordinal.Brouwer.Phase13 |
| 75 | + using (_≤′_; _<′_; ≤′-refl; ≤′-trans; f-in-lim′) |
| 76 | +open import Ordinal.Brouwer.OrdinalExp using (ω^^_; ω^^-infl) |
| 77 | +open import Ordinal.Brouwer.VeblenPhiNormal using (ω^^-mono-≤′) |
| 78 | + |
| 79 | +---------------------------------------------------------------------- |
| 80 | +-- The generic fixed-point engine (independent of φ). |
| 81 | +---------------------------------------------------------------------- |
| 82 | + |
| 83 | +-- Iterate g from a base, ℕ-many times. |
| 84 | +g-tower : (Ord → Ord) → Ord → ℕ → Ord |
| 85 | +g-tower g x zero = x |
| 86 | +g-tower g x (suc n) = g (g-tower g x n) |
| 87 | + |
| 88 | +-- The least fixed point of g strictly above x: the supremum of the |
| 89 | +-- g-iteration tower started at `osuc x`. Generalises `VeblenPhi.next-ε`. |
| 90 | +nextFix : (Ord → Ord) → Ord → Ord |
| 91 | +nextFix g x = olim (g-tower g (osuc x)) |
| 92 | + |
| 93 | +-- Enumerate the fixed points of g. Recursion on the SECOND argument, |
| 94 | +-- with g fixed; generalises `VeblenPhi.φ₁`. |
| 95 | +deriv : (Ord → Ord) → Ord → Ord |
| 96 | +deriv g oz = nextFix g oz |
| 97 | +deriv g (osuc β) = nextFix g (deriv g β) |
| 98 | +deriv g (olim h) = olim (λ n → deriv g (h n)) |
| 99 | + |
| 100 | +-- Package a countable family of normal functions into one whose fixed |
| 101 | +-- points are the COMMON fixed points of the family. |
| 102 | +commonStep : (ℕ → (Ord → Ord)) → Ord → Ord |
| 103 | +commonStep F x = olim (λ n → F n x) |
| 104 | + |
| 105 | +---------------------------------------------------------------------- |
| 106 | +-- Binary Veblen function. Structural recursion on the FIRST argument. |
| 107 | +---------------------------------------------------------------------- |
| 108 | + |
| 109 | +φ : Ord → Ord → Ord |
| 110 | +φ oz = ω^^_ |
| 111 | +φ (osuc α) = deriv (φ α) |
| 112 | +φ (olim f) = deriv (commonStep (λ n → φ (f n))) |
| 113 | + |
| 114 | +-- The recurrences (definitional). |
| 115 | +φ-oz : φ oz ≡ ω^^_ |
| 116 | +φ-oz = refl |
| 117 | + |
| 118 | +φ-osuc : ∀ α → φ (osuc α) ≡ deriv (φ α) |
| 119 | +φ-osuc _ = refl |
| 120 | + |
| 121 | +φ-olim : ∀ f → φ (olim f) ≡ deriv (commonStep (λ n → φ (f n))) |
| 122 | +φ-olim _ = refl |
| 123 | + |
| 124 | +-- φ is CONTINUOUS in its second argument: it commutes with `olim`. A |
| 125 | +-- defining property of a normal function, here definitional because every |
| 126 | +-- branch (ω^^ / deriv) commutes with `olim` by its own `olim` clause. |
| 127 | +φ-cont : ∀ α h → φ α (olim h) ≡ olim (λ n → φ α (h n)) |
| 128 | +φ-cont oz h = refl |
| 129 | +φ-cont (osuc α) h = refl |
| 130 | +φ-cont (olim f) h = refl |
| 131 | + |
| 132 | +---------------------------------------------------------------------- |
| 133 | +-- Correctness of the fixed-point engine (generic, then at ω^^). |
| 134 | +---------------------------------------------------------------------- |
| 135 | + |
| 136 | +-- `nextFix g x` lies strictly above x (tower index 0 = osuc x). |
| 137 | +nextFix-above : ∀ g x → osuc x ≤′ nextFix g x |
| 138 | +nextFix-above g x = 0 , ≤′-refl {x} |
| 139 | + |
| 140 | +-- One step of the tower is `g` of the previous (definitional); recorded |
| 141 | +-- for readability. |
| 142 | +g-tower-suc : ∀ g x n → g (g-tower g x n) ≡ g-tower g x (suc n) |
| 143 | +g-tower-suc g x n = refl |
| 144 | + |
| 145 | +-- `g (nextFix g x) ≤′ nextFix g x` for continuous g. The supremum of the |
| 146 | +-- tower SHIFTED by one (= g applied through the limit) is below the |
| 147 | +-- supremum of the tower. |
| 148 | +nextFix-fixed-≤ : |
| 149 | + (g : Ord → Ord) |
| 150 | + (g-cont : ∀ h → g (olim h) ≤′ olim (λ n → g (h n))) |
| 151 | + (x : Ord) → |
| 152 | + g (nextFix g x) ≤′ nextFix g x |
| 153 | +nextFix-fixed-≤ g g-cont x = |
| 154 | + ≤′-trans {g (olim T)} {olim (λ n → g (T n))} {olim T} |
| 155 | + (g-cont T) (λ n → f-in-lim′ T (suc n)) |
| 156 | + where T = g-tower g (osuc x) |
| 157 | + |
| 158 | +-- `nextFix g x ≤′ g (nextFix g x)` for monotone inflationary g. Each |
| 159 | +-- tower approximant is below `g (olim T)`: index 0 via inflationarity, |
| 160 | +-- successors via monotonicity. |
| 161 | +nextFix-fixed-≥ : |
| 162 | + (g : Ord → Ord) |
| 163 | + (g-mono : ∀ {a b} → a ≤′ b → g a ≤′ g b) |
| 164 | + (g-infl : ∀ y → y ≤′ g y) |
| 165 | + (x : Ord) → |
| 166 | + nextFix g x ≤′ g (nextFix g x) |
| 167 | +nextFix-fixed-≥ g g-mono g-infl x = go |
| 168 | + where |
| 169 | + T = g-tower g (osuc x) |
| 170 | + go : ∀ n → T n ≤′ g (olim T) |
| 171 | + go zero = |
| 172 | + ≤′-trans {osuc x} {olim T} {g (olim T)} (f-in-lim′ T 0) (g-infl (olim T)) |
| 173 | + go (suc m) = g-mono {T m} {olim T} (f-in-lim′ T m) |
| 174 | + |
| 175 | +---------------------------------------------------------------------- |
| 176 | +-- The engine subsumes the ε-number story: instantiate at g = ω^^. |
| 177 | +-- ω^^ is continuous by definition (its `olim` clause), monotone |
| 178 | +-- (`ω^^-mono-≤′`), and inflationary (`ω^^-infl`). So `nextFix ω^^ x` is |
| 179 | +-- a genuine ε-number (fixed point of ω-exponentiation), recovered from the |
| 180 | +-- generic engine — exactly the role `next-ε` plays in `VeblenPhi`. |
| 181 | +---------------------------------------------------------------------- |
| 182 | + |
| 183 | +ω^^-nextFix-fixed-≤ : ∀ x → ω^^ (nextFix ω^^_ x) ≤′ nextFix ω^^_ x |
| 184 | +ω^^-nextFix-fixed-≤ = |
| 185 | + nextFix-fixed-≤ ω^^_ (λ h → ≤′-refl {olim (λ n → ω^^ (h n))}) |
| 186 | + |
| 187 | +ω^^-nextFix-fixed-≥ : ∀ x → nextFix ω^^_ x ≤′ ω^^ (nextFix ω^^_ x) |
| 188 | +ω^^-nextFix-fixed-≥ = |
| 189 | + nextFix-fixed-≥ ω^^_ (λ {a} {b} → ω^^-mono-≤′ {a} {b}) ω^^-infl |
| 190 | + |
| 191 | +---------------------------------------------------------------------- |
| 192 | +-- Γ₀ — the diagonal (Feferman–Schütte ordinal). |
| 193 | +---------------------------------------------------------------------- |
| 194 | + |
| 195 | +-- The diagonal tower: 0, φ_0(0), φ_{φ_0(0)}(0), φ_{φ_{φ_0(0)}(0)}(0), … |
| 196 | +Γ-tower : ℕ → Ord |
| 197 | +Γ-tower zero = oz |
| 198 | +Γ-tower (suc n) = φ (Γ-tower n) oz |
| 199 | + |
| 200 | +Γ₀ : Ord |
| 201 | +Γ₀ = olim Γ-tower |
| 202 | + |
| 203 | +-- Γ₀ is positive: the first diagonal step is φ_0(0) = ω^^ 0 = 1. |
| 204 | +Γ₀-pos : oz <′ Γ₀ |
| 205 | +Γ₀-pos = 1 , ≤′-refl {oz} |
| 206 | + |
| 207 | +-- Every diagonal approximant is below Γ₀ (it is their supremum). |
| 208 | +Γ-tower-below-Γ₀ : ∀ n → Γ-tower n ≤′ Γ₀ |
| 209 | +Γ-tower-below-Γ₀ n = f-in-lim′ Γ-tower n |
| 210 | + |
| 211 | +-- The diagonal map applied to an approximant stays below Γ₀: |
| 212 | +-- φ_{Γ-tower n}(0) = Γ-tower (suc n) ≤′ Γ₀. Γ₀ is closed under the |
| 213 | +-- diagonal on its own approximants (the constructive seed of "Γ₀ is a |
| 214 | +-- fixed point of α ↦ φ_α(0)"; the full bi-`≤′` fixed point is the next |
| 215 | +-- slice — see the honest-scope note in the module header). |
| 216 | +φ-diagonal-step : ∀ n → φ (Γ-tower n) oz ≤′ Γ₀ |
| 217 | +φ-diagonal-step n = f-in-lim′ Γ-tower (suc n) |
0 commit comments