|
| 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 — RUNG 5: EVERY level φ_α is a NORMAL FUNCTION, and |
| 6 | +-- φ_{α+1} ENUMERATES the fixed points of φ_α. Target-side climb toward |
| 7 | +-- ψ₀(Ω_ω) (BH order-type fidelity, open problem D-2026-06-14). Builds on |
| 8 | +-- `VeblenBinary` (the binary φ + the generic fixed-point engine) and |
| 9 | +-- `VeblenPhiNormal` (ω^^-monotonicity). 2026-06-20. |
| 10 | +-- |
| 11 | +-- ## What this slice adds |
| 12 | +-- |
| 13 | +-- `VeblenBinary` defined φ and proved continuity (`φ-cont`) + the generic |
| 14 | +-- engine correctness (`nextFix-fixed-{≤,≥}`). This slice closes the two |
| 15 | +-- remaining normal-function properties FOR EVERY LEVEL, by induction on |
| 16 | +-- the level α through the generic engine: |
| 17 | +-- |
| 18 | +-- * `φ-mono₂` — every φ_α is monotone in its argument |
| 19 | +-- (α fixed; a ≤′ b → φ_α a ≤′ φ_α b); |
| 20 | +-- * `φ-infl` — every φ_α is inflationary (β ≤′ φ_α β). |
| 21 | +-- |
| 22 | +-- Together with `VeblenBinary.φ-cont` this gives: EVERY Veblen level is a |
| 23 | +-- normal function (strictly-monotone-or-equal + continuous + inflationary |
| 24 | +-- — the three properties a fixed-point enumeration needs). |
| 25 | +-- |
| 26 | +-- And the defining property of the hierarchy: |
| 27 | +-- |
| 28 | +-- * `φ-level-fixed-{≤,≥}` — φ_{α+1}(β) IS a fixed point of φ_α |
| 29 | +-- (φ_α (φ_{α+1} β) ≃ φ_{α+1} β, bi-`≤′`). |
| 30 | +-- |
| 31 | +-- The generic engine lemmas (`deriv-mono`, `deriv-infl`, `deriv-fixed-*`, |
| 32 | +-- `nextFix-mono`, `commonStep-mono`) are proved once for an arbitrary |
| 33 | +-- (monotone / continuous) `g` and then instantiated at each level — the |
| 34 | +-- same reuse pattern `VeblenPhiNormal` used for φ₁, now generic. |
| 35 | +-- |
| 36 | +-- ## Honest scope (still a LONG climb) |
| 37 | +-- |
| 38 | +-- This is the normal-function backbone needed for "Γ₀ is the LEAST |
| 39 | +-- diagonal fixed point" (the next slice) and for the eventual |
| 40 | +-- ordinal-collapsing layer. It does NOT prove Γ₀ least, does NOT reach |
| 41 | +-- the collapsing layer, and closes NO postulate. Order-type fidelity |
| 42 | +-- (ψ₀(Ω_ω)) REMAINS OPEN (D-2026-06-14). bi-`≤′` (not `≡`) for the |
| 43 | +-- fixed-point facts, as throughout the Brouwer climb. |
| 44 | + |
| 45 | +module Ordinal.Brouwer.VeblenBinaryNormal where |
| 46 | + |
| 47 | +open import Data.Nat.Base using (ℕ; zero; suc) |
| 48 | +open import Data.Product.Base using (Σ; _,_) |
| 49 | +open import Data.Empty using (⊥-elim) |
| 50 | +open import Relation.Binary.PropositionalEquality using (_≡_; refl) |
| 51 | + |
| 52 | +open import Ordinal.Brouwer using (Ord; oz; osuc; olim) |
| 53 | +open import Ordinal.Brouwer.Phase13 |
| 54 | + using (_≤′_; _<′_; ≤′-refl; ≤′-trans; ≤′-lim; ≤′-zero; ≤′-self-osuc |
| 55 | + ; osuc-mono-≤′; f-in-lim′) |
| 56 | +open import Ordinal.Brouwer.OrdinalExp using (ω^^_; ω^^-infl) |
| 57 | +open import Ordinal.Brouwer.VeblenPhiNormal using (ω^^-mono-≤′) |
| 58 | +open import Ordinal.Brouwer.VeblenBinary |
| 59 | + using (φ; deriv; nextFix; commonStep; g-tower; nextFix-above |
| 60 | + ; nextFix-fixed-≤; nextFix-fixed-≥; φ-cont) |
| 61 | + |
| 62 | +---------------------------------------------------------------------- |
| 63 | +-- Propositional equality into `≤′` (continuity is stated as `≡`; the |
| 64 | +-- generic fixed-point lemmas want the `≤′` form). |
| 65 | +---------------------------------------------------------------------- |
| 66 | + |
| 67 | +≡→≤′ : ∀ {a b} → a ≡ b → a ≤′ b |
| 68 | +≡→≤′ {a} refl = ≤′-refl {a} |
| 69 | + |
| 70 | +---------------------------------------------------------------------- |
| 71 | +-- Generic monotonicity of the engine (for a monotone g). |
| 72 | +---------------------------------------------------------------------- |
| 73 | + |
| 74 | +-- The g-tower is monotone in its base. |
| 75 | +g-tower-mono : |
| 76 | + (g : Ord → Ord) (gm : ∀ {a b} → a ≤′ b → g a ≤′ g b) |
| 77 | + (a b : Ord) → a ≤′ b → ∀ n → g-tower g a n ≤′ g-tower g b n |
| 78 | +g-tower-mono g gm a b p zero = p |
| 79 | +g-tower-mono g gm a b p (suc n) = |
| 80 | + gm {g-tower g a n} {g-tower g b n} (g-tower-mono g gm a b p n) |
| 81 | + |
| 82 | +-- nextFix is monotone in its base (for monotone g). |
| 83 | +nextFix-mono : |
| 84 | + (g : Ord → Ord) (gm : ∀ {a b} → a ≤′ b → g a ≤′ g b) |
| 85 | + {x y : Ord} → x ≤′ y → nextFix g x ≤′ nextFix g y |
| 86 | +nextFix-mono g gm {x} {y} p = |
| 87 | + λ n → ≤′-lim {g-tower g (osuc x) n} (g-tower g (osuc y)) n |
| 88 | + (g-tower-mono g gm (osuc x) (osuc y) p n) |
| 89 | + |
| 90 | +-- One enumeration step is non-decreasing: deriv g b ≤′ deriv g (osuc b). |
| 91 | +-- (No monotonicity hypothesis needed — nextFix lands strictly above.) |
| 92 | +deriv-step-≤ : (g : Ord → Ord) (b : Ord) → deriv g b ≤′ deriv g (osuc b) |
| 93 | +deriv-step-≤ g b = |
| 94 | + ≤′-trans {deriv g b} {osuc (deriv g b)} {nextFix g (deriv g b)} |
| 95 | + (≤′-self-osuc (deriv g b)) (nextFix-above g (deriv g b)) |
| 96 | + |
| 97 | +-- deriv g oz is the least enumerated value. |
| 98 | +deriv-oz-least : (g : Ord → Ord) (b : Ord) → deriv g oz ≤′ deriv g b |
| 99 | +deriv-oz-least g oz = ≤′-refl {deriv g oz} |
| 100 | +deriv-oz-least g (osuc b) = |
| 101 | + ≤′-trans {deriv g oz} {deriv g b} {deriv g (osuc b)} |
| 102 | + (deriv-oz-least g b) (deriv-step-≤ g b) |
| 103 | +deriv-oz-least g (olim h) = ≤′-lim {deriv g oz} (λ k → deriv g (h k)) 0 (deriv-oz-least g (h 0)) |
| 104 | + |
| 105 | +-- deriv is monotone in its argument (for monotone g). Structural |
| 106 | +-- recursion on the `_≤′_` shape — the φ₁-mono pattern, now generic. |
| 107 | +deriv-mono : |
| 108 | + (g : Ord → Ord) (gm : ∀ {a b} → a ≤′ b → g a ≤′ g b) |
| 109 | + {a b : Ord} → a ≤′ b → deriv g a ≤′ deriv g b |
| 110 | +deriv-mono g gm {oz} {b} _ = deriv-oz-least g b |
| 111 | +deriv-mono g gm {osuc a} {oz} p = ⊥-elim p |
| 112 | +deriv-mono g gm {osuc a} {osuc b} p = |
| 113 | + nextFix-mono g gm {deriv g a} {deriv g b} (deriv-mono g gm {a} {b} p) |
| 114 | +deriv-mono g gm {osuc a} {olim h} (n , q) = |
| 115 | + ≤′-lim {deriv g (osuc a)} (λ k → deriv g (h k)) n (deriv-mono g gm {osuc a} {h n} q) |
| 116 | +deriv-mono g gm {olim a₁} {b} p = |
| 117 | + λ n → deriv-mono g gm {a₁ n} {b} (p n) |
| 118 | + |
| 119 | +-- commonStep is monotone when every family member is. |
| 120 | +commonStep-mono : |
| 121 | + (F : ℕ → Ord → Ord) (Fm : ∀ n {x y} → x ≤′ y → F n x ≤′ F n y) |
| 122 | + {x y : Ord} → x ≤′ y → commonStep F x ≤′ commonStep F y |
| 123 | +commonStep-mono F Fm {x} {y} p = |
| 124 | + λ n → ≤′-lim {F n x} (λ k → F k y) n (Fm n p) |
| 125 | + |
| 126 | +---------------------------------------------------------------------- |
| 127 | +-- Every Veblen level is monotone in its argument. |
| 128 | +---------------------------------------------------------------------- |
| 129 | + |
| 130 | +φ-mono₂ : ∀ α {a b} → a ≤′ b → φ α a ≤′ φ α b |
| 131 | +φ-mono₂ oz {a} {b} p = ω^^-mono-≤′ {a} {b} p |
| 132 | +φ-mono₂ (osuc α) {a} {b} p = |
| 133 | + deriv-mono (φ α) (λ {c} {d} → φ-mono₂ α {c} {d}) {a} {b} p |
| 134 | +φ-mono₂ (olim f) {a} {b} p = |
| 135 | + deriv-mono (commonStep (λ n → φ (f n))) |
| 136 | + (commonStep-mono (λ n → φ (f n)) (λ n {x} {y} → φ-mono₂ (f n) {x} {y})) {a} {b} p |
| 137 | + |
| 138 | +---------------------------------------------------------------------- |
| 139 | +-- Every Veblen level is inflationary. |
| 140 | +---------------------------------------------------------------------- |
| 141 | + |
| 142 | +-- deriv is inflationary (no hypothesis on g — nextFix lands above). |
| 143 | +deriv-infl : (g : Ord → Ord) → ∀ β → β ≤′ deriv g β |
| 144 | +deriv-infl g oz = ≤′-zero {deriv g oz} |
| 145 | +deriv-infl g (osuc β) = |
| 146 | + ≤′-trans {osuc β} {osuc (deriv g β)} {nextFix g (deriv g β)} |
| 147 | + (osuc-mono-≤′ {β} {deriv g β} (deriv-infl g β)) (nextFix-above g (deriv g β)) |
| 148 | +deriv-infl g (olim h) = |
| 149 | + λ n → ≤′-lim {h n} (λ k → deriv g (h k)) n (deriv-infl g (h n)) |
| 150 | + |
| 151 | +φ-infl : ∀ α β → β ≤′ φ α β |
| 152 | +φ-infl oz β = ω^^-infl β |
| 153 | +φ-infl (osuc α) β = deriv-infl (φ α) β |
| 154 | +φ-infl (olim f) β = deriv-infl (commonStep (λ n → φ (f n))) β |
| 155 | + |
| 156 | +---------------------------------------------------------------------- |
| 157 | +-- φ_{α+1} enumerates the fixed points of φ_α. |
| 158 | +-- |
| 159 | +-- Every value `deriv g β` is a fixed point of `g` (for continuous / |
| 160 | +-- monotone-inflationary g), generalising `nextFix-fixed-*` from the base |
| 161 | +-- of the tower to the whole enumeration; instantiated at g = φ_α this is |
| 162 | +-- the defining Veblen recurrence φ_α(φ_{α+1}(β)) ≃ φ_{α+1}(β). |
| 163 | +---------------------------------------------------------------------- |
| 164 | + |
| 165 | +deriv-fixed-≤ : |
| 166 | + (g : Ord → Ord) (gc : ∀ h → g (olim h) ≤′ olim (λ n → g (h n))) |
| 167 | + (β : Ord) → g (deriv g β) ≤′ deriv g β |
| 168 | +deriv-fixed-≤ g gc oz = nextFix-fixed-≤ g gc oz |
| 169 | +deriv-fixed-≤ g gc (osuc β) = nextFix-fixed-≤ g gc (deriv g β) |
| 170 | +deriv-fixed-≤ g gc (olim h) = |
| 171 | + ≤′-trans {g (olim D)} {olim (λ n → g (D n))} {olim D} |
| 172 | + (gc D) |
| 173 | + (λ n → ≤′-trans {g (D n)} {D n} {olim D} |
| 174 | + (deriv-fixed-≤ g gc (h n)) (f-in-lim′ D n)) |
| 175 | + where D = λ k → deriv g (h k) |
| 176 | + |
| 177 | +deriv-fixed-≥ : |
| 178 | + (g : Ord → Ord) (gm : ∀ {a b} → a ≤′ b → g a ≤′ g b) (gi : ∀ y → y ≤′ g y) |
| 179 | + (β : Ord) → deriv g β ≤′ g (deriv g β) |
| 180 | +deriv-fixed-≥ g gm gi oz = nextFix-fixed-≥ g gm gi oz |
| 181 | +deriv-fixed-≥ g gm gi (osuc β) = nextFix-fixed-≥ g gm gi (deriv g β) |
| 182 | +deriv-fixed-≥ g gm gi (olim h) = |
| 183 | + λ n → ≤′-trans {D n} {g (D n)} {g (olim D)} |
| 184 | + (deriv-fixed-≥ g gm gi (h n)) (gm {D n} {olim D} (f-in-lim′ D n)) |
| 185 | + where D = λ k → deriv g (h k) |
| 186 | + |
| 187 | +-- The Veblen recurrence: φ_{α+1}(β) is a fixed point of φ_α (bi-`≤′`). |
| 188 | +φ-level-fixed-≤ : ∀ α β → φ α (φ (osuc α) β) ≤′ φ (osuc α) β |
| 189 | +φ-level-fixed-≤ α β = deriv-fixed-≤ (φ α) (λ h → ≡→≤′ (φ-cont α h)) β |
| 190 | + |
| 191 | +φ-level-fixed-≥ : ∀ α β → φ (osuc α) β ≤′ φ α (φ (osuc α) β) |
| 192 | +φ-level-fixed-≥ α β = |
| 193 | + deriv-fixed-≥ (φ α) (λ {a} {b} → φ-mono₂ α {a} {b}) (φ-infl α) β |
0 commit comments