Skip to content

Commit 3008931

Browse files
claudeclaude
committed
proof(ordinal): unbudgeted sound-carrier recursive surface wf-<ᵇʳᶠ²
The recursive-surface route to well-foundedness WITHOUT the ℕ budget, realised over the doubled-ladder sound carrier `_<ᵇ²_` instead of native `_<ᵇ_`. `_<ᵇʳᶠ²_` = `_<ᵇ²_` (sound core) + the two same-binder congruence rules (`<ᵇʳᶠ²-ψα`, `<ᵇʳᶠ²-+2`). All three cases are rank2-embeddable: * <ᵇʳᶠ²-core — rank2-mono-<ᵇ² (this session's umbrella); * <ᵇʳᶠ²-ψα — ⊕-mono-<-right on rank2 α <′ rank2 β (rank2 (bpsi ν α) = ω-rank-pow (double ν) ⊕ rank2 α); * <ᵇʳᶠ²-+2 — ⊕-mono-<-right on rank2 y <′ rank2 z (rank2 (bplus x y) = rank2 x ⊕ rank2 y). So `wf-<ᵇʳᶠ² : WellFounded _<ᵇʳᶠ²_` follows by the standard rank transport (Subrelation + On.wellFounded rank2 wf-<′) with NO budget. Why this is the right form of the "eliminate the budget" goal: the budget in RecursiveSurfaceBudget._<ᵇʳᶠᵇ_ was an artefact of native _<ᵇ_'s ordinal UNsoundness — its <ᵇʳᶠ-core case admits no rank (the <ᵇ-+Ω counterexample; rank2 does not escape it either). All five standard routes to the GLOBAL unbudgeted wf-<ᵇʳᶠ over native _<ᵇ_ are walled (see RankBrouwer.agda preamble + buchholz-rank-obstruction.adoc). The documented "recommended next move 1" is the WF-restricted relation; this module realises it on the sound carrier, where the budget simply isn't needed — the two congruence cases are exactly the ⊕-mono-<-right discharges the RankBrouwer preamble already identified, and the doubled ladder supplies the previously-missing core case. Honest scope: _<ᵇʳᶠ² is to _<ᵇʳᶠ_ what _<ᵇ² is to native _<ᵇ_ — the ordinally-sound restriction. Does NOT claim the global unbudgeted wf-<ᵇʳᶠ over native _<ᵇ_ (still walled). Build: All.agda + Smoke exit 0 under --safe --without-K, zero postulates, structural recursion (no TERMINATING). https://claude.ai/code/session_017t53M7W7ubmXpwymveLcCE
1 parent 0469e91 commit 3008931

3 files changed

Lines changed: 129 additions & 0 deletions

File tree

‎proofs/agda/All.agda‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -166,6 +166,7 @@ open import Ordinal.Buchholz.RankMonoUnion
166166
open import Ordinal.Buchholz.RankMonoUnionWF
167167
open import Ordinal.Buchholz.RankMonoUnionWfCNF
168168
open import Ordinal.Buchholz.RecursiveSurfaceOrder
169+
open import Ordinal.Buchholz.RecursiveSurfaceSound
169170
open import Ordinal.Buchholz.RecursiveSurfaceBudget
170171
open import Ordinal.Buchholz.SurfaceOrder
171172
open import Ordinal.Buchholz.VeblenObligations

‎proofs/agda/Ordinal/Buchholz/RecursiveSurfaceSound.agda‎

Lines changed: 119 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,119 @@
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+
-- Unbudgeted recursive-surface descent over the SOUND carrier
6+
-- (2026-06-14).
7+
--
8+
-- ## What this lands
9+
--
10+
-- `_<ᵇʳᶠ²_` — the recursive same-binder closure over the doubled-ladder
11+
-- sound carrier `_<ᵇ²_` (`RankDoubledLadderUmbrella`) instead of native
12+
-- `_<ᵇ_`, with its UNBUDGETED well-foundedness:
13+
--
14+
-- * `rank2-mono-<ᵇʳᶠ² : s <ᵇʳᶠ² t → rank2 s <′ rank2 t`
15+
-- * `wf-<ᵇʳᶠ² : WellFounded _<ᵇʳᶠ²_`
16+
--
17+
-- ## Why the budget is no longer needed
18+
--
19+
-- The existing `RecursiveSurfaceBudget._<ᵇʳᶠᵇ_` carries an explicit ℕ
20+
-- depth budget precisely because its `_<ᵇʳᶠ_` is built over NATIVE
21+
-- `_<ᵇ_`, whose `<ᵇʳᶠ-core` case is ordinally UNSOUND: no rank embeds
22+
-- it (the `<ᵇ-+Ω` counterexample `bplus bzero (bOmega (fin 1)) <ᵇ
23+
-- bOmega (fin 0)` forces `rank-mono` to invert). See
24+
-- `RankBrouwer.agda`'s preamble and `buchholz-rank-obstruction.adoc`:
25+
-- the rank / direct-mutual / lex / tower / inverse-image routes to the
26+
-- GLOBAL unbudgeted `wf-<ᵇʳᶠ` over native `_<ᵇ_` are all walled, and
27+
-- `rank2` does not escape it (the same counterexample defeats `rank2`).
28+
--
29+
-- The documented "recommended next move 1" is the WF-RESTRICTED
30+
-- relation. This module realises it: building the recursive surface
31+
-- over the SOUND carrier `_<ᵇ²_` makes all three cases rank2-embeddable,
32+
-- so well-foundedness follows by the standard rank transport WITHOUT a
33+
-- budget:
34+
--
35+
-- * `<ᵇʳᶠ²-core` — `rank2-mono-<ᵇ²` (this session's umbrella);
36+
-- * `<ᵇʳᶠ²-ψα` — `⊕-mono-<-right` on `rank2 α <′ rank2 β`
37+
-- (`rank2 (bpsi ν α) = ω-rank-pow (double ν) ⊕ rank2 α`);
38+
-- * `<ᵇʳᶠ²-+2` — `⊕-mono-<-right` on `rank2 y <′ rank2 z`
39+
-- (`rank2 (bplus x y) = rank2 x ⊕ rank2 y`).
40+
--
41+
-- The latter two are exactly the two congruence cases the
42+
-- `RankBrouwer` preamble already identified as discharged by
43+
-- `⊕-mono-<-right`; the doubled ladder supplies the missing core case.
44+
--
45+
-- ## Honest scope
46+
--
47+
-- `_<ᵇʳᶠ²_` is the sound-carrier recursive surface — it is to
48+
-- `_<ᵇʳᶠ_` what `_<ᵇ²_` is to native `_<ᵇ_`: the ordinally-sound
49+
-- restriction. It does NOT claim the GLOBAL unbudgeted `wf-<ᵇʳᶠ` over
50+
-- native `_<ᵇ_` (that remains walled per the obstruction note). Its
51+
-- contribution is that the recursive-surface route is well-founded
52+
-- WITHOUT the ℕ budget once the core is the sound carrier — the budget
53+
-- was an artefact of native unsoundness, not of the same-binder
54+
-- recursion itself.
55+
--
56+
-- ## Headlines (pin in `Ordinal/Buchholz/Smoke.agda`)
57+
--
58+
-- * `_<ᵇʳᶠ²_`
59+
-- * `rank2-mono-<ᵇʳᶠ²`
60+
-- * `wf-<ᵇʳᶠ²`
61+
62+
module Ordinal.Buchholz.RecursiveSurfaceSound where
63+
64+
open import Induction.WellFounded using (WellFounded; module Subrelation)
65+
open import Relation.Binary.Construct.On as On using (wellFounded)
66+
67+
open import Ordinal.Brouwer using (Ord)
68+
open import Ordinal.Brouwer.Phase13 using (_<′_; ⊕-mono-<-right; wf-<′)
69+
open import Ordinal.Brouwer.Arithmetic using (_⊕_)
70+
open import Ordinal.Buchholz.Syntax using (BT; bpsi; bplus)
71+
open import Ordinal.Buchholz.RankPow using (ω-rank-pow)
72+
open import Ordinal.Buchholz.RankDoubledLadder using (rank2; double)
73+
open import Ordinal.Buchholz.RankDoubledLadderUmbrella using
74+
( _<ᵇ²_
75+
; rank2-mono-<ᵇ²
76+
)
77+
78+
----------------------------------------------------------------------
79+
-- The sound-carrier recursive surface `_<ᵇʳᶠ²_`
80+
----------------------------------------------------------------------
81+
82+
-- Native `_<ᵇ_` replaced by the sound carrier `_<ᵇ²_` in the core
83+
-- rule; the two same-binder congruence rules are unchanged.
84+
infix 4 _<ᵇʳᶠ²_
85+
86+
data _<ᵇʳᶠ²_ : BT → BT → Set where
87+
<ᵇʳᶠ²-core : ∀ {x y} → x <ᵇ² y → x <ᵇʳᶠ² y
88+
<ᵇʳᶠ²-ψα : ∀ {ν α β} → α <ᵇʳᶠ² β → bpsi ν α <ᵇʳᶠ² bpsi ν β
89+
<ᵇʳᶠ²-+2 : ∀ {x y z} → y <ᵇʳᶠ² z → bplus x y <ᵇʳᶠ² bplus x z
90+
91+
----------------------------------------------------------------------
92+
-- rank2 strict-monotonicity — no budget
93+
----------------------------------------------------------------------
94+
95+
-- All three cases land directly: the core via the doubled-ladder
96+
-- umbrella, the two congruences via right-strict-monotonicity of `⊕`
97+
-- (the ψ-block leading power / the bplus head are the fixed left
98+
-- summand). Structural recursion on the `_<ᵇʳᶠ²_` derivation.
99+
rank2-mono-<ᵇʳᶠ² : ∀ {s t} → s <ᵇʳᶠ² t → rank2 s <′ rank2 t
100+
rank2-mono-<ᵇʳᶠ² (<ᵇʳᶠ²-core p) = rank2-mono-<ᵇ² p
101+
rank2-mono-<ᵇʳᶠ² (<ᵇʳᶠ²-ψα {ν} {α} {β} p) =
102+
⊕-mono-<-right {ω-rank-pow (double ν)} {rank2 α} {rank2 β}
103+
(rank2-mono-<ᵇʳᶠ² p)
104+
rank2-mono-<ᵇʳᶠ² (<ᵇʳᶠ²-+2 {x} {y} {z} p) =
105+
⊕-mono-<-right {rank2 x} {rank2 y} {rank2 z}
106+
(rank2-mono-<ᵇʳᶠ² p)
107+
108+
----------------------------------------------------------------------
109+
-- Unbudgeted well-foundedness via the rank2 embedding
110+
----------------------------------------------------------------------
111+
112+
-- Step 1 — InverseImage transport of `wf-<′` along `rank2`.
113+
wf-rank2-pullback : WellFounded (λ x y → rank2 x <′ rank2 y)
114+
wf-rank2-pullback = On.wellFounded rank2 wf-<′
115+
116+
-- Step 2 — Subrelation transport: `rank2-mono-<ᵇʳᶠ²` witnesses that
117+
-- `_<ᵇʳᶠ²_` is a sub-relation of the pullback. NO ℕ budget.
118+
wf-<ᵇʳᶠ² : WellFounded _<ᵇʳᶠ²_
119+
wf-<ᵇʳᶠ² = Subrelation.wellFounded rank2-mono-<ᵇʳᶠ² wf-rank2-pullback

‎proofs/agda/Ordinal/Buchholz/Smoke.agda‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -521,6 +521,15 @@ open import Ordinal.Buchholz.RankDoubledLadderUmbrella using
521521
; wf-<ᵇ²
522522
)
523523

524+
-- Unbudgeted sound-carrier recursive surface (own block per CLAUDE.md
525+
-- Working rules): the recursive same-binder closure over `_<ᵇ²_` and
526+
-- its budget-free well-foundedness.
527+
open import Ordinal.Buchholz.RecursiveSurfaceSound using
528+
( _<ᵇʳᶠ²_
529+
; rank2-mono-<ᵇʳᶠ²
530+
; wf-<ᵇʳᶠ²
531+
)
532+
524533
-- Slice 3 prerequisites (own block per CLAUDE.md Working rules):
525534
-- the left-spine NonBzero predicate, the strict-jump bridge from
526535
-- `μ <Ω ν` to `ω-rank-pow-succ μ ≤′ ω-rank-pow ν`, and the head-Ω

0 commit comments

Comments
 (0)