brouwer(arithmetic): checked refutations of strict-left-mono of _⊕_ and additive-principal closure on generic sums

proofs/agda/All.agda

@@ -107,6 +107,8 @@ open import Ordinal.Brouwer
 open import Ordinal.Brouwer.Arithmetic
 open import Ordinal.Brouwer.Phase13
 open import Ordinal.Brouwer.OmegaPow
+open import Ordinal.Brouwer.StrictLeftMonoRefuted
+open import Ordinal.Brouwer.AdditivePrincipalGenericRefuted
 open import Ordinal.Buchholz.Syntax
 open import Ordinal.Buchholz.Closure
 open import Ordinal.Buchholz.Order

proofs/agda/Ordinal/Brouwer/AdditivePrincipalGenericRefuted.agda

@@ -0,0 +1,107 @@
+{-# OPTIONS --safe --without-K #-}
+
+-- Checked refutation of "additive-principal closure on generic sums".
+--
+-- The Phase13/RankLexSlice3 design notes flag this as one of two
+-- potential unblock routes for the bplus-chain-level extension of
+-- the joint-bplus rank-mono primitive — but mark it as "not
+-- available", citing that `rank-adm y₁ = ω-rank-pow ν ⊕ rank-pow β`
+-- is a generic sum and the existing `additive-principal-ω-rank-pow`
+-- only applies to pure ω-powers (single-marker form).  This module
+-- promotes that prose claim into a CHECKED REFUTATION: the
+-- generic-sum form fails outright at the obvious counterexample
+-- (X = Y = ω; α = β = ω).
+--
+-- Concretely, the hypothesised property
+--
+--   AdditivePrincipalGenericSum :=
+--     ∀ {X Y α β} → α <′ X ⊕ Y → β <′ X ⊕ Y → α ⊕ β <′ X ⊕ Y
+--
+-- would imply `ω ⊕ ω <′ ω ⊕ ω` (irreflexive ⇒ ⊥) at
+-- `X = Y = α = β = olim nat-to-ord (= ω)`.  Both premises
+-- `ω <′ ω ⊕ ω` hold (branch 1 of the limit suffices via
+-- `osuc (olim f) ≤′ osuc (olim f ⊕ oz) = osuc (olim f)`); the
+-- conclusion contradicts `<′-irrefl`.
+--
+-- Cited by `Ordinal.Buchholz.RankLexSlice3` as the structural
+-- blocker for route (a) of its design-note's open follow-on plan.
+-- Promoting prose to a named theorem makes the closure-decision
+-- auditable.
+--
+-- ## What lands
+--
+--   * `AdditivePrincipalGenericSum` — the hypothesised property.
+--   * `ω<′ω⊕ω` — `olim nat-to-ord <′ olim nat-to-ord ⊕ olim nat-to-ord`,
+--     concretely via branch index 1 in the outer olim.
+--   * `additive-principal-generic-sum-refuted` — the headline
+--     `¬ AdditivePrincipalGenericSum`.
+--
+-- ## Headlines (pin in `Smoke.agda`)
+--
+--   * `AdditivePrincipalGenericSum`
+--   * `additive-principal-generic-sum-refuted`
+
+module Ordinal.Brouwer.AdditivePrincipalGenericRefuted where
+
+open import Data.Nat.Base                        using (ℕ; zero; suc)
+open import Data.Empty                           using (⊥)
+open import Data.Product.Base                    using (_,_)
+open import Relation.Nullary                     using (¬_)
+
+open import Ordinal.Brouwer                      using (Ord; oz; osuc; olim)
+open import Ordinal.Brouwer.Arithmetic           using (_⊕_; nat-to-ord)
+open import Ordinal.Brouwer.Phase13              using
+  ( _≤′_
+  ; _<′_
+  ; ≤′-refl
+  )
+open import Ordinal.Brouwer.StrictLeftMonoRefuted using (<′-irrefl)
+
+----------------------------------------------------------------------
+-- The hypothesised property
+----------------------------------------------------------------------
+
+-- "Additive-principal closure on generic sums": if both summands
+-- of `α ⊕ β` are strictly below `X ⊕ Y`, then so is the sum.
+-- This generalises `additive-principal-ω-rank-pow` (which holds
+-- only when the target is a pure ω-power `ω-rank-pow μ`).  REFUTED
+-- below.
+
+AdditivePrincipalGenericSum : Set
+AdditivePrincipalGenericSum =
+  ∀ {X Y α β} → α <′ X ⊕ Y → β <′ X ⊕ Y → α ⊕ β <′ X ⊕ Y
+
+----------------------------------------------------------------------
+-- The counterexample witness: ω <′ ω ⊕ ω
+----------------------------------------------------------------------
+
+-- The premise `ω <′ ω ⊕ ω` we need to feed to the refutation chain.
+-- Concretely: `osuc (olim nat-to-ord) ≤′ olim nat-to-ord ⊕ olim
+-- nat-to-ord = olim (λ n → olim nat-to-ord ⊕ nat-to-ord n)`.
+-- The `osuc (olim f) ≤′ olim g` clause of `_≤′_` reduces to
+-- `Σ ℕ (λ n → osuc (olim f) ≤′ g n)`; we pick branch n = 1.
+--
+-- At n = 1: `g 1 = olim nat-to-ord ⊕ nat-to-ord 1
+--                = olim nat-to-ord ⊕ osuc oz
+--                = osuc (olim nat-to-ord ⊕ oz)
+--                = osuc (olim nat-to-ord)` (all definitional).
+-- So we need `osuc (olim nat-to-ord) ≤′ osuc (olim nat-to-ord)`,
+-- which is `≤′-refl`.
+
+ω<′ω⊕ω : olim nat-to-ord <′ olim nat-to-ord ⊕ olim nat-to-ord
+ω<′ω⊕ω = suc zero , ≤′-refl {olim nat-to-ord}
+
+----------------------------------------------------------------------
+-- The headline refutation
+----------------------------------------------------------------------
+
+-- Instantiating the hypothesised property at X = Y = α = β = ω
+-- yields `ω ⊕ ω <′ ω ⊕ ω`; `<′-irrefl` (from the (b) refutation
+-- module) refutes it.  Both premises are `ω<′ω⊕ω`.
+
+additive-principal-generic-sum-refuted : ¬ AdditivePrincipalGenericSum
+additive-principal-generic-sum-refuted apgs =
+  <′-irrefl {olim nat-to-ord ⊕ olim nat-to-ord}
+    (apgs {olim nat-to-ord} {olim nat-to-ord}
+          {olim nat-to-ord} {olim nat-to-ord}
+          ω<′ω⊕ω ω<′ω⊕ω)

proofs/agda/Ordinal/Brouwer/StrictLeftMonoRefuted.agda

@@ -0,0 +1,149 @@
+{-# OPTIONS --safe --without-K #-}
+
+-- Checked refutation of strict left-monotonicity of `_⊕_`.
+--
+-- The Phase13 block comment near `⊕-mono-≤-left` notes that the
+-- strict-left-mono claim
+--
+--   ∀ {α β γ} → α <′ β → α ⊕ γ <′ β ⊕ γ
+--
+-- is NOT a theorem under Brouwer arithmetic, citing the
+-- counterexample at α = oz, β = osuc oz, γ = olim nat-to-ord (= ω):
+-- both `α ⊕ γ` and `β ⊕ γ` denote the same ordinal (the limit ω),
+-- so a strict inequality cannot hold.
+--
+-- This module promotes that prose claim into a CHECKED REFUTATION:
+-- it states `StrictLeftMonoSum` as a named hypothesis, exhibits the
+-- counterexample as a finite chain that derives `⊥`, and packages
+-- the result as `strict-left-mono-refuted : ¬ StrictLeftMonoSum`.
+--
+-- Cited by `Ordinal.Buchholz.RankLexSlice3` as the structural
+-- blocker for the bplus-chain-level extension of the joint-bplus
+-- rank-mono primitive (route (b) of its design-note's open
+-- follow-on plan).  Promoting prose to a named theorem makes the
+-- closure-decision auditable.
+--
+-- ## What lands
+--
+--   * `StrictLeftMonoSum` — the hypothesised property (as a `Set`).
+--   * `<′-irrefl` — Brouwer well-foundedness-derived irreflexivity
+--     of `_<′_` (small standalone helper; standard derivation from
+--     `wf-<′`).
+--   * `osuc-oz-⊕-nat≤osuc-oz-⊕-nat` — the structural-recursion
+--     helper `osuc oz ⊕ nat-to-ord k ≤′ osuc (oz ⊕ nat-to-ord k)`.
+--   * `osuc-oz-⊕-ω≤oz-⊕-ω` — the limit-level companion: both olims
+--     denote the same ordinal (ω) so the larger side `≤′` the smaller.
+--   * `strict-left-mono-refuted` — the headline `¬ StrictLeftMonoSum`.
+--
+-- ## Headlines (pin in `Smoke.agda`)
+--
+--   * `StrictLeftMonoSum`
+--   * `strict-left-mono-refuted`
+
+module Ordinal.Brouwer.StrictLeftMonoRefuted where
+
+open import Data.Nat.Base                        using (ℕ; zero; suc)
+open import Data.Empty                           using (⊥)
+open import Data.Product.Base                    using (_,_)
+open import Relation.Nullary                     using (¬_)
+open import Induction.WellFounded                using (Acc; acc)
+
+open import Ordinal.Brouwer                      using (Ord; oz; osuc; olim)
+open import Ordinal.Brouwer.Arithmetic           using (_⊕_; nat-to-ord)
+open import Ordinal.Brouwer.Phase13              using
+  ( _≤′_
+  ; _<′_
+  ; ≤′-refl
+  ; ≤′-trans
+  ; wf-<′
+  )
+
+----------------------------------------------------------------------
+-- The hypothesised property
+----------------------------------------------------------------------
+
+-- Strict left-monotonicity of `_⊕_`: if `α <′ β` then for every
+-- right addend `γ`, `α ⊕ γ <′ β ⊕ γ`.  Refuted below.
+
+StrictLeftMonoSum : Set
+StrictLeftMonoSum = ∀ {α β γ} → α <′ β → α ⊕ γ <′ β ⊕ γ
+
+----------------------------------------------------------------------
+-- Irreflexivity of `_<′_` from well-foundedness
+----------------------------------------------------------------------
+
+-- Standard derivation: structural recursion on `Acc _<′_ α`.
+
+acc-no-self : ∀ {α} → Acc _<′_ α → α <′ α → ⊥
+acc-no-self (acc rec) α<α = acc-no-self (rec α<α) α<α
+
+<′-irrefl : ∀ {α} → ¬ (α <′ α)
+<′-irrefl {α} = acc-no-self (wf-<′ α)
+
+----------------------------------------------------------------------
+-- The counterexample: γ = ω (= olim nat-to-ord)
+----------------------------------------------------------------------
+
+-- Step a) Per-index dominance: `osuc oz ⊕ nat-to-ord k ≤′ osuc (oz
+-- ⊕ nat-to-ord k)`.  Each side is a finite stack of osucs over oz;
+-- both reduce to `nat-to-ord (suc k)` semantically.  Proved by
+-- structural recursion on k:
+--
+--   * k = 0:  `osuc oz ⊕ oz = osuc oz` and `osuc (oz ⊕ oz) = osuc oz`
+--             (both definitional), so `osuc oz ≤′ osuc oz` is `≤′-refl`.
+--   * k = suc k':  Both sides reduce one `osuc` step; the `osuc / osuc`
+--             clause of `_≤′_` collapses to the inductive hypothesis.
+
+osuc-oz-⊕-nat≤osuc-of-oz-⊕-nat : ∀ k →
+    (osuc oz) ⊕ nat-to-ord k ≤′ osuc (oz ⊕ nat-to-ord k)
+osuc-oz-⊕-nat≤osuc-of-oz-⊕-nat zero    = ≤′-refl {osuc oz}
+osuc-oz-⊕-nat≤osuc-of-oz-⊕-nat (suc k) =
+  osuc-oz-⊕-nat≤osuc-of-oz-⊕-nat k
+
+-- Step b) Branch-selection lemma in the olim: the k-th branch of the
+-- "osuc oz" side is bounded by the (suc k)-th branch of the "oz" side,
+-- which in turn lives in the limit `oz ⊕ ω`.
+--
+-- Concretely: `osuc oz ⊕ nat-to-ord k ≤′ oz ⊕ nat-to-ord (suc k)`.
+-- Both sides reduce: LHS as `osuc-oz-⊕-nat≤osuc-of-oz-⊕-nat`'s upper
+-- bound; RHS by the `_⊕_` definitional clause `α ⊕ osuc β = osuc
+-- (α ⊕ β)`, giving exactly `osuc (oz ⊕ nat-to-ord k)`.
+
+osuc-oz-⊕-nat≤oz-⊕-nat-suc : ∀ k →
+    (osuc oz) ⊕ nat-to-ord k ≤′ oz ⊕ nat-to-ord (suc k)
+osuc-oz-⊕-nat≤oz-⊕-nat-suc k = osuc-oz-⊕-nat≤osuc-of-oz-⊕-nat k
+
+-- Step c) The limit-level companion lemma: `osuc oz ⊕ ω ≤′ oz ⊕ ω`.
+-- The "larger" side actually `≤′` the smaller because both olims
+-- enumerate the same ordinal ω.
+--
+-- Per the `olim f ≤′ β` clause of `_≤′_`, we need each branch of
+-- the LHS olim to be `≤′` the RHS olim.  For branch k, pick branch
+-- `suc k` in the RHS olim and apply `osuc-oz-⊕-nat≤oz-⊕-nat-suc`.
+
+osuc-oz-⊕-ω≤oz-⊕-ω :
+    (osuc oz) ⊕ (olim nat-to-ord) ≤′ oz ⊕ (olim nat-to-ord)
+osuc-oz-⊕-ω≤oz-⊕-ω zero    = suc zero    , osuc-oz-⊕-nat≤oz-⊕-nat-suc zero
+osuc-oz-⊕-ω≤oz-⊕-ω (suc k) = suc (suc k) , osuc-oz-⊕-nat≤oz-⊕-nat-suc (suc k)
+
+----------------------------------------------------------------------
+-- The headline refutation
+----------------------------------------------------------------------
+
+-- If strict-left-mono held, applying it at α = oz, β = osuc oz,
+-- γ = ω would produce `oz ⊕ ω <′ osuc oz ⊕ ω`.  Combined with
+-- `osuc-oz-⊕-ω≤oz-⊕-ω` (the other direction) via `≤′-trans`, we get
+-- `oz ⊕ ω <′ oz ⊕ ω`, which `<′-irrefl` refutes.
+--
+-- The premise `oz <′ osuc oz` is `osuc oz ≤′ osuc oz` (= `oz ≤′ oz`
+-- = `⊤`).
+
+strict-left-mono-refuted : ¬ StrictLeftMonoSum
+strict-left-mono-refuted slm =
+  <′-irrefl {oz ⊕ olim nat-to-ord}
+    (≤′-trans
+      {osuc (oz ⊕ olim nat-to-ord)}
+      {osuc oz ⊕ olim nat-to-ord}
+      {oz ⊕ olim nat-to-ord}
+      (slm {oz} {osuc oz} {olim nat-to-ord} (≤′-refl {osuc oz}))
+      osuc-oz-⊕-ω≤oz-⊕-ω)

proofs/agda/Smoke.agda

@@ -1086,6 +1086,37 @@ open import Ordinal.Buchholz.RankBrouwer using
   ( rank
   )
 
+-- Brouwer-arithmetic CHECKED REFUTATIONS (2026-05-28).  Promote
+-- the two prose obstacles from `RankLexSlice3`'s design note and
+-- `Phase13`'s `⊕-mono-≤-left` block comment into named theorems:
+--
+-- (b) strict-left-mono of `_⊕_` is NOT a theorem
+--     (`strict-left-mono-refuted`).  Counterexample at α = oz,
+--     β = osuc oz, γ = ω: both sides equal ω, so the strict step
+--     fails.  Refutation derives ⊥ from the hypothesis + `<′-irrefl`
+--     (also exposed here for downstream use).
+--
+-- (a) "additive-principal closure on generic sums" is NOT a theorem
+--     (`additive-principal-generic-sum-refuted`).  Counterexample
+--     at X = Y = α = β = ω: `ω ⊕ ω <′ ω ⊕ ω` would follow,
+--     refuted by `<′-irrefl`.
+--
+-- These pin the two routes documented as "structurally blocked"
+-- in `Ordinal.Buchholz.RankLexSlice3` as CHECKED dead-ends
+-- rather than prose claims.
+open import Ordinal.Brouwer.StrictLeftMonoRefuted using
+  ( StrictLeftMonoSum
+  ; <′-irrefl
+  ; osuc-oz-⊕-ω≤oz-⊕-ω
+  ; strict-left-mono-refuted
+  )
+
+open import Ordinal.Brouwer.AdditivePrincipalGenericRefuted using
+  ( AdditivePrincipalGenericSum
+  ; ω<′ω⊕ω
+  ; additive-principal-generic-sum-refuted
+  )
+
 -- ω-power rank for Ω-markers and Buchholz terms.  Limit-shaped
 -- replacement for `nat-to-ord (suc n)` successor stacks.  Compositional
 -- rank-mono primitives (right-mono on `bplus`) reusable across both