Add Ω/+ open-case inversion lemmas for Buchholz order

Author: hyperpolymath

proofs/agda/Ordinal/Buchholz/Order.agda

@@ -115,6 +115,20 @@ infix 4 _<ᵇ_
 -- Left leg: <ᵇ-+1 (x = bplus _ _, y = bplus _ _)
 <ᵇ-trans (<ᵇ-+1 p)    (<ᵇ-+1 q)            = <ᵇ-+1 (<ᵇ-trans p q)
 
+----------------------------------------------------------------------------
+-- 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.
+
+<ᵇ-inv-Ω+ : ∀ {μ x y} → bOmega μ <ᵇ bplus x y → ⊥
+<ᵇ-inv-Ω+ ()
+
+<ᵇ-inv-+Ω : ∀ {x y μ} → bplus x y <ᵇ bOmega μ → ⊥
+<ᵇ-inv-+Ω ()
+
 ----------------------------------------------------------------------------
 -- Strict-below-ψ examples, for downstream ordering checks
 ----------------------------------------------------------------------------

proofs/agda/Smoke.agda

@@ -181,6 +181,8 @@ open import Ordinal.Buchholz.Order using
   ; <ᵇ-+1
   ; <ᵇ-irrefl
   ; <ᵇ-trans
+  ; <ᵇ-inv-Ω+
+  ; <ᵇ-inv-+Ω
   ; bzero<Ω0
   ; Ω0<Ω1
   ; Ω1<Ωω