docs: reinforce Slice 2 / Slice 2-omega / inversion narrative across the wiki

Cross-doc consistency sweep after PRs #129/#130/#131 landed.  Five
docs had stale Slice 1-era wording that pre-dated the head-Ω route's
Slice 2 + Slice 2-omega + option-(b) inversion landings:

* `docs/echo-types/buchholz-rank-obstruction.adoc` (the live per-
  constructor verdict tracker).  The `<ᵇ-+1` row flipped from
  "⏳ joint-bplus, needs coarser bound" to "⏳ joint-bplus, head-Ω
  route in flight" with the full prerequisite-landings list and the
  Slice 2-bplus remaining-work note.  Score-paragraph + "What remains
  open" section + "See also" file list all updated.

* `roadmap.adoc` § Lane 3.  Bottleneck description + close-out
  criterion refreshed to reflect that the head-Ω abstraction +
  per-marker dominances + inversion lemmas have all landed across
  PRs #124/#130/#131; only Slice 2-bplus (the WfCNF-carrier
  structural recursion) remains.

* `EXPLAINME.adoc`.  One-paragraph ongoing-tracks line for the
  ordinal track refreshed from "first slice landed; rank-mono
  follow-ons designed" to the current "abstraction + per-marker
  dominances + inversion landed; structural WfCNF recursion
  remaining" state.

* `CHANGELOG.md` § Added (2026-05-27).  Two new bullets land:
  the Slice 2 + Slice 2-omega + inversion follow-on entry
  (records the Brouwer-encoding hazard the originally-proposed
  ω-branch shape would have tripped — the `ω^(suc(suc n))` and
  `ω^(suc n)` limits denote the same `ω^ω` ordinal — and the
  revised shape `olim (λ n → ω-rank-pow ω ·ℕ n)` denoting
  `ω^(ω+1)` that resolves it); and the decoration-bridge R5
  exploratory scaffold from PR #129.

* `docs/echo-types/MAP.adoc`.  Buchholz module list adds
  `HeadOmegaInversion` next to `HeadOmega`.

No prose-vs-proof inconsistency remains: every doc that mentions
the head-Ω route now reports its current state (which slices landed,
which slice remains, what the prerequisites for the remaining slice
are) consistent with the Agda artefacts in
`Ordinal.Buchholz.{HeadOmega,HeadOmegaInversion,RankPow}` and the
session-arc entry in `CLAUDE.md`.

`scripts/kernel-guard.sh`: PASS.  No Agda modules touched.

https://claude.ai/code/session_013nLEeKZXpvHnrDZMgRm19S

Author: claude

CHANGELOG.md

@@ -23,6 +23,52 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
     a two-level compositional convenience) — first slice of option
     (A) for the remaining `<ᵇ-+1` joint-bplus discharge; no
     rank-mono yet.
+- *Lane 3 head-Ω route — Slice 2 + Slice 2-omega + inversion (option (b))
+  landed.* Follow-on to the Slice 1 head-Ω landing above (session night,
+  PRs #130 + #131):
+  - `Ordinal.Buchholz.RankPow` gains `ω-rank-pow-succ : OmegaIndex →
+    Ord` with per-marker strict dominance at *both* branches
+    (`ω-rank-pow-<-succ-fin` via `ω^-strict-mono-suc`;
+    `ω-rank-pow-<-succ-omega` via the `Brouwer/OmegaPow.ω^-strict-mono-suc`
+    template mirrored at `ω-rank-pow ω`) plus the unified
+    `ω-rank-pow-<-succ : ∀ μ → ω-rank-pow μ <′ ω-rank-pow-succ μ`,
+    plus atomic-rank factoring through `head-Ω`
+    (`rank-pow-bOmega-via-head-Ω`, `rank-pow-bpsi-via-head-Ω`).
+  - Slice 2-omega closes a Brouwer-encoding hazard the original
+    CLAUDE.md proposal would have tripped: the proposed
+    `ω-rank-pow-succ ω = olim (λ n → ω^(suc(suc n)))` is
+    equi-ordinal with `ω-rank-pow ω = olim (λ n → ω^(suc n))`
+    (both denote `ω^ω`), so cannot strictly dominate.  The
+    revised shape `olim (λ n → ω-rank-pow ω ·ℕ n)` denotes
+    `ω^(ω+1)` and goes strictly higher via `X≤′oz⊕X` +
+    `⊕-mono-<-right (ω-rank-pow-pos ω)`.  Full record in
+    `Ordinal.Buchholz.RankPow`'s "History note" block.
+  - New module `Ordinal.Buchholz.HeadOmegaInversion` lands the
+    option-(b) inversion lemmas `head-Ω-inv-bOmega :
+    bOmega ν <ᵇ y → ν <Ω head-Ω y` (strict — three constructors
+    with `bOmega ν` LHS all carry strict `<Ω` witnesses) and
+    `head-Ω-inv-bpsi : bpsi ν α <ᵇ y → ν ≤Ω head-Ω y` (non-strict —
+    the `<ᵇ-ψΩ≤` constructor tops out at `≤Ω`).  Both proved by
+    structural recursion on the `<ᵇ` derivation; no rank-mono
+    dependency.  Picking option (b) over option (a) keeps the
+    eventual `rank-pow-dominated-by-head-Ω` (Slice 2-bplus,
+    remaining open) independent of the still-open `rank-pow-mono-≤ᵇ`
+    on the original `_<ᵇ_`.
+- *Decoration bridge — R5 exploratory entry scaffolded (PR #129).*
+  `docs/echo-types/explorations/decoration-bridge/` lands a bounded
+  exploration of whether the Choreo × Graded integration shape
+  resembles adjacent-domain decoration constructions (CRDTs, gossip,
+  local-first causal histories).  Scope strictly the one axis pair
+  `EchoIntegration.agda` already integrates; external candidates
+  framed as analogies-with-falsifiers, never as evidence of recipe
+  generalisation.  Sits as `roadmap.adoc` § R5 (deferred research)
+  with explicit termination criteria (Track A/B/C failure, all
+  candidates retired, redundancy with retracted framing,
+  forbidden-rebrandings register addition, retraction-watch trip).
+  Companion Agda module `proofs/agda/EchoDecorationBridge.agda` —
+  deliberately not in `All.agda`, classified as "Exploratory (not in
+  All.agda)" in `docs/echo-types/echo-kernel-note.adoc` so CI's
+  classification-drift lint stays green.
 - *Lane 5 tutorial track — the originally-scaffolded triplet is
   complete.* `tutorial/` ships three worked walkthroughs with
   honest-bound disclosure at top + matched-negative `NotProved-*`

EXPLAINME.adoc

@@ -33,7 +33,7 @@ Per `.machine_readable/6a2/STATE.a2ml`:
 Ongoing tracks at a glance (point-in-time, see `roadmap.adoc` for the live status):
 
 * *Identity claim.* `docs/retractions.adoc` R-2026-05-18 narrows the public claim to a *loss-graded reindexing modality* over a thin poset (not a graded comonad). Every newer artefact is stated within those narrowings.
-* *Ordinal / Buchholz track.* 11 of 13 per-constructor rank-mono cases closed under the WfCNF-restricted `_<ᵇ⁻_` via the `RankPow` / `RankAdm` / `RankLex` slices. Remaining open case `<ᵇ-+1` joint-bplus has the `Ordinal.Buchholz.HeadOmega` first slice landed; rank-mono follow-ons designed. See `docs/echo-types/buchholz-rank-obstruction.adoc`.
+* *Ordinal / Buchholz track.* 11 of 13 per-constructor rank-mono cases closed under the WfCNF-restricted `_<ᵇ⁻_` via the `RankPow` / `RankAdm` / `RankLex` slices. Remaining open case `<ᵇ-+1` joint-bplus is in flight under the head-Ω domination route: `head-Ω` (Slice 1) + `ω-rank-pow-succ` with per-marker strict dominance at both branches (Slice 2 + Slice 2-omega) + the option-(b) head-Ω inversion lemmas (`Ordinal.Buchholz.HeadOmegaInversion`) all landed; only the WfCNF-carrier structural recursion (Slice 2-bplus) remains. See `docs/echo-types/buchholz-rank-obstruction.adoc`.
 * *Tutorial track (Lane 5).* Three worked walkthroughs under `tutorial/` (certified region-exit audit, epistemic erasure, provenance/debugging echo); each carries an honest-bound disclosure at the top and a matched-negative block at the bottom. The tutorial tree builds with the repo root added to the Agda include path; see `tutorial/README.adoc`.
 * *Establishment track (Pillar E).* Internal programme (Pillars A–D) complete since 2026-05-17. The paper (`docs/echo-types/paper.adoc`) is a living draft with remaining `[EXPAND]` tags; the venue + Zenodo + outreach plan sits in `docs/echo-types/pillar-e-offline.adoc` (author-driven).
 

docs/echo-types/MAP.adoc

@@ -92,7 +92,7 @@ Staged Buchholz-style collapsing in `--safe --without-K`.
 
 * Proofs: `proofs/agda/Ordinal/` (`Buchholz/`, `Brouwer`, `CNF`,
   `Closure`, `Psi…`, `ExtendedOrder`, `RankPow`, `RankAdm`,
-  `RankLex`, `HeadOmega`).
+  `RankLex`, `HeadOmega`, `HeadOmegaInversion`).
 * 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,18 +305,22 @@ 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 | `rank-pow (bplus z₁ z₂)` is not additive principal in general (it's a sum of additive principals).  Discharging requires a coarser bound (e.g., dominate by `ω-rank-pow` of the leading subterm's Ω-index) or a structurally richer rank.
+| `<ᵇ-+1`    | ⏳ joint-bplus, head-Ω route in flight | The dominator-function unblock (option A from `RankPow.agda`'s preamble) is now partially landed: `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`, and the option-(b) head-Ω inversion lemmas `head-Ω-inv-{bOmega,bpsi}` (`Ordinal.Buchholz.HeadOmegaInversion`).  Remaining: the WfCNF-carrier structural recursion `rank-pow-dominated-by-head-Ω` (Slice 2-bplus) + the headline `rank-mono-<ᵇ-+1-via-head-Ω` discharge.  No further rank-mono dependency in the bplus case — option (b) bought independence from the still-open `rank-pow-mono-≤ᵇ`.
 | `<ᵇ-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 deferred under an explicit blocker (`<ᵇ-+1` joint-bplus);
-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).
-Only `<ᵇ-+1` joint-bplus remains in the per-constructor matrix.*
+slice); 1 in flight under the head-Ω route with abstraction +
+per-marker dominances + inversion lemmas landed (`<ᵇ-+1` joint-bplus,
+Slice 2-bplus 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,
+session-night PR #130 closing Slice 2, PR #131 closing Slice 2-omega +
+option (b) inversion).  Only `<ᵇ-+1` joint-bplus remains in the
+per-constructor matrix.*
 
 === What remains open
 
@@ -331,13 +335,22 @@ Only `<ᵇ-+1` joint-bplus remains in the per-constructor matrix.*
   case ν=μ no longer needs the additive-principal closure; the
   admissibility bound `rank-pow α <′ ω-rank-pow ν` discharges it
   directly on the second component of the lex pair.
-* *`<ᵇ-+1` joint-bplus*.  Needs either a coarser dominator (e.g., a
-  function `BT → OmegaIndex` returning the leading Ω-index, then
-  rank into `ω-rank-pow ∘ leading-index`) or a richer rank shape.
-  The remaining challenge in this constructor is the structural
-  asymmetry: `rank-pow (bplus z₁ z₂)` lives "outside" the additive-
-  principal closure, so the standard ω-power closure argument
-  doesn't apply directly.
+* *`<ᵇ-+1` joint-bplus* — *Slice 2-bplus remaining only.*  The
+  head-Ω route's prerequisite slices are all landed: `head-Ω`
+  (Slice 1), `ω-rank-pow-succ` + per-marker strict dominance at
+  both branches (Slice 2 + Slice 2-omega), and the option-(b)
+  head-Ω inversion lemmas (preserving the dependency-graph
+  invariant that the eventual `rank-pow-dominated-by-head-Ω`
+  doesn't depend on the still-open `rank-pow-mono-≤ᵇ`).
+  Slice 2-bplus proves the WfCNF-carrier structural recursion
+  `rank-pow-dominated-by-head-Ω : (t : BT) → NonBzero t → WfCNF t
+  → rank-pow t <′ ω-rank-pow-succ (head-Ω t)` and the headline
+  `rank-mono-<ᵇ-+1-via-head-Ω`.  The `Slice 2-omega` historical
+  hazard (the originally-proposed `ω-rank-pow-succ ω` shape
+  `olim (λ n → ω^(suc(suc n)))` is equi-ordinal with `ω-rank-pow ω`,
+  so doesn't strictly dominate) is resolved by the revised shape
+  `olim (λ n → ω-rank-pow ω ·ℕ n)` (denoting `ω^(ω+1)`) — see
+  `RankPow.agda`'s "History note" comment block for the full record.
 * *Mutual recursion for `rank-pow-mono-<ᵇ⁻`*.  The case-specific
   primitives above are individually proven, but the umbrella theorem
   `x <ᵇ⁻ y → rank-pow x <′ rank-pow y` needs a mutual `<ᵇ` / `≤ᵇ`
@@ -360,6 +373,16 @@ exhibited.
 
 == See also
 
+* `proofs/agda/Ordinal/Buchholz/HeadOmega.agda` — Slice 1; the
+  `head-Ω : BT → OmegaIndex` leading-Ω-index head function + four
+  per-constructor sanity lemmas.
+* `proofs/agda/Ordinal/Buchholz/HeadOmegaInversion.agda` — option (b)
+  Slice 2-bplus prerequisite; `head-Ω-inv-bOmega`, `head-Ω-inv-bpsi`
+  extracting `head-Ω` bounds from an `<ᵇ` witness without a
+  rank-mono dependency.
+* `proofs/agda/Ordinal/Buchholz/RankPow.agda` — Slice 2 + Slice 2-omega;
+  `ω-rank-pow-succ` + per-marker strict dominance at both branches +
+  the unified `ω-rank-pow-<-succ`.
 * `proofs/agda/Ordinal/Buchholz/Order.agda` — the K-free core; the
   13 constructors that pin the syntactic order.
 * `proofs/agda/Ordinal/Buchholz/WellFounded.agda` — the direct

roadmap.adoc

@@ -202,18 +202,24 @@ separate branches.
 constructors closed via the budgeted route + `_<ᵇ⁰_` umbrella + Lane 3
 follow-ons (`<ᵇ⁺-ψα` via `RankAdm` 2026-05-26; `<ᵇ-ψΩ≤` at both
 `ν<μ` and the `ν=μ` boundary via `RankLex` 2026-05-27). One
-constructor case (`<ᵇ-+1` joint-bplus) remains open with the
-`Ordinal.Buchholz.HeadOmega` first slice landed 2026-05-27; rank-mono
-follow-ons designed in `RankPow.agda`'s preamble and the obstruction
-doc.
+constructor case (`<ᵇ-+1` joint-bplus) is in flight under the
+head-Ω domination route (option A from `RankPow.agda`'s preamble):
+the abstraction (`head-Ω` + `ω-rank-pow-succ`), the per-marker
+strict dominances at *both* branches, the unified `ω-rank-pow-<-succ`,
+and the option-(b) head-Ω inversion lemmas have all landed across
+PRs #124 (Slice 1, 2026-05-27 late evening), #130 (Slice 2, session
+night), and #131 (Slice 2-omega + inversion + ledger).  Only Slice
+2-bplus — the WfCNF-carrier structural recursion — remains.
 
 *Close-out criterion.* Either:
 
 * the remaining `<ᵇ-+1` joint-bplus case closes via the head-Ω
-  domination route (Slice 2 = `ω-rank-pow-succ` + the domination
-  lemma; Slice 3 = the headline `rank-mono-<ᵇ-+1-via-head-Ω`;
-  Slice 4 = full `rank-pow-mono-<ᵇ⁻` umbrella composition),
-  unblocking full `wf-<ᵇʳᶠ`; OR
+  domination route's Slice 2-bplus (`rank-pow-dominated-by-head-Ω`
+  by structural recursion on WfCNF, consuming the already-landed
+  `head-Ω-inv-{bOmega,bpsi}` + `ω-rank-pow-<-succ`; then the
+  headline `rank-mono-<ᵇ-+1-via-head-Ω` discharge, then the full
+  `rank-pow-mono-<ᵇ⁻` umbrella composition), unblocking full
+  `wf-<ᵇʳᶠ`; OR
 * a falsifiable verdict lands stating that the unbudgeted promotion
   cannot close under `--safe --without-K` for the current `_<ᵇ_`,
   with the WfCNF-restricted `_<ᵇ⁻_` accepted as the final form.