From 642760a639caa9fb5d026d29818946e2fbf6edd6 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 18 Jun 2026 01:12:09 +0000 Subject: [PATCH] =?UTF-8?q?proof(ordinal):=20ordinal=20exponentiation=20?= =?UTF-8?q?=CF=89^^=20+=20first=20=CE=B5-number=20=CE=B5=E2=82=80=20(BH=20?= =?UTF-8?q?climb=20rung=201)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add Brouwer ordinal exponentiation base ω (ω^^_ : Ord → Ord, generalising OmegaPow's finite ω^_ : ℕ → Ord to limit exponents) and the first ε-number ε₀ as a concrete Ord value. Rung 1 of the target-side climb toward ψ₀(Ω_ω) (BH order-type fidelity, D-2026-06-14). New module Ordinal.Brouwer.OrdinalExp (--safe --without-K, zero postulates): ω^^_, ω^^-pos (positivity, mirrors ω^_-pos), ε-tower, ε₀, ε₀-pos, ε-tower-below-ε₀ (approximant bound via f-in-lim′). Honest scope: ε₀ ≪ ψ₀(Ω_ω) — lands the exponentiation primitive every higher rung needs and pins ε₀ (= the collapse ψ₀(Ω₁)) as the first checkable milestone value. Does NOT plug Fidelity.AtHeight's height parameter, and does NOT prove ε₀ is an ε-number (ω^^ ε₀ ≡ ε₀) — follow-on rungs. Wired into All.agda + Smoke.agda; agda All.agda (191 modules) + guardrails + kernel-guard all pass. https://claude.ai/code/session_01GJatEm2TVFSTBEkKXmserJ --- proofs/agda/All.agda | 1 + proofs/agda/Ordinal/Brouwer/OrdinalExp.agda | 85 +++++++++++++++++++++ proofs/agda/Smoke.agda | 18 +++++ 3 files changed, 104 insertions(+) create mode 100644 proofs/agda/Ordinal/Brouwer/OrdinalExp.agda diff --git a/proofs/agda/All.agda b/proofs/agda/All.agda index 6ddd59c..0a411eb 100644 --- a/proofs/agda/All.agda +++ b/proofs/agda/All.agda @@ -118,6 +118,7 @@ open import Ordinal.Brouwer open import Ordinal.Brouwer.Arithmetic open import Ordinal.Brouwer.Phase13 open import Ordinal.Brouwer.OmegaPow +open import Ordinal.Brouwer.OrdinalExp open import Ordinal.Brouwer.StrictLeftMonoRefuted open import Ordinal.Brouwer.AdditivePrincipalGenericRefuted open import Ordinal.Buchholz.Syntax diff --git a/proofs/agda/Ordinal/Brouwer/OrdinalExp.agda b/proofs/agda/Ordinal/Brouwer/OrdinalExp.agda new file mode 100644 index 0000000..1fb0620 --- /dev/null +++ b/proofs/agda/Ordinal/Brouwer/OrdinalExp.agda @@ -0,0 +1,85 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell + +-- Ordinal exponentiation base ω + the first ε-number ε₀ — RUNG 1 of the +-- target-side Brouwer-ordinal climb toward ψ₀(Ω_ω) (the BH order-type +-- fidelity milestone, open problem D-2026-06-14). 2026-06-15. +-- +-- ## What this module IS +-- +-- * `ω^^_ : Ord → Ord` — ω raised to an ORDINAL power, generalising +-- `OmegaPow.ω^_ : ℕ → Ord` (finite exponent) to limit exponents. +-- * `ε₀ : Ord` — the first ε-number, sup{1, ω, ω^ω, ω^(ω^ω), …}, +-- built as the `olim` of the ω-exponentiation tower. +-- * Positivity (`ω^^-pos`, `ε₀-pos`) + the approximant bound +-- (`ε-tower-below-ε₀`), all postulate-free under `--safe --without-K`. +-- +-- ## Honest scope (rung 1 of a LONG climb — do not overclaim) +-- +-- ε₀ is the first named milestone above the existing `ω^_` / +-- `ω-rank-pow` arithmetic, and it is ENORMOUSLY below ψ₀(Ω_ω): the +-- fidelity height `bh-height = ψ₀(Ω_ω)` (the `Fidelity.AtHeight` +-- parameter) sits far above ε₀ ≪ Γ₀ ≪ … ≪ ψ₀(Ω_ω). This module does +-- NOT plug that parameter. It builds the ordinal-exponentiation +-- primitive every higher rung needs and pins ε₀ as the first checkable +-- 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. + +module Ordinal.Brouwer.OrdinalExp where + +open import Data.Nat.Base using (ℕ; zero; suc) +open import Data.Product.Base using (Σ; _,_) +open import Data.Unit.Base using (tt) +open import Relation.Binary.PropositionalEquality using (_≡_; refl) + +open import Ordinal.Brouwer using (Ord; oz; osuc; olim) +open import Ordinal.Brouwer.Phase13 using (_≤′_; _<′_; f-in-lim′) +open import Ordinal.Brouwer.OmegaPow using (_·ℕ_; oz<′oz⊕) + +---------------------------------------------------------------------- +-- Ordinal exponentiation base ω +---------------------------------------------------------------------- + +-- ω^^ α = ω to the ordinal power α. oz ↦ 1; successor ↦ a limit of +-- finite products (ω^(α+1) = sup_n (ω^α ·ℕ n)); limit ↦ pointwise sup. +-- Structural recursion on the Ord exponent. +ω^^_ : Ord → Ord +ω^^ oz = osuc oz +ω^^ (osuc α) = olim (λ n → (ω^^ α) ·ℕ n) +ω^^ (olim f) = olim (λ n → ω^^ (f n)) + +ω^^-zero : ω^^ oz ≡ osuc oz +ω^^-zero = refl + +-- ω^^ is strictly positive everywhere (mirrors OmegaPow.ω^_-pos). +ω^^-pos : ∀ α → oz <′ ω^^ α +ω^^-pos oz = tt +ω^^-pos (osuc α) = 1 , oz<′oz⊕ {ω^^ α} (ω^^-pos α) +ω^^-pos (olim f) = 0 , ω^^-pos (f 0) + +---------------------------------------------------------------------- +-- ε₀ — the first ε-number +---------------------------------------------------------------------- + +-- The ω-exponentiation tower 1, ω, ω^ω, ω^(ω^ω), … and its supremum. +ε-tower : ℕ → Ord +ε-tower zero = osuc oz +ε-tower (suc n) = ω^^ (ε-tower n) + +ε-tower-suc : ∀ n → ε-tower (suc n) ≡ ω^^ (ε-tower n) +ε-tower-suc _ = refl + +ε₀ : Ord +ε₀ = olim ε-tower + +-- ε₀ is positive, and every tower approximant sits at-or-below it. +ε₀-pos : oz <′ ε₀ +ε₀-pos = 0 , tt + +ε-tower-below-ε₀ : ∀ n → ε-tower n ≤′ ε₀ +ε-tower-below-ε₀ n = f-in-lim′ ε-tower n diff --git a/proofs/agda/Smoke.agda b/proofs/agda/Smoke.agda index 52c435f..00a316e 100644 --- a/proofs/agda/Smoke.agda +++ b/proofs/agda/Smoke.agda @@ -1164,6 +1164,24 @@ open import Ordinal.Brouwer.OmegaPow using ; additive-principal ) +-- Ordinal exponentiation + ε₀ (2026-06-15, own block per CLAUDE.md +-- Working rules): rung 1 of the target-side Brouwer climb toward +-- ψ₀(Ω_ω) (BH order-type fidelity, D-2026-06-14). `ω^^_` is ω to an +-- ORDINAL power (generalising OmegaPow.ω^_ : ℕ → Ord); `ε₀` is the +-- first ε-number. Honest scope: ε₀ ≪ ψ₀(Ω_ω) — this lands the +-- exponentiation primitive every higher rung needs and pins ε₀ as the +-- first checkable milestone value. +open import Ordinal.Brouwer.OrdinalExp using + ( ω^^_ + ; ω^^-zero + ; ω^^-pos + ; ε-tower + ; ε-tower-suc + ; ε₀ + ; ε₀-pos + ; ε-tower-below-ε₀ + ) + -- 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