agda: add dec-ψα projection lemma in Veblen obligations

Author: hyperpolymath

docs/buchholz-plan.adoc

@@ -110,9 +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.7 (`Ordinal.Buchholz.VeblenObligations`): start discharging
-  same-binder obligation shapes; first landed lemma is
-  `dec-+2-plus-right` (projection-model form).
+* WF-1.7 (`Ordinal.Buchholz.VeblenObligations`): discharge
+  same-binder obligation shapes in projection-model form; landed lemmas:
+  `dec-+2-plus-right`, `dec-ψα-psi-arg`.
 * WF-2 (in progress): explicit inversion lemmas for the still-open
   mixed head cases (`Ω/+`, `ψ/+`) and the newly admitted comparison
   bridge `bpsi ν α <ᵇ bOmega μ` under `ν ≤Ω μ`.

proofs/agda/Ordinal/Buchholz/Smoke.agda

@@ -120,5 +120,7 @@ open import Ordinal.Buchholz.VeblenIdentityModel using
 
 open import Ordinal.Buchholz.VeblenObligations using
   ( plus-right
+  ; psi-arg
   ; dec-+2-plus-right
+  ; dec-ψα-psi-arg
   )

proofs/agda/Ordinal/Buchholz/VeblenObligations.agda

@@ -27,4 +27,17 @@ dec-+2-plus-right :
   plus-right (bplus x y₂) <ᵇ plus-right (bplus x z₂)
 dec-+2-plus-right y₂<z₂ = y₂<z₂
 
--- The sibling obligation shape (`dec-ψα`) is kept for the next step.
+-- Project the ψ argument; non-ψ heads map to bzero.
+psi-arg : BT → BT
+psi-arg bzero      = bzero
+psi-arg (bOmega _) = bzero
+psi-arg (bplus _ _) = bzero
+psi-arg (bpsi _ α) = α
+
+-- Sibling same-binder obligation shape:
+-- if α <ᵇ β then ψ-argument projection decreases across bpsi ν _.
+dec-ψα-psi-arg :
+  ∀ {ν α β} →
+  α <ᵇ β →
+  psi-arg (bpsi ν α) <ᵇ psi-arg (bpsi ν β)
+dec-ψα-psi-arg α<β = α<β

readme.adoc

@@ -82,7 +82,9 @@ 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.VeblenObligations` starts the hard-obligation discharge track with a first concrete lemma for the `dec-+2` shape (`dec-+2-plus-right`).
+* `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 remains for general `Ω/+` and `ψ/+` comparisons and for the shared-binder cases (`<ᵇ-ψα`, `<ᵇ-+2`) in a `--without-K`-compatible style.
 
 == External Bridge Targets (local workspace)