From bf004386836f9693d4b663fb0d7494dc911fb713 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 20 Jun 2026 00:46:28 +0000 Subject: [PATCH] =?UTF-8?q?proof(ordinal):=20first-argument=20monotonicity?= =?UTF-8?q?;=20=CE=93=E2=82=80=20=E2=89=A4=E2=80=B2=20=CF=86=5F=CE=93?= =?UTF-8?q?=E2=82=80(0)=20(BH=20climb=20rung=206)?= 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 + VeblenBinaryNormal (every level a normal function; the Veblen recurrence; the generic fixed-point engine). The diagonal Γ₀ was DEFINED in rung 4 with only ≤′-upper-bound sanity. Showing it is a FIXED POINT of the diagonal D(α) = φ_α(0) needs monotonicity of φ in its FIRST argument. New module proofs/agda/Ordinal/Brouwer/VeblenBinaryMono.agda (--safe --without-K, zero postulates): * commonStep-absorb — a fixed point of commonStep F is a fixed point of every family member (one step, via the supremum embedding). * commonStep-cont — commonStep F is continuous (the ≤′ form deriv-fixed-≤ wants) when every member is. * φ-mono₁-step — adjacent levels ordered: φ_α x ≤′ φ_{α+1} x. (φ_{α+1} x is a fixed point of φ_α by the Veblen recurrence, so φ_α x ≤′ φ_α (φ_{α+1} x) = φ_{α+1} x.) * φ-mono₁-into-lim — a level below a limit is dominated by the limit level: φ_{h m} x ≤′ φ_{olim h} x. (φ_{olim h} x is a fixed point of commonStep (n ↦ φ_{h n}), hence of each φ_{h m}.) * Γ₀-prefixed — Γ₀ ≤′ φ_Γ₀(0): Γ₀ is a pre-fixed point of the diagonal (each successor approximant Γ-tower (suc m) = φ_{Γ-tower m}(0) is ≤′ φ_Γ₀(0) by φ-mono₁-into-lim, so their sup Γ₀ is too). Honest scope: this closes only the ≤′ direction Γ₀ ≤′ φ_Γ₀(0). 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 collapsing layer; order-type fidelity REMAINS OPEN (D-2026-06-14). No postulate is closed. Wiring: All.agda import; Smoke.agda pin block (5 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/VeblenBinaryMono.agda | 127 ++++++++++++++++++ proofs/agda/Smoke.agda | 17 +++ 3 files changed, 145 insertions(+) create mode 100644 proofs/agda/Ordinal/Brouwer/VeblenBinaryMono.agda diff --git a/proofs/agda/All.agda b/proofs/agda/All.agda index 49f2a98..9fd5313 100644 --- a/proofs/agda/All.agda +++ b/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 diff --git a/proofs/agda/Ordinal/Brouwer/VeblenBinaryMono.agda b/proofs/agda/Ordinal/Brouwer/VeblenBinaryMono.agda new file mode 100644 index 0000000..a194ac1 --- /dev/null +++ b/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 + +-- 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 diff --git a/proofs/agda/Smoke.agda b/proofs/agda/Smoke.agda index ea8e710..9f1861c 100644 --- a/proofs/agda/Smoke.agda +++ b/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