Binary Veblen φ_α(β) + the diagonal Γ₀ (BH climb rung 4)

proofs/agda/All.agda

@@ -122,6 +122,7 @@ open import Ordinal.Brouwer.OmegaPow
 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.StrictLeftMonoRefuted
 open import Ordinal.Brouwer.AdditivePrincipalGenericRefuted
 open import Ordinal.Buchholz.Syntax

proofs/agda/Ordinal/Brouwer/VeblenBinary.agda

@@ -0,0 +1,217 @@
+{-# OPTIONS --safe --without-K #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+-- Binary Veblen φ_α(β) + the diagonal Γ₀ over Brouwer ordinals — RUNG 4
+-- of the target-side climb toward ψ₀(Ω_ω) (BH order-type fidelity, open
+-- problem D-2026-06-14).  Builds on `OrdinalExp` (ω^^ = φ₀),
+-- `VeblenPhi` / `VeblenPhiNormal` (φ₁ = the ε-number enumeration, now a
+-- normal function).  2026-06-20.
+--
+-- ## The construction (the load-bearing tractability move)
+--
+-- The two-argument Veblen function is defined by STRUCTURAL RECURSION ON
+-- THE FIRST ARGUMENT, returning a function `Ord → Ord`:
+--
+--   φ oz       = ω^^_                                   (φ₀ = ω-exponentiation)
+--   φ (osuc α) = deriv (φ α)                            (enumerate fixed points of φ_α)
+--   φ (olim f) = deriv (commonStep (n ↦ φ (f n)))       (common fixed points)
+--
+-- The SECOND-argument recursion lives entirely inside the generic
+-- fixed-point enumerator `deriv` (independent of φ), so φ's own recursion
+-- is purely first-argument-structural and Agda accepts its termination
+-- WITHOUT a `TERMINATING` pragma.  This is the move that makes binary
+-- Veblen tractable here:
+--
+--   * `deriv g` enumerates the fixed points of a (continuous) `g`, by
+--     recursion on its own argument — `deriv g (osuc β) = nextFix g
+--     (deriv g β)`, `deriv g (olim h) = olim (deriv g ∘ h)`;
+--   * `nextFix g x = olim (g-tower g (osuc x))` is the least fixed point
+--     of `g` strictly above `x` (sup of the `g`-iteration tower from
+--     `osuc x`) — the exact generalisation of `next-ε` from `VeblenPhi`;
+--   * `commonStep F x = olim (n ↦ F n x)` packages a countable family of
+--     normal functions into one whose fixed points are the COMMON fixed
+--     points of the family — the limit case.
+--
+-- Γ₀ (the Feferman–Schütte ordinal) is the diagonal:
+--   Γ₀ = sup { 0, φ_0(0), φ_{φ_0(0)}(0), … } = olim Γ-tower.
+--
+-- ## What is proved here
+--
+--   * the recurrences (`φ-oz`, `φ-osuc`, `φ-olim`) — definitional;
+--   * φ is CONTINUOUS in its second argument (`φ-cont`) — a normal-
+--     function property, definitional from `deriv`'s `olim` clause;
+--   * the generic fixed-point engine is CORRECT: for continuous monotone
+--     inflationary `g`, `nextFix g x` is a fixed point of `g` (bi-`≤′`,
+--     `nextFix-fixed-≤` / `nextFix-fixed-≥`) and lies strictly above `x`
+--     (`nextFix-above`);
+--   * the engine SUBSUMES the ε-number story: instantiated at ω^^ it
+--     reproves `ω^^ (nextFix ω^^ x) ≃ nextFix ω^^ x` (`ω^^-nextFix-fixed-{≤,≥}`);
+--   * Γ₀ is defined, positive (`Γ₀-pos`), an upper bound of its diagonal
+--     approximants (`Γ-tower-below-Γ₀`, `φ-diagonal-step`).
+--
+-- ## Honest scope (rung 4 of a LONG climb — do not overclaim)
+--
+-- Γ₀ is DEFINED and given basic properties; the full theorem that Γ₀ is
+-- the LEAST fixed point of the diagonal α ↦ φ_α(0) (the proper
+-- characterisation of the Feferman–Schütte ordinal) is NOT proved here —
+-- it needs the common-fixed-point correctness of `commonStep` plus
+-- monotonicity/inflationarity of every φ level, and is the next slice.
+-- ψ₀(Ω_ω) sits FAR above Γ₀ and additionally needs the ordinal-collapsing
+-- layer; order-type fidelity (ψ₀(Ω_ω)) therefore REMAINS OPEN
+-- (D-2026-06-14).  This slice neither characterises Γ₀ as least nor plugs
+-- `Fidelity.AtHeight`, and closes NO postulate.  bi-`≤′` (not `≡`) is used
+-- for fixed-point facts (Brouwer `olim`s of different ℕ-indexings of one
+-- supremum are not definitionally equal).
+
+module Ordinal.Brouwer.VeblenBinary where
+
+open import Data.Nat.Base using (ℕ; zero; suc)
+open import Data.Product.Base using (Σ; _,_)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+
+open import Ordinal.Brouwer using (Ord; oz; osuc; olim)
+open import Ordinal.Brouwer.Phase13
+  using (_≤′_; _<′_; ≤′-refl; ≤′-trans; f-in-lim′)
+open import Ordinal.Brouwer.OrdinalExp using (ω^^_; ω^^-infl)
+open import Ordinal.Brouwer.VeblenPhiNormal using (ω^^-mono-≤′)
+
+----------------------------------------------------------------------
+-- The generic fixed-point engine (independent of φ).
+----------------------------------------------------------------------
+
+-- Iterate g from a base, ℕ-many times.
+g-tower : (Ord → Ord) → Ord → ℕ → Ord
+g-tower g x zero    = x
+g-tower g x (suc n) = g (g-tower g x n)
+
+-- The least fixed point of g strictly above x: the supremum of the
+-- g-iteration tower started at `osuc x`.  Generalises `VeblenPhi.next-ε`.
+nextFix : (Ord → Ord) → Ord → Ord
+nextFix g x = olim (g-tower g (osuc x))
+
+-- Enumerate the fixed points of g.  Recursion on the SECOND argument,
+-- with g fixed; generalises `VeblenPhi.φ₁`.
+deriv : (Ord → Ord) → Ord → Ord
+deriv g oz       = nextFix g oz
+deriv g (osuc β) = nextFix g (deriv g β)
+deriv g (olim h) = olim (λ n → deriv g (h n))
+
+-- Package a countable family of normal functions into one whose fixed
+-- points are the COMMON fixed points of the family.
+commonStep : (ℕ → (Ord → Ord)) → Ord → Ord
+commonStep F x = olim (λ n → F n x)
+
+----------------------------------------------------------------------
+-- Binary Veblen function.  Structural recursion on the FIRST argument.
+----------------------------------------------------------------------
+
+φ : Ord → Ord → Ord
+φ oz       = ω^^_
+φ (osuc α) = deriv (φ α)
+φ (olim f) = deriv (commonStep (λ n → φ (f n)))
+
+-- The recurrences (definitional).
+φ-oz : φ oz ≡ ω^^_
+φ-oz = refl
+
+φ-osuc : ∀ α → φ (osuc α) ≡ deriv (φ α)
+φ-osuc _ = refl
+
+φ-olim : ∀ f → φ (olim f) ≡ deriv (commonStep (λ n → φ (f n)))
+φ-olim _ = refl
+
+-- φ is CONTINUOUS in its second argument: it commutes with `olim`.  A
+-- defining property of a normal function, here definitional because every
+-- branch (ω^^ / deriv) commutes with `olim` by its own `olim` clause.
+φ-cont : ∀ α h → φ α (olim h) ≡ olim (λ n → φ α (h n))
+φ-cont oz       h = refl
+φ-cont (osuc α) h = refl
+φ-cont (olim f) h = refl
+
+----------------------------------------------------------------------
+-- Correctness of the fixed-point engine (generic, then at ω^^).
+----------------------------------------------------------------------
+
+-- `nextFix g x` lies strictly above x (tower index 0 = osuc x).
+nextFix-above : ∀ g x → osuc x ≤′ nextFix g x
+nextFix-above g x = 0 , ≤′-refl {x}
+
+-- One step of the tower is `g` of the previous (definitional); recorded
+-- for readability.
+g-tower-suc : ∀ g x n → g (g-tower g x n) ≡ g-tower g x (suc n)
+g-tower-suc g x n = refl
+
+-- `g (nextFix g x) ≤′ nextFix g x` for continuous g.  The supremum of the
+-- tower SHIFTED by one (= g applied through the limit) is below the
+-- supremum of the tower.
+nextFix-fixed-≤ :
+  (g : Ord → Ord)
+  (g-cont : ∀ h → g (olim h) ≤′ olim (λ n → g (h n)))
+  (x : Ord) →
+  g (nextFix g x) ≤′ nextFix g x
+nextFix-fixed-≤ g g-cont x =
+  ≤′-trans {g (olim T)} {olim (λ n → g (T n))} {olim T}
+    (g-cont T) (λ n → f-in-lim′ T (suc n))
+  where T = g-tower g (osuc x)
+
+-- `nextFix g x ≤′ g (nextFix g x)` for monotone inflationary g.  Each
+-- tower approximant is below `g (olim T)`: index 0 via inflationarity,
+-- successors via monotonicity.
+nextFix-fixed-≥ :
+  (g : Ord → Ord)
+  (g-mono : ∀ {a b} → a ≤′ b → g a ≤′ g b)
+  (g-infl : ∀ y → y ≤′ g y)
+  (x : Ord) →
+  nextFix g x ≤′ g (nextFix g x)
+nextFix-fixed-≥ g g-mono g-infl x = go
+  where
+  T = g-tower g (osuc x)
+  go : ∀ n → T n ≤′ g (olim T)
+  go zero    =
+    ≤′-trans {osuc x} {olim T} {g (olim T)} (f-in-lim′ T 0) (g-infl (olim T))
+  go (suc m) = g-mono {T m} {olim T} (f-in-lim′ T m)
+
+----------------------------------------------------------------------
+-- The engine subsumes the ε-number story: instantiate at g = ω^^.
+-- ω^^ is continuous by definition (its `olim` clause), monotone
+-- (`ω^^-mono-≤′`), and inflationary (`ω^^-infl`).  So `nextFix ω^^ x` is
+-- a genuine ε-number (fixed point of ω-exponentiation), recovered from the
+-- generic engine — exactly the role `next-ε` plays in `VeblenPhi`.
+----------------------------------------------------------------------
+
+ω^^-nextFix-fixed-≤ : ∀ x → ω^^ (nextFix ω^^_ x) ≤′ nextFix ω^^_ x
+ω^^-nextFix-fixed-≤ =
+  nextFix-fixed-≤ ω^^_ (λ h → ≤′-refl {olim (λ n → ω^^ (h n))})
+
+ω^^-nextFix-fixed-≥ : ∀ x → nextFix ω^^_ x ≤′ ω^^ (nextFix ω^^_ x)
+ω^^-nextFix-fixed-≥ =
+  nextFix-fixed-≥ ω^^_ (λ {a} {b} → ω^^-mono-≤′ {a} {b}) ω^^-infl
+
+----------------------------------------------------------------------
+-- Γ₀ — the diagonal (Feferman–Schütte ordinal).
+----------------------------------------------------------------------
+
+-- The diagonal tower:  0, φ_0(0), φ_{φ_0(0)}(0), φ_{φ_{φ_0(0)}(0)}(0), …
+Γ-tower : ℕ → Ord
+Γ-tower zero    = oz
+Γ-tower (suc n) = φ (Γ-tower n) oz
+
+Γ₀ : Ord
+Γ₀ = olim Γ-tower
+
+-- Γ₀ is positive: the first diagonal step is φ_0(0) = ω^^ 0 = 1.
+Γ₀-pos : oz <′ Γ₀
+Γ₀-pos = 1 , ≤′-refl {oz}
+
+-- Every diagonal approximant is below Γ₀ (it is their supremum).
+Γ-tower-below-Γ₀ : ∀ n → Γ-tower n ≤′ Γ₀
+Γ-tower-below-Γ₀ n = f-in-lim′ Γ-tower n
+
+-- The diagonal map applied to an approximant stays below Γ₀:
+-- φ_{Γ-tower n}(0) = Γ-tower (suc n) ≤′ Γ₀.  Γ₀ is closed under the
+-- diagonal on its own approximants (the constructive seed of "Γ₀ is a
+-- fixed point of α ↦ φ_α(0)"; the full bi-`≤′` fixed point is the next
+-- slice — see the honest-scope note in the module header).
+φ-diagonal-step : ∀ n → φ (Γ-tower n) oz ≤′ Γ₀
+φ-diagonal-step n = f-in-lim′ Γ-tower (suc n)

proofs/agda/Smoke.agda

@@ -1261,6 +1261,33 @@ open import Ordinal.Brouwer.VeblenPhiNormal using
   ; φ₁-continuous                   -- φ₁ continuous at limits (normal-function half 2)
   )
 
+-- Binary Veblen φ_α(β) + the diagonal Γ₀ (2026-06-20, own block per
+-- CLAUDE.md Working rules): the two-argument Veblen function by structural
+-- recursion on the FIRST argument (returning Ord → Ord; second-argument
+-- recursion lives in the generic fixed-point enumerator `deriv`, so no
+-- TERMINATING pragma).  `φ` extends ω^^ = φ₀; `φ-cont` is continuity in
+-- the 2nd argument; `nextFix-fixed-{≤,≥}` is the generic fixed-point
+-- correctness (instantiated at ω^^ as `ω^^-nextFix-fixed-{≤,≥}`); `Γ₀` is
+-- the Feferman–Schütte ordinal (DEFINED + basic properties; "Γ₀ is the
+-- LEAST diagonal fixed point" is the next slice).  ψ₀(Ω_ω) sits far above
+-- Γ₀; order-type fidelity REMAINS OPEN (D-2026-06-14).
+open import Ordinal.Brouwer.VeblenBinary using
+  ( φ                               -- binary Veblen φ_α(β)
+  ; deriv                           -- generic fixed-point enumerator
+  ; nextFix                         -- least fixed point of g strictly above x
+  ; φ-oz                            -- φ₀ = ω^^
+  ; φ-cont                          -- φ continuous in the 2nd argument
+  ; nextFix-above                   -- nextFix g x is strictly above x
+  ; nextFix-fixed-≤                 -- engine correctness: g (nextFix g x) ≤′ nextFix g x
+  ; nextFix-fixed-≥                 -- engine correctness: nextFix g x ≤′ g (nextFix g x)
+  ; ω^^-nextFix-fixed-≤             -- engine subsumes ε-numbers (at ω^^)
+  ; ω^^-nextFix-fixed-≥
+  ; Γ₀                              -- the Feferman–Schütte ordinal (diagonal)
+  ; Γ₀-pos
+  ; Γ-tower-below-Γ₀
+  ; φ-diagonal-step                 -- φ_{Γ-tower n}(0) ≤′ Γ₀
+  )
+
 -- 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