proof(architecture): RankMonoUnion umbrella over source-rule extensions

Realises the architectural recommendation from PR #167's closing
note: the future bplus-chain rank-mono umbrella shipped as a
UNION OF SOURCE-RULE EXTENSIONS rather than a single enriched
rank function.  Zero new proof obligations; purely structural
composition via Sum + `[_,_]` mediator.  `--safe --without-K`,
no postulates, no funext.

## The architectural design realised

PR #167's closing observation:

> The future bplus-chain rank-mono umbrella may want to be designed
> as a UNION OF SOURCE-RULE EXTENSIONS (Path-3 style for cleanly-
> decomposable cases) rather than a single enriched rank function
> (rank-lex-jb style for cross-head cases).

This PR mechanises that recommendation as `Ordinal.Buchholz.
RankMonoUnion`.

## What the union umbrella ships

`_<ᵇᵘ_ : BT → BT → Set` — the disjoint sum of `_<ᵇ¹_` (Slice 3
extension, `RankMonoUmbrellaSlice3`) and `_<ᵇ⁺²_` (Path-3
extension, `RankMonoSameLeft`).  Either extension's witness is
accepted.

`rank-pow-mono-<ᵇᵘ : ∀ {x y} → x <ᵇᵘ y → rank-pow x <′ rank-pow y`
— the COPRODUCT MEDIATOR of `rank-pow-mono-<ᵇ¹` and
`rank-pow-mono-<ᵇ⁺²` via `[_,_]`.  ONE LINE.  No new proof
obligation: the union's discharge is purely structural.

Convenience embeddings: `<ᵇᵘ-from-<ᵇ¹`, `<ᵇᵘ-from-<ᵇ⁺²`,
`<ᵇᵘ-from-<ᵇ⁰` (transitive via `<ᵇ¹`),
`<ᵇᵘ-from-<ᵇ⁰-via-<ᵇ⁺²` (symmetric via `<ᵇ⁺²`).

## Why this architectural shape (three observations)

1. Different sub-cases of `<ᵇ-+1`-style joint-bplus close at
   DIFFERENT rank-relation levels.  Strict-head case
   (`<ᵇ¹-+1-+`) closes via head-Ω inversion +
   `ω-rank-pow-succ`.  Same-left case (`<ᵇ⁺²-same-left`)
   closes via `rank-pow-bplus-right-mono` on the tail.
   Cross-head rank-equal case (`bpsi ν α` vs `bOmega ν`)
   closes at the LEX-RANK level via `rank-lex-jb`.  Each
   sub-case prefers a DIFFERENT rank-mono machinery.

2. A single enriched rank function (rank-lex-jb) handles
   multiple sub-cases via a uniform second-component
   discriminator, but the consumer-side first-eq derivation
   is structurally simpler when the source rule itself
   carries the enrichment (Path-3 verdict, PR #167).

3. UNION OF EXTENSIONS SCALES: every new sub-case added to
   the bplus-chain rank-mono programme can ship as a new
   extension `_<ᵇⁿ_` with its own `rank-pow-mono-<ᵇⁿ`, then
   be unioned in mechanically via Sum + `[_,_]`.  No
   interference between extensions; closure is local to
   each extension's structural recursion.

## Extension recipe (in module preamble for future contributors)

To add a new source-rule extension `_<ᵇⁿ_` with
`rank-pow-mono-<ᵇⁿ`:

  1. Define relation + rank-pow-mono in its own module
     (use `RankMonoSameLeft` as the canonical template).
  2. Re-export through `Ordinal/Buchholz/Smoke.agda` with
     its own `using` block.
  3. Update this module to extend `_<ᵇᵘ_` with the new
     disjunct and extend `rank-pow-mono-<ᵇᵘ` with the new
     case via `[_,_]`.  Both edits mechanical; no new proof
     obligations.

Per-extension proof work + structural composition is the
architectural payoff, vs proof obligations multiplying as the
rank function gains discriminators.

## What this module does NOT do

- Does NOT wrap with WfCNF endpoints (à la
  `RankMonoUmbrellaSlice4._<ᵇ⁻ⁿ_`).  Consumers needing WfCNF
  compose with the predicates separately or extend with a
  WfCNF-bundled variant.
- Does NOT include `rank-lex-jb` discharge — the cross-head
  rank-equal case discharges at LEX-RANK level, not rank-pow
  level, so it lives in a different rank-relation.  The union
  here is over `rank-pow <′` discharges only.
- Does NOT prove well-foundedness of the union — orthogonal
  to rank-mono; would need a single Brouwer-rank embedding.
  `rank-pow` provides the seed.

## Local verification

- `agda -i proofs/agda proofs/agda/Ordinal/Buchholz/RankMonoUnion.agda` — clean.
- `agda -i proofs/agda proofs/agda/Ordinal/Buchholz/Smoke.agda` — clean, exit 0.
- `agda -i proofs/agda proofs/agda/Smoke.agda` — clean, exit 0.
- `agda -i proofs/agda proofs/agda/All.agda` — clean, exit 0.
- `bash tools/check-guardrails.sh proofs/agda` — **162 modules** pass.
- `sh scripts/kernel-guard.sh` — PASS.

Six new names pinned in `Ordinal/Buchholz/Smoke.agda` under a
new `RankMonoUnion` `using` block.  Module wired into
`proofs/agda/All.agda` between `RankMonoSameLeft` and
`RecursiveSurfaceOrder`.

## Slice 3+4 Route A arc summary (4 PRs total)

After this PR the Slice 3+4 Route A session arc is closed:

  * PR #165 — (b) `<lex-first` primitive + bpsi sub-case discharge.
  * PR #166 — (c) trichotomy data type + first-eq derivation.
  * PR #167 — Path-3 prototype (same-left source-rule extension).
  * THIS PR — RankMonoUnion (architectural realisation).

The full bplus-chain rank-mono umbrella over all 13 `_<ᵇ_`
constructors is still gated on (i) tail-rank-equality discharge
for the bpsi-source-at-equal-head case AND (ii) the cross-head
rank-equal case via rank-lex-jb's structural research; neither
is closed by THIS PR.  The architecture, however, is now in
place for those closures to plug in mechanically as they land.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

proofs/agda/All.agda

@@ -150,6 +150,7 @@ open import Ordinal.Buchholz.RankMonoUmbrella
 open import Ordinal.Buchholz.RankMonoUmbrellaSlice3
 open import Ordinal.Buchholz.RankMonoUmbrellaSlice4
 open import Ordinal.Buchholz.RankMonoSameLeft
+open import Ordinal.Buchholz.RankMonoUnion
 open import Ordinal.Buchholz.RecursiveSurfaceOrder
 open import Ordinal.Buchholz.RecursiveSurfaceBudget
 open import Ordinal.Buchholz.SurfaceOrder

proofs/agda/Ordinal/Buchholz/RankMonoUnion.agda

@@ -0,0 +1,161 @@
+{-# OPTIONS --safe --without-K #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+-- Union umbrella over source-rule rank-mono extensions (2026-05-30).
+--
+-- ## The architectural recommendation realised
+--
+-- PR #167's closing observation: "the future bplus-chain rank-mono
+-- umbrella may want to be designed as a UNION OF SOURCE-RULE
+-- EXTENSIONS (Path-3 style for cleanly-decomposable cases) rather
+-- than a single enriched rank function (rank-lex-jb style for
+-- cross-head cases)".
+--
+-- This module mechanises that pattern.  The UNION RELATION
+-- `_<ᵇᵘ_` combines:
+--
+--   1. `_<ᵇ¹_` (Slice 3 extension, `RankMonoUmbrellaSlice3`) — 10
+--      inherited K-free cases via `<ᵇ¹-from-<ᵇ⁰` + the strict-head
+--      joint-bplus case `<ᵇ¹-+1-+` (`PR #142`).
+--   2. `_<ᵇ⁺²_` (Path-3 extension, `RankMonoSameLeft`) — 10
+--      inherited K-free cases via `<ᵇ⁺²-from-<ᵇ⁰` + the same-left
+--      joint-bplus case `<ᵇ⁺²-same-left` (PR #167).
+--
+-- The union is the SUM of the two relations.  Rank-pow monotonicity
+-- on the union dispatches by case-analysis: either the relation is
+-- witnessed by the `<ᵇ¹` umbrella (which `rank-pow-mono-<ᵇ¹`
+-- discharges) or by the `<ᵇ⁺²` umbrella (which `rank-pow-mono-<ᵇ⁺²`
+-- discharges).  Zero new proof obligations: the union is purely
+-- structural.
+--
+-- ## Why this architectural shape
+--
+-- Three observations from the Slice 3+4 Route A session arc:
+--
+-- 1. Different sub-cases of `<ᵇ-+1`-style joint-bplus close at
+--    DIFFERENT rank-relation levels.  The strict-head case
+--    (`<ᵇ¹-+1-+`) closes via head-Ω inversion + `ω-rank-pow-succ`.
+--    The same-left case (`<ᵇ⁺²-same-left`) closes via
+--    `rank-pow-bplus-right-mono` on the tail.  The cross-head
+--    rank-equal case (`bpsi ν α` vs `bOmega ν`) closes at the
+--    LEX-RANK level via `rank-lex-jb`.  Each sub-case prefers a
+--    DIFFERENT rank-mono machinery.
+--
+-- 2. A SINGLE enriched rank function (rank-lex-jb) tries to handle
+--    multiple sub-cases via a uniform second-component
+--    discriminator, but the consumer-side first-eq derivation is
+--    structurally simpler when the source rule itself carries the
+--    enrichment (Path-3 verdict, PR #167).
+--
+-- 3. UNION OF EXTENSIONS scales: every new sub-case added to the
+--    bplus-chain rank-mono programme can ship as a new extension
+--    `_<ᵇⁿ_` with its own `rank-pow-mono-<ᵇⁿ`, then be unioned
+--    in mechanically via Sum + `[_,_]`.  No interference between
+--    extensions; the closure is local to each extension's
+--    structural recursion.
+--
+-- ## What this module does NOT do
+--
+-- * Does NOT wrap with WfCNF endpoints (à la
+--   `RankMonoUmbrellaSlice4._<ᵇ⁻ⁿ_`).  Consumers needing WfCNF
+--   compose with the predicates separately, or extend this union
+--   with a WfCNF-bundled variant.
+-- * Does NOT include `rank-lex-jb` discharge — the cross-head
+--   rank-equal case discharges at LEX-RANK level, not at rank-pow
+--   level, so it lives in a different rank-relation.  The union
+--   here is over `rank-pow <′` discharges only.
+-- * Does NOT prove well-foundedness of the union — orthogonal to
+--   rank-mono; would need a single Brouwer-rank embedding.
+--   `rank-pow` provides the seed.
+--
+-- ## Extension recipe (for future contributors)
+--
+-- To add a new source-rule extension `_<ᵇⁿ_` with `rank-pow-mono-<ᵇⁿ`:
+--
+--   1. Define the relation + the rank-pow-mono theorem in its own
+--      module (use `RankMonoSameLeft` as the canonical template).
+--   2. Re-export the headlines through `Ordinal/Buchholz/Smoke.agda`
+--      with their own `using` block.
+--   3. Update this module to extend `_<ᵇᵘ_` with the new disjunct
+--      and extend `rank-pow-mono-<ᵇᵘ` with the new case via `[_,_]`.
+--      Both edits are mechanical; no new proof obligations.
+--
+-- The mechanical-ness of the union extension is the architectural
+-- payoff: per-extension proof work + structural composition, vs
+-- proof obligations multiplying as the rank function gains
+-- discriminators.
+
+module Ordinal.Buchholz.RankMonoUnion where
+
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
+
+open import Ordinal.Brouwer.Phase13 using (_<′_)
+open import Ordinal.Buchholz.Syntax using (BT)
+open import Ordinal.Buchholz.RankPow using (rank-pow)
+open import Ordinal.Buchholz.RankMonoUmbrella using (_<ᵇ⁰_)
+open import Ordinal.Buchholz.RankMonoUmbrellaSlice3 using
+  ( _<ᵇ¹_
+  ; <ᵇ¹-from-<ᵇ⁰
+  ; rank-pow-mono-<ᵇ¹
+  )
+open import Ordinal.Buchholz.RankMonoSameLeft using
+  ( _<ᵇ⁺²_
+  ; <ᵇ⁺²-from-<ᵇ⁰
+  ; rank-pow-mono-<ᵇ⁺²
+  )
+
+----------------------------------------------------------------------
+-- The union relation `_<ᵇᵘ_`
+----------------------------------------------------------------------
+
+-- Disjoint sum of `_<ᵇ¹_` and `_<ᵇ⁺²_`.  Either extension's witness
+-- is accepted; rank-pow-mono dispatches accordingly.
+
+_<ᵇᵘ_ : BT → BT → Set
+x <ᵇᵘ y = (x <ᵇ¹ y) ⊎ (x <ᵇ⁺² y)
+
+infix 4 _<ᵇᵘ_
+
+----------------------------------------------------------------------
+-- Rank-pow monotonicity by case analysis
+----------------------------------------------------------------------
+
+-- The union's rank-mono is the COPRODUCT MEDIATOR of the two
+-- per-extension umbrellas.  Each disjunct's discharge is the
+-- existing rank-mono theorem for that extension — no new proof
+-- obligation.  The mediator `[_,_]` is purely structural.
+
+rank-pow-mono-<ᵇᵘ : ∀ {x y} → x <ᵇᵘ y → rank-pow x <′ rank-pow y
+rank-pow-mono-<ᵇᵘ = [ rank-pow-mono-<ᵇ¹ , rank-pow-mono-<ᵇ⁺² ]
+
+----------------------------------------------------------------------
+-- Convenience embeddings
+----------------------------------------------------------------------
+
+-- Direct embeddings from each contributing relation into the union.
+-- These are `inj₁` / `inj₂` specialised, but named for readability
+-- at consumer call sites.
+
+<ᵇᵘ-from-<ᵇ¹ : ∀ {x y} → x <ᵇ¹ y → x <ᵇᵘ y
+<ᵇᵘ-from-<ᵇ¹ = inj₁
+
+<ᵇᵘ-from-<ᵇ⁺² : ∀ {x y} → x <ᵇ⁺² y → x <ᵇᵘ y
+<ᵇᵘ-from-<ᵇ⁺² = inj₂
+
+-- Transitive embedding from the 10-constructor closed umbrella
+-- via either path.  The choice between `<ᵇ¹` and `<ᵇ⁺²` is
+-- definitionally irrelevant for `<ᵇ⁰` derivations (both embed
+-- the same witness); we choose `<ᵇ¹` as the canonical path so
+-- consumers reasoning about the strict-head joint-bplus case
+-- don't need to switch disjuncts mid-proof.
+
+<ᵇᵘ-from-<ᵇ⁰ : ∀ {x y} → x <ᵇ⁰ y → x <ᵇᵘ y
+<ᵇᵘ-from-<ᵇ⁰ p = <ᵇᵘ-from-<ᵇ¹ (<ᵇ¹-from-<ᵇ⁰ p)
+
+-- Symmetric alternative: embed via `<ᵇ⁺²` instead.  Same content;
+-- offered for consumer call sites where the `<ᵇ⁺²` path is
+-- already in scope.
+
+<ᵇᵘ-from-<ᵇ⁰-via-<ᵇ⁺² : ∀ {x y} → x <ᵇ⁰ y → x <ᵇᵘ y
+<ᵇᵘ-from-<ᵇ⁰-via-<ᵇ⁺² p = <ᵇᵘ-from-<ᵇ⁺² (<ᵇ⁺²-from-<ᵇ⁰ p)

proofs/agda/Ordinal/Buchholz/Smoke.agda

@@ -585,3 +585,21 @@ open import Ordinal.Buchholz.RankMonoSameLeft using
   ; rank-pow-mono-<ᵇ⁺²
   ; rank-pow-mono-same-left
   )
+
+-- Union umbrella 2026-05-30 (own block per CLAUDE.md Working rules):
+-- realises the architectural recommendation from PR #167's closing
+-- note — bplus-chain rank-mono umbrella as a UNION OF SOURCE-RULE
+-- EXTENSIONS rather than a single enriched rank function.  Combines
+-- `_<ᵇ¹_` (Slice 3 strict-head joint-bplus) with `_<ᵇ⁺²_` (Path-3
+-- same-left joint-bplus) via Sum + `[_,_]` mediator.  Zero new
+-- proof obligations; the union is purely structural over the two
+-- per-extension umbrellas.  Extension recipe (for new sub-cases)
+-- documented in the module preamble.
+open import Ordinal.Buchholz.RankMonoUnion using
+  ( _<ᵇᵘ_
+  ; rank-pow-mono-<ᵇᵘ
+  ; <ᵇᵘ-from-<ᵇ¹
+  ; <ᵇᵘ-from-<ᵇ⁺²
+  ; <ᵇᵘ-from-<ᵇ⁰
+  ; <ᵇᵘ-from-<ᵇ⁰-via-<ᵇ⁺²
+  )