docs: record recursive Buchholz depth bridge

Author: hyperpolymath

README.md

@@ -86,11 +86,13 @@ Ordinal/Buchholz track status:
 - `Ordinal.Buchholz.LiftedExtendedOrder` now adds the next honest wrapper `_ <ᵇ⁺¹ _`: the blocked self-lift of `_ <ᵇ⁺ _` fails, but same-binder moves from `_ <ᵇ⁺ _` into `_ <ᵇ⁺¹ _` are derivable and `_ <ᵇ⁺¹ _` is well-founded
 - `Ordinal.Buchholz.IteratedExtendedOrder` now packages that repair as a finite iteration scheme: `LiftedOrder n` gives the `n`th wrapper layer, same-binder moves lift one level at a time, and exact finite same-binder depth is tracked by `SurfaceDepth n` with an embedding into `LiftedOrder (suc n)`
 - `Ordinal.Buchholz.SurfaceOrder` now adds a direct inductive surface `_ <ᵇˢ _` for the two historical same-binder shapes, with an embedding into `_ <ᵇ⁺ _` and inherited well-foundedness
+- `Ordinal.Buchholz.RecursiveSurfaceOrder` now adds a genuinely recursive finite-closure candidate `_ <ᵇʳᶠ _`: every derivation extracts an exact finite depth and embeds into `LiftedOrder (suc n)`, so irreflexivity follows without requiring a single self-stable wrapper
 - the exact remaining recursive frontier is now explicit in code as a blocked self-lift: `SurfaceLiftInterface` is refuted by a concrete same-left `bplus` counterexample, and the surviving route is finite wrapper iteration rather than self-stability
 - the Veblen comparison route is now closed for the current admitted constructor core
 - the new `_ <ᵇ⁺ _` wrapper advances the full-order line by giving a mediated closed relation on all terms
 - the new `_ <ᵇˢ _` surface is the first direct bridge candidate between the current core presentation and that mediated wrapper
 - the new `LiftedOrder n` / `SurfaceDepth n` family shows that arbitrary finite same-binder depth can already be handled by iterated mediated wrappers
+- the new `_ <ᵇʳᶠ _` candidate shows that direct recursive derivations also reduce to those finite-depth fragments; what is still open is a single global mediated well-foundedness theorem for that union
 - this still does not internalize the historically blocked shared-binder shapes as actual constructors of `_ <ᵇ _`; the full intended Buchholz order remains open at that step
 - remaining live mathematical work is therefore not the current-core WF route, but the mediated internalization of the shared-binder cases back into the real order package
 

docs/buchholz-plan.adoc

@@ -153,6 +153,11 @@ The order / well-foundedness track now has an explicit staged split:
   iterates the wrapper construction over `ℕ`, `LiftedOrder-lift`
   embeds each level into the next, and `SurfaceDepth n` records exact
   same-binder depth with an embedding into `LiftedOrder (suc n)`.
+* WF-1.89 (`Ordinal.Buchholz.RecursiveSurfaceOrder`): a direct
+  recursive finite-closure candidate `_ <ᵇʳᶠ _` is now in place.
+  Every derivation yields an exact depth witness `n` together with a
+  `SurfaceDepth n` derivation, hence embeds into
+  `LiftedOrder (suc n)` and is irreflexive.
 * WF-2 (completed for mixed-head cases): bridge layer now includes
   `bpsi ν α <ᵇ bOmega μ` (under `ν ≤Ω μ`), left-summand bridges into
   additive terms (`<ᵇ-Ω+`, `<ᵇ-ψ+`), and additive-target bridges
@@ -187,6 +192,10 @@ Current Veblen-route status after this update:
   arbitrary finite depth: the wrapper construction is iterated over
   `ℕ`, and exact finite same-binder nesting is tracked by
   `SurfaceDepth`.
+* `Ordinal.Buchholz.RecursiveSurfaceOrder` now turns that indexed
+  picture back into a single direct recursive candidate. The current
+  theorem is per-derivation: any proof in `_ <ᵇʳᶠ _` has some finite
+  depth and therefore lands in a suitable iterated wrapper.
 * It does *not* yet promote the historically blocked shared-binder
   shapes into actual constructors of `_ <ᵇ _`; that remains the
   missing step between the current core and the full intended

readme.adoc

@@ -96,6 +96,7 @@ Ordinal/Buchholz track status:
 * `Ordinal.Buchholz.LiftedExtendedOrder` now adds the next honest wrapper `_ <ᵇ⁺¹ _`: the blocked self-lift of `_ <ᵇ⁺ _` fails, but same-binder moves from `_ <ᵇ⁺ _` into `_ <ᵇ⁺¹ _` are derivable and `_ <ᵇ⁺¹ _` is well-founded.
 * `Ordinal.Buchholz.IteratedExtendedOrder` now packages that repair as a finite iteration scheme: `LiftedOrder n` gives the `n`th wrapper layer, same-binder moves lift one level at a time, and exact finite same-binder depth is tracked by `SurfaceDepth n` with an embedding into `LiftedOrder (suc n)`.
 * `Ordinal.Buchholz.SurfaceOrder` now adds a direct inductive surface `_ <ᵇˢ _` for the two historical same-binder shapes, with an embedding into `_ <ᵇ⁺ _` and inherited well-foundedness.
+* `Ordinal.Buchholz.RecursiveSurfaceOrder` now adds a genuinely recursive finite-closure candidate `_ <ᵇʳᶠ _`: every derivation extracts an exact finite depth and embeds into `LiftedOrder (suc n)`, so irreflexivity follows without requiring a single self-stable wrapper.
 * The exact remaining recursive frontier is now explicit in code as a blocked self-lift: `SurfaceLiftInterface` is refuted by a concrete same-left `bplus` counterexample, and the surviving route is finite wrapper iteration rather than self-stability.
 * `Ordinal.Buchholz.VeblenObligations` advances the hard-obligation discharge track with concrete projection-model lemmas for both same-binder shapes:
 ** `dec-+2-plus-right`
@@ -104,6 +105,7 @@ Ordinal/Buchholz track status:
 * The new `_ <ᵇ⁺ _` wrapper advances the full-order line by giving a mediated closed relation on all terms.
 * The new `_ <ᵇˢ _` surface is the first direct bridge candidate between the current core presentation and that mediated wrapper.
 * The new `LiftedOrder n` / `SurfaceDepth n` family shows that arbitrary finite same-binder depth can already be handled by iterated mediated wrappers.
+* The new `_ <ᵇʳᶠ _` candidate shows that direct recursive derivations also reduce to those finite-depth fragments; what is still open is a single global mediated well-foundedness theorem for that union.
 * This still does not internalize the historically blocked shared-binder shapes as actual constructors of `_ <ᵇ _`; the full intended Buchholz order remains open at that step.
 * The remaining live mathematical gap is therefore not current-core well-foundedness, but mediated internalization of the shared-binder cases back into the real order package.