docs: clarify Buchholz current-core scope

Author: hyperpolymath

README.md

@@ -82,7 +82,9 @@ Ordinal/Buchholz track status:
 - `Ordinal.Buchholz.VeblenProjectionMeasure` is retained as an explanatory scaffold: it makes the projection-style measure into that target explicit and discharges the shared-binder obligations there as target lemmas
 - `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 _<ᵇ_`
-- the Veblen comparison route is now closed at the current constructor core; remaining work is cleanup and route consolidation rather than a live same-index proof gap
+- the Veblen comparison route is now closed for the current admitted constructor core
+- 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
 
 ## External Bridge Targets (local workspace)
 

docs/buchholz-plan.adoc

@@ -139,10 +139,21 @@ Current Veblen-route status after this update:
   interface without deferred assumptions.
 * `core-wf-from-comparison` now gives a concrete well-foundedness
   route for the current constructor core.
+* This closure is deliberately scoped: it closes the route for the
+  currently admitted constructors already present in
+  `Ordinal.Buchholz.Order`.
+* 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
+  Buchholz order.
 * `VeblenIdentityModel` and `VeblenProjectionMeasure` remain in-tree
   as explanatory scaffolds, not as live proof gaps.
-* Remaining follow-up is cleanup: decide which older intermediate
-  scaffolds stay as explanatory stages and which can be demoted.
+* So there are two distinct follow-ups:
+** editorial cleanup: decide which older intermediate scaffolds stay
+   as explanatory stages and which can be demoted
+** mathematical completion: internalize the shared-binder cases back
+   into the real order package and then re-close inversion,
+   transitivity, and well-foundedness for that enlarged order
 
 Risk-gated bridge currently admitted:
 

readme.adoc

@@ -95,7 +95,9 @@ Ordinal/Buchholz track status:
 * `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 at the current constructor core; remaining work is cleanup and route consolidation rather than a live same-index proof gap.
+* The Veblen comparison route is now closed for the current admitted constructor core.
+* 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.
 
 == External Bridge Targets (local workspace)