Skip to content

Commit 3f5f266

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
φ₁ is a normal function; next-ε β is the LEAST ε-number above β (BH climb rung 3, slice 3) (#244)
## What & why Target-side climb toward ψ₀(Ω_ω) (BH order-type fidelity, open problem `D-2026-06-14`). Slice 2 (`VeblenPhi`) proved every value of φ₁ **is** an ε-number and that `next-ε β` is *an* ε-number above β. This slice upgrades that to the two defining properties of an ε-number **enumeration**. ## New module `Ordinal/Brouwer/VeblenPhiNormal.agda` `--safe --without-K`, **zero postulates**, structural recursion (no `TERMINATING`): | Theorem | Statement | |---|---| | `ω^^-mono-≤′` | ω-exponentiation is monotone (`α ≤′ β → ω^^ α ≤′ ω^^ β`) — the one missing prerequisite; structural recursion on the `_≤′_` shape | | **`next-ε-least`** | **the headline:** `next-ε β` is the *least* ω^^-closed ordinal strictly above β (for any γ with `osuc β ≤′ γ` and `ω^^ γ ≤′ γ`, `next-ε β ≤′ γ`) | | `next-ε-mono` | `next-ε` is monotone | | `φ₁-mono` | φ₁ monotone | | `φ₁-lt-succ` | φ₁ strictly increasing at successors | | **`φ₁-strict-mono`** | φ₁ strictly monotone | | **`φ₁-continuous`** | φ₁ continuous at limits (definitional `refl`) | | `ε₀-least` | `ε₀ = φ₁ oz` is the least φ₁ value (the `oz` base case) | A **normal function** is precisely a strictly-monotone, continuous ordinal function — φ₁ is now mechanically one, the standard precondition for taking its fixed points (next Veblen level), the binary φ_α, and ultimately Γ₀. The `next-ε-least` proof is clean because the Brouwer `olim` LUB is *definitional*: `olim f ≤′ γ` reduces to `∀ n → f n ≤′ γ`, so it's tower-index induction using `ω^^-mono-≤′` + the ω^^-closure hypothesis. ## Honest scope Does **not** reach Γ₀; ψ₀(Ω_ω) sits far above even Γ₀ and additionally needs the ordinal-collapsing layer. **Order-type fidelity (ψ₀(Ω_ω)) REMAINS OPEN (`D-2026-06-14`)** — this slice neither reaches Γ₀ nor plugs `Fidelity.AtHeight`, and closes **no** postulate. ## Design note Every `≤′-lim` / `ω^^-mono-≤′` / `·ℕ-mono-≤-left` call pins its implicit *source* explicitly — `_≤′_` is a reducing relation, so the unifier cannot infer it from the goal (the lesson the φ₁ slice already recorded). ## Wiring `All.agda` import; `Smoke.agda` pin block (8 headlines). ## Verification - `agda proofs/agda/All.agda` → exit 0 - `agda proofs/agda/Smoke.agda` → exit 0 - `scripts/kernel-guard.sh` → **PASS** - zero postulates; `--safe --without-K` throughout 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01Rw1RpYXU5Q7rzy2bVofVeB --- _Generated by [Claude Code](https://claude.ai/code/session_01Rw1RpYXU5Q7rzy2bVofVeB)_ Co-authored-by: Claude <noreply@anthropic.com>
1 parent de02dd9 commit 3f5f266

3 files changed

Lines changed: 182 additions & 0 deletions

File tree

‎proofs/agda/All.agda‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -121,6 +121,7 @@ open import Ordinal.Brouwer.Phase13
121121
open import Ordinal.Brouwer.OmegaPow
122122
open import Ordinal.Brouwer.OrdinalExp
123123
open import Ordinal.Brouwer.VeblenPhi
124+
open import Ordinal.Brouwer.VeblenPhiNormal -- φ₁ a normal function; next-ε β LEAST ε-number above β
124125
open import Ordinal.Brouwer.StrictLeftMonoRefuted
125126
open import Ordinal.Brouwer.AdditivePrincipalGenericRefuted
126127
open import Ordinal.Buchholz.Syntax

‎proofs/agda/Ordinal/Brouwer/VeblenPhiNormal.agda‎

Lines changed: 161 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,161 @@
1+
{-# OPTIONS --safe --without-K #-}
2+
-- SPDX-License-Identifier: MPL-2.0
3+
-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
4+
5+
-- Veblen φ-hierarchy over Brouwer ordinals — RUNG 3 (slice 3): φ₁ is a
6+
-- NORMAL FUNCTION, and `next-ε β` is the LEAST ε-number above β. Target-
7+
-- side climb toward ψ₀(Ω_ω) (BH order-type fidelity, open problem
8+
-- D-2026-06-14). Builds directly on `VeblenPhi` (φ₁ / next-ε defined and
9+
-- proved ε-valued) and `OrdinalExp` (ω^^). 2026-06-19.
10+
--
11+
-- ## What this slice adds
12+
--
13+
-- The previous slice (`VeblenPhi`) proved that every value of φ₁ IS an
14+
-- ε-number (`φ₁-ε-number`) and that `next-ε β` is AN ε-number strictly
15+
-- above β. This slice upgrades that to the two defining properties of an
16+
-- ε-number ENUMERATION:
17+
--
18+
-- * `next-ε-least` — `next-ε β` is the LEAST ω^^-closed ordinal strictly
19+
-- above β. This is what makes `next-ε` the genuine "next ε-number"
20+
-- operator (not merely *an* ε-number above β). Definitional, because
21+
-- `olim f ≤′ γ` reduces to `∀ n → f n ≤′ γ` (olim is the least upper
22+
-- bound), so the proof is induction on the ω^^-tower index using
23+
-- ω^^-monotonicity + the ω^^-closure hypothesis on γ.
24+
-- * `φ₁` is a NORMAL FUNCTION:
25+
-- - `φ₁-mono` — monotone (α ≤′ β → φ₁ α ≤′ φ₁ β)
26+
-- - `φ₁-strict-mono` — strictly monotone (α <′ β → φ₁ α <′ φ₁ β)
27+
-- - `φ₁-continuous` — continuous at limits (definitional, `refl`)
28+
-- A normal function is precisely a strictly-monotone, continuous
29+
-- ordinal function; φ₁ is now mechanically one.
30+
--
31+
-- The one prerequisite the previous slices left open is `ω^^-mono-≤′`
32+
-- (monotonicity of ω-exponentiation), proved here by structural recursion
33+
-- on the `_≤′_` shape; it is a pure ω^^ fact and a natural candidate to
34+
-- migrate into `OrdinalExp` when the binary Veblen rung needs it.
35+
--
36+
-- ## Honest scope (still rung 3 of a LONG climb — do not overclaim)
37+
--
38+
-- φ₁ being a normal function is the standard precondition for taking its
39+
-- fixed points (the next Veblen level) and ultimately the binary φ_α and
40+
-- its diagonal → Γ₀. It does NOT reach Γ₀, and ψ₀(Ω_ω) sits far above
41+
-- even Γ₀ and additionally needs the ordinal-collapsing layer. Order-type
42+
-- fidelity (ψ₀(Ω_ω)) REMAINS OPEN (D-2026-06-14); this slice neither
43+
-- reaches Γ₀ nor plugs `Fidelity.AtHeight`. bi-`≤′` (not `≡`) is used for
44+
-- the fixed-point facts because Brouwer `olim`s of different ℕ-indexings of
45+
-- one supremum are not definitionally equal; the monotonicity results are
46+
-- single-`≤′` / single-`<′` and exact.
47+
48+
module Ordinal.Brouwer.VeblenPhiNormal where
49+
50+
open import Data.Nat.Base using (ℕ; zero; suc)
51+
open import Data.Product.Base using (Σ; _,_)
52+
open import Data.Empty using (⊥-elim)
53+
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
54+
55+
open import Ordinal.Brouwer using (Ord; oz; osuc; olim)
56+
open import Ordinal.Brouwer.Phase13
57+
using (_≤′_; _<′_; ≤′-refl; ≤′-trans; ≤′-lim; ≤′-self-osuc)
58+
open import Ordinal.Brouwer.OmegaPow using (_·ℕ_; ·ℕ-mono-≤-left)
59+
open import Ordinal.Brouwer.OrdinalExp using (ω^^_; ε₀; ω^^-pos)
60+
open import Ordinal.Brouwer.VeblenPhi
61+
using (tower-from; next-ε; φ₁; ω^^-next-ε-≤; β<next-ε)
62+
63+
----------------------------------------------------------------------
64+
-- ω-exponentiation is monotone (the one missing prerequisite).
65+
--
66+
-- `α ≤′ β → ω^^ α ≤′ ω^^ β`, by structural recursion on the `_≤′_` shape
67+
-- of (α, β) — the same descent pattern as `Phase13.≤′-trans`. Uses only
68+
-- ω^^-positivity (the `oz` base), `·ℕ`-left-monotonicity (the
69+
-- successor/successor case, where `ω^^ (osuc α) = olim (n ↦ ω^^ α ·ℕ n)`),
70+
-- and the olim least-upper-bound `≤′-lim`.
71+
----------------------------------------------------------------------
72+
73+
ω^^-mono-≤′ : ∀ {α β} → α ≤′ β → ω^^ α ≤′ ω^^ β
74+
ω^^-mono-≤′ {oz} {β} _ = ω^^-pos β
75+
ω^^-mono-≤′ {osuc α} {oz} p = ⊥-elim p
76+
ω^^-mono-≤′ {osuc α} {osuc β} p =
77+
λ n → ≤′-lim {(ω^^ α) ·ℕ n} (λ m → (ω^^ β) ·ℕ m) n
78+
(·ℕ-mono-≤-left {ω^^ α} {ω^^ β} n (ω^^-mono-≤′ {α} {β} p))
79+
ω^^-mono-≤′ {osuc α} {olim f} (n , q) =
80+
≤′-lim {ω^^ (osuc α)} (λ k → ω^^ (f k)) n (ω^^-mono-≤′ {osuc α} {f n} q)
81+
ω^^-mono-≤′ {olim g} {β} p =
82+
λ n → ω^^-mono-≤′ {g n} {β} (p n)
83+
84+
----------------------------------------------------------------------
85+
-- `next-ε β` is the LEAST ω^^-closed ordinal strictly above β.
86+
--
87+
-- For any γ with `osuc β ≤′ γ` (β strictly below γ) and `ω^^ γ ≤′ γ`
88+
-- (γ is closed under ω-exponentiation — the direction of the ε-number
89+
-- property we need), `next-ε β ≤′ γ`. `next-ε β = olim (tower-from
90+
-- (osuc β))`, and `olim … ≤′ γ` is definitionally "every tower approximant
91+
-- is ≤′ γ", proved by induction on the tower index n:
92+
-- * n = 0 : `tower-from (osuc β) 0 = osuc β ≤′ γ` (hypothesis)
93+
-- * n+1 : `ω^^ (tower-from … n) ≤′ ω^^ γ ≤′ γ` (ω^^-mono + closure)
94+
----------------------------------------------------------------------
95+
96+
next-ε-least : ∀ {β γ} → osuc β ≤′ γ → ω^^ γ ≤′ γ → next-ε β ≤′ γ
97+
next-ε-least {β} {γ} β<γ ω^^γ≤γ = go
98+
where
99+
go : ∀ n → tower-from (osuc β) n ≤′ γ
100+
go zero = β<γ
101+
go (suc m) =
102+
≤′-trans {ω^^ (tower-from (osuc β) m)} {ω^^ γ} {γ}
103+
(ω^^-mono-≤′ {tower-from (osuc β) m} {γ} (go m)) ω^^γ≤γ
104+
105+
-- Monotonicity of `next-ε`: a larger base gives a larger next ε-number.
106+
-- By `next-ε-least` with γ := next-ε β (which is ω^^-closed by
107+
-- `ω^^-next-ε-≤`), since `osuc α ≤′ osuc β ≤′ next-ε β`.
108+
next-ε-mono : ∀ {α β} → α ≤′ β → next-ε α ≤′ next-ε β
109+
next-ε-mono {α} {β} p =
110+
next-ε-least {α} {next-ε β}
111+
(≤′-trans {osuc α} {osuc β} {next-ε β} p (β<next-ε β))
112+
(ω^^-next-ε-≤ β)
113+
114+
----------------------------------------------------------------------
115+
-- ε₀ is the least value of φ₁ (φ₁ oz), hence ≤′ every φ₁ value.
116+
-- The `oz` base case of monotonicity; recursion on β alone.
117+
----------------------------------------------------------------------
118+
119+
ε₀-least : ∀ β → ε₀ ≤′ φ₁ β
120+
ε₀-least oz = ≤′-refl {ε₀}
121+
ε₀-least (osuc β) =
122+
≤′-trans {ε₀} {φ₁ β} {next-ε (φ₁ β)}
123+
(ε₀-least β)
124+
(≤′-trans {φ₁ β} {osuc (φ₁ β)} {next-ε (φ₁ β)}
125+
(≤′-self-osuc (φ₁ β)) (β<next-ε (φ₁ β)))
126+
ε₀-least (olim f) = ≤′-lim {ε₀} (λ n → φ₁ (f n)) 0 (ε₀-least (f 0))
127+
128+
----------------------------------------------------------------------
129+
-- φ₁ is a NORMAL FUNCTION.
130+
----------------------------------------------------------------------
131+
132+
-- Monotone. Structural recursion on the `_≤′_` shape of (α, β):
133+
-- * oz base reduces to `ε₀-least`;
134+
-- * successor/successor is `next-ε-mono` of the inductive step;
135+
-- * the two olim cases thread through `≤′-lim` / the pointwise olim rule.
136+
φ₁-mono : ∀ {α β} → α ≤′ β → φ₁ α ≤′ φ₁ β
137+
φ₁-mono {oz} {β} _ = ε₀-least β
138+
φ₁-mono {osuc α} {oz} p = ⊥-elim p
139+
φ₁-mono {osuc α} {osuc β} p = next-ε-mono {φ₁ α} {φ₁ β} (φ₁-mono {α} {β} p)
140+
φ₁-mono {osuc α} {olim f} (n , q) =
141+
≤′-lim {φ₁ (osuc α)} (λ k → φ₁ (f k)) n (φ₁-mono {osuc α} {f n} q)
142+
φ₁-mono {olim g} {β} p = λ n → φ₁-mono {g n} {β} (p n)
143+
144+
-- Strictly increasing at successors: φ₁ α <′ φ₁ (osuc α). Immediate,
145+
-- since `φ₁ (osuc α) = next-ε (φ₁ α)` and `β<next-ε` places `φ₁ α` strictly
146+
-- below `next-ε (φ₁ α)`.
147+
φ₁-lt-succ : ∀ α → φ₁ α <′ φ₁ (osuc α)
148+
φ₁-lt-succ α = β<next-ε (φ₁ α)
149+
150+
-- Strictly monotone. `α <′ β` is `osuc α ≤′ β`; chain the successor jump
151+
-- `φ₁ α <′ φ₁ (osuc α)` with `φ₁ (osuc α) ≤′ φ₁ β` (monotonicity).
152+
φ₁-strict-mono : ∀ {α β} → α <′ β → φ₁ α <′ φ₁ β
153+
φ₁-strict-mono {α} {β} α<β =
154+
≤′-trans {osuc (φ₁ α)} {φ₁ (osuc α)} {φ₁ β}
155+
(φ₁-lt-succ α) (φ₁-mono {osuc α} {β} α<β)
156+
157+
-- Continuous at limits. φ₁ commutes with `olim` definitionally
158+
-- (the `olim` clause of φ₁), so continuity is `refl` — exactly the
159+
-- supremum-preservation a normal function requires.
160+
φ₁-continuous : ∀ f → φ₁ (olim f) ≡ olim (λ n → φ₁ (f n))
161+
φ₁-continuous f = refl

‎proofs/agda/Smoke.agda‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1241,6 +1241,26 @@ open import Ordinal.Brouwer.VeblenPhi using
12411241
; φ₁-ε-number
12421242
)
12431243

1244+
-- Veblen φ-hierarchy slice 3 (2026-06-19, own block per CLAUDE.md
1245+
-- Working rules): φ₁ is a NORMAL FUNCTION and `next-ε β` is the LEAST
1246+
-- ω^^-closed ordinal above β (slice 2 only proved it was AN ε-number
1247+
-- above β). `ω^^-mono-≤′` is the missing monotonicity prerequisite;
1248+
-- `next-ε-least` is the headline; `φ₁-strict-mono` + `φ₁-continuous`
1249+
-- make φ₁ mechanically a normal function — the standard precondition for
1250+
-- the next Veblen level / binary φ_α / Γ₀. Order-type fidelity ψ₀(Ω_ω)
1251+
-- REMAINS OPEN (D-2026-06-14); this neither reaches Γ₀ nor plugs
1252+
-- `Fidelity.AtHeight`.
1253+
open import Ordinal.Brouwer.VeblenPhiNormal using
1254+
( ω^^-mono-≤′ -- ω-exponentiation is monotone (prerequisite)
1255+
; next-ε-least -- next-ε β is the LEAST ω^^-closed ordinal above β
1256+
; next-ε-mono -- next-ε is monotone
1257+
; ε₀-least -- ε₀ = φ₁ oz is the least φ₁ value
1258+
; φ₁-mono -- φ₁ monotone
1259+
; φ₁-lt-succ -- φ₁ strictly increasing at successors
1260+
; φ₁-strict-mono -- φ₁ strictly monotone (normal-function half 1)
1261+
; φ₁-continuous -- φ₁ continuous at limits (normal-function half 2)
1262+
)
1263+
12441264
-- Recommended rank function for unbudgeted `wf-<ᵇʳᶠ_` per Echidna's
12451265
-- design search; transport theorem deferred until Phase 1.3 lemmas land.
12461266
open import Ordinal.Buchholz.RankBrouwer using

0 commit comments

Comments
 (0)