From ce0f47db74259a989f98ab5f604c45c79bc581c9 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Sun, 14 Jun 2026 10:58:13 +0000
Subject: [PATCH] =?UTF-8?q?docs(ordinal):=20record=20the=20unbudgeted=20so?=
 =?UTF-8?q?und-carrier=20wf-<=E1=B5=87=CA=B3=E1=B6=A0=C2=B2=20closure=20(#?=
 =?UTF-8?q?212)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Consolidation follow-through for PR #212. Records across the canonical
docs that roadmap open-item #1 ("eliminate the ℕ budget from
wf-<ᵇʳᶠᵇ") is discharged in its achievable form — the sound-carrier
recursive surface RecursiveSurfaceSound.wf-<ᵇʳᶠ² (unbudgeted, via the
rank2 embedding over _<ᵇ²_) — while the GLOBAL form over native _<ᵇ_
stays walled (all five routes; rank2 does not escape the <ᵇ-+Ω
counterexample), with a falsifiable verdict as its realistic close-out.

  * wiki/Roadmap.adoc — recast open-item #1.
  * roadmap.adoc — Lane 3 note appended.
  * buchholz-rank-obstruction.adoc — "recommended next move 1" UPDATE.
  * CLAUDE.md — session-arc follow-on + DO-NOT-REOPEN on the global form.

Doc-only; no .agda touched.

https://claude.ai/code/session_017t53M7W7ubmXpwymveLcCE
---
 CLAUDE.md                                      | 14 ++++++++++++++
 docs/echo-types/buchholz-rank-obstruction.adoc | 15 +++++++++++++++
 roadmap.adoc                                   | 16 +++++++++++++---
 wiki/Roadmap.adoc                              | 11 ++++++++---
 4 files changed, 50 insertions(+), 6 deletions(-)

diff --git a/CLAUDE.md b/CLAUDE.md
index 7ce381b..e35e8d8 100644
--- a/CLAUDE.md
+++ b/CLAUDE.md
@@ -265,6 +265,20 @@ single-ladder union `_<ᵇᵘ_`: it closes the equal-Ω boundary
 `<ᵇ-ψΩ≤` and the bplus-target `<ᵇ-+1` (the single-ladder Gate 1's
 open blocker) with ONE ordinally-sound scalar rank.
 
+*Follow-on (PR #212): the recursive-surface budget eliminated on the
+sound carrier.* `Ordinal.Buchholz.RecursiveSurfaceSound` lands
+`_<ᵇʳᶠ²_` (= `_<ᵇ²_` core + the two same-binder congruences `ψα`/`+2`)
+and its UNBUDGETED `wf-<ᵇʳᶠ²` via the `rank2` embedding: `<ᵇʳᶠ²-core`
+→ `rank2-mono-<ᵇ²`, the two congruences → `⊕-mono-<-right`. This is
+roadmap open-item #1 ("eliminate the ℕ budget from `wf-<ᵇʳᶠᵇ`") in its
+ACHIEVABLE form. The budget was an artefact of native `_<ᵇ_`'s
+unsoundness, not of the same-binder recursion. DO NOT reopen the
+GLOBAL unbudgeted `wf-<ᵇʳᶠ` over native `_<ᵇ_`: all five routes are
+walled (`RankBrouwer.agda` preamble) and `rank2` does NOT escape the
+`<ᵇ-+Ω` counterexample — its realistic close-out is the falsifiable
+"cannot close under `--safe --without-K`" verdict, not a positive
+proof.
+
 *The `<ᵇ-+ψ` leading-power subtlety (load-bearing).* `rank2-mono-+ψ`
 needs the source pieces below the ψ-block's LEADING power
 `ω-rank-pow (double ν)` — strictly stronger than "below the whole
diff --git a/docs/echo-types/buchholz-rank-obstruction.adoc b/docs/echo-types/buchholz-rank-obstruction.adoc
index eeadcf2..d1f399d 100644
--- a/docs/echo-types/buchholz-rank-obstruction.adoc
+++ b/docs/echo-types/buchholz-rank-obstruction.adoc
@@ -234,6 +234,21 @@ losing well-foundedness. Pinned in `Smoke.agda`; wired into
    into Brouwer or directly. Substantial: the 13-constructor
    matrix + the inversion lemmas all need restating. Likely 2–3
    weeks of disciplined proof work.
++
+*UPDATE 2026-06-14 — this route is now realised on the sound carrier.*
+The doubled-ladder `rank2` (§"Doubled-ladder closure") IS the
+WF-restricted rank: `_<ᵇ²_` is the sound carrier and
+`rank2-mono-<ᵇ²` ranks all 12 core constructors. For the
+*recursive-surface* consumer specifically, this discharges the
+"eliminate the ℕ budget" goal — `Ordinal.Buchholz.RecursiveSurfaceSound`
+lands `_<ᵇʳᶠ²_` (= `_<ᵇ²_` core + the two same-binder congruences) and
+its UNBUDGETED `wf-<ᵇʳᶠ²` via the `rank2` embedding (the two congruence
+cases are the `⊕-mono-<-right` discharges this note already identified;
+the doubled ladder supplies the core). The budget in
+`RecursiveSurfaceBudget._<ᵇʳᶠᵇ_` was an artefact of native
+unsoundness, not of the same-binder recursion. What remains genuinely
+open is only the GLOBAL form over *native* `_<ᵇ_` (route still walled;
+realistic close-out is the falsifiable verdict of move 3, NOT move 2).
 
 2. *Non-additive denotational measure*. Replace the Brouwer-rank
    shape with a function `BT → α` for some target `α` whose order
diff --git a/roadmap.adoc b/roadmap.adoc
index a15d4c0..ecbb6ce 100644
--- a/roadmap.adoc
+++ b/roadmap.adoc
@@ -401,9 +401,19 @@ there is no faithful native projection (native `_<ᵇ_` is ordinally
 unsound — see the `<ᵇ-+Ω` counterexample in the obstruction note),
 and native WF is already proved directly in `WellFounded.wf-<ᵇ`. So
 this closes the *carrier* Gate-1 story but does NOT discharge the
-three open items above (unbudgeted `_<ᵇʳᶠ_` WF; the K-limited
-shared-binder cases; native-`_<ᵇ_` internalisation, which is
-rank-embedding-impossible).
+native-`_<ᵇ_` internalisation (rank-embedding-impossible) or the
+K-limited shared-binder cases above.
+
+*Recursive-surface budget eliminated on the sound carrier (2026-06-14,
+PR #212).* Open item 1 ("unbudgeted `_<ᵇʳᶠ_` WF") is discharged in its
+achievable form: `Ordinal.Buchholz.RecursiveSurfaceSound` lands
+`_<ᵇʳᶠ²_` (= the sound carrier `_<ᵇ²_` + the two same-binder
+congruences `ψα`/`+2`) and its UNBUDGETED `wf-<ᵇʳᶠ²` via the `rank2`
+embedding — no ℕ budget. The budget in `RecursiveSurfaceBudget` was an
+artefact of native `_<ᵇ_`'s unsoundness, not of the recursion. The
+GLOBAL form over native `_<ᵇ_` stays walled (all five routes; `rank2`
+does not escape the `<ᵇ-+Ω` counterexample); its realistic close-out
+is the falsifiable verdict, not a positive proof.
 
 *Artefacts.* See `docs/buchholz-plan.adoc`,
 `docs/echo-types/buchholz-rank-obstruction.adoc` (live per-constructor
diff --git a/wiki/Roadmap.adoc b/wiki/Roadmap.adoc
index 8d23b6b..2ab5ea8 100644
--- a/wiki/Roadmap.adoc
+++ b/wiki/Roadmap.adoc
@@ -59,9 +59,14 @@ consolidation / doc-threading.
 
 Target: *Bachmann–Howard* ψ₀(Ω_ω). Open, in priority order:
 
-. *Unbudgeted `_<ᵇʳᶠ_` global WF* — eliminate the explicit ℕ budget from
-  `wf-<ᵇʳᶠᵇ` without leaving `--safe --without-K`. The named next bottleneck;
-  solo, not swarmable.
+. *Unbudgeted `_<ᵇʳᶠ_` global WF* — the GLOBAL form over native `_<ᵇ_`
+  is *walled* (all five standard routes; native `_<ᵇ_` is ordinally
+  unsound — see `buchholz-rank-obstruction.adoc`). The SOUND-CARRIER
+  form is *DONE* (2026-06-14, PR #212): `RecursiveSurfaceSound.wf-<ᵇʳᶠ²`
+  is unbudgeted, built over `_<ᵇ²_` + the doubled-ladder `rank2`
+  embedding. Remaining open is only the global-over-native form, whose
+  realistic close-out is a falsifiable "cannot close under
+  `--safe --without-K`" verdict rather than a positive proof.
 . *Full constructor set beyond the admitted core* — the K-limited shared-binder
   cases `<ᵇ-ψα`, `<ᵇ-+2`.
 . *Push the surface-route WF back* into `Order.agda`'s main `_<ᵇ_` package.