Merge branch 'main' into claude/echo-types-docs-sync

Author: hyperpolymath

docs/buchholz-plan.adoc

@@ -103,16 +103,26 @@ The order / well-foundedness track now has an explicit staged split:
   current core, with irreflexivity recovered as a corollary
   (`<ᵇ-irreflexive`) instead of a direct shared-binder elimination
   proof.
-* WF-2 (in progress): explicit inversion lemmas for the still-open
-  mixed head cases (`Ω/+`, `ψ/+`) and the newly admitted comparison
-  bridge `bpsi ν α <ᵇ bOmega μ` under `ν ≤Ω μ`.
+* WF-1.5 (`Ordinal.Buchholz.VeblenInterface`): measure-route interface
+  pinning constructor-by-constructor decrease obligations and explicit
+  deferred same-binder obligations (`dec-ψα`, `dec-+2`) for the Veblen
+  follow-up.
+* 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`): discharge
+  same-binder obligation shapes in projection-model form; landed lemmas:
+  `dec-+2-plus-right`, `dec-ψα-psi-arg`.
+* WF-2 (in progress): mixed-head bridge layer now includes
+  `bpsi ν α <ᵇ bOmega μ` (under `ν ≤Ω μ`) and left-summand bridges
+  into additive terms (`<ᵇ-Ω+`, `<ᵇ-ψ+`) with inversions.
 
 Remaining open comparison work after this update:
 
-* Constructor-level comparison rules for `bOmega` vs `bplus` (both
-  directions) in the intended normal-form discipline.
-* Constructor-level comparison rules for `bpsi` vs `bplus` (both
-  directions).
+* Constructor-level comparison rules for non-top `bplus` vs `bOmega`
+  (the `bplus → bOmega` direction beyond `<ᵇ-+ω`).
+* Constructor-level comparison rules for non-top `bplus` vs `bpsi`
+  (the `bplus → bpsi` direction beyond `<ᵇ-+ψω`).
 * Shared-binder same-index/same-left sub-cases in a K-free style
   (do not return to the blocked direct reflexive-equation elimination
   route).

proofs/agda/All.agda

@@ -39,6 +39,9 @@ open import Ordinal.Buchholz.Psi
 open import Ordinal.Buchholz.Examples
 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/Order.agda

@@ -8,25 +8,24 @@
 -- the term heads naturally determine. Totality is *not* proved here
 -- and neither is well-foundedness; those are WF-1 and WF-2.
 --
--- Scope of this module. The 7 constructors below cover the head
+-- Scope of this module. The constructors below cover the head
 -- pairs marked ✓ in the matrix, with the lex-on-left-summand case
 -- for bplus and the lex-on-Ω-index case for bpsi:
 --
 --   head of x \ head of y │ bzero │ bOmega │ bplus │ bpsi
 --   ──────────────────────┼───────┼────────┼───────┼──────
 --   bzero                 │   –   │   ✓    │   ✓   │  ✓
---   bOmega                │       │   ✓    │       │  ✓ (when μ <Ω ν)
+--   bOmega                │       │   ✓    │   ✓   │  ✓ (when μ <Ω ν)
 --   bplus                 │       │        │   ✓   │
---   bpsi                  │       │   ✓    │       │  ✓ (when μ <Ω ν)
+--   bpsi                  │       │   ✓    │   ✓   │  ✓ (when μ <Ω ν)
 --
 -- Open cases (no constructor yet; must be discharged in follow-ups
 -- before `<ᵇ`-totality and well-foundedness can land):
 --
---   * bOmega vs bplus (general case) — requires a comparison
---     between atomic heads and additive normal forms. A narrow
---     top-marker bridge is admitted by `<ᵇ-+ω`.
---   * bpsi vs bplus (either direction) — same reason, mediated by
---     the leading bpsi summand of a bplus in CNF.
+--   * bplus vs bOmega (general case) — currently only the top-marker
+--     bridge `<ᵇ-+ω` is admitted.
+--   * bplus vs bpsi (general case) — currently only the top-marker
+--     bridge `<ᵇ-+ψω` is admitted.
 --   * Two same-binder sub-cases whose natural shapes run into Agda
 --     2.6.3's `--without-K` restriction on reflexive-equation
 --     elimination and are deferred pending a K-free reformulation:
@@ -76,6 +75,10 @@ data _<ᵇ_ : BT → BT → Set where
   <ᵇ-ψΩ  : ∀ {μ ν α β} → μ <Ω ν → bpsi μ α <ᵇ bpsi ν β
   <ᵇ-ψΩ≤ : ∀ {ν μ α}   → ν ≤Ω μ → bpsi ν α <ᵇ bOmega μ
 
+  -- Left-summand bridge into additive terms.
+  <ᵇ-Ω+  : ∀ {μ x y}    → bOmega μ <ᵇ x → bOmega μ <ᵇ bplus x y
+  <ᵇ-ψ+  : ∀ {ν α x y}  → bpsi ν α <ᵇ x → bpsi ν α <ᵇ bplus x y
+
   -- bplus comparison by the left summand. The same-left sub-case
   -- (compare right summands when lefts agree) is deferred for the
   -- same `--without-K` reason as `<ᵇ-ψα` above: its natural shape
@@ -115,27 +118,43 @@ infix 4 _<ᵇ_
 -- Left leg: <ᵇ-0-Ω (x = bzero, y = bOmega _)
 <ᵇ-trans <ᵇ-0-Ω       (<ᵇ-ΩΩ _)            = <ᵇ-0-Ω
 <ᵇ-trans <ᵇ-0-Ω       (<ᵇ-Ωψ _)            = <ᵇ-0-ψ
+<ᵇ-trans <ᵇ-0-Ω       (<ᵇ-Ω+ _)            = <ᵇ-0-+
 -- Left leg: <ᵇ-0-+ (x = bzero, y = bplus _ _)
 <ᵇ-trans <ᵇ-0-+       (<ᵇ-+1 _)            = <ᵇ-0-+
 <ᵇ-trans <ᵇ-0-+       (<ᵇ-+ω _)            = <ᵇ-0-Ω
 <ᵇ-trans <ᵇ-0-+       (<ᵇ-+ψω _)           = <ᵇ-0-ψ
 -- Left leg: <ᵇ-0-ψ (x = bzero, y = bpsi _ _)
 <ᵇ-trans <ᵇ-0-ψ       (<ᵇ-ψΩ _)            = <ᵇ-0-ψ
+<ᵇ-trans <ᵇ-0-ψ       (<ᵇ-ψ+ _)            = <ᵇ-0-+
 -- Left leg: <ᵇ-ΩΩ (x = bOmega _, y = bOmega _)
 <ᵇ-trans (<ᵇ-ΩΩ p)    (<ᵇ-ΩΩ q)            = <ᵇ-ΩΩ (<Ω-trans p q)
 <ᵇ-trans (<ᵇ-ΩΩ p)    (<ᵇ-Ωψ q)            = <ᵇ-Ωψ (<Ω-trans p q)
+<ᵇ-trans (<ᵇ-ΩΩ p)    (<ᵇ-Ω+ q)            = <ᵇ-Ω+ (<ᵇ-trans (<ᵇ-ΩΩ p) q)
 -- Left leg: <ᵇ-Ωψ (x = bOmega _, y = bpsi _ _)
 <ᵇ-trans (<ᵇ-Ωψ p)    (<ᵇ-ψΩ q)            = <ᵇ-Ωψ (<Ω-trans p q)
+<ᵇ-trans (<ᵇ-Ωψ p)    (<ᵇ-ψ+ q)            = <ᵇ-Ω+ (<ᵇ-trans (<ᵇ-Ωψ p) q)
 -- Left leg: <ᵇ-ψΩ (x = bpsi _ _, y = bpsi _ _)
 <ᵇ-trans (<ᵇ-ψΩ p)    (<ᵇ-ψΩ q)            = <ᵇ-ψΩ (<Ω-trans p q)
 <ᵇ-trans (<ᵇ-ψΩ p)    (<ᵇ-ψΩ≤ q)           = <ᵇ-ψΩ≤ (≤Ω-trans (<Ω→≤Ω p) q)
+<ᵇ-trans (<ᵇ-ψΩ p)    (<ᵇ-ψ+ q)            = <ᵇ-ψ+ (<ᵇ-trans (<ᵇ-ψΩ p) q)
 -- Left leg: <ᵇ-ψΩ≤ (x = bpsi _ _, y = bOmega _)
 <ᵇ-trans (<ᵇ-ψΩ≤ p)   (<ᵇ-ΩΩ q)            = <ᵇ-ψΩ≤ (≤Ω-trans p (<Ω→≤Ω q))
 <ᵇ-trans (<ᵇ-ψΩ≤ p)   (<ᵇ-Ωψ q)            = <ᵇ-ψΩ (≤Ω-<Ω-trans p q)
+<ᵇ-trans (<ᵇ-ψΩ≤ p)   (<ᵇ-Ω+ q)            = <ᵇ-ψ+ (<ᵇ-trans (<ᵇ-ψΩ≤ p) q)
 -- Left leg: <ᵇ-+1 (x = bplus _ _, y = bplus _ _)
 <ᵇ-trans (<ᵇ-+1 p)    (<ᵇ-+1 q)            = <ᵇ-+1 (<ᵇ-trans p q)
 <ᵇ-trans (<ᵇ-+1 p)    (<ᵇ-+ω q)            = <ᵇ-+ω (<ᵇ-trans p q)
 <ᵇ-trans (<ᵇ-+1 p)    (<ᵇ-+ψω q)           = <ᵇ-+ψω (<ᵇ-trans p q)
+-- Left leg: <ᵇ-Ω+ (x = bOmega _, y = bplus _ _)
+<ᵇ-trans (<ᵇ-Ω+ p)    (<ᵇ-+1 q)            = <ᵇ-Ω+ (<ᵇ-trans p q)
+<ᵇ-trans (<ᵇ-Ω+ p)    (<ᵇ-+ω q)            = <ᵇ-trans p q
+<ᵇ-trans (<ᵇ-Ω+ p)    (<ᵇ-+ψω q)           = <ᵇ-trans p q
+-- Left leg: <ᵇ-ψ+ (x = bpsi _ _, y = bplus _ _)
+<ᵇ-trans (<ᵇ-ψ+ p)    (<ᵇ-+1 q)            = <ᵇ-ψ+ (<ᵇ-trans p q)
+<ᵇ-trans (<ᵇ-ψ+ p)    (<ᵇ-+ω q)            = <ᵇ-trans p q
+<ᵇ-trans (<ᵇ-ψ+ p)    (<ᵇ-+ψω q)           = <ᵇ-trans p q
+<ᵇ-trans (<ᵇ-+ω p)    (<ᵇ-Ω+ q)            = <ᵇ-+1 (<ᵇ-trans p q)
+<ᵇ-trans (<ᵇ-+ψω p)   (<ᵇ-ψ+ q)            = <ᵇ-+1 (<ᵇ-trans p q)
 -- Left leg: <ᵇ-+ψω (x = bplus _ _, y = bpsi ω _)
 <ᵇ-trans (<ᵇ-+ψω p)   (<ᵇ-ψΩ≤ ω≤ω)         = <ᵇ-+ω (<ᵇ-trans p (<ᵇ-ψΩ≤ ω≤ω))
 -- Right leg: <ᵇ-ψΩ≤ (y = bpsi _ _, z = bOmega _)
@@ -146,12 +165,11 @@ infix 4 _<ᵇ_
 -- WF-2 open-case inversions (Ω vs +)
 ----------------------------------------------------------------------------
 
--- The current 7-constructor core has no witness for either direction.
--- These inversion lemmas pin that fact explicitly for downstream case
--- splits while the comparison rule is still deferred.
+-- The Ω→+ bridge is admitted (`<ᵇ-Ω+`), while the non-top
+-- bplus→Ω case remains deferred.
 
-<ᵇ-inv-Ω+ : ∀ {μ x y} → bOmega μ <ᵇ bplus x y → ⊥
-<ᵇ-inv-Ω+ ()
+<ᵇ-inv-Ω+ : ∀ {μ x y} → bOmega μ <ᵇ bplus x y → bOmega μ <ᵇ x
+<ᵇ-inv-Ω+ (<ᵇ-Ω+ Ω<x) = Ω<x
 
 <ᵇ-inv-+Ωfin : ∀ {x y n} → bplus x y <ᵇ bOmega (fin n) → ⊥
 <ᵇ-inv-+Ωfin ()
@@ -164,11 +182,11 @@ infix 4 _<ᵇ_
 -- WF-2 open-case inversions (ψ vs +)
 ----------------------------------------------------------------------------
 
--- Like Ω-vs-+, these comparisons are still deferred and currently
--- have no constructors in either direction.
+-- The ψ→+ bridge is admitted (`<ᵇ-ψ+`), while the non-top
+-- bplus→ψ case remains deferred.
 
-<ᵇ-inv-ψ+ : ∀ {μ α x y} → bpsi μ α <ᵇ bplus x y → ⊥
-<ᵇ-inv-ψ+ ()
+<ᵇ-inv-ψ+ : ∀ {μ α x y} → bpsi μ α <ᵇ bplus x y → bpsi μ α <ᵇ x
+<ᵇ-inv-ψ+ (<ᵇ-ψ+ ψ<x) = ψ<x
 
 <ᵇ-inv-+ψfin : ∀ {x y n α} → bplus x y <ᵇ bpsi (fin n) α → ⊥
 <ᵇ-inv-+ψfin ()

proofs/agda/Ordinal/Buchholz/Smoke.agda

@@ -55,6 +55,8 @@ open import Ordinal.Buchholz.Order using
   ; <ᵇ-Ωψ
   ; <ᵇ-ψΩ
   ; <ᵇ-ψΩ≤
+  ; <ᵇ-Ω+
+  ; <ᵇ-ψ+
   ; <ᵇ-+ω
   ; <ᵇ-+ψω
   ; <ᵇ-+1
@@ -108,3 +110,19 @@ open import Ordinal.Buchholz.WellFormed using
   ; psi-OmegaOmega
   ; psi-OmegaOmega-wf
   )
+
+open import Ordinal.Buchholz.VeblenInterface using
+  ( VeblenWFInterface
+  )
+
+open import Ordinal.Buchholz.VeblenIdentityModel using
+  ( identity-interface
+  ; core-wf-from-identity
+  )
+
+open import Ordinal.Buchholz.VeblenObligations using
+  ( plus-right
+  ; psi-arg
+  ; dec-+2-plus-right
+  ; dec-ψα-psi-arg
+  )

proofs/agda/Ordinal/Buchholz/VeblenIdentityModel.agda

@@ -0,0 +1,61 @@
+{-# OPTIONS --safe --without-K #-}
+
+-- 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.
+
+module Ordinal.Buchholz.VeblenIdentityModel where
+
+open import Induction.WellFounded using (WellFounded)
+
+open import Ordinal.Buchholz.Syntax using (BT; bzero; bOmega; bplus; bpsi)
+open import Ordinal.Buchholz.Order using
+  ( _<ᵇ_
+  ; <ᵇ-0-Ω
+  ; <ᵇ-0-+
+  ; <ᵇ-0-ψ
+  ; <ᵇ-ΩΩ
+  ; <ᵇ-Ωψ
+  ; <ᵇ-ψΩ
+  ; <ᵇ-ψΩ≤
+  ; <ᵇ-Ω+
+  ; <ᵇ-ψ+
+  ; <ᵇ-+ω
+  ; <ᵇ-+ψω
+  ; <ᵇ-+1
+  )
+open import Ordinal.Buchholz.WellFounded using (wf-<ᵇ)
+open import Ordinal.Buchholz.VeblenInterface using (VeblenWFInterface)
+
+identity-interface :
+  (dec-ψα : ∀ {ν α β} → α <ᵇ β → bpsi ν α <ᵇ bpsi ν β) →
+  (dec-+2 : ∀ {x y₂ z₂} → y₂ <ᵇ z₂ → bplus x y₂ <ᵇ bplus x z₂) →
+  VeblenWFInterface BT _<ᵇ_
+identity-interface dec-ψα dec-+2 = record
+  { measure = λ x → x
+  ; ≺-wf = wf-<ᵇ
+  ; dec-0-Ω = <ᵇ-0-Ω
+  ; dec-0-+ = <ᵇ-0-+
+  ; dec-0-ψ = <ᵇ-0-ψ
+  ; dec-ΩΩ = <ᵇ-ΩΩ
+  ; dec-Ωψ = <ᵇ-Ωψ
+  ; dec-ψΩ = <ᵇ-ψΩ
+  ; dec-ψΩ≤ = <ᵇ-ψΩ≤
+  ; dec-Ω+ = <ᵇ-Ω+
+  ; dec-ψ+ = <ᵇ-ψ+
+  ; dec-+ω = <ᵇ-+ω
+  ; dec-+ψω = <ᵇ-+ψω
+  ; dec-+1 = <ᵇ-+1
+  ; dec-ψα = dec-ψα
+  ; dec-+2 = dec-+2
+  }
+
+core-wf-from-identity :
+  (dec-ψα : ∀ {ν α β} → α <ᵇ β → bpsi ν α <ᵇ bpsi ν β) →
+  (dec-+2 : ∀ {x y₂ z₂} → y₂ <ᵇ z₂ → bplus x y₂ <ᵇ bplus x z₂) →
+  WellFounded _<ᵇ_
+core-wf-from-identity dec-ψα dec-+2 =
+  VeblenWFInterface.core-wf (identity-interface dec-ψα dec-+2)

proofs/agda/Ordinal/Buchholz/VeblenInterface.agda

@@ -0,0 +1,87 @@
+{-# OPTIONS --safe --without-K #-}
+
+-- Veblen-route interface for Buchholz WF follow-up work.
+--
+-- This module is intentionally small: it does not implement a concrete
+-- 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.
+
+module Ordinal.Buchholz.VeblenInterface where
+
+open import Agda.Primitive using (Level; lsuc; _⊔_)
+open import Function.Base using (_on_)
+open import Relation.Binary.Core using (Rel; _⇒_)
+open import Induction.WellFounded as WF using (WellFounded; module Subrelation)
+open import Relation.Binary.Construct.On as On using (wellFounded)
+
+open import Ordinal.OmegaMarkers using (OmegaIndex; _<Ω_; _≤Ω_; ω)
+open import Ordinal.Buchholz.Syntax using (BT; bzero; bOmega; bplus; bpsi)
+open import Ordinal.Buchholz.Order using
+  ( _<ᵇ_
+  ; <ᵇ-0-Ω
+  ; <ᵇ-0-+
+  ; <ᵇ-0-ψ
+  ; <ᵇ-ΩΩ
+  ; <ᵇ-Ωψ
+  ; <ᵇ-ψΩ
+  ; <ᵇ-ψΩ≤
+  ; <ᵇ-Ω+
+  ; <ᵇ-ψ+
+  ; <ᵇ-+ω
+  ; <ᵇ-+ψω
+  ; <ᵇ-+1
+  )
+
+record VeblenWFInterface {ℓm ℓr : Level}
+                         (M : Set ℓm)
+                         (_≺_ : Rel M ℓr)
+                         : Set (lsuc (ℓm ⊔ ℓr)) where
+  field
+    measure : BT → M
+    ≺-wf    : WellFounded _≺_
+
+    -- Constructor-by-constructor decrease obligations for the current core.
+    dec-0-Ω  : ∀ {μ} → measure bzero ≺ measure (bOmega μ)
+    dec-0-+  : ∀ {x y} → measure bzero ≺ measure (bplus x y)
+    dec-0-ψ  : ∀ {ν α} → measure bzero ≺ measure (bpsi ν α)
+
+    dec-ΩΩ   : ∀ {μ ν} → μ <Ω ν → measure (bOmega μ) ≺ measure (bOmega ν)
+    dec-Ωψ   : ∀ {μ ν α} → μ <Ω ν → measure (bOmega μ) ≺ measure (bpsi ν α)
+    dec-ψΩ   : ∀ {μ ν α β} → μ <Ω ν → measure (bpsi μ α) ≺ measure (bpsi ν β)
+    dec-ψΩ≤  : ∀ {ν μ α} → ν ≤Ω μ → measure (bpsi ν α) ≺ measure (bOmega μ)
+    dec-Ω+   : ∀ {μ x y} → measure (bOmega μ) ≺ measure x →
+               measure (bOmega μ) ≺ measure (bplus x y)
+    dec-ψ+   : ∀ {ν α x y} → measure (bpsi ν α) ≺ measure x →
+               measure (bpsi ν α) ≺ measure (bplus x y)
+
+    dec-+ω   : ∀ {x y} → x <ᵇ bOmega ω → measure (bplus x y) ≺ measure (bOmega ω)
+    dec-+ψω  : ∀ {x y α} → x <ᵇ bpsi ω α → measure (bplus x y) ≺ measure (bpsi ω α)
+    dec-+1   : ∀ {x₁ x₂ y₁ y₂} → x₁ <ᵇ y₁ → measure (bplus x₁ x₂) ≺ measure (bplus y₁ y₂)
+
+    -- Deferred same-binder obligations for the extended comparison layer.
+    dec-ψα   : ∀ {ν α β} → α <ᵇ β → measure (bpsi ν α) ≺ measure (bpsi ν β)
+    dec-+2   : ∀ {x y₂ z₂} → y₂ <ᵇ z₂ → measure (bplus x y₂) ≺ measure (bplus x z₂)
+
+  core-monotone : _<ᵇ_ ⇒ (_≺_ on measure)
+  core-monotone <ᵇ-0-Ω = dec-0-Ω
+  core-monotone <ᵇ-0-+ = dec-0-+
+  core-monotone <ᵇ-0-ψ = dec-0-ψ
+  core-monotone (<ᵇ-ΩΩ μ<ν) = dec-ΩΩ μ<ν
+  core-monotone (<ᵇ-Ωψ μ<ν) = dec-Ωψ μ<ν
+  core-monotone (<ᵇ-ψΩ μ<ν) = dec-ψΩ μ<ν
+  core-monotone (<ᵇ-ψΩ≤ ν≤μ) = dec-ψΩ≤ ν≤μ
+  core-monotone (<ᵇ-Ω+ Ω<x) = dec-Ω+ (core-monotone Ω<x)
+  core-monotone (<ᵇ-ψ+ ψ<x) = dec-ψ+ (core-monotone ψ<x)
+  core-monotone (<ᵇ-+ω x<ω) = dec-+ω x<ω
+  core-monotone (<ᵇ-+ψω x<ψω) = dec-+ψω x<ψω
+  core-monotone (<ᵇ-+1 x₁<y₁) = dec-+1 x₁<y₁
+
+  -- Generic derivation route: well-founded target + constructor monotonicity
+  -- gives well-foundedness of the current `_ <ᵇ _` core via subrelation.
+  core-wf : WellFounded _<ᵇ_
+  core-wf =
+    let module SR = Subrelation core-monotone
+    in SR.wellFounded (wellFounded measure ≺-wf)

proofs/agda/Ordinal/Buchholz/VeblenObligations.agda

@@ -0,0 +1,43 @@
+{-# 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₂
+
+-- 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 α<β = α<β