docs: mark comparison route as primary

Author: hyperpolymath

README.md

@@ -77,11 +77,11 @@ Ordinal/Buchholz track status:
 - top-marker `bplus` bridges are admitted and inverted: `<ᵇ-+ω`, `<ᵇ-+ψω`, `<ᵇ-inv-+Ωω`, `<ᵇ-inv-+ψω`
 - left-summand bridges into additive terms are admitted and inverted: `<ᵇ-Ω+`, `<ᵇ-ψ+`, `<ᵇ-inv-Ω+`, `<ᵇ-inv-ψ+`
 - general additive-target bridges are admitted and inverted: `<ᵇ-+Ω`, `<ᵇ-+ψ`, `<ᵇ-inv-+Ω`, `<ᵇ-inv-+ψ`
-- `Ordinal.Buchholz.VeblenInterface` pins the measure-based WF interface with explicit constructor obligations and deferred same-binder obligations (`dec-ψα`, `dec-+2`)
+- `Ordinal.Buchholz.VeblenInterface` pins the measure-based WF interface with explicit constructor obligations; the historical same-binder fields (`dec-ψα`, `dec-+2`) remain part of the generic interface, but the closed comparison route now discharges them internally
 - `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.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` now instantiates the Veblen interface without deferred assumptions and exposes `core-wf-from-comparison : WellFounded _<ᵇ_`
+- `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
 
 ## External Bridge Targets (local workspace)

docs/buchholz-plan.adoc

@@ -119,10 +119,11 @@ The order / well-foundedness track now has an explicit staged split:
   `proj-dec-+2` and `proj-dec-ψα`.
 * WF-1.69 (`Ordinal.Buchholz.VeblenComparisonTarget`,
   `Ordinal.Buchholz.VeblenComparisonModel`): comparison-lex target on
-  `BT × BT` with coarse same-binder side-condition; packages a
-  reduced-assumption interface model in which `dec-ψα` and `dec-+2`
-  are discharged internally, leaving one lifted same-index `ψ`-to-`+`
-  lemma as the remaining assumption.
+  `BT × Payload` with recursive `ψ`-compatibility on the first
+  coordinate and tagged payload descent on the second; now packages
+  an assumption-free interface model in which `dec-ψα`, `dec-+2`,
+  and the lifted same-index `ψ`-to-`+` comparison are all discharged
+  internally.
 * WF-1.7 (`Ordinal.Buchholz.VeblenObligations`): discharge
   same-binder obligation shapes in projection-model form; landed lemmas:
   `dec-+2-plus-right`, `dec-ψα-psi-arg`.
@@ -138,6 +139,8 @@ 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.
+* `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.
 

readme.adoc

@@ -86,12 +86,12 @@ Ordinal/Buchholz track status:
 * General additive-target bridges are now admitted and inverted:
 ** `<ᵇ-+Ω`, `<ᵇ-+ψ`
 ** `<ᵇ-inv-+Ω`, `<ᵇ-inv-+ψ`
-* `Ordinal.Buchholz.VeblenInterface` now pins a measure-based WF interface with explicit constructor obligations and deferred same-binder obligations (`dec-ψα`, `dec-+2`) for the Veblen-route follow-up.
-* `Ordinal.Buchholz.VeblenIdentityModel` provides a first concrete instantiation of that interface (identity measure bootstrap), with `dec-ψα` / `dec-+2` kept as explicit parameters.
+* `Ordinal.Buchholz.VeblenInterface` now pins a measure-based WF interface with explicit constructor obligations. The historical same-binder fields (`dec-ψα`, `dec-+2`) remain part of the generic record, but the closed comparison route now discharges them internally.
+* `Ordinal.Buchholz.VeblenIdentityModel` is retained as a bootstrap/interface-coherence scaffold, with `dec-ψα` / `dec-+2` kept as explicit parameters on purpose.
 * `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.VeblenProjectionMeasure` is retained as an explanatory scaffold: it 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 × 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.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.VeblenObligations` advances the hard-obligation discharge track with concrete projection-model lemmas for both same-binder shapes:
 ** `dec-+2-plus-right`
 ** `dec-ψα-psi-arg`