From 52540bbed97830c2c8b7b3effc67865dbc841a8f Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 20 Jun 2026 00:27:27 +0000 Subject: [PATCH] =?UTF-8?q?proof(ordinal):=20every=20Veblen=20level=20is?= =?UTF-8?q?=20a=20normal=20function;=20=CF=86=5F{=CE=B1+1}=20enumerates=20?= =?UTF-8?q?fixed=20points=20of=20=CF=86=5F=CE=B1=20(BH=20climb=20rung=205)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Target-side climb toward ψ₀(Ω_ω) (BH order-type fidelity, open problem D-2026-06-14). Builds on VeblenBinary (binary φ + generic fixed-point engine) and VeblenPhiNormal (ω^^-monotonicity). New module proofs/agda/Ordinal/Brouwer/VeblenBinaryNormal.agda (--safe --without-K, zero postulates, structural recursion): VeblenBinary proved continuity (φ-cont) + base-of-tower fixed-point correctness (nextFix-fixed-{≤,≥}). This slice closes the two remaining normal-function properties FOR EVERY LEVEL, by induction on the level α through the generic engine: * φ-mono₂ — every φ_α is monotone in its argument; * φ-infl — every φ_α is inflationary (β ≤′ φ_α β). With VeblenBinary.φ-cont this gives: EVERY Veblen level is a normal function. And the defining property of the hierarchy: * φ-level-fixed-{≤,≥} — φ_{α+1}(β) IS a fixed point of φ_α (φ_α (φ_{α+1} β) ≃ φ_{α+1} β, bi-≤′). Generic engine lemmas proved once for an arbitrary monotone/continuous g and instantiated at each level (the VeblenPhiNormal reuse pattern, now generic): g-tower-mono, nextFix-mono, deriv-step-≤, deriv-oz-least, deriv-mono, commonStep-mono; deriv-infl; deriv-fixed-≤ (continuous g), deriv-fixed-≥ (monotone + inflationary g); plus ≡→≤′. Design note: every deriv-mono / ≤′-lim / ω^^-mono-≤′ call (and the ⊤-valued ≤′-zero) pins its implicit source explicitly — _≤′_ is a reducing relation. Honest scope: this is the normal-function backbone for "Γ₀ is the LEAST diagonal fixed point" (the next slice) and the eventual ordinal-collapsing layer. It does NOT prove Γ₀ least, does NOT reach the collapsing layer, and closes NO postulate. Order-type fidelity (ψ₀(Ω_ω)) REMAINS OPEN (D-2026-06-14). Wiring: All.agda import; Smoke.agda pin block (9 headlines). agda proofs/agda/All.agda and proofs/agda/Smoke.agda exit 0 under --safe --without-K; kernel-guard.sh PASS; zero postulates. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01Rw1RpYXU5Q7rzy2bVofVeB --- proofs/agda/All.agda | 1 + .../Ordinal/Brouwer/VeblenBinaryNormal.agda | 193 ++++++++++++++++++ proofs/agda/Smoke.agda | 21 ++ 3 files changed, 215 insertions(+) create mode 100644 proofs/agda/Ordinal/Brouwer/VeblenBinaryNormal.agda diff --git a/proofs/agda/All.agda b/proofs/agda/All.agda index e61397c..49f2a98 100644 --- a/proofs/agda/All.agda +++ b/proofs/agda/All.agda @@ -123,6 +123,7 @@ open import Ordinal.Brouwer.OrdinalExp open import Ordinal.Brouwer.VeblenPhi open import Ordinal.Brouwer.VeblenPhiNormal -- φ₁ a normal function; next-ε β LEAST ε-number above β open import Ordinal.Brouwer.VeblenBinary -- binary Veblen φ_α(β) + the diagonal Γ₀ +open import Ordinal.Brouwer.VeblenBinaryNormal -- every φ_α a normal function; φ_{α+1} enumerates fixed points of φ_α open import Ordinal.Brouwer.StrictLeftMonoRefuted open import Ordinal.Brouwer.AdditivePrincipalGenericRefuted open import Ordinal.Buchholz.Syntax diff --git a/proofs/agda/Ordinal/Brouwer/VeblenBinaryNormal.agda b/proofs/agda/Ordinal/Brouwer/VeblenBinaryNormal.agda new file mode 100644 index 0000000..d1819dd --- /dev/null +++ b/proofs/agda/Ordinal/Brouwer/VeblenBinaryNormal.agda @@ -0,0 +1,193 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell + +-- Binary Veblen — RUNG 5: EVERY level φ_α is a NORMAL FUNCTION, and +-- φ_{α+1} ENUMERATES the fixed points of φ_α. Target-side climb toward +-- ψ₀(Ω_ω) (BH order-type fidelity, open problem D-2026-06-14). Builds on +-- `VeblenBinary` (the binary φ + the generic fixed-point engine) and +-- `VeblenPhiNormal` (ω^^-monotonicity). 2026-06-20. +-- +-- ## What this slice adds +-- +-- `VeblenBinary` defined φ and proved continuity (`φ-cont`) + the generic +-- engine correctness (`nextFix-fixed-{≤,≥}`). This slice closes the two +-- remaining normal-function properties FOR EVERY LEVEL, by induction on +-- the level α through the generic engine: +-- +-- * `φ-mono₂` — every φ_α is monotone in its argument +-- (α fixed; a ≤′ b → φ_α a ≤′ φ_α b); +-- * `φ-infl` — every φ_α is inflationary (β ≤′ φ_α β). +-- +-- Together with `VeblenBinary.φ-cont` this gives: EVERY Veblen level is a +-- normal function (strictly-monotone-or-equal + continuous + inflationary +-- — the three properties a fixed-point enumeration needs). +-- +-- And the defining property of the hierarchy: +-- +-- * `φ-level-fixed-{≤,≥}` — φ_{α+1}(β) IS a fixed point of φ_α +-- (φ_α (φ_{α+1} β) ≃ φ_{α+1} β, bi-`≤′`). +-- +-- The generic engine lemmas (`deriv-mono`, `deriv-infl`, `deriv-fixed-*`, +-- `nextFix-mono`, `commonStep-mono`) are proved once for an arbitrary +-- (monotone / continuous) `g` and then instantiated at each level — the +-- same reuse pattern `VeblenPhiNormal` used for φ₁, now generic. +-- +-- ## Honest scope (still a LONG climb) +-- +-- This is the normal-function backbone needed for "Γ₀ is the LEAST +-- diagonal fixed point" (the next slice) and for the eventual +-- ordinal-collapsing layer. It does NOT prove Γ₀ least, does NOT reach +-- the collapsing layer, and closes NO postulate. Order-type fidelity +-- (ψ₀(Ω_ω)) REMAINS OPEN (D-2026-06-14). bi-`≤′` (not `≡`) for the +-- fixed-point facts, as throughout the Brouwer climb. + +module Ordinal.Brouwer.VeblenBinaryNormal where + +open import Data.Nat.Base using (ℕ; zero; suc) +open import Data.Product.Base using (Σ; _,_) +open import Data.Empty using (⊥-elim) +open import Relation.Binary.PropositionalEquality using (_≡_; refl) + +open import Ordinal.Brouwer using (Ord; oz; osuc; olim) +open import Ordinal.Brouwer.Phase13 + using (_≤′_; _<′_; ≤′-refl; ≤′-trans; ≤′-lim; ≤′-zero; ≤′-self-osuc + ; osuc-mono-≤′; f-in-lim′) +open import Ordinal.Brouwer.OrdinalExp using (ω^^_; ω^^-infl) +open import Ordinal.Brouwer.VeblenPhiNormal using (ω^^-mono-≤′) +open import Ordinal.Brouwer.VeblenBinary + using (φ; deriv; nextFix; commonStep; g-tower; nextFix-above + ; nextFix-fixed-≤; nextFix-fixed-≥; φ-cont) + +---------------------------------------------------------------------- +-- Propositional equality into `≤′` (continuity is stated as `≡`; the +-- generic fixed-point lemmas want the `≤′` form). +---------------------------------------------------------------------- + +≡→≤′ : ∀ {a b} → a ≡ b → a ≤′ b +≡→≤′ {a} refl = ≤′-refl {a} + +---------------------------------------------------------------------- +-- Generic monotonicity of the engine (for a monotone g). +---------------------------------------------------------------------- + +-- The g-tower is monotone in its base. +g-tower-mono : + (g : Ord → Ord) (gm : ∀ {a b} → a ≤′ b → g a ≤′ g b) + (a b : Ord) → a ≤′ b → ∀ n → g-tower g a n ≤′ g-tower g b n +g-tower-mono g gm a b p zero = p +g-tower-mono g gm a b p (suc n) = + gm {g-tower g a n} {g-tower g b n} (g-tower-mono g gm a b p n) + +-- nextFix is monotone in its base (for monotone g). +nextFix-mono : + (g : Ord → Ord) (gm : ∀ {a b} → a ≤′ b → g a ≤′ g b) + {x y : Ord} → x ≤′ y → nextFix g x ≤′ nextFix g y +nextFix-mono g gm {x} {y} p = + λ n → ≤′-lim {g-tower g (osuc x) n} (g-tower g (osuc y)) n + (g-tower-mono g gm (osuc x) (osuc y) p n) + +-- One enumeration step is non-decreasing: deriv g b ≤′ deriv g (osuc b). +-- (No monotonicity hypothesis needed — nextFix lands strictly above.) +deriv-step-≤ : (g : Ord → Ord) (b : Ord) → deriv g b ≤′ deriv g (osuc b) +deriv-step-≤ g b = + ≤′-trans {deriv g b} {osuc (deriv g b)} {nextFix g (deriv g b)} + (≤′-self-osuc (deriv g b)) (nextFix-above g (deriv g b)) + +-- deriv g oz is the least enumerated value. +deriv-oz-least : (g : Ord → Ord) (b : Ord) → deriv g oz ≤′ deriv g b +deriv-oz-least g oz = ≤′-refl {deriv g oz} +deriv-oz-least g (osuc b) = + ≤′-trans {deriv g oz} {deriv g b} {deriv g (osuc b)} + (deriv-oz-least g b) (deriv-step-≤ g b) +deriv-oz-least g (olim h) = ≤′-lim {deriv g oz} (λ k → deriv g (h k)) 0 (deriv-oz-least g (h 0)) + +-- deriv is monotone in its argument (for monotone g). Structural +-- recursion on the `_≤′_` shape — the φ₁-mono pattern, now generic. +deriv-mono : + (g : Ord → Ord) (gm : ∀ {a b} → a ≤′ b → g a ≤′ g b) + {a b : Ord} → a ≤′ b → deriv g a ≤′ deriv g b +deriv-mono g gm {oz} {b} _ = deriv-oz-least g b +deriv-mono g gm {osuc a} {oz} p = ⊥-elim p +deriv-mono g gm {osuc a} {osuc b} p = + nextFix-mono g gm {deriv g a} {deriv g b} (deriv-mono g gm {a} {b} p) +deriv-mono g gm {osuc a} {olim h} (n , q) = + ≤′-lim {deriv g (osuc a)} (λ k → deriv g (h k)) n (deriv-mono g gm {osuc a} {h n} q) +deriv-mono g gm {olim a₁} {b} p = + λ n → deriv-mono g gm {a₁ n} {b} (p n) + +-- commonStep is monotone when every family member is. +commonStep-mono : + (F : ℕ → Ord → Ord) (Fm : ∀ n {x y} → x ≤′ y → F n x ≤′ F n y) + {x y : Ord} → x ≤′ y → commonStep F x ≤′ commonStep F y +commonStep-mono F Fm {x} {y} p = + λ n → ≤′-lim {F n x} (λ k → F k y) n (Fm n p) + +---------------------------------------------------------------------- +-- Every Veblen level is monotone in its argument. +---------------------------------------------------------------------- + +φ-mono₂ : ∀ α {a b} → a ≤′ b → φ α a ≤′ φ α b +φ-mono₂ oz {a} {b} p = ω^^-mono-≤′ {a} {b} p +φ-mono₂ (osuc α) {a} {b} p = + deriv-mono (φ α) (λ {c} {d} → φ-mono₂ α {c} {d}) {a} {b} p +φ-mono₂ (olim f) {a} {b} p = + deriv-mono (commonStep (λ n → φ (f n))) + (commonStep-mono (λ n → φ (f n)) (λ n {x} {y} → φ-mono₂ (f n) {x} {y})) {a} {b} p + +---------------------------------------------------------------------- +-- Every Veblen level is inflationary. +---------------------------------------------------------------------- + +-- deriv is inflationary (no hypothesis on g — nextFix lands above). +deriv-infl : (g : Ord → Ord) → ∀ β → β ≤′ deriv g β +deriv-infl g oz = ≤′-zero {deriv g oz} +deriv-infl g (osuc β) = + ≤′-trans {osuc β} {osuc (deriv g β)} {nextFix g (deriv g β)} + (osuc-mono-≤′ {β} {deriv g β} (deriv-infl g β)) (nextFix-above g (deriv g β)) +deriv-infl g (olim h) = + λ n → ≤′-lim {h n} (λ k → deriv g (h k)) n (deriv-infl g (h n)) + +φ-infl : ∀ α β → β ≤′ φ α β +φ-infl oz β = ω^^-infl β +φ-infl (osuc α) β = deriv-infl (φ α) β +φ-infl (olim f) β = deriv-infl (commonStep (λ n → φ (f n))) β + +---------------------------------------------------------------------- +-- φ_{α+1} enumerates the fixed points of φ_α. +-- +-- Every value `deriv g β` is a fixed point of `g` (for continuous / +-- monotone-inflationary g), generalising `nextFix-fixed-*` from the base +-- of the tower to the whole enumeration; instantiated at g = φ_α this is +-- the defining Veblen recurrence φ_α(φ_{α+1}(β)) ≃ φ_{α+1}(β). +---------------------------------------------------------------------- + +deriv-fixed-≤ : + (g : Ord → Ord) (gc : ∀ h → g (olim h) ≤′ olim (λ n → g (h n))) + (β : Ord) → g (deriv g β) ≤′ deriv g β +deriv-fixed-≤ g gc oz = nextFix-fixed-≤ g gc oz +deriv-fixed-≤ g gc (osuc β) = nextFix-fixed-≤ g gc (deriv g β) +deriv-fixed-≤ g gc (olim h) = + ≤′-trans {g (olim D)} {olim (λ n → g (D n))} {olim D} + (gc D) + (λ n → ≤′-trans {g (D n)} {D n} {olim D} + (deriv-fixed-≤ g gc (h n)) (f-in-lim′ D n)) + where D = λ k → deriv g (h k) + +deriv-fixed-≥ : + (g : Ord → Ord) (gm : ∀ {a b} → a ≤′ b → g a ≤′ g b) (gi : ∀ y → y ≤′ g y) + (β : Ord) → deriv g β ≤′ g (deriv g β) +deriv-fixed-≥ g gm gi oz = nextFix-fixed-≥ g gm gi oz +deriv-fixed-≥ g gm gi (osuc β) = nextFix-fixed-≥ g gm gi (deriv g β) +deriv-fixed-≥ g gm gi (olim h) = + λ n → ≤′-trans {D n} {g (D n)} {g (olim D)} + (deriv-fixed-≥ g gm gi (h n)) (gm {D n} {olim D} (f-in-lim′ D n)) + where D = λ k → deriv g (h k) + +-- The Veblen recurrence: φ_{α+1}(β) is a fixed point of φ_α (bi-`≤′`). +φ-level-fixed-≤ : ∀ α β → φ α (φ (osuc α) β) ≤′ φ (osuc α) β +φ-level-fixed-≤ α β = deriv-fixed-≤ (φ α) (λ h → ≡→≤′ (φ-cont α h)) β + +φ-level-fixed-≥ : ∀ α β → φ (osuc α) β ≤′ φ α (φ (osuc α) β) +φ-level-fixed-≥ α β = + deriv-fixed-≥ (φ α) (λ {a} {b} → φ-mono₂ α {a} {b}) (φ-infl α) β diff --git a/proofs/agda/Smoke.agda b/proofs/agda/Smoke.agda index 3448f64..ea8e710 100644 --- a/proofs/agda/Smoke.agda +++ b/proofs/agda/Smoke.agda @@ -1288,6 +1288,27 @@ open import Ordinal.Brouwer.VeblenBinary using ; φ-diagonal-step -- φ_{Γ-tower n}(0) ≤′ Γ₀ ) +-- Binary Veblen rung 5 (2026-06-20, own block per CLAUDE.md Working +-- rules): EVERY Veblen level φ_α is a normal function, and φ_{α+1} +-- enumerates the fixed points of φ_α. `φ-mono₂` (every level monotone in +-- its argument) + `φ-infl` (every level inflationary) complete the +-- normal-function trio with `VeblenBinary.φ-cont`; `φ-level-fixed-{≤,≥}` +-- is the defining Veblen recurrence φ_α(φ_{α+1}(β)) ≃ φ_{α+1}(β). Generic +-- engine lemmas (`deriv-mono`/`deriv-infl`/`deriv-fixed-*`) proved once and +-- instantiated. Backbone for "Γ₀ is the LEAST diagonal fixed point" (next +-- slice); order-type fidelity ψ₀(Ω_ω) REMAINS OPEN (D-2026-06-14). +open import Ordinal.Brouwer.VeblenBinaryNormal using + ( φ-mono₂ -- every φ_α monotone in its argument + ; φ-infl -- every φ_α inflationary + ; deriv-mono -- generic: deriv g monotone (g monotone) + ; deriv-infl -- generic: deriv g inflationary + ; nextFix-mono -- generic: nextFix g monotone (g monotone) + ; deriv-fixed-≤ -- generic: deriv g β is a fixed point of g + ; deriv-fixed-≥ + ; φ-level-fixed-≤ -- φ_α (φ_{α+1} β) ≃ φ_{α+1} β (the Veblen recurrence) + ; φ-level-fixed-≥ + ) + -- Recommended rank function for unbudgeted `wf-<ᵇʳᶠ_` per Echidna's -- design search; transport theorem deferred until Phase 1.3 lemmas land. open import Ordinal.Buchholz.RankBrouwer using