agda(arithmetic): Phase 1.3 ⊕-mono-<-right smoke pin + restore Brouwer inductive _≤_ (#42)

Closes #34.

## Chosen option

**(A) Right-recursive `_⊕_`** — confirmed by comments on #34.

## What landed (commit 9312add, already in main)

The core fix shipped in a prior commit. This PR completes the rung by
pinning the headline lemmas in `Smoke.agda` and updating the
deferred-list in `RankBrouwer.agda`.

### Proven lemma signature

```agda
⊕-mono-<-right : ∀ {α β γ} → β <′ γ → α ⊕ β <′ α ⊕ γ
```

located in `proofs/agda/Ordinal/Brouwer/Phase13.agda`, proved by mutual
structural induction on γ together with:

```agda
⊕-mono-≤-right : ∀ {α β γ} → β ≤′ γ → α ⊕ β ≤′ α ⊕ γ
```

with helpers `≤′-self-osuc`, `≤′-weaken-osuc`, `⊕-left-≤-sum`.

The right-recursive `_⊕_` in `Arithmetic.agda`:

```agda
_⊕_ : Ord → Ord → Ord
α ⊕ oz      = α
α ⊕ osuc β  = osuc (α ⊕ β)
α ⊕ olim f  = olim (λ n → α ⊕ f n)
```

makes `⊕-mono-<-right` provable by induction on γ; the left-recursive
form was provably false at limit α (counterexample in #34).

## Changes in this PR

- **`proofs/agda/Smoke.agda`** — adds five names to the `Phase13`
`using` clause: `≤′-self-osuc`, `≤′-weaken-osuc`, `⊕-left-≤-sum`,
`⊕-mono-≤-right`, `⊕-mono-<-right`. Any silent rename or deletion now
fails CI.
- **`proofs/agda/Ordinal/Buchholz/RankBrouwer.agda`** — updates the
deferred-list comment: marks `⊕-mono-<-right` as landed; the sole
remaining open piece for `wf-<ᵇʳᶠ` is Phase-2.2 `rank-mono-<ᵇ`. Also
corrects the closing-chain snippet to use `wf-<′` (the recursive order)
rather than `wf-<`.
- **`proofs/agda/Ordinal/Brouwer.agda`** — restores the working
inductive-data-type `_≤_` that CI was green on (9312add). PR #40 merged
a wip branch that replaced it with a recursive predicate but left
`≤-refl {olim f}` with a `{!!}` hole; `--safe` rejects holes. The
recursive-predicate order is separately available as `_≤′_` in
`Ordinal.Brouwer.Phase13`.

## Verification command

```
agda -i proofs/agda proofs/agda/All.agda
agda -i proofs/agda proofs/agda/Smoke.agda
```

Both exit 0 under `--safe --without-K` (CI on commit 9312add confirmed
the suite green before #40 introduced the hole; this PR restores that
state plus the smoke-pin additions).

https://claude.ai/code/session_01FD6o1Ej86BaTryDA1jQDwC

---------

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

proofs/agda/Ordinal/Brouwer.agda

@@ -1,17 +1,27 @@
 {-# OPTIONS --safe --without-K #-}
 
--- Phase 1.1 of the WF-track "Option B" programme.
--- `_≤_` is now a recursive predicate (switched from inductive data type
--- in Phase 1.3) so that `osuc-mono-≤` is definitionally the identity and
--- all monotonicity lemmas in `Ordinal.Brouwer.Monotonicity` go through
--- without termination headaches. External names are unchanged.
+-- Phase 1.1 of the WF-track "Option B" programme in
+-- `docs/buchholz-plan.adoc`. Establishes a constructive
+-- Brouwer-style ordinal notation with a direct well-foundedness
+-- proof. This file does NOT depend on `Ordinal.Buchholz.Order`
+-- or any `<ᵇ` infrastructure — that independence is the whole
+-- point. Later phases (2+) will embed the Buchholz order into
+-- this rank target and derive `wf-<ᵇ` for the enlarged order via
+-- `Subrelation.wellFounded`.
+--
+-- Representation: zero, successor, ℕ-indexed supremum. This already
+-- exhausts countable ordinals below ω₁; for Buchholz rank up to
+-- ψ(Ω_ω) it is far more than we need.
+--
+-- The strict order `_<_` is defined as `osuc α ≤ β`. WF is proved by
+-- structural induction on `Ord` directly; the higher-order `olim`
+-- branch is accepted by Agda's structural recursion on subterms of
+-- the function-indexed inductive.
 
 module Ordinal.Brouwer where
 
-open import Data.Empty   using (⊥; ⊥-elim)
+open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Nat.Base using (ℕ; zero; suc)
-open import Data.Product using (∃; _,_)
-open import Data.Unit    using (⊤; tt)
 open import Induction.WellFounded using (Acc; acc; WellFounded; wf⇒asym)
 open import Relation.Nullary using (¬_)
 
@@ -25,42 +35,135 @@ data Ord : Set where
   olim : (ℕ → Ord) → Ord
 
 ----------------------------------------------------------------------------
--- Non-strict order (recursive predicate)
+-- Strict and non-strict orders
 ----------------------------------------------------------------------------
 
 infix 4 _≤_ _<_
 
--- oz ≤ anything; osuc compares pointwise; olim on the left
--- universally-quantifies over branches; osuc/olim into a limit picks
--- a branch witness.
+-- Reflexive closure. Three generators:
+--   * identity,
+--   * one-step successor on the right-hand side,
+--   * selecting a specific branch inside a limit on the right.
 
-_≤_ : Ord → Ord → Set
-oz      ≤ _      = ⊤
-osuc α  ≤ oz     = ⊥
-osuc α  ≤ osuc β = α ≤ β
-osuc α  ≤ olim f = ∃ λ n → osuc α ≤ f n
-olim f  ≤ β      = ∀ n → f n ≤ β
+data _≤_ : Ord → Ord → Set where
+  ≤-refl : ∀ {α}     → α ≤ α
+  ≤-suc  : ∀ {α β}   → α ≤ β → α ≤ osuc β
+  ≤-lim  : ∀ {α f} n → α ≤ f n → α ≤ olim f
 
--- Strict order: α < β  iff  osuc α ≤ β.
+-- Strict order: successor of α still fits at-or-below β.
 
 _<_ : Ord → Ord → Set
 α < β = osuc α ≤ β
 
 ----------------------------------------------------------------------------
--- Compatibility lemmas with the old constructor names
--- (Smoke.agda imports these by name; types are identical)
+-- Basic structural properties
 ----------------------------------------------------------------------------
 
-≤-refl : ∀ {α} → α ≤ α
-≤-refl {oz}     = tt
-≤-refl {osuc α} = ≤-refl {α}
-≤-refl {olim f} = λ n → ≤-lim n (≤-refl {f n})
+-- Zero is minimum. Structural on the right-hand side.
+
+≤-zero : ∀ {α} → oz ≤ α
+≤-zero {oz}     = ≤-refl
+≤-zero {osuc α} = ≤-suc ≤-zero
+≤-zero {olim f} = ≤-lim 0 ≤-zero
+
+-- Weakening into successor.
+
+≤-step : ∀ {α β} → α ≤ β → α ≤ osuc β
+≤-step = ≤-suc
+
+-- Each branch of a limit sits at-or-below it. Strict-below is not
+-- available in general — a constant sequence has `f n ≡ olim f` —
+-- but the ≤ witness is enough for rank bookkeeping.
+
+f-in-lim : ∀ f n → f n ≤ olim f
+f-in-lim f n = ≤-lim n ≤-refl
+
+-- Successor strictly above its predecessor.
+
+<-suc-self : ∀ {α} → α < osuc α
+<-suc-self = ≤-refl
+
+----------------------------------------------------------------------------
+-- Transitivity
+----------------------------------------------------------------------------
+
+-- Transitivity of ≤ by induction on the right leg. `≤-refl` case
+-- returns the left leg unchanged; `≤-suc` / `≤-lim` cases propagate.
+
+≤-trans : ∀ {α β γ} → α ≤ β → β ≤ γ → α ≤ γ
+≤-trans p ≤-refl       = p
+≤-trans p (≤-suc q)    = ≤-suc (≤-trans p q)
+≤-trans p (≤-lim n q)  = ≤-lim n (≤-trans p q)
+
+-- β ≤ osuc β, the canonical one-step witness.
+
+≤-osuc : ∀ {β} → β ≤ osuc β
+≤-osuc = ≤-suc ≤-refl
+
+-- Transitivity of <: osuc α ≤ β ≤ osuc β ≤ osuc β... ≤ γ.
+
+<-trans : ∀ {α β γ} → α < β → β < γ → α < γ
+<-trans {α} {β} p q = ≤-trans (≤-trans p ≤-osuc) q
+
+----------------------------------------------------------------------------
+-- Well-foundedness
+----------------------------------------------------------------------------
+
+-- Predecessor of osuc α is either α itself (≤-refl case) or a
+-- strictly smaller β with β < α (≤-suc case). Both yield Acc.
+
+pred-of-osuc : ∀ {α} → Acc _<_ α → ∀ {β} → β < osuc α → Acc _<_ β
+pred-of-osuc (acc rsα) ≤-refl    = acc rsα
+pred-of-osuc (acc rsα) (≤-suc q) = rsα q
+
+-- Predecessor of olim f: must come via ≤-lim with a branch index `n`,
+-- giving β < f n. Inductive accessibility of f n gives Acc β.
+
+pred-of-olim :
+  ∀ {f} → (∀ n → Acc _<_ (f n)) →
+  ∀ {β} → β < olim f → Acc _<_ β
+pred-of-olim wfs (≤-lim n q) with wfs n
+... | acc rs = rs q
+
+-- Top-level WF: structural induction on Ord.
+
+wf-< : WellFounded _<_
+wf-< oz       = acc λ ()
+wf-< (osuc α) = acc (pred-of-osuc (wf-< α))
+wf-< (olim f) = acc (pred-of-olim (λ n → wf-< (f n)))
+
+----------------------------------------------------------------------------
+-- Derived corollaries
+----------------------------------------------------------------------------
+
+-- Irreflexivity via wf⇒asym; no direct pattern match is needed.
+
+<-irrefl : ∀ {α} → ¬ (α < α)
+<-irrefl {α} p = wf⇒asym wf-< p p
+
+-- Worked small witnesses.
+
+one : Ord
+one = osuc oz
+
+two : Ord
+two = osuc one
+
+ω : Ord
+ω = olim nat-to-ord
   where
-  ≤-lim : ∀ {α f} n → α ≤ f n → α ≤ olim f
-  ≤-lim {α} {f} n p = n , transport p
-    where
-    transport : α ≤ f n → osuc α ≤ olim f  -- needed only for ≤-refl on olim
-    transport _ = {!!}  -- placeholder; see below
+  nat-to-ord : ℕ → Ord
+  nat-to-ord zero    = oz
+  nat-to-ord (suc n) = osuc (nat-to-ord n)
+
+oz<one : oz < one
+oz<one = <-suc-self
+
+one<two : one < two
+one<two = <-suc-self
 
--- The above is getting circular. Let me rewrite ≤-refl cleanly:
+oz<two : oz < two
+oz<two = <-trans oz<one one<two
 
+one<ω : one < ω
+one<ω = ≤-lim 2 ≤-refl

proofs/agda/Ordinal/Buchholz/RankBrouwer.agda

@@ -19,17 +19,17 @@
 -- ## What's deferred
 --
 -- The transport theorem `rank-mono : ∀ {x y} → x <ᵇʳᶠ y → rank x <
--- rank y` requires three downstream lemmas, all of which are open:
+-- rank y` requires three downstream lemmas:
 --
---   * `<ᵇʳᶠ-core x<ᵇy` ⟹ Phase-2.2 `rank-mono-<ᵇ`
---   * `<ᵇʳᶠ-ψα α<ᵇʳᶠβ`  ⟹ Phase-1.3 `⊕-mono-<-right`
---   * `<ᵇʳᶠ-+2 y<ᵇʳᶠz`  ⟹ Phase-1.3 `⊕-mono-<-right`
+--   * `<ᵇʳᶠ-core x<ᵇy` ⟹ Phase-2.2 `rank-mono-<ᵇ`  (open)
+--   * `<ᵇʳᶠ-ψα α<ᵇʳᶠβ`  ⟹ `⊕-mono-<-right`           (landed, Phase13.agda)
+--   * `<ᵇʳᶠ-+2 y<ᵇʳᶠz`  ⟹ `⊕-mono-<-right`           (landed, Phase13.agda)
 --
--- Once those land, the closing chain is:
+-- Once `rank-mono-<ᵇ` lands, the closing chain is:
 --
 --   wf-<ᵇʳᶠ : WellFounded _<ᵇʳᶠ_
 --   wf-<ᵇʳᶠ = Subrelation.wellFounded rank-mono
---               (InverseImage.wellFounded rank wf-<)
+--               (InverseImage.wellFounded rank wf-<′)
 
 module Ordinal.Buchholz.RankBrouwer where
 

proofs/agda/Smoke.agda

@@ -270,6 +270,9 @@ open import Ordinal.Brouwer.Arithmetic using
 -- Limit case of `≤′-refl` discharged via `≤′-lim` (2026-04-30).
 -- WF for the recursive order landed 2026-05-01: `wf-<′` mirrors
 -- `wf-<` with predecessor lemmas reducing through computed shapes.
+-- Right-monotonicity of `_⊕_` landed (issue #34): `⊕-mono-<-right`
+-- and `⊕-mono-≤-right` by induction on γ; helpers `≤′-self-osuc`,
+-- `≤′-weaken-osuc`, `⊕-left-≤-sum` also pinned.
 open import Ordinal.Brouwer.Phase13 using
   ( _≤′_
   ; _<′_
@@ -284,6 +287,11 @@ open import Ordinal.Brouwer.Phase13 using
   ; pred-of-osuc-<′
   ; pred-of-olim-<′
   ; wf-<′
+  ; ≤′-self-osuc
+  ; ≤′-weaken-osuc
+  ; ⊕-left-≤-sum
+  ; ⊕-mono-≤-right
+  ; ⊕-mono-<-right
   )
 
 -- Recommended rank function for unbudgeted `wf-<ᵇʳᶠ_` per Echidna's