docs: stale-claim sweep after Slice 3+4 Route A 6-PR arc (#165-#170) (#171)

## Summary

Seam-analyst gigafan agent surfaced three documents enumerating the
ordinal-track work that referenced only the pre-2026-05-30 state.
Updates reflect the **rank-lex-jb (a)+(b)+(c) assembly completion**, the
**Path-3 source-rule enrichment**, the **RankMonoUnion architectural
realisation**, the **WfCNF wrap**, and the **Gate 2 (well-foundedness)
closure**.

## Files

| File | Update |
|---|---|
| \`docs/echo-types/MAP.adoc\` §"Ordinal" Proofs line | Extends the
per-module enumeration to mention the six new modules from PRs #165-#170
with their roles |
| \`roadmap.adoc\` Lane 3 close-out | Adds the "Slice 3+4 Route A 6-PR
arc" subsection with the (a)+(b)+(c) + Path-3 + union + WfCNF + WF
breakdown |
| \`docs/echo-types/buchholz-rank-obstruction.adoc\` per-constructor
verdict table | Updates the \`<ᵇ-+1\` row from "Slice 3 headline
remaining" to "closed for strict-head + literal-same-left sub-cases;
cross-head rank-equal (Gate 1) open with documented structural
blockers". Score footer revised to "12/13 at the per-case level" |

## Honest scope preserved

Documents what LANDED, not what's CLOSED-OPEN conceptually. The
\`<ᵇ-+1\` joint-bplus case now has **two of three sub-cases closed**
(strict-head + literal-same-left); the cross-head rank-equal sub-case
(Gate 1) is explicitly documented as still open with both pre-identified
unblock routes refuted in PR #146 AND the WfCNF-constraint refutation
also closed.

R-2026-05-18 retraction narrowings respected: no "graded comonad" /
"model-independence" / "universal property" / "conservativity
metatheorem" language added.

## Local verification

- \`bash tools/check-guardrails.sh proofs/agda\` — 163 modules pass (no
Agda touched; docs-only change).

## Test plan

- [x] No Agda touched; docs-only diff.
- [x] Foundation guardrail still passes.
- [ ] CI: governance lanes green.
- [ ] Auto-merge on green.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

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

Author: hyperpolymath

docs/echo-types/MAP.adoc

@@ -244,12 +244,27 @@ Staged Buchholz-style collapsing in `--safe --without-K`.
   to rank-adm / rank-lex)), `RankLexJointBplus` (2026-05-28 PR #147
   — parallel rank with `leftmost-α` discriminator for the bpsi-source-
   at-equality joint-bplus sub-case; second-component strict-mono at
-  equal first components scaffolded), `RankMonoUmbrellaSlice4`
+  equal first components scaffolded; (a)+(b)+(c) assembly
+  completed 2026-05-30 via PRs #165 (b lex-first primitive) + #166
+  (c `BplusFirstTri` trichotomy + `first-eq-from-bpsi-source-at-
+  equal-head` consumer-side derivation)), `RankMonoUmbrellaSlice4`
   (2026-05-28 PR #149 — narrowed `_<ᵇ⁻ⁿ_` umbrella record bundling
   WfCNF endpoints + `_<ᵇ¹_` derivation; covers all 10 inherited
   `_<ᵇ⁰_` cases + the strict-head joint-bplus; two shortfalls
   (`<ᵇ-ψΩ≤` boundary; `<ᵇ-+1` at equal-head) pinned as `⊤`-aliases
-  with explicit lex-rank / rank-lex-jb pointers).
+  with explicit lex-rank / rank-lex-jb pointers),
+  `RankMonoSameLeft` (2026-05-30 PR #167 — Path-3 prototype
+  source-rule enrichment via `<ᵇ⁺²-same-left`; one-line closure via
+  `rank-pow-bplus-right-mono`), `RankMonoUnion` (2026-05-30 PR #168
+  — architectural realisation: union umbrella
+  `_<ᵇᵘ_ = _<ᵇ¹_ ⊎ _<ᵇ⁺²_` via Sum + `[_,_]` mediator; per-extension
+  proof work + structural composition; extension recipe in preamble),
+  `RankMonoUnionWfCNF` (2026-05-30 PR #169 — WfCNF wrap `_<ᵇᵘⁿ_`
+  bundling canonical-form invariant alongside the union; mirrors
+  Slice 4's pattern, propagates automatically through new
+  extensions), `RankMonoUnionWF` (2026-05-30 PR #170 — Gate 2
+  closure: `WellFounded _<ᵇᵘ_` via `Subrelation.wellFounded` +
+  `On.wellFounded` rank-embedding transport from `wf-<′`).
 * Docs: `docs/buchholz-plan.adoc`,
   `docs/echo-types/buchholz-extended-wf.md`,
   `docs/echo-types/buchholz-rank-obstruction.adoc` (per-constructor

docs/echo-types/buchholz-rank-obstruction.adoc

@@ -305,23 +305,25 @@ constructors discharge by additive-principal closure.
 | `<ᵇ-+ψ`    | ✓ closed  | Same as `<ᵇ-+Ω` since `rank-pow (bpsi ν _) = ω-rank-pow ν`.
 | `<ᵇ⁺-ψα`   | ✓ closed (Lane 3, 2026-05-26) | `rank-adm (bpsi ν α) = ω-rank-pow ν ⊕ rank-pow α`; `⊕-mono-<-right` closes the shared-Ω-index lex case from `rank-pow α <′ rank-pow β` (which the existing `_<ᵇ⁰_` umbrella discharges).  Primitive `rank-mono-<ᵇ⁺-ψα-from-pow` in `Ordinal.Buchholz.RankAdm`.
 | `<ᵇ-ψΩ≤`   | ✓ closed (Lane 3 follow-on, 2026-05-27) | Lex-pair rank `rank-lex : BT → RankLex` in `Ordinal.Buchholz.RankLex`, with `rank-lex (bOmega ν) = mkLex (ω-rank-pow ν) (ω-rank-pow ν)` and `rank-lex (bpsi ν α) = mkLex (ω-rank-pow ν) (rank-pow α)`.  Both sub-cases close via `rank-mono-<ᵇ-ψΩ≤-lex`: ν<μ via `<lex-first` + `ω-rank-pow-mono`; ν=μ via `<lex-second` + the admissibility bound `rank-pow α <′ ω-rank-pow ν`.  The "structurally impossible under any rank shape with `ω-rank-pow ν ≤ rank-adm (bpsi ν α)`" verdict from `RankAdm.agda` was scoped to *scalar* ranks; option (A) lex-pair sidesteps it cleanly.
-| `<ᵇ-+1`    | ⏳ joint-bplus, headline `rank-mono-<ᵇ-+1-via-head-Ω` remaining (Slice 3) | The dominator-function unblock (option A from `RankPow.agda`'s preamble) is now COMPLETE on the WfCNF-carrier domination side: `head-Ω : BT → OmegaIndex` (Slice 1, `Ordinal.Buchholz.HeadOmega`), `ω-rank-pow-succ` + per-marker strict dominance at *both* branches (Slice 2 + Slice 2-omega, `Ordinal.Buchholz.RankPow`), the unified `ω-rank-pow-<-succ`, the option-(b) head-Ω inversion lemmas `head-Ω-inv-{bOmega,bpsi}` (`Ordinal.Buchholz.HeadOmegaInversion`), AND the WfCNF-carrier structural recursion `rank-pow-dominated-by-head-Ω : ∀ {t} → WfCNF t → rank-pow t <′ ω-rank-pow-succ (head-Ω t)` (Slice 2-bplus, `Ordinal.Buchholz.RankPowDomination` — landed via PRs #133+#134 2026-05-27).  Remaining: the headline `rank-mono-<ᵇ-+1-via-head-Ω` discharge (Slice 3), consuming the domination lemma plus a head-Ω lower-bound + strict-jump bridge.  No further rank-mono dependency anywhere in the chain — option (b) bought independence from the still-open `rank-pow-mono-≤ᵇ`.
+| `<ᵇ-+1`    | ✓ closed for strict-head + literal-same-left sub-cases (Slice 3+4 Route A, 2026-05-30); ⏳ cross-head rank-equal sub-case open (Gate 1) | The headline `rank-mono-<ᵇ-+1-via-head-Ω` (Slice 3 discharge) closed under a strict-head premise via PRs #141-#143 (2026-05-28). Strict-head joint-bplus extension `<ᵇ¹-+1-+` lands in `RankMonoUmbrellaSlice3` + the WfCNF-bundled form `_<ᵇ⁻ⁿ_` in `RankMonoUmbrellaSlice4` (PR #149). The bpsi-source-at-equal-head sub-case advanced via rank-lex-jb (a)+(b)+(c) assembly: PR #147 (a) equal-first lex-second + PR #165 (b) strict-first lex-first primitive + PR #166 (c) `BplusFirstTri` trichotomy data type + `first-eq-from-bpsi-source-at-equal-head` consumer-side derivation. Path-3 alternative shipped in PR #167 as `RankMonoSameLeft` (`_<ᵇ⁺²-same-left`: source-rule enrichment closing the literal-same-left sub-case in one line via `rank-pow-bplus-right-mono`). Union architecture `_<ᵇᵘ_ = _<ᵇ¹_ ⊎ _<ᵇ⁺²_` lands in PR #168 (`RankMonoUnion`) via Sum + `[_,_]` mediator, with WfCNF wrap (PR #169) and well-foundedness (PR #170, Gate 2 closure via `Subrelation` + `On.wellFounded` transport). Cross-head rank-equal sub-case (Gate 1) remains open: case (iii) "anti-strict tail rank" not refutable from WfCNF constraints alone (the tail bound `y₂ ≤ᵇ x₁` is ordinal-level only; cannot distinguish within equal-marker ψ-sources); both pre-identified scalar-transport unblock routes CHECKED-REFUTED in PR #146 (`StrictLeftMonoRefuted`, `AdditivePrincipalGenericRefuted`).
 | `<ᵇ-0-+`   | ✓ closed* | `rank-pow bzero = oz`, and `rank-pow (bplus x y) ≥′ oz` strictly when *either* `x` or `y` is non-`bzero` and the term is WfCNF.  The degenerate `bplus bzero bzero` is excluded by WfCNF (atomic-right ≤ left forces both `bzero` and then the sum reduces to a `bzero`-shaped equivalent that doesn't pattern-match as a `bplus` under CNF normalisation — covered as a side-condition).
 |===
 
-*Score: 11/13 constructors closed (9 under the original `rank-pow`
-umbrella + 1 under the `rank-adm` slice + 1 under the `rank-lex`
-slice); 1 in flight under the head-Ω route with the WfCNF-carrier
-domination lemma `rank-pow-dominated-by-head-Ω` landed (the headline
-`rank-mono-<ᵇ-+1-via-head-Ω` Slice 3 discharge remaining); 1 closed
-conditionally with documented side condition.  The Lane-3 active-push
-slice on 2026-05-26 closed `<ᵇ⁺-ψα` (rank-adm) and re-classified
-`<ᵇ-ψΩ≤` to "encoding mismatch"; the Lane-3 follow-on slice on
-2026-05-27 closed `<ᵇ-ψΩ≤` via option (A) (lex pair); the head-Ω
-route landed in stages across 2026-05-27 (Slice 1 PR #124, Slice 2
-PR #130, Slice 2-omega + option (b) inversion PR #131, Slice 2-bplus
-domination PRs #133+#134).  Only the headline `rank-mono-<ᵇ-+1-via-head-Ω`
-discharge (Slice 3) remains in the per-constructor matrix.*
+*Score (2026-05-30 close): 12/13 constructors closed at the per-case
+level (9 under the original `rank-pow` umbrella + 1 under the
+`rank-adm` slice + 1 under the `rank-lex` slice + 1 (the `<ᵇ-+1`
+joint-bplus case) closed for two sub-cases — strict-head via Slice 3
+headline + literal-same-left via Path-3 — under the union umbrella
+`_<ᵇᵘ_` from PR #168); 1 closed conditionally with documented side
+condition. The Slice 3+4 Route A arc (PRs #165-#170, 2026-05-30)
+shipped the rank-lex-jb (a)+(b)+(c) assembly, the Path-3 source-rule
+enrichment prototype, the union-of-extensions architecture, the
+WfCNF wrap, and Gate 2 (well-foundedness) closure. Gate 1 — the
+cross-head rank-equal sub-case of `<ᵇ-+1` — remains open as the sole
+documented structural blocker, with both pre-identified scalar-
+transport unblock routes CHECKED-REFUTED in PR #146 and the
+WfCNF-constraint refutation path also closed (the tail bound is
+ordinal-level only; see the `<ᵇ-+1` row above).*
 
 === What remains open
 

roadmap.adoc

@@ -333,10 +333,42 @@ strict-head joint-bplus) LANDED 2026-05-28 via PR #149
 (`RankMonoUmbrellaSlice4`); two constructor-level shortfalls
 (`<ᵇ-ψΩ≤` boundary closes at lex-rank level; `<ᵇ-+1` at equal-head
 gated on the `RankLexJointBplus` pivot from PR #147) are pinned as
-`⊤`-aliases. The remaining ordinal-track work is the unbudgeted
+`⊤`-aliases.
+
+*Slice 3+4 Route A 6-PR arc* (2026-05-30) advanced the
+`<ᵇ-+1`-at-equal-head closure on TWO converging paths and shipped
+the union-of-extensions architecture:
+
+* PRs #165+#166 — rank-lex-jb (b) `<lex-first` primitive + (c)
+  `BplusFirstTri` trichotomy data type + `first-eq-from-bpsi-source-
+  at-equal-head` consumer-side derivation. Key insight: the
+  consumer's first-eq obligation reduces to *tail-rank-equality*
+  via `cong₂ _⊕_`; the same residual obligation gates BOTH the
+  ψ-rank-level and the bplus-chain-level closures.
+* PR #167 — Path-3 prototype `RankMonoSameLeft` (`_<ᵇ⁺²_` with
+  `<ᵇ⁺²-same-left`). Demonstrates that ENRICHING THE SOURCE RULE
+  is structurally simpler than enriching the rank function for
+  the literal-same-left sub-case; one-line closure via
+  `rank-pow-bplus-right-mono`.
+* PR #168 — `RankMonoUnion` architecture. Union umbrella
+  `_<ᵇᵘ_ = _<ᵇ¹_ ⊎ _<ᵇ⁺²_` via Sum + `[_,_]` mediator. Per-
+  extension proof work + structural composition; extension recipe
+  documented for future source-rule additions.
+* PR #169 — `RankMonoUnionWfCNF` WfCNF wrap (mirrors Slice 4 over
+  the union; canonical-form invariant propagates automatically
+  through new extensions).
+* PR #170 — Gate 2 closure: `WellFounded _<ᵇᵘ_` via the standard
+  `Subrelation` + `On.wellFounded` rank-embedding transport from
+  `wf-<′` (`Ordinal.Buchholz.RankBrouwer`'s preamble recipe).
+
+The remaining ordinal-track work is the unbudgeted
 `_<ᵇʳᶠ_` global well-foundedness (per `RankBrouwer.agda` preamble)
 and the full-order internalisation back into `Order.agda`'s main
-`_<ᵇ_` package.
+`_<ᵇ_` package. Gate 1 (cross-head rank-equal tail-rank-equality
+discharge) and Gate 3 (Path-4 and further source-rule extensions)
+both remain open at the close of the 2026-05-30 arc; Gate 1's
+both pre-identified unblock routes are CHECKED-REFUTED in PR #146,
+and Path-4 same-right is refuted by the same lemma.
 
 *Close-out criterion.* Either: