docs: record Buchholz surface-order bridge

Author: hyperpolymath

README.md

@@ -83,8 +83,10 @@ Ordinal/Buchholz track status:
 - `Ordinal.Buchholz.VeblenComparisonTarget` adds a second concrete target: a lexicographic order on `BT × Payload` with recursive `ψ`-compatibility on the first coordinate and tagged payload descent for the same-binder follow-up cases
 - `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 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
 - this does not yet 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

@@ -132,6 +132,10 @@ The order / well-foundedness track now has an explicit staged split:
   exposing same-binder principles as derived lemmas; transitivity and
   well-foundedness now come from the closed comparison target rather
   than direct constructor recursion.
+* WF-1.85 (`Ordinal.Buchholz.SurfaceOrder`): first direct inductive
+  surface `_ <ᵇˢ _` adding the two historical same-binder shapes as
+  constructors over current-core premises; embeds into `_ <ᵇ⁺ _` and
+  therefore inherits well-foundedness immediately.
 * WF-2 (completed for mixed-head cases): bridge layer now includes
   `bpsi ν α <ᵇ bOmega μ` (under `ν ≤Ω μ`), left-summand bridges into
   additive terms (`<ᵇ-Ω+`, `<ᵇ-ψ+`), and additive-target bridges
@@ -151,6 +155,10 @@ Current Veblen-route status after this update:
   relation on `BT` by pulling the comparison target back along
   `cmp-measure`; this relation includes the historical same-binder
   principles as lemmas and is transitive / well-founded.
+* `Ordinal.Buchholz.SurfaceOrder` now gives the first direct
+  constructor-level bridge candidate: the same-binder shapes exist as
+  constructors there, but still over current-core premises, and the
+  closure argument runs by embedding into `_ <ᵇ⁺ _`.
 * 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

@@ -93,11 +93,13 @@ Ordinal/Buchholz track status:
 * `Ordinal.Buchholz.VeblenComparisonTarget` adds a second concrete target: a lexicographic order on `BT × Payload` whose first coordinate is relaxed by recursive `ψ`-compatibility, and whose tagged payload order handles the same-binder descent cases without introducing unstable extra comparisons.
 * `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.
 * `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`
 * 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.
 * This does not yet 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.