agda: generalize Buchholz bplus target bridges

Author: hyperpolymath

docs/buchholz-plan.adoc

@@ -113,25 +113,21 @@ The order / well-foundedness track now has an explicit staged split:
 * 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.
+* WF-2 (completed for mixed-head cases): bridge layer now includes
+  `bpsi ν α <ᵇ bOmega μ` (under `ν ≤Ω μ`), left-summand bridges into
+  additive terms (`<ᵇ-Ω+`, `<ᵇ-ψ+`), and additive-target bridges
+  (`<ᵇ-+Ω`, `<ᵇ-+ψ`) with inversions.
 
 Remaining open comparison work after this update:
 
-* 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).
 
 Risk-gated bridge currently admitted:
 
-* `bplus x y <ᵇ bOmega ω` from `x <ᵇ bOmega ω` (top-marker-only
-  directional bridge). This is intentionally narrow to avoid forcing
-  immediate `bplus` vs `bpsi` constructor commitments.
+* The original top-marker bridges remain as named specialised lemmas
+  (`<ᵇ-+ω`, `<ᵇ-+ψω`) over the now-general additive-target bridges.
 
 == The very first Agda proof: `C-monotone`
 

proofs/agda/Ordinal/Buchholz/Order.agda

@@ -22,10 +22,6 @@
 -- Open cases (no constructor yet; must be discharged in follow-ups
 -- before `<ᵇ`-totality and well-foundedness can land):
 --
---   * 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:
@@ -83,8 +79,8 @@ data _<ᵇ_ : BT → BT → Set where
   -- (compare right summands when lefts agree) is deferred for the
   -- same `--without-K` reason as `<ᵇ-ψα` above: its natural shape
   -- `bplus x y₂ <ᵇ bplus x z₂` shares the binder `x` on both sides.
-  <ᵇ-+ω  : ∀ {x y}     → x <ᵇ bOmega ω → bplus x y <ᵇ bOmega ω
-  <ᵇ-+ψω : ∀ {x y α}   → x <ᵇ bpsi ω α → bplus x y <ᵇ bpsi ω α
+  <ᵇ-+Ω  : ∀ {x y μ}   → x <ᵇ bOmega μ → bplus x y <ᵇ bOmega μ
+  <ᵇ-+ψ  : ∀ {x y ν α} → x <ᵇ bpsi ν α → bplus x y <ᵇ bpsi ν α
   <ᵇ-+1  : ∀ {x₁ x₂ y₁ y₂} → x₁ <ᵇ y₁ → bplus x₁ x₂ <ᵇ bplus y₁ y₂
 
 infix 4 _<ᵇ_
@@ -121,8 +117,8 @@ infix 4 _<ᵇ_
 <ᵇ-trans <ᵇ-0-Ω       (<ᵇ-Ω+ _)            = <ᵇ-0-+
 -- Left leg: <ᵇ-0-+ (x = bzero, y = bplus _ _)
 <ᵇ-trans <ᵇ-0-+       (<ᵇ-+1 _)            = <ᵇ-0-+
-<ᵇ-trans <ᵇ-0-+       (<ᵇ-+ω _)            = <ᵇ-0-Ω
-<ᵇ-trans <ᵇ-0-+       (<ᵇ-+ψω _)           = <ᵇ-0-ψ
+<ᵇ-trans <ᵇ-0-+       (<ᵇ-+Ω _)            = <ᵇ-0-Ω
+<ᵇ-trans <ᵇ-0-+       (<ᵇ-+ψ _)            = <ᵇ-0-ψ
 -- Left leg: <ᵇ-0-ψ (x = bzero, y = bpsi _ _)
 <ᵇ-trans <ᵇ-0-ψ       (<ᵇ-ψΩ _)            = <ᵇ-0-ψ
 <ᵇ-trans <ᵇ-0-ψ       (<ᵇ-ψ+ _)            = <ᵇ-0-+
@@ -143,57 +139,71 @@ infix 4 _<ᵇ_
 <ᵇ-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)
+<ᵇ-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
+<ᵇ-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 (<ᵇ-ψΩ≤ ω≤ω))
+<ᵇ-trans (<ᵇ-ψ+ p)    (<ᵇ-+Ω q)            = <ᵇ-trans p q
+<ᵇ-trans (<ᵇ-ψ+ p)    (<ᵇ-+ψ q)            = <ᵇ-trans p q
+-- Left leg: <ᵇ-+Ω (x = bplus _ _, y = bOmega _)
+<ᵇ-trans (<ᵇ-+Ω p)    (<ᵇ-ΩΩ q)            = <ᵇ-+Ω (<ᵇ-trans p (<ᵇ-ΩΩ q))
+<ᵇ-trans (<ᵇ-+Ω p)    (<ᵇ-Ωψ q)            = <ᵇ-+ψ (<ᵇ-trans p (<ᵇ-Ωψ q))
+<ᵇ-trans (<ᵇ-+Ω p)    (<ᵇ-Ω+ q)            = <ᵇ-+1 (<ᵇ-trans p q)
+-- Left leg: <ᵇ-+ψ (x = bplus _ _, y = bpsi _ _)
+<ᵇ-trans (<ᵇ-+ψ p)    (<ᵇ-ψΩ q)            = <ᵇ-+ψ (<ᵇ-trans p (<ᵇ-ψΩ q))
+<ᵇ-trans (<ᵇ-+ψ p)    (<ᵇ-ψΩ≤ q)           = <ᵇ-+Ω (<ᵇ-trans p (<ᵇ-ψΩ≤ q))
+<ᵇ-trans (<ᵇ-+ψ p)    (<ᵇ-ψ+ q)            = <ᵇ-+1 (<ᵇ-trans p q)
 -- Right leg: <ᵇ-ψΩ≤ (y = bpsi _ _, z = bOmega _)
 <ᵇ-trans <ᵇ-0-ψ       (<ᵇ-ψΩ≤ _)           = <ᵇ-0-Ω
 <ᵇ-trans (<ᵇ-Ωψ p)    (<ᵇ-ψΩ≤ q)           = <ᵇ-ΩΩ (<Ω-≤Ω-trans p q)
 
-----------------------------------------------------------------------------
--- WF-2 open-case inversions (Ω vs +)
+-- WF-2 mixed-head inversions (Ω vs +)
 ----------------------------------------------------------------------------
 
--- The Ω→+ bridge is admitted (`<ᵇ-Ω+`), while the non-top
--- bplus→Ω case remains deferred.
+-- Mixed-head bridges now run both ways between `bplus` and `bOmega`.
 
 <ᵇ-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 ()
+<ᵇ-inv-+Ω : ∀ {x y μ} → bplus x y <ᵇ bOmega μ → x <ᵇ bOmega μ
+<ᵇ-inv-+Ω (<ᵇ-+Ω x<Ω) = x<Ω
+
+<ᵇ-inv-+Ωfin : ∀ {x y n} → bplus x y <ᵇ bOmega (fin n) → x <ᵇ bOmega (fin n)
+<ᵇ-inv-+Ωfin = <ᵇ-inv-+Ω
 
 -- Inversion for the admitted top-marker bridge.
 <ᵇ-inv-+Ωω : ∀ {x y} → bplus x y <ᵇ bOmega ω → x <ᵇ bOmega ω
-<ᵇ-inv-+Ωω (<ᵇ-+ω x<ω) = x<ω
+<ᵇ-inv-+Ωω = <ᵇ-inv-+Ω
 
-----------------------------------------------------------------------------
--- WF-2 open-case inversions (ψ vs +)
+-- WF-2 mixed-head inversions (ψ vs +)
 ----------------------------------------------------------------------------
 
--- The ψ→+ bridge is admitted (`<ᵇ-ψ+`), while the non-top
--- bplus→ψ case remains deferred.
+-- Mixed-head bridges now run both ways between `bplus` and `bpsi`.
 
 <ᵇ-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 ()
+<ᵇ-inv-+ψ : ∀ {x y ν α} → bplus x y <ᵇ bpsi ν α → x <ᵇ bpsi ν α
+<ᵇ-inv-+ψ (<ᵇ-+ψ x<ψ) = x<ψ
+
+<ᵇ-inv-+ψfin : ∀ {x y n α} → bplus x y <ᵇ bpsi (fin n) α → x <ᵇ bpsi (fin n) α
+<ᵇ-inv-+ψfin = <ᵇ-inv-+ψ
 
 -- Inversion for the admitted top-marker bridge.
 <ᵇ-inv-+ψω : ∀ {x y α} → bplus x y <ᵇ bpsi ω α → x <ᵇ bpsi ω α
-<ᵇ-inv-+ψω (<ᵇ-+ψω x<ψω) = x<ψω
+<ᵇ-inv-+ψω = <ᵇ-inv-+ψ
+
+-- Backwards-compatible specialised names for the former top-marker-only
+-- constructors.
+<ᵇ-+ω : ∀ {x y} → x <ᵇ bOmega ω → bplus x y <ᵇ bOmega ω
+<ᵇ-+ω = <ᵇ-+Ω
+
+<ᵇ-+ψω : ∀ {x y α} → x <ᵇ bpsi ω α → bplus x y <ᵇ bpsi ω α
+<ᵇ-+ψω = <ᵇ-+ψ
 
 ----------------------------------------------------------------------------
 -- Strict-below-ψ examples, for downstream ordering checks

proofs/agda/Ordinal/Buchholz/Smoke.agda

@@ -57,15 +57,19 @@ open import Ordinal.Buchholz.Order using
   ; <ᵇ-ψΩ≤
   ; <ᵇ-Ω+
   ; <ᵇ-ψ+
+  ; <ᵇ-+Ω
+  ; <ᵇ-+ψ
   ; <ᵇ-+ω
   ; <ᵇ-+ψω
   ; <ᵇ-+1
   ; <ᵇ-irrefl
   ; <ᵇ-trans
   ; <ᵇ-inv-Ω+
+  ; <ᵇ-inv-+Ω
   ; <ᵇ-inv-+Ωfin
   ; <ᵇ-inv-+Ωω
   ; <ᵇ-inv-ψ+
+  ; <ᵇ-inv-+ψ
   ; <ᵇ-inv-+ψfin
   ; <ᵇ-inv-+ψω
   )

proofs/agda/Ordinal/Buchholz/VeblenIdentityModel.agda

@@ -23,8 +23,8 @@ open import Ordinal.Buchholz.Order using
   ; <ᵇ-ψΩ≤
   ; <ᵇ-Ω+
   ; <ᵇ-ψ+
-  ; <ᵇ-+ω
-  ; <ᵇ-+ψω
+  ; <ᵇ-+Ω
+  ; <ᵇ-+ψ
   ; <ᵇ-+1
   )
 open import Ordinal.Buchholz.WellFounded using (wf-<ᵇ)
@@ -46,8 +46,8 @@ identity-interface dec-ψα dec-+2 = record
   ; dec-ψΩ≤ = <ᵇ-ψΩ≤
   ; dec-Ω+ = <ᵇ-Ω+
   ; dec-ψ+ = <ᵇ-ψ+
-  ; dec-+ω = <ᵇ-+ω
-  ; dec-+ψω = <ᵇ-+ψω
+  ; dec-+Ω = <ᵇ-+Ω
+  ; dec-+ψ = <ᵇ-+ψ
   ; dec-+1 = <ᵇ-+1
   ; dec-ψα = dec-ψα
   ; dec-+2 = dec-+2

proofs/agda/Ordinal/Buchholz/VeblenInterface.agda

@@ -30,8 +30,8 @@ open import Ordinal.Buchholz.Order using
   ; <ᵇ-ψΩ≤
   ; <ᵇ-Ω+
   ; <ᵇ-ψ+
-  ; <ᵇ-+ω
-  ; <ᵇ-+ψω
+  ; <ᵇ-+Ω
+  ; <ᵇ-+ψ
   ; <ᵇ-+1
   )
 
@@ -57,8 +57,8 @@ record VeblenWFInterface {ℓm ℓr : Level}
     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-+Ω   : ∀ {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.
@@ -75,8 +75,8 @@ record VeblenWFInterface {ℓm ℓr : Level}
   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 (<ᵇ-+Ω 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

proofs/agda/Ordinal/Buchholz/WellFounded.agda

@@ -36,8 +36,8 @@ open import Ordinal.Buchholz.Order using
   ; <ᵇ-ψΩ≤
   ; <ᵇ-Ω+
   ; <ᵇ-ψ+
-  ; <ᵇ-+ω
-  ; <ᵇ-+ψω
+  ; <ᵇ-+Ω
+  ; <ᵇ-+ψ
   ; <ᵇ-+1
   )
 
@@ -90,13 +90,13 @@ mutual
     predOmega (<ᵇ-ψΩ≤ {α = α} ν≤μ) with ≤Ω-split ν≤μ
     ... | inj₁ ν<μ = proj₂ (<ᵇ-bundle-fromΩ (rsμ ν<μ)) α
     ... | inj₂ refl = psiAcc α
-    predOmega (<ᵇ-+ω {x = x} {y = y} x<ω) = <ᵇ-acc-bplus-from (predOmega x<ω) y
+    predOmega (<ᵇ-+Ω {x = x} {y = y} x<μ) = <ᵇ-acc-bplus-from (predOmega x<μ) y
 
     predPsi : (α : BT) → ∀ {x} → x <ᵇ bpsi μ α → Acc _<ᵇ_ x
     predPsi α <ᵇ-0-ψ = <ᵇ-acc-bzero
     predPsi α (<ᵇ-Ωψ κ<μ) = proj₁ (<ᵇ-bundle-fromΩ (rsμ κ<μ))
     predPsi α (<ᵇ-ψΩ {α = β} κ<μ) = proj₂ (<ᵇ-bundle-fromΩ (rsμ κ<μ)) β
-    predPsi α (<ᵇ-+ψω {x = x} {y = y} x<ψω) = <ᵇ-acc-bplus-from (predPsi α x<ψω) y
+    predPsi α (<ᵇ-+ψ {x = x} {y = y} x<ψ) = <ᵇ-acc-bplus-from (predPsi α x<ψ) y
 
     psiAcc : (α : BT) → Acc _<ᵇ_ (bpsi μ α)
     psiAcc α = acc (predPsi α)

proofs/agda/Smoke.agda

@@ -184,15 +184,19 @@ open import Ordinal.Buchholz.Order using
   ; <ᵇ-ψΩ≤
   ; <ᵇ-Ω+
   ; <ᵇ-ψ+
+  ; <ᵇ-+Ω
+  ; <ᵇ-+ψ
   ; <ᵇ-+ω
   ; <ᵇ-+ψω
   ; <ᵇ-+1
   ; <ᵇ-irrefl
   ; <ᵇ-trans
   ; <ᵇ-inv-Ω+
+  ; <ᵇ-inv-+Ω
   ; <ᵇ-inv-+Ωfin
   ; <ᵇ-inv-+Ωω
   ; <ᵇ-inv-ψ+
+  ; <ᵇ-inv-+ψ
   ; <ᵇ-inv-+ψfin
   ; <ᵇ-inv-+ψω
   ; bzero<Ω0

readme.adoc

@@ -83,12 +83,15 @@ Ordinal/Buchholz track status:
 * Left-summand bridges into additive terms are admitted and inverted:
 ** `<ᵇ-Ω+`, `<ᵇ-ψ+`
 ** `<ᵇ-inv-Ω+`, `<ᵇ-inv-ψ+`
+* General additive-target bridges are now admitted and inverted:
+** `<ᵇ-+Ω`, `<ᵇ-+ψ`
+** `<ᵇ-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` 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 non-top `bplus` vs `bOmega`/`bpsi` comparisons and for the shared-binder cases (`<ᵇ-ψα`, `<ᵇ-+2`) in a `--without-K`-compatible style.
+* Open work is now concentrated in the shared-binder cases (`<ᵇ-ψα`, `<ᵇ-+2`) and their discharge into a `--without-K`-compatible measure model.
 
 == External Bridge Targets (local workspace)