proof: well-foundedness of _<ᵇᵘ_ via rank-embedding transport

Closes Gate 2 of the Slice 3+4 Route A session arc.  Derives
`WellFounded _<ᵇᵘ_` mechanically from `rank-pow-mono-<ᵇᵘ` (PR
#168) and the existing `wf-<′` via the standard Subrelation +
InverseImage transport pattern documented in
`Ordinal.Buchholz.RankBrouwer`'s preamble.  Zero new proof
obligations; purely structural.  `--safe --without-K`, no
postulates, no funext.

## The rank-embedding recipe

```agda
wf-rank-pow-pullback : WellFounded (λ x y → rank-pow x <′ rank-pow y)
wf-rank-pow-pullback = On.wellFounded rank-pow wf-<′

wf-<ᵇᵘ : WellFounded _<ᵇᵘ_
wf-<ᵇᵘ = Subrelation.wellFounded rank-pow-mono-<ᵇᵘ wf-rank-pow-pullback
```

Two steps:

1. `On.wellFounded` (= `InverseImage.wellFounded`) lifts well-
   foundedness of `_<′_` on `Ord` to the pullback `_<′_ on rank-pow`
   on `BT`.
2. `Subrelation.wellFounded` transports well-foundedness from the
   pullback to `_<ᵇᵘ_`, consuming `rank-pow-mono-<ᵇᵘ` as the
   witness that `_<ᵇᵘ_` is a sub-relation of the pullback.

The recipe is documented in `RankBrouwer.agda:55-56`:

  > wf-<ᵇʳᶠ = Subrelation.wellFounded rank-mono
  >            (InverseImage.wellFounded rank wf-<′)

`On.wellFounded` is the modern (non-deprecated) alias for
`InverseImage.wellFounded`.

## Slice 3+4 Route A gate status after this PR

| Gate | Status |
|---|---|
| 1 — tail-rank-equality discharge (cross-head rank-equal case) | open (structural blocker) |
| **2 — well-foundedness of `_<ᵇᵘ_`** | **CLOSED HERE** |
| 3 — Path-4 + further source-rule extensions | open (future-work, mechanical) |

## What this does NOT do

- Does NOT prove well-foundedness of the WfCNF-narrowed `_<ᵇᵘⁿ_`
  (PR #169) separately — follows by the same Subrelation
  transport from `wf-<ᵇᵘ` via the canonical `<ᵇᵘⁿ → <ᵇᵘ`
  projection.  Left for a thin follow-on if specifically needed.
- Does NOT add a Brouwer-rank embedding stronger than `rank-pow`
  — `rank-pow` is K-free + lands in `Ord` + already discharges
  the WF transport.  Nothing more sophisticated is needed.

## Local verification

- All four Agda lanes typecheck clean, exit 0.
- `bash tools/check-guardrails.sh proofs/agda` — 163 modules pass.
- `sh scripts/kernel-guard.sh` — PASS.

Two new names pinned in `Ordinal/Buchholz/Smoke.agda`:
`wf-rank-pow-pullback`, `wf-<ᵇᵘ`.

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

Author: hyperpolymath

proofs/agda/All.agda

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

proofs/agda/Ordinal/Buchholz/RankMonoUnionWF.agda

@@ -0,0 +1,95 @@
+{-# 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>
+
+-- Well-foundedness of the union rank-mono umbrella (2026-05-30).
+--
+-- ## What this lands
+--
+-- `wf-<ᵇᵘ : WellFounded _<ᵇᵘ_` — every union-derivation chain
+-- terminates.  Derived mechanically from `rank-pow-mono-<ᵇᵘ`
+-- (PR #168) and the well-foundedness of Brouwer's `_<′_` (already
+-- proved in `Ordinal.Brouwer.Phase13.wf-<′`) via the standard
+-- Subrelation + InverseImage combinators from
+-- `Induction.WellFounded` / `Relation.Binary.Construct.On`.
+--
+-- ## The rank-embedding recipe
+--
+-- This is the standard rank-WF transport pattern documented in
+-- `Ordinal.Buchholz.RankBrouwer`'s preamble:
+--
+--   wf-<ᵇᵘ = Subrelation.wellFounded rank-pow-mono-<ᵇᵘ
+--              (On.wellFounded rank-pow wf-<′)
+--
+-- 1. `On.wellFounded rank-pow wf-<′` lifts well-foundedness of
+--    `_<′_` on `Ord` to the pullback `_<′_ on rank-pow` on `BT`
+--    — InverseImage transport.
+-- 2. `Subrelation.wellFounded rank-pow-mono-<ᵇᵘ` then transports
+--    well-foundedness from the pullback to `_<ᵇᵘ_` itself,
+--    consuming `rank-pow-mono-<ᵇᵘ : x <ᵇᵘ y → rank-pow x <′ rank-pow y`
+--    as the witness that `_<ᵇᵘ_` is a sub-relation of the pullback.
+--
+-- The recipe is purely structural: zero new proof obligations.
+-- Closure follows from the existing `rank-pow-mono-<ᵇᵘ` (#168)
+-- + the existing `wf-<′` (`Phase13`).
+--
+-- ## Slice 3+4 Route A gate 2 closure
+--
+-- Per #168's closing note, three gates remained open at the
+-- architectural-realisation moment.  This module discharges
+-- **Gate 2** (well-foundedness of `_<ᵇᵘ_`) via the rank-embedding
+-- transport, leaving:
+--
+--   * Gate 1 — tail-rank-equality discharge for the cross-head
+--     rank-equal case (structural ordinal-arithmetic blocker).
+--   * Gate 3 — Path-4 + further source-rule extensions
+--     (future-work, mechanical per the extension recipe).
+--
+-- ## What this does NOT do
+--
+-- * Does NOT prove well-foundedness of the WfCNF-narrowed
+--   `_<ᵇᵘⁿ_` (PR #169) separately — it follows by the same
+--   Subrelation transport from `wf-<ᵇᵘ` via the canonical
+--   `<ᵇᵘⁿ → <ᵇᵘ` projection.  Left for a thin follow-on if a
+--   consumer needs the WfCNF-bundled form's WF specifically.
+-- * Does NOT add a Brouwer-rank embedding stronger than
+--   `rank-pow` — `rank-pow` is K-free + lands in `Ord` (Brouwer
+--   ordinals) + already discharges the WF transport.  Nothing
+--   more sophisticated is needed for this consumer.
+
+module Ordinal.Buchholz.RankMonoUnionWF where
+
+open import Induction.WellFounded               using
+  ( WellFounded
+  ; module Subrelation
+  )
+open import Relation.Binary.Construct.On as On  using (wellFounded)
+
+open import Ordinal.Brouwer                     using (Ord)
+open import Ordinal.Brouwer.Phase13             using (_<′_; wf-<′)
+open import Ordinal.Buchholz.Syntax             using (BT)
+open import Ordinal.Buchholz.RankPow            using (rank-pow)
+open import Ordinal.Buchholz.RankMonoUnion      using
+  ( _<ᵇᵘ_
+  ; rank-pow-mono-<ᵇᵘ
+  )
+
+----------------------------------------------------------------------
+-- Well-foundedness of `_<ᵇᵘ_`
+----------------------------------------------------------------------
+
+-- Step 1 — InverseImage transport: well-foundedness of `_<′_` on
+-- `Ord` lifts to well-foundedness of `_<′_ on rank-pow` on `BT`.
+-- Note that the pullback relation has the same shape as
+-- `rank-pow x <′ rank-pow y` but is named `_<′_ on rank-pow`.
+
+wf-rank-pow-pullback : WellFounded (λ x y → rank-pow x <′ rank-pow y)
+wf-rank-pow-pullback = On.wellFounded rank-pow wf-<′
+
+-- Step 2 — Subrelation transport: any sub-relation of a well-
+-- founded relation is well-founded.  `rank-pow-mono-<ᵇᵘ` is the
+-- witness that `_<ᵇᵘ_` is a sub-relation of `_<′_ on rank-pow`,
+-- so `_<ᵇᵘ_` inherits well-foundedness.
+
+wf-<ᵇᵘ : WellFounded _<ᵇᵘ_
+wf-<ᵇᵘ = Subrelation.wellFounded rank-pow-mono-<ᵇᵘ wf-rank-pow-pullback

proofs/agda/Ordinal/Buchholz/Smoke.agda

@@ -603,3 +603,17 @@ open import Ordinal.Buchholz.RankMonoUnion using
   ; <ᵇᵘ-from-<ᵇ⁰
   ; <ᵇᵘ-from-<ᵇ⁰-via-<ᵇ⁺²
   )
+
+-- Union umbrella well-foundedness 2026-05-30 (own block per
+-- CLAUDE.md Working rules): closes Gate 2 of the Slice 3+4 Route
+-- A session arc.  `wf-<ᵇᵘ` derives WellFounded `_<ᵇᵘ_` via the
+-- standard Subrelation + InverseImage rank-embedding transport
+-- (rank-pow ∘ wf-<′).  Zero new proof obligations; purely
+-- structural.  Together with the WfCNF wrap (PR #169) this
+-- equips downstream Buchholz consumers with both the
+-- canonical-form invariant AND termination of union-derivation
+-- chains.
+open import Ordinal.Buchholz.RankMonoUnionWF using
+  ( wf-rank-pow-pullback
+  ; wf-<ᵇᵘ
+  )