agda: add concrete Veblen measure target scaffold

Author: hyperpolymath

docs/buchholz-plan.adoc

@@ -110,6 +110,9 @@ The order / well-foundedness track now has an explicit staged split:
 * WF-1.6 (`Ordinal.Buchholz.VeblenIdentityModel`): first concrete
   instantiation of the interface (identity-measure bootstrap), keeping
   `dec-ψα` and `dec-+2` as explicit assumptions.
+* WF-1.65 (`Ordinal.Buchholz.VeblenMeasureTarget`): first concrete
+  measure target fixed as a lexicographic order on `OmegaIndex × BT`,
+  with well-foundedness reduced to `×-wellFounded <Ω-wf wf-<ᵇ`.
 * WF-1.7 (`Ordinal.Buchholz.VeblenObligations`): discharge
   same-binder obligation shapes in projection-model form; landed lemmas:
   `dec-+2-plus-right`, `dec-ψα-psi-arg`.
@@ -118,11 +121,12 @@ The order / well-foundedness track now has an explicit staged split:
   additive terms (`<ᵇ-Ω+`, `<ᵇ-ψ+`), and additive-target bridges
   (`<ᵇ-+Ω`, `<ᵇ-+ψ`) with inversions.
 
-Remaining open comparison work after this update:
+Remaining open Veblen-route work after this update:
 
-* Shared-binder same-index/same-left sub-cases in a K-free style
-  (do not return to the blocked direct reflexive-equation elimination
-  route).
+* Define the concrete measure into `OmegaIndex × BT`.
+* Discharge the shared-binder same-index/same-left sub-cases in that
+  target, in a K-free style.
+* Instantiate the Veblen interface without deferred assumptions.
 
 Risk-gated bridge currently admitted:
 

proofs/agda/All.agda

@@ -41,6 +41,7 @@ open import Ordinal.Buchholz.WellFormed
 open import Ordinal.Buchholz.WellFounded
 open import Ordinal.Buchholz.VeblenInterface
 open import Ordinal.Buchholz.VeblenIdentityModel
+open import Ordinal.Buchholz.VeblenMeasureTarget
 open import Ordinal.Buchholz.VeblenObligations
 open import Ordinal.Buchholz.Smoke
 

proofs/agda/Ordinal/Buchholz/Smoke.agda

@@ -124,6 +124,14 @@ open import Ordinal.Buchholz.VeblenIdentityModel using
   ; core-wf-from-identity
   )
 
+open import Ordinal.Buchholz.VeblenMeasureTarget using
+  ( Measure
+  ; _≺M_
+  ; by-index
+  ; by-term
+  ; ≺M-wf
+  )
+
 open import Ordinal.Buchholz.VeblenObligations using
   ( plus-right
   ; psi-arg

proofs/agda/Ordinal/Buchholz/VeblenMeasureTarget.agda

@@ -0,0 +1,38 @@
+{-# OPTIONS --safe --without-K #-}
+
+-- First concrete target carrier for the Veblen-route measure work.
+--
+-- This module only fixes the target order. The remaining Veblen work is
+-- then about defining a measure into this carrier and proving the
+-- deferred same-binder obligations there.
+
+module Ordinal.Buchholz.VeblenMeasureTarget where
+
+open import Data.Product.Base using (_×_; _,_)
+open import Data.Product.Relation.Binary.Lex.Strict using (×-Lex; ×-wellFounded)
+open import Data.Sum.Base using (inj₁; inj₂)
+open import Induction.WellFounded using (WellFounded)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
+
+open import Ordinal.OmegaMarkers using (OmegaIndex; _<Ω_)
+open import Ordinal.Buchholz.Syntax using (BT)
+open import Ordinal.Buchholz.Order using (_<ᵇ_)
+open import Ordinal.Buchholz.WellFounded using (<Ω-wf; wf-<ᵇ)
+
+Measure : Set
+Measure = OmegaIndex × BT
+
+infix 4 _≺M_
+
+_≺M_ : Rel Measure _
+_≺M_ = ×-Lex _≡_ _<Ω_ _<ᵇ_
+
+by-index : ∀ {ν μ α β} → ν <Ω μ → (ν , α) ≺M (μ , β)
+by-index = inj₁
+
+by-term : ∀ {ν α β} → α <ᵇ β → (ν , α) ≺M (ν , β)
+by-term α<β = inj₂ (refl , α<β)
+
+≺M-wf : WellFounded _≺M_
+≺M-wf = ×-wellFounded <Ω-wf wf-<ᵇ

readme.adoc

@@ -88,10 +88,11 @@ Ordinal/Buchholz track status:
 ** `<ᵇ-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.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.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 the shared-binder cases (`<ᵇ-ψα`, `<ᵇ-+2`) and their discharge into a `--without-K`-compatible measure model.
+* Open work is now concentrated in defining the actual measure into that target and discharging the shared-binder cases (`<ᵇ-ψα`, `<ᵇ-+2`) there in a `--without-K`-compatible way.
 
 == External Bridge Targets (local workspace)