fix: right-recursive _oplus_ + Phase 1.3 right-monotonicity (closes #34) (#39)

## Summary

Root cause: left-recursive _oplus_ made oplus-mono-less-right false at
limit alpha (counterexample in issue #34). Fix: flip _oplus_ to
right-recursive in Arithmetic.agda and add four helper lemmas to
Phase13.agda.

## Changes

Ordinal/Brouwer/Arithmetic.agda: flip _oplus_ equations, replace
oplus-oz-left with oplus-oz-right (right-unit is now definitional).

Ordinal/Brouwer/Phase13.agda: add le-self-osuc, le-weaken-osuc,
oplus-left-le-sum, and the mutual pair oplus-mono-less-right /
oplus-mono-le-right closing issue #34.

Smoke.agda: update import from oplus-oz-left to oplus-oz-right.

## Verification

agda -i proofs/agda proofs/agda/All.agda passes locally (full suite, 60+
modules).

Closes #34

Author: hyperpolymath

proofs/agda/Ordinal/Brouwer/Arithmetic.agda

@@ -3,21 +3,16 @@
 -- Phase 1.2 of the Option B programme (see `docs/buchholz-plan.adoc`).
 --
 -- Ordinal arithmetic on Brouwer notations: *definitions* only.
--- All non-trivial monotonicity proofs are scheduled for Phase 1.3,
--- where they may drive a small redesign of `_≤_` in the base
--- `Ordinal.Brouwer` module (the current data-type axiomatisation
--- proves key lemmas like `osuc-mono-≤` only with some care, and
--- the Phase 1.3 work will decide whether to add constructors or
--- switch to a recursive `_≤_`).
+-- All non-trivial monotonicity proofs are in Phase 1.3 (Phase13.agda).
 --
 -- Contents:
 --
--- * `_⊕_` — left-recursive naive ordinal sum. Not Hessenberg; the
---   full natural-sum definition (commutative + bi-monotonic) needs
---   more machinery than pays off for the rank we actually need.
---   This is the cheapest sum that still lets `psi-rank` propagate
---   ordinal-argument descent via right-monotonicity, which is the
---   only direction we need for Phase 2.2.
+-- * `_⊕_` — right-recursive ordinal sum. Recursion is on the right
+--   argument, mirroring `_≤′_`'s second-argument structure, so that
+--   `⊕-mono-<-right` and `⊕-mono-≤-right` are provable by structural
+--   induction on `γ` (see issue #34 for the counterexample that ruled
+--   out the original left-recursive form). Right-unit `α ⊕ oz = α` is
+--   definitional; left-unit `oz ⊕ β = β` is propositional (Phase 1.3).
 -- * `nat-to-ord` — the standard successor-stack encoding of ℕ.
 -- * `ω-rank : OmegaIndex → Ord` — rank for Ω-markers. `fin n` maps
 --   to `osuc^(n+1) oz`, `ω` maps to the canonical Brouwer ω.
@@ -35,19 +30,20 @@ open import Ordinal.OmegaMarkers using (OmegaIndex; fin; ω)
 open import Ordinal.Brouwer using (Ord; oz; osuc; olim)
 
 ----------------------------------------------------------------------------
--- Naive ordinal sum
+-- Ordinal sum (right-recursive)
 ----------------------------------------------------------------------------
 
--- Left-recursive: zero on the left is the unit definitionally,
--- successor on the left lifts the successor past the sum, limit on
--- the left distributes under the sum.
+-- Right-recursive: right-unit `α ⊕ oz = α` is definitional; successor
+-- on the right lifts past the sum; limit on the right distributes.
+-- This direction aligns with `_≤′_`'s second-argument recursion and
+-- makes `⊕-mono-<-right` provable by induction on γ (Phase 1.3).
 
 infixl 6 _⊕_
 
 _⊕_ : Ord → Ord → Ord
-oz      ⊕ β = β
-osuc α  ⊕ β = osuc (α ⊕ β)
-olim f  ⊕ β = olim (λ n → f n ⊕ β)
+α ⊕ oz      = α
+α ⊕ osuc β  = osuc (α ⊕ β)
+α ⊕ olim f  = olim (λ n → α ⊕ f n)
 
 ----------------------------------------------------------------------------
 -- Rank target for Ω-indices
@@ -95,10 +91,7 @@ open import Ordinal.Brouwer using (one; two)
 ω-rank-fin1 : ω-rank (fin 1) ≡ two
 ω-rank-fin1 = refl
 
--- `psi-rank ν oz = osuc (ω-rank ν ⊕ oz)`. Since `⊕`'s right-identity
--- is only up to `≤` (proved in Phase 1.3), we don't state `≡` here.
+-- Right-unit of `⊕` is definitional.
 
--- Left-unit of `⊕` is definitional.
-
-⊕-oz-left : ∀ β → oz ⊕ β ≡ β
-⊕-oz-left _ = refl
+⊕-oz-right : ∀ α → α ⊕ oz ≡ α
+⊕-oz-right _ = refl

proofs/agda/Ordinal/Brouwer/Phase13.agda

@@ -30,6 +30,13 @@
 --   on `Ord` mirroring `Ordinal.Brouwer.wf-<`.  Predecessor lemmas
 --   `pred-of-osuc-<′` and `pred-of-olim-<′` reduce through the
 --   computed shape of `_<′_` rather than constructor pattern-match.
+-- * `≤′-self-osuc` — every ordinal is below its successor: x ≤′ osuc x.
+-- * `≤′-weaken-osuc` — weakening: x ≤′ y → x ≤′ osuc y.
+-- * `⊕-left-≤-sum` — left addend ≤ sum: α ≤′ α ⊕ γ.
+-- * `⊕-mono-≤-right` — `_⊕_` is monotone on the right w.r.t. `≤′`.
+-- * `⊕-mono-<-right` — `_⊕_` is strictly monotone on the right
+--   w.r.t. `<′`.  Closes the `<ᵇʳᶠ-ψα` and `<ᵇʳᶠ-+2` cases of
+--   `rank-mono` in `Ordinal.Buchholz.RankBrouwer` (issue #34).
 --
 -- ## Closure of the original obstacle
 --
@@ -49,6 +56,7 @@ open import Data.Empty using (⊥; ⊥-elim)
 open import Induction.WellFounded using (Acc; acc; WellFounded)
 
 open import Ordinal.Brouwer using (Ord; oz; osuc; olim)
+open import Ordinal.Brouwer.Arithmetic using (_⊕_)
 
 ----------------------------------------------------------------------------
 -- Recursive `_≤′_` per the Echidna SA recommendation
@@ -189,3 +197,69 @@ wf-<′ : WellFounded _<′_
 wf-<′ oz       = acc (λ {β} ())
 wf-<′ (osuc α) = acc (pred-of-osuc-<′ (wf-<′ α))
 wf-<′ (olim f) = acc (pred-of-olim-<′ (λ n → wf-<′ (f n)))
+
+----------------------------------------------------------------------------
+-- x ≤′ osuc x (every ordinal is strictly below its successor)
+----------------------------------------------------------------------------
+
+-- Structural recursion on x.  The `olim f` case uses f-in-lim′ to
+-- route through the branch: f n ≤′ osuc (f n) ≤′ osuc (olim f).
+-- The last step holds because `osuc (f n) ≤′ osuc (olim f)` reduces
+-- definitionally to `f n ≤′ olim f`, which is f-in-lim′.
+
+≤′-self-osuc : ∀ x → x ≤′ osuc x
+≤′-self-osuc oz       = tt
+≤′-self-osuc (osuc x) = ≤′-self-osuc x
+≤′-self-osuc (olim f) = λ n →
+  ≤′-trans {f n} {osuc (f n)} {osuc (olim f)}
+    (≤′-self-osuc (f n))
+    (f-in-lim′ f n)
+
+-- Weakening: x ≤′ y → x ≤′ osuc y.  One-liner via transitivity and
+-- ≤′-self-osuc; no case analysis needed.
+
+≤′-weaken-osuc : ∀ {x y} → x ≤′ y → x ≤′ osuc y
+≤′-weaken-osuc {x} {y} p = ≤′-trans {x} {y} {osuc y} p (≤′-self-osuc y)
+
+----------------------------------------------------------------------------
+-- α ≤′ α ⊕ γ (left addend is always ≤ the sum)
+----------------------------------------------------------------------------
+
+-- Structural recursion on γ.  Right-recursive `_⊕_` is essential:
+-- each case of γ reduces `α ⊕ γ` to a form whose `_≤′_` target is
+-- immediately dischargeable.
+
+⊕-left-≤-sum : ∀ {α} γ → α ≤′ α ⊕ γ
+⊕-left-≤-sum {α}        oz       = ≤′-refl {α}
+⊕-left-≤-sum {α}        (osuc γ') = ≤′-weaken-osuc {α} {α ⊕ γ'} (⊕-left-≤-sum {α} γ')
+⊕-left-≤-sum {α}        (olim g)  =
+  ≤′-trans {α} {α ⊕ g 0} {α ⊕ olim g}
+    (⊕-left-≤-sum {α} (g 0))
+    (f-in-lim′ (λ n → α ⊕ g n) 0)
+
+----------------------------------------------------------------------------
+-- Right monotonicity of `_⊕_` (issue #34 fix)
+----------------------------------------------------------------------------
+
+-- `⊕-mono-<-right` and `⊕-mono-≤-right` are mutually recursive.
+-- Both induct primarily on γ (for <) or β (for ≤), with the other
+-- position decreasing in cross-calls.  Agda's termination checker
+-- accepts the lex pair (β, γ) as the measure.
+--
+-- Right-recursive `_⊕_` is the enabling change: each constructor of
+-- γ in `⊕-mono-<-right` matches exactly one clause of `_≤′_`'s
+-- second-argument computation, giving a direct proof path.
+
+mutual
+
+  ⊕-mono-<-right : ∀ {α β γ} → β <′ γ → α ⊕ β <′ α ⊕ γ
+  ⊕-mono-<-right {_} {_} {oz}      ()
+  ⊕-mono-<-right {α} {β} {osuc γ'} p       = ⊕-mono-≤-right {α} {β}  {γ'} p
+  ⊕-mono-<-right {α} {β} {olim g}  (n , p) = n , ⊕-mono-<-right {α} {β} {g n} p
+
+  ⊕-mono-≤-right : ∀ {α β γ} → β ≤′ γ → α ⊕ β ≤′ α ⊕ γ
+  ⊕-mono-≤-right {α} {oz}      {γ}       _       = ⊕-left-≤-sum {α} γ
+  ⊕-mono-≤-right {_} {osuc _}  {oz}      ()
+  ⊕-mono-≤-right {α} {osuc β'} {osuc γ'} p       = ⊕-mono-≤-right {α} {β'} {γ'} p
+  ⊕-mono-≤-right {α} {osuc β'} {olim g}  (n , p) = n , ⊕-mono-<-right {α} {β'} {g n} p
+  ⊕-mono-≤-right {α} {olim f}  {γ}       p       = λ n → ⊕-mono-≤-right {α} {f n} {γ} (p n)

proofs/agda/Smoke.agda

@@ -260,7 +260,7 @@ open import Ordinal.Brouwer.Arithmetic using
   ; nat-to-ord
   ; ω-rank
   ; psi-rank
-  ; ⊕-oz-left
+  ; ⊕-oz-right
   ; ω-rank-fin0
   ; ω-rank-fin1
   )
@@ -432,3 +432,4 @@ open import Ordinal.Buchholz.WellFormed using
   ; psi-OmegaOmega
   ; psi-OmegaOmega-wf
   )
+