First-argument monotonicity; Γ₀ ≤′ φ_Γ₀(0) (BH climb rung 6)

proofs/agda/All.agda

@@ -124,6 +124,7 @@ 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.VeblenBinaryMono -- first-arg monotonicity; Γ₀ ≤′ φ_Γ₀(0) (diagonal pre-fixed point)
 open import Ordinal.Brouwer.StrictLeftMonoRefuted
 open import Ordinal.Brouwer.AdditivePrincipalGenericRefuted
 open import Ordinal.Buchholz.Syntax

proofs/agda/Ordinal/Brouwer/VeblenBinaryMono.agda

@@ -0,0 +1,127 @@
+{-# 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 — RUNG 6: first-argument monotonicity (toward Γ₀ as a
+-- diagonal fixed point).  Target-side climb toward ψ₀(Ω_ω) (BH order-type
+-- fidelity, open problem D-2026-06-14).  Builds on `VeblenBinary` and
+-- `VeblenBinaryNormal` (every level a normal function; the Veblen
+-- recurrence; the generic fixed-point engine).  2026-06-20.
+--
+-- ## What this slice adds
+--
+-- The diagonal Γ₀ = φ_0(0), φ_{φ_0(0)}(0), … was DEFINED in `VeblenBinary`
+-- with only `≤′`-upper-bound sanity.  Showing it is a FIXED POINT of the
+-- diagonal map D(α) = φ_α(0) needs monotonicity of φ in its FIRST
+-- argument.  This slice proves the two forms of first-argument
+-- monotonicity that the diagonal needs, and uses them to close ONE
+-- direction of the Γ₀ fixed point:
+--
+--   * `φ-mono₁-step`     — adjacent levels are ordered: φ_α x ≤′ φ_{α+1} x.
+--   * `φ-mono₁-into-lim` — a level below a limit is dominated by the limit
+--                          level: φ_{h m} x ≤′ φ_{olim h} x.
+--   * `Γ₀-prefixed`      — Γ₀ ≤′ φ_Γ₀(0): Γ₀ is a pre-fixed point of the
+--                          diagonal (φ_Γ₀(0) is at least Γ₀).
+--
+-- Both monotonicity results rest on the SAME idea, now mechanised: the
+-- value φ_β(x) is a fixed point of every lower level φ_α (α below β), so
+--     φ_α x ≤′ φ_α (φ_β x)            [φ_α monotone, x ≤′ φ_β x]
+--          = φ_β x                    [φ_β x is a fixed point of φ_α].
+-- For the successor case the absorbing fixed point is `φ-level-fixed`
+-- (rung 5); for the limit case it is supplied by `commonStep`
+-- correctness: a fixed point of `commonStep F` is a common fixed point of
+-- every family member (`commonStep-absorb`), and `deriv` lands on such a
+-- fixed point (`deriv-fixed-≤` + `commonStep-cont`).
+--
+-- ## Honest scope (still a LONG climb)
+--
+-- This closes the `≤′` direction `Γ₀ ≤′ φ_Γ₀(0)` only.  The reverse
+-- `φ_Γ₀(0) ≤′ Γ₀` (closure from above) and full "Γ₀ is the LEAST diagonal
+-- fixed point" need general first-argument monotonicity / common-fixed-
+-- point-from-above and remain OPEN — the next slice.  ψ₀(Ω_ω) sits far
+-- above Γ₀ behind the ordinal-collapsing layer; order-type fidelity
+-- REMAINS OPEN (D-2026-06-14).  No postulate is closed.
+
+module Ordinal.Brouwer.VeblenBinaryMono where
+
+open import Data.Nat.Base using (ℕ; zero; suc)
+open import Relation.Binary.PropositionalEquality using (refl)
+
+open import Ordinal.Brouwer using (Ord; oz; osuc; olim)
+open import Ordinal.Brouwer.Phase13
+  using (_≤′_; ≤′-trans; ≤′-zero; f-in-lim′)
+open import Ordinal.Brouwer.VeblenBinary
+  using (φ; deriv; commonStep; Γ₀; Γ-tower; φ-cont)
+open import Ordinal.Brouwer.VeblenBinaryNormal
+  using (≡→≤′; φ-mono₂; φ-infl; deriv-fixed-≤; φ-level-fixed-≤)
+
+----------------------------------------------------------------------
+-- commonStep correctness.
+----------------------------------------------------------------------
+
+-- A pre-fixed point of `commonStep F` is a pre-fixed point of every
+-- family member: F m y ≤′ commonStep F y ≤′ y.  One step, via the
+-- supremum embedding.
+commonStep-absorb :
+  (F : ℕ → Ord → Ord) (m : ℕ) {y : Ord} →
+  commonStep F y ≤′ y → F m y ≤′ y
+commonStep-absorb F m {y} p =
+  ≤′-trans {F m y} {commonStep F y} {y} (f-in-lim′ (λ n → F n y) m) p
+
+-- `commonStep F` is continuous (in the `≤′` form `deriv-fixed-≤` wants)
+-- when every family member is.
+commonStep-cont :
+  (F : ℕ → Ord → Ord)
+  (Fc : ∀ n k → F n (olim k) ≤′ olim (λ m → F n (k m))) →
+  ∀ k → commonStep F (olim k) ≤′ olim (λ m → commonStep F (k m))
+commonStep-cont F Fc k = λ n →
+  ≤′-trans {F n (olim k)} {olim (λ m → F n (k m))} {olim (λ m → commonStep F (k m))}
+    (Fc n k)
+    (λ m → ≤′-trans {F n (k m)} {commonStep F (k m)} {olim (λ m′ → commonStep F (k m′))}
+             (f-in-lim′ (λ n′ → F n′ (k m)) n)
+             (f-in-lim′ (λ m′ → commonStep F (k m′)) m))
+
+----------------------------------------------------------------------
+-- First-argument monotonicity.
+----------------------------------------------------------------------
+
+-- Adjacent levels are ordered.  φ_{α+1} x is a fixed point of φ_α
+-- (`φ-level-fixed-≤`), so φ_α x ≤′ φ_α (φ_{α+1} x) = φ_{α+1} x.
+φ-mono₁-step : ∀ α x → φ α x ≤′ φ (osuc α) x
+φ-mono₁-step α x =
+  ≤′-trans {φ α x} {φ α (φ (osuc α) x)} {φ (osuc α) x}
+    (φ-mono₂ α {x} {φ (osuc α) x} (φ-infl (osuc α) x))
+    (φ-level-fixed-≤ α x)
+
+-- A level below a limit is dominated by the limit level.  φ_{olim h} x is
+-- a fixed point of `commonStep (n ↦ φ_{h n})`, hence (by
+-- `commonStep-absorb`) a fixed point of each φ_{h m}; so
+-- φ_{h m} x ≤′ φ_{h m} (φ_{olim h} x) = φ_{olim h} x.
+φ-mono₁-into-lim : ∀ h m x → φ (h m) x ≤′ φ (olim h) x
+φ-mono₁-into-lim h m x =
+  ≤′-trans {φ (h m) x} {φ (h m) (φ (olim h) x)} {φ (olim h) x}
+    (φ-mono₂ (h m) {x} {φ (olim h) x} (φ-infl (olim h) x))
+    (commonStep-absorb F m {φ (olim h) x} prefixed)
+  where
+  F = λ n → φ (h n)
+  -- φ (olim h) x = deriv (commonStep F) x, and `deriv` lands on a fixed
+  -- point of `commonStep F` (the ≤′ direction).
+  prefixed : commonStep F (φ (olim h) x) ≤′ φ (olim h) x
+  prefixed =
+    deriv-fixed-≤ (commonStep F)
+      (commonStep-cont F (λ n k → ≡→≤′ (φ-cont (h n) k))) x
+
+----------------------------------------------------------------------
+-- Γ₀ is a pre-fixed point of the diagonal D(α) = φ_α(0).
+--
+-- Γ₀ = olim Γ-tower, and each successor approximant
+-- Γ-tower (suc m) = φ_{Γ-tower m}(0) is ≤′ φ_{olim Γ-tower}(0) = φ_Γ₀(0)
+-- by `φ-mono₁-into-lim`.  So the supremum Γ₀ is ≤′ φ_Γ₀(0).
+----------------------------------------------------------------------
+
+Γ₀-prefixed : Γ₀ ≤′ φ Γ₀ oz
+Γ₀-prefixed = go
+  where
+  go : ∀ n → Γ-tower n ≤′ φ Γ₀ oz
+  go zero    = ≤′-zero {φ Γ₀ oz}
+  go (suc m) = φ-mono₁-into-lim Γ-tower m oz

proofs/agda/Smoke.agda

@@ -1309,6 +1309,23 @@ open import Ordinal.Brouwer.VeblenBinaryNormal using
   ; φ-level-fixed-≥
   )
 
+-- Binary Veblen rung 6 (2026-06-20, own block per CLAUDE.md Working
+-- rules): first-argument monotonicity toward Γ₀ as a diagonal fixed
+-- point.  `φ-mono₁-step` (adjacent levels ordered) + `φ-mono₁-into-lim`
+-- (a level below a limit is dominated by the limit level) rest on the
+-- Veblen recurrence + `commonStep` correctness (`commonStep-absorb` /
+-- `commonStep-cont`).  `Γ₀-prefixed` closes ONE direction of the diagonal
+-- fixed point: Γ₀ ≤′ φ_Γ₀(0).  The reverse direction + "Γ₀ is LEAST"
+-- remain the next slice; order-type fidelity ψ₀(Ω_ω) REMAINS OPEN
+-- (D-2026-06-14).
+open import Ordinal.Brouwer.VeblenBinaryMono using
+  ( commonStep-absorb               -- fixed point of commonStep F ⇒ fixed point of each F m
+  ; commonStep-cont                 -- commonStep F continuous when each member is
+  ; φ-mono₁-step                    -- φ_α x ≤′ φ_{α+1} x  (adjacent levels)
+  ; φ-mono₁-into-lim                -- φ_{h m} x ≤′ φ_{olim h} x  (level below a limit)
+  ; Γ₀-prefixed                     -- Γ₀ ≤′ φ_Γ₀(0): Γ₀ is a diagonal pre-fixed point
+  )
+
 -- 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