proof(ordinal): ε₀ is an ε-number — ω^^ ε₀ ≃ ε₀ (BH climb rung 2)

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

Author: claude

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 = ω^^-ε₀-≤ , ε₀-≤-ω^^-ε₀

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