agda: start discharging Veblen same-binder obligations

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.7 (`Ordinal.Buchholz.VeblenObligations`): start discharging
+  same-binder obligation shapes; first landed lemma is
+  `dec-+2-plus-right` (projection-model form).
 * 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/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.VeblenObligations
 open import Ordinal.Buchholz.Smoke
 
 open import Smoke

proofs/agda/Ordinal/Buchholz/Smoke.agda

@@ -117,3 +117,8 @@ open import Ordinal.Buchholz.VeblenIdentityModel using
   ( identity-interface
   ; core-wf-from-identity
   )
+
+open import Ordinal.Buchholz.VeblenObligations using
+  ( plus-right
+  ; dec-+2-plus-right
+  )

proofs/agda/Ordinal/Buchholz/VeblenObligations.agda

@@ -0,0 +1,30 @@
+{-# OPTIONS --safe --without-K #-}
+
+-- Step 7a (Veblen-route obligations): isolate the deferred same-binder
+-- obligations and prove the easiest one first.
+--
+-- This module does not yet provide a full Veblen measure model. It
+-- records/proves obligation-shaped lemmas that can be reused when the
+-- final measure is assembled.
+
+module Ordinal.Buchholz.VeblenObligations where
+
+open import Ordinal.Buchholz.Syntax using (BT; bzero; bOmega; bplus; bpsi)
+open import Ordinal.Buchholz.Order using (_<ᵇ_)
+
+-- Project the right summand of a plus-term; non-plus heads map to bzero.
+plus-right : BT → BT
+plus-right bzero        = bzero
+plus-right (bOmega _)   = bzero
+plus-right (bpsi _ _)   = bzero
+plus-right (bplus _ y₂) = y₂
+
+-- First discharged same-binder obligation shape:
+-- if y₂ <ᵇ z₂ then right-projection decreases across bplus x _.
+dec-+2-plus-right :
+  ∀ {x y₂ z₂} →
+  y₂ <ᵇ z₂ →
+  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.

readme.adoc

@@ -82,6 +82,7 @@ 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`).
 * 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)