docs: record closed Veblen comparison route

Author: hyperpolymath

README.md

@@ -80,9 +80,9 @@ Ordinal/Buchholz track status:
 - `Ordinal.Buchholz.VeblenInterface` pins the measure-based WF interface with explicit constructor obligations and deferred same-binder obligations (`dec-ψα`, `dec-+2`)
 - `Ordinal.Buchholz.VeblenMeasureTarget` fixes a first concrete target carrier: a lexicographic order on `OmegaIndex × BT`
 - `Ordinal.Buchholz.VeblenProjectionMeasure` 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 × BT` with a coarse same-binder side-condition
-- `Ordinal.Buchholz.VeblenComparisonModel` reduces the remaining Veblen assumption set to one lifted same-index `ψ`-to-`+` lemma
-- open work is now concentrated in discharging that final lifted same-index `ψ`-to-`+` comparison so the comparison model can instantiate the Veblen interface without assumptions
+- `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` now 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
 
 ## External Bridge Targets (local workspace)
 

docs/buchholz-plan.adoc

@@ -131,13 +131,15 @@ The order / well-foundedness track now has an explicit staged split:
   additive terms (`<ᵇ-Ω+`, `<ᵇ-ψ+`), and additive-target bridges
   (`<ᵇ-+Ω`, `<ᵇ-+ψ`) with inversions.
 
-Remaining open Veblen-route work after this update:
-
-* Discharge the remaining lifted same-index `ψ`-to-`+` lemma in the
-  comparison model.
-* Instantiate the Veblen interface without deferred assumptions.
-* Collapse the now-obsolete intermediate scaffolds if the comparison
-  model fully closes.
+Current Veblen-route status after this update:
+
+* The comparison model now discharges the lifted same-index
+  `ψ`-to-`+` comparison internally and instantiates the Veblen
+  interface without deferred assumptions.
+* `core-wf-from-comparison` now gives a concrete well-foundedness
+  route for the current constructor core.
+* Remaining follow-up is cleanup: decide which older intermediate
+  scaffolds stay as explanatory stages and which can be demoted.
 
 Risk-gated bridge currently admitted:
 

readme.adoc

@@ -90,12 +90,12 @@ Ordinal/Buchholz track status:
 * `Ordinal.Buchholz.VeblenIdentityModel` provides a first concrete instantiation of that interface (identity measure bootstrap), with `dec-ψα` / `dec-+2` kept as explicit parameters.
 * `Ordinal.Buchholz.VeblenMeasureTarget` now fixes the first concrete target carrier for the Veblen route: a lexicographic order on `OmegaIndex × BT`, with `≺M-wf` proved from the existing `Ω` and Buchholz well-foundedness results.
 * `Ordinal.Buchholz.VeblenProjectionMeasure` now makes the projection-style measure into that target explicit and discharges the two deferred shared-binder obligations there (`proj-dec-ψα`, `proj-dec-+2`), along with the already index-driven strict cases.
-* `Ordinal.Buchholz.VeblenComparisonTarget` adds a second concrete target: a lexicographic order on `BT × BT` whose equality side-condition is relaxed to “same comparison binder”, so same-left `bplus` and same-index `bpsi` cases can use the second coordinate.
-* `Ordinal.Buchholz.VeblenComparisonModel` packages that target into a reduced-assumption Veblen interface instantiation: the original deferred obligations `dec-ψα` and `dec-+2` are discharged internally, and the remaining assumption is now one lifted same-index `ψ`-to-`+` lemma.
+* `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` now packages that target into an assumption-free Veblen interface instantiation: the original deferred obligations `dec-ψα` and `dec-+2`, and the lifted same-index `ψ`-to-`+` comparison, are all discharged internally.
 * `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`
-* Open work is now concentrated in discharging that final lifted same-index `ψ`-to-`+` comparison, so the comparison model can instantiate the Veblen interface without assumptions.
+* 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.
 
 == External Bridge Targets (local workspace)