From dc8b84e090db1ae347eb1682207b1d7cc3f14600 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 18 Jun 2026 06:23:04 +0000 Subject: [PATCH] =?UTF-8?q?proof(ordinal):=20=CE=B5=E2=82=80=20is=20an=20?= =?UTF-8?q?=CE=B5-number=20=E2=80=94=20=CF=89^^=20=CE=B5=E2=82=80=20?= =?UTF-8?q?=E2=89=83=20=CE=B5=E2=82=80=20(BH=20climb=20rung=202)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Prove the first ε-number ε₀ is a fixed point of ω-exponentiation, as _≤′_ in both directions (ω^^-ε₀-≤, ε₀-≤-ω^^-ε₀, packaged ε₀-ε-number) in Ordinal.Brouwer.OrdinalExp. bi-≤′ rather than ≡ because two Brouwer olims of different ℕ-indexings of the same supremum are not definitionally equal. No general inflationary lemma needed: ω^^ ε₀ is definitionally the olim of the tower shifted by one (ε-tower (suc n) = ω^^ (ε-tower n)), so each direction reduces to a one-step f-in-lim′ (+ ω^^-pos for the base index). The strict inflationary α <′ ω^^ α is deliberately NOT pursued — it is false exactly at the ε-numbers (ε₀ = ω^^ ε₀ is the counterexample). Honest scope unchanged: order-type fidelity (ψ₀(Ω_ω)) remains OPEN (D-2026-06-14); ε₀ ≪ Γ₀ ≪ … ≪ ψ₀(Ω_ω). Pinned in Smoke.agda. Verified: agda OrdinalExp + All.agda (193 modules) exit 0; check-guardrails + kernel-guard PASS; zero postulates. https://claude.ai/code/session_01GJatEm2TVFSTBEkKXmserJ --- proofs/agda/Ordinal/Brouwer/OrdinalExp.agda | 43 +++++++++++++++++++-- proofs/agda/Smoke.agda | 3 ++ 2 files changed, 42 insertions(+), 4 deletions(-) diff --git a/proofs/agda/Ordinal/Brouwer/OrdinalExp.agda b/proofs/agda/Ordinal/Brouwer/OrdinalExp.agda index 1fb0620..109cac4 100644 --- a/proofs/agda/Ordinal/Brouwer/OrdinalExp.agda +++ b/proofs/agda/Ordinal/Brouwer/OrdinalExp.agda @@ -26,14 +26,22 @@ -- value. (ε₀ is itself the collapse ψ₀(Ω₁) — the first nontrivial data -- point the eventual `denotation` ⟦·⟧ must reproduce.) -- --- This module does NOT prove ε₀ is an ε-number (`ω^^ ε₀ ≡ ε₀`); that --- fixpoint property and the inflationary `α <′ ω^^ α` are follow-on --- rungs. +-- RUNG 2 (2026-06-18): ε₀ IS an ε-number — `ω^^ ε₀ ≃ ε₀` as `_≤′_` in +-- BOTH directions (`ω^^-ε₀-≤`, `ε₀-≤-ω^^-ε₀`, packaged `ε₀-ε-number`). +-- bi-`≤′`, not `≡`, because two `olim`s of different ℕ-indexings of the +-- same supremum are not definitionally equal. No general inflationary +-- lemma is needed: `ω^^ ε₀` is definitionally the `olim` of the shifted +-- tower `n ↦ ε-tower (suc n)`, so each direction reduces to one-step +-- `f-in-lim′` (+ `ω^^-pos` for the base index). +-- +-- The *strict* inflationary `α <′ ω^^ α` is deliberately NOT pursued: it +-- is FALSE exactly at the ε-numbers (ε₀ = ω^^ ε₀ is the counterexample); +-- the non-strict `α ≤′ ω^^ α` holds but is not needed for the fixed point. module Ordinal.Brouwer.OrdinalExp where open import Data.Nat.Base using (ℕ; zero; suc) -open import Data.Product.Base using (Σ; _,_) +open import Data.Product.Base using (Σ; _,_; _×_) open import Data.Unit.Base using (tt) open import Relation.Binary.PropositionalEquality using (_≡_; refl) @@ -83,3 +91,30 @@ open import Ordinal.Brouwer.OmegaPow using (_·ℕ_; oz<′oz⊕) ε-tower-below-ε₀ : ∀ n → ε-tower n ≤′ ε₀ ε-tower-below-ε₀ n = f-in-lim′ ε-tower n + +---------------------------------------------------------------------- +-- ε₀ is an ε-number: a fixed point of ω-exponentiation (RUNG 2) +---------------------------------------------------------------------- + +-- `ω^^ ε₀ ≃ ε₀`, as `_≤′_` in both directions. `ω^^ ε₀ = ω^^ (olim +-- ε-tower)` reduces to `olim (n ↦ ω^^ (ε-tower n))`, and each +-- `ω^^ (ε-tower n)` is definitionally `ε-tower (suc n)` — i.e. `ω^^ ε₀` +-- is the supremum of the tower SHIFTED by one. A shifted supremum has +-- the same value, so both inequalities are one-step `f-in-lim′`s. + +-- Upper: every element of the shifted tower is below ε₀. +ω^^-ε₀-≤ : ω^^ ε₀ ≤′ ε₀ +ω^^-ε₀-≤ n = f-in-lim′ ε-tower (suc n) + +-- Lower: every tower element is below the shifted tower's supremum. +-- The base index ε-tower 0 = 1 sits below ε-tower 1 = ω^^ 1 by `ω^^-pos`; +-- every successor element ε-tower (suc m) = ω^^ (ε-tower m) IS the m-th +-- element of the shifted tower, so it is below by `f-in-lim′`. +ε₀-≤-ω^^-ε₀ : ε₀ ≤′ ω^^ ε₀ +ε₀-≤-ω^^-ε₀ zero = 0 , ω^^-pos (osuc oz) +ε₀-≤-ω^^-ε₀ (suc m) = f-in-lim′ (λ k → ω^^ (ε-tower k)) m + +-- ε₀ is a fixed point of ω-exponentiation (the defining property of an +-- ε-number), packaged as bi-`≤′`. +ε₀-ε-number : (ω^^ ε₀ ≤′ ε₀) × (ε₀ ≤′ ω^^ ε₀) +ε₀-ε-number = ω^^-ε₀-≤ , ε₀-≤-ω^^-ε₀ diff --git a/proofs/agda/Smoke.agda b/proofs/agda/Smoke.agda index 00a316e..b9abfbf 100644 --- a/proofs/agda/Smoke.agda +++ b/proofs/agda/Smoke.agda @@ -1180,6 +1180,9 @@ open import Ordinal.Brouwer.OrdinalExp using ; ε₀ ; ε₀-pos ; ε-tower-below-ε₀ + ; ω^^-ε₀-≤ + ; ε₀-≤-ω^^-ε₀ + ; ε₀-ε-number ) -- Recommended rank function for unbudgeted `wf-<ᵇʳᶠ_` per Echidna's