agda: add Ω+/ψ+ left-summand bridges for Buchholz order

Author: hyperpolymath

docs/buchholz-plan.adoc

@@ -113,16 +113,16 @@ 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): explicit inversion lemmas for the still-open
-  mixed head cases (`Ω/+`, `ψ/+`) and the newly admitted comparison
-  bridge `bpsi ν α <ᵇ bOmega μ` under `ν ≤Ω μ`.
+* 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/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

proofs/agda/Ordinal/Buchholz/VeblenIdentityModel.agda

@@ -21,6 +21,8 @@ open import Ordinal.Buchholz.Order using
   ; <ᵇ-Ωψ
   ; <ᵇ-ψΩ
   ; <ᵇ-ψΩ≤
+  ; <ᵇ-Ω+
+  ; <ᵇ-ψ+
   ; <ᵇ-+ω
   ; <ᵇ-+ψω
   ; <ᵇ-+1
@@ -42,6 +44,8 @@ identity-interface dec-ψα dec-+2 = record
   ; dec-Ωψ = <ᵇ-Ωψ
   ; dec-ψΩ = <ᵇ-ψΩ
   ; dec-ψΩ≤ = <ᵇ-ψΩ≤
+  ; dec-Ω+ = <ᵇ-Ω+
+  ; dec-ψ+ = <ᵇ-ψ+
   ; dec-+ω = <ᵇ-+ω
   ; dec-+ψω = <ᵇ-+ψω
   ; dec-+1 = <ᵇ-+1

proofs/agda/Ordinal/Buchholz/VeblenInterface.agda

@@ -28,6 +28,8 @@ open import Ordinal.Buchholz.Order using
   ; <ᵇ-Ωψ
   ; <ᵇ-ψΩ
   ; <ᵇ-ψΩ≤
+  ; <ᵇ-Ω+
+  ; <ᵇ-ψ+
   ; <ᵇ-+ω
   ; <ᵇ-+ψω
   ; <ᵇ-+1
@@ -50,6 +52,10 @@ record VeblenWFInterface {ℓm ℓr : Level}
     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 ω α)
@@ -67,6 +73,8 @@ record VeblenWFInterface {ℓm ℓr : Level}
   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₁

proofs/agda/Ordinal/Buchholz/WellFounded.agda

@@ -34,6 +34,8 @@ open import Ordinal.Buchholz.Order using
   ; <ᵇ-Ωψ
   ; <ᵇ-ψΩ
   ; <ᵇ-ψΩ≤
+  ; <ᵇ-Ω+
+  ; <ᵇ-ψ+
   ; <ᵇ-+ω
   ; <ᵇ-+ψω
   ; <ᵇ-+1
@@ -64,6 +66,8 @@ mutual
 
   <ᵇ-pred-bplus-from : ∀ {α β x} → Acc _<ᵇ_ α → x <ᵇ bplus α β → Acc _<ᵇ_ x
   <ᵇ-pred-bplus-from _          <ᵇ-0-+                  = <ᵇ-acc-bzero
+  <ᵇ-pred-bplus-from (acc rsα)  (<ᵇ-Ω+ Ω<α)             = rsα Ω<α
+  <ᵇ-pred-bplus-from (acc rsα)  (<ᵇ-ψ+ ψ<α)             = rsα ψ<α
   <ᵇ-pred-bplus-from (acc rsα)  (<ᵇ-+1 {x₂ = x₂} x₁<α)  = <ᵇ-acc-bplus-from (rsα x₁<α) x₂
 
   <ᵇ-acc-bplus-from : ∀ {α} → Acc _<ᵇ_ α → (β : BT) → Acc _<ᵇ_ (bplus α β)

proofs/agda/Smoke.agda

@@ -182,6 +182,8 @@ open import Ordinal.Buchholz.Order using
   ; <ᵇ-Ωψ
   ; <ᵇ-ψΩ
   ; <ᵇ-ψΩ≤
+  ; <ᵇ-Ω+
+  ; <ᵇ-ψ+
   ; <ᵇ-+ω
   ; <ᵇ-+ψω
   ; <ᵇ-+1

readme.adoc

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