docs: record recursive surface frontier

Author: hyperpolymath

README.md

@@ -84,6 +84,7 @@ Ordinal/Buchholz track status:
 - `Ordinal.Buchholz.VeblenComparisonModel` is now the primary closed Veblen route: it instantiates the Veblen interface without deferred assumptions and exposes `core-wf-from-comparison : WellFounded _<ᵇ_`
 - `Ordinal.Buchholz.ExtendedOrder` now packages a closed comparison-induced extension `_ <ᵇ⁺ _` of `BT`: it contains the current core, exposes the historical same-binder principles as lemmas, and is transitive and well-founded
 - `Ordinal.Buchholz.SurfaceOrder` now adds a direct inductive surface `_ <ᵇˢ _` for the two historical same-binder shapes, with an embedding into `_ <ᵇ⁺ _` and inherited well-foundedness
+- the exact remaining recursive frontier is now explicit in code as `SurfaceLiftInterface`: if `_ <ᵇ⁺ _` is shown stable under same-binder descent with `_ <ᵇ⁺ _` premises, a genuinely recursive surface order `_ <ᵇʳ _` follows immediately
 - 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

docs/buchholz-plan.adoc

@@ -136,6 +136,11 @@ The order / well-foundedness track now has an explicit staged split:
   surface `_ <ᵇˢ _` adding the two historical same-binder shapes as
   constructors over current-core premises; embeds into `_ <ᵇ⁺ _` and
   therefore inherits well-foundedness immediately.
+* WF-1.86 (`SurfaceLiftInterface` / recursive `_ <ᵇʳ _` skeleton in
+  `Ordinal.Buchholz.SurfaceOrder`): the exact remaining frontier is
+  now formalized as two lifted same-binder closure obligations over
+  `_ <ᵇ⁺ _`; if those are discharged, a genuinely recursive surface
+  relation follows by subrelation into the closed wrapper.
 * WF-2 (completed for mixed-head cases): bridge layer now includes
   `bpsi ν α <ᵇ bOmega μ` (under `ν ≤Ω μ`), left-summand bridges into
   additive terms (`<ᵇ-Ω+`, `<ᵇ-ψ+`), and additive-target bridges

readme.adoc

@@ -94,6 +94,7 @@ Ordinal/Buchholz track status:
 * `Ordinal.Buchholz.VeblenComparisonModel` is now the primary closed Veblen route: it packages that target into an assumption-free Veblen interface instantiation in which the original deferred obligations `dec-ψα` and `dec-+2`, and the lifted same-index `ψ`-to-`+` comparison, are all discharged internally.
 * `Ordinal.Buchholz.ExtendedOrder` now packages a closed comparison-induced extension `_ <ᵇ⁺ _` of `BT`: it contains the current core, exposes the historical same-binder principles as lemmas, and is transitive and well-founded.
 * `Ordinal.Buchholz.SurfaceOrder` now adds a direct inductive surface `_ <ᵇˢ _` for the two historical same-binder shapes, with an embedding into `_ <ᵇ⁺ _` and inherited well-foundedness.
+* The exact remaining recursive frontier is now explicit in code as `SurfaceLiftInterface`: if `_ <ᵇ⁺ _` can be shown stable under same-binder descent with `_ <ᵇ⁺ _` premises, then a genuinely recursive surface order `_ <ᵇʳ _` follows immediately.
 * `Ordinal.Buchholz.VeblenObligations` advances the hard-obligation discharge track with concrete projection-model lemmas for both same-binder shapes:
 ** `dec-+2-plus-right`
 ** `dec-ψα-psi-arg`