agda: add projection measure shared-binder lemmas

Author: hyperpolymath

docs/buchholz-plan.adoc

@@ -113,6 +113,10 @@ The order / well-foundedness track now has an explicit staged split:
 * 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.68 (`Ordinal.Buchholz.VeblenProjectionMeasure`): projection
+  measure into that target made explicit; the two deferred
+  shared-binder obligations now land as concrete target lemmas
+  `proj-dec-+2` and `proj-dec-ψα`.
 * WF-1.7 (`Ordinal.Buchholz.VeblenObligations`): discharge
   same-binder obligation shapes in projection-model form; landed lemmas:
   `dec-+2-plus-right`, `dec-ψα-psi-arg`.
@@ -123,9 +127,10 @@ The order / well-foundedness track now has an explicit staged split:
 
 Remaining open Veblen-route work after this update:
 
-* 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.
+* Reconcile the projection-style same-binder measure pieces with the
+  remaining constructor obligations into one single concrete measure.
+* Cover the non-shared-binder interface fields not yet realized by the
+  current projection measure.
 * Instantiate the Veblen interface without deferred assumptions.
 
 Risk-gated bridge currently admitted:

proofs/agda/All.agda

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

proofs/agda/Ordinal/Buchholz/Smoke.agda

@@ -132,6 +132,18 @@ open import Ordinal.Buchholz.VeblenMeasureTarget using
   ; ≺M-wf
   )
 
+open import Ordinal.Buchholz.VeblenProjectionMeasure using
+  ( proj-index
+  ; proj-term
+  ; proj-measure
+  ; proj-dec-+2
+  ; proj-dec-ψα
+  ; proj-dec-ΩΩ
+  ; proj-dec-Ωψ
+  ; proj-dec-ψΩ
+  ; proj-dec-ψΩ<
+  )
+
 open import Ordinal.Buchholz.VeblenObligations using
   ( plus-right
   ; psi-arg

proofs/agda/Ordinal/Buchholz/VeblenProjectionMeasure.agda

@@ -0,0 +1,82 @@
+{-# OPTIONS --safe --without-K #-}
+
+-- 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
+-- shared-binder follow-up explicit, and discharge those two deferred
+-- obligations in `≺M` itself.
+
+module Ordinal.Buchholz.VeblenProjectionMeasure where
+
+open import Data.Product.Base using (_,_)
+
+open import Ordinal.OmegaMarkers using
+  ( OmegaIndex
+  ; Omega0
+  ; _<Ω_
+  )
+open import Ordinal.Buchholz.Syntax using (BT; bzero; bOmega; bplus; bpsi)
+open import Ordinal.Buchholz.Order using (_<ᵇ_)
+open import Ordinal.Buchholz.VeblenMeasureTarget using
+  ( Measure
+  ; _≺M_
+  ; by-index
+  ; by-term
+  )
+open import Ordinal.Buchholz.VeblenObligations using (plus-right; psi-arg)
+
+proj-index : BT → OmegaIndex
+proj-index bzero       = Omega0
+proj-index (bOmega μ)  = μ
+proj-index (bplus x _) = proj-index x
+proj-index (bpsi ν _)  = ν
+
+proj-term : BT → BT
+proj-term bzero       = bzero
+proj-term (bOmega _)  = bzero
+proj-term (bplus x y) = plus-right (bplus x y)
+proj-term (bpsi ν α)  = psi-arg (bpsi ν α)
+
+proj-measure : BT → Measure
+proj-measure t = proj-index t , proj-term t
+
+-- The same-binder target obligations now become direct lexicographic
+-- decreases on the projected payload.
+proj-dec-+2 :
+  ∀ {x y₂ z₂} →
+  y₂ <ᵇ z₂ →
+  proj-measure (bplus x y₂) ≺M proj-measure (bplus x z₂)
+proj-dec-+2 y₂<z₂ = by-term y₂<z₂
+
+proj-dec-ψα :
+  ∀ {ν α β} →
+  α <ᵇ β →
+  proj-measure (bpsi ν α) ≺M proj-measure (bpsi ν β)
+proj-dec-ψα α<β = by-term α<β
+
+-- The index-driven cases already fit the first lexicographic
+-- component of the same target.
+proj-dec-ΩΩ :
+  ∀ {μ ν} →
+  μ <Ω ν →
+  proj-measure (bOmega μ) ≺M proj-measure (bOmega ν)
+proj-dec-ΩΩ μ<ν = by-index μ<ν
+
+proj-dec-Ωψ :
+  ∀ {μ ν α} →
+  μ <Ω ν →
+  proj-measure (bOmega μ) ≺M proj-measure (bpsi ν α)
+proj-dec-Ωψ μ<ν = by-index μ<ν
+
+proj-dec-ψΩ :
+  ∀ {μ ν α β} →
+  μ <Ω ν →
+  proj-measure (bpsi μ α) ≺M proj-measure (bpsi ν β)
+proj-dec-ψΩ μ<ν = by-index μ<ν
+
+proj-dec-ψΩ< :
+  ∀ {ν μ α} →
+  ν <Ω μ →
+  proj-measure (bpsi ν α) ≺M proj-measure (bOmega μ)
+proj-dec-ψΩ< ν<μ = by-index ν<μ

readme.adoc

@@ -89,10 +89,11 @@ Ordinal/Buchholz track status:
 * `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.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.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 defining the actual measure into that target and discharging the shared-binder cases (`<ᵇ-ψα`, `<ᵇ-+2`) there in a `--without-K`-compatible way.
+* Open work is now concentrated in turning those target-level pieces into one full concrete interface instantiation: the remaining non-shared-binder constructor obligations still need to be made compatible with a single measure, in a `--without-K`-compatible way.
 
 == External Bridge Targets (local workspace)