agda: clarify primary Veblen route and scaffolds

Author: hyperpolymath

proofs/agda/Ordinal/Buchholz/VeblenComparisonModel.agda

@@ -74,7 +74,7 @@ cmp-dec-Ω+ :
   cmp-measure (bOmega μ) ≺C cmp-measure (bplus x y)
 cmp-dec-Ω+ (inj₁ Ω<x) = by-first (<ᵇ-Ω+ Ω<x)
 cmp-dec-Ω+ {x = bzero}      (inj₂ ())
-cmp-dec-Ω+ {x = bOmega _}   (inj₂ (≈ᶜ-Ω , ()))
+cmp-dec-Ω+ {x = bOmega _}   (inj₂ (_ , ()))
 cmp-dec-Ω+ {x = bplus _ _}  (inj₂ ())
 cmp-dec-Ω+ {x = bpsi _ _}   (inj₂ ())
 

proofs/agda/Ordinal/Buchholz/VeblenIdentityModel.agda

@@ -2,10 +2,10 @@
 
 -- Minimal concrete instantiation of the Veblen WF interface.
 --
--- This uses the identity measure on BT as a bootstrap model to confirm
--- interface coherence. The two same-binder obligations remain explicit
--- parameters (`dec-ψα`, `dec-+2`), matching the currently deferred hard
--- cases.
+-- This bootstrap model is retained as an interface-coherence check.
+-- It is no longer the primary Veblen route: the closed comparison
+-- model now discharges the same-binder obligations internally. Here
+-- they remain explicit parameters (`dec-ψα`, `dec-+2`) on purpose.
 
 module Ordinal.Buchholz.VeblenIdentityModel where
 

proofs/agda/Ordinal/Buchholz/VeblenInterface.agda

@@ -6,8 +6,10 @@
 -- measure. Instead it states, in one place, the obligations required
 -- to prove `WellFounded _<ᵇ_` via a measure into a well-founded target.
 --
--- The final two fields (`dec-ψα`, `dec-+2`) are the deferred same-binder
--- obligations corresponding to the blocked shared-binder shapes.
+-- The final two fields (`dec-ψα`, `dec-+2`) are the historical
+-- same-binder obligations corresponding to the blocked shared-binder
+-- shapes. The closed comparison route now discharges them internally;
+-- they remain here because this record packages the generic interface.
 
 module Ordinal.Buchholz.VeblenInterface where
 

proofs/agda/Ordinal/Buchholz/VeblenProjectionMeasure.agda

@@ -2,10 +2,11 @@
 
 -- Projection-style concrete measure into the current Veblen target.
 --
--- This is not yet the final single measure model for the whole
--- interface. Its role is narrower: make the target images used by the
+-- This module is retained as an explanatory scaffold, not the final
+-- route. Its role is narrower: make the target images used by the
 -- shared-binder follow-up explicit, and discharge those two deferred
--- obligations in `≺M` itself.
+-- obligations in `≺M` itself. The assumption-free closure now happens
+-- in `VeblenComparisonModel`.
 
 module Ordinal.Buchholz.VeblenProjectionMeasure where
 

proofs/agda/Ordinal/Buchholz/WellFounded.agda

@@ -1,7 +1,10 @@
 {-# OPTIONS --safe --without-K #-}
 
--- WF-1 skeleton: prove accessibility by term constructor, with
--- predecessor/inversion lemmas separated from the top-level theorem.
+-- Direct constructor-recursive WF proof for the current Buchholz core.
+--
+-- This remains one complete route to `wf-<ᵇ`. The closed Veblen-side
+-- comparison model now gives a second route; the two coexist so the
+-- direct recursion and the mediated measure proof can both be read.
 
 module Ordinal.Buchholz.WellFounded where