docs(ordinal): record the unbudgeted sound-carrier wf-<ᵇʳᶠ² closure (#212)

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

Author: claude

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

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

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

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.