ordinal(buchholz): head-Ω Slice 2 closure + inversion + cross-doc + ledger reinforcement (#131)

Six commits closing out the Lane 3 head-Ω route's Slice 2 family:

1. CLAUDE.md session-arc entry for Slice 2 (PR #130's rung).
2. New module Ordinal.Buchholz.HeadOmegaInversion with option-(b)
   head-Ω inversion lemmas — no rank-mono dependency.
3. Slice 2-omega: ω branch of ω-rank-pow-succ replaced with a
   strictly-larger shape; per-marker dominance proved at both
   branches; unified ω-rank-pow-<-succ lemma added.
4. CLAUDE.md next-Claude plan updated.
5. Cross-doc consistency sweep across buchholz-rank-obstruction,
   roadmap § Lane 3, EXPLAINME, CHANGELOG, MAP.
6. Deeper-sweep gaps closed: bridge-status row #4 refreshed +
   new row #6 for decoration bridge; CAUTION banner on
   buchholz-plan.adoc pointing to the live tracker.

Only Slice 2-bplus (the WfCNF-carrier structural recursion)
remains; all prerequisites landed.

scripts/kernel-guard.sh PASS.  No postulates introduced.
--safe --without-K throughout.

Admin-merged before CI green at user request.

Author: hyperpolymath

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-*`

CLAUDE.md

@@ -193,7 +193,107 @@ work to `main` and refresh all documentation:
 
 ## Current rung state (2026-05-27)
 
-### Session arc 2026-05-27 evening — Lane 5 Walkthrough 3 landed (read this first)
+### Session arc 2026-05-27 night — Lane 3 head-Ω Slice 2 landed (read this first)
+
+*Where we started today (commit `65806f4` on `main`, post-#129):* the
+PR #129 decoration-bridge scaffold landed under R5; Lane 3's head-Ω
+domination route had Slice 1 (`HeadOmega.agda`) but no Slice 2 work.
+The `<ᵇ-+1` joint-bplus case remained open with `head-Ω` defined but
+not yet consumed by any rank-mono primitive.
+
+*Where we ended today (commit `bf9ee6e` on `main`, post-#130):* Slice 2
+lands the abstraction (`ω-rank-pow-succ` + the fin-branch strict
+dominance) plus an honest obstruction note on the ω branch:
+
+1. *`Ordinal.Buchholz.RankPow.agda` additions.*
+   * `ω-rank-pow-succ : OmegaIndex → Ord` — the per-marker "next
+     ω-power up" target.  Fin branch is `ω^(suc(suc n))`; ω branch
+     reuses the original CLAUDE.md proposal `olim (λ n →
+     ω^(suc(suc n)))` so the abstraction is in place for follow-on
+     slices to inspect and (if needed) override.
+   * `ω-rank-pow-succ-fin` — definitional sanity at the fin branch.
+   * `ω-rank-pow-<-succ-fin` — per-marker strict dominance at fin
+     via `ω^-strict-mono-suc (suc n)`.
+   * `rank-pow-bOmega-via-head-Ω`, `rank-pow-bpsi-via-head-Ω` —
+     atomic-rank `refl`-shape primitives factoring `rank-pow` through
+     `head-Ω` for the two non-bplus, non-bzero `BT` constructors.
+
+2. *`Ordinal.Buchholz.Smoke.agda` pinning.*  Five headlines pinned
+   under their own `using` block with a header comment, per CLAUDE.md
+   Working rules.
+
+*Obstruction note.*  The originally-proposed CLAUDE.md shape
+`ω-rank-pow-succ ω = olim (λ n → ω^(suc(suc n)))` represents the
+**same** ordinal as `ω-rank-pow ω = olim (λ n → ω^(suc n))` — both
+are `sup{ω^(n+1) : n ∈ ℕ} = ω^ω`, with different ℕ-indexings of the
+same tail.  Strict dominance at the ω branch therefore cannot hold
+under that shape.  Inline `RankPow.agda` comments document two
+follow-on slices:
+
+* *Slice 2-omega.*  Replace the ω branch with a genuinely
+  strictly-larger ordinal.  Candidate: `ω^(ω+1)` encoded as
+  `olim (λ n → (ω-rank-pow ω) ·ℕ n)`.  Three cross-checks
+  documented inline before committing (closure under ordinal
+  addition; the consumer's actual additive-principal need; sanity-
+  check of the indexing's leading `oz ⊕` which is NOT definitionally
+  `ω-rank-pow ω` under Brouwer's right-recursing `_⊕_`).
+* *Slice 2-bplus.*  Prove the full
+  `rank-pow-dominated-by-head-Ω : (t : BT) → NonBzero t → WfCNF t →
+  rank-pow t <′ ω-rank-pow-succ (head-Ω t)` by structural recursion
+  on WfCNF.  The bplus case needs a `rank-pow-mono-≤ᵇ` companion for
+  the original `_<ᵇ_` (the WfCNF tail bound is `_≤ᵇ_`, not `_≤ᵇ⁰_`).
+  Marked `TODO(slice-2-bplus)` inline.  Option (b) — head-Ω inversion
+  that does not transitively depend on rank-mono — is preferred
+  because it keeps `rank-pow-dominated-by-head-Ω` independent of
+  the companion so signature changes don't silently propagate.
+
+Build invariant held: `proofs/agda/All.agda` + `proofs/agda/Smoke.agda`
++ `Ordinal/Buchholz/Smoke.agda` all exit 0 under `--safe --without-K`,
+zero postulates, no funext.  `scripts/kernel-guard.sh` PASS.
+
+PR #130 was admin-merged before CI green at user direction; CI was
+still all-12-queued at merge time.  No CI failures have surfaced
+since (treat any later red as authoritative if it does).
+
+*Plan for the next Claude.*
+
+Within this same session (2026-05-27 night, PR #131), items (1) and
+(2) from the original plan also landed:
+
+* *(1) Option (b) head-Ω inversion lemma — LANDED* (commit `560f904`).
+  New module `Ordinal.Buchholz.HeadOmegaInversion` ships
+  `head-Ω-inv-bOmega : bOmega ν <ᵇ y → ν <Ω head-Ω y` (strict) and
+  `head-Ω-inv-bpsi : bpsi ν α <ᵇ y → ν ≤Ω head-Ω y` (non-strict —
+  tracks the `<ᵇ-ψΩ≤` constructor).  Pinned in
+  `Ordinal/Buchholz/Smoke.agda` under its own `using` block.  Wired
+  into `All.agda`.  No rank-mono dependency — that was the
+  load-bearing dependency-graph invariant the design called for.
+* *(2) Slice 2-omega — LANDED* (commit `07abc15`).  ω branch of
+  `ω-rank-pow-succ` replaced with `olim (λ n → ω-rank-pow ω ·ℕ n)`
+  (= `ω^(ω+1)`); per-marker strict dominance proved at the ω
+  branch via a mirror of `Brouwer/OmegaPow.ω^-strict-mono-suc`
+  (branch-index-2 + `X≤′oz⊕X` + `⊕-mono-<-right (ω-rank-pow-pos ω)`).
+  Unified `ω-rank-pow-<-succ : ∀ μ → ω-rank-pow μ <′
+  ω-rank-pow-succ μ` covers both branches.
+
+Only one item remains open:
+
+3. *Slice 2-bplus* — prove the full domination lemma
+   `rank-pow-dominated-by-head-Ω : (t : BT) → NonBzero t → WfCNF t →
+   rank-pow t <′ ω-rank-pow-succ (head-Ω t)` by structural recursion
+   on the WfCNF carrier.  Both per-marker dominances now hold; the
+   atomic cases discharge via `rank-pow-{bOmega,bpsi}-via-head-Ω` +
+   `ω-rank-pow-<-succ`.  The bplus case consumes
+   `head-Ω-inv-{bOmega,bpsi}` from `HeadOmegaInversion` to pull
+   `head-Ω` bounds from the WfCNF tail's `<ᵇ` witness.  No further
+   inversion-via-rank-mono dependency is introduced — that's what
+   option (b) bought.
+
+DO NOT reopen: the closed 11/13 Buchholz constructors; the W1/W2/W3
+walkthroughs; the R-2026-05-18 narrowings; the closed fin-branch /
+ω-branch / unified dominances; the head-Ω inversion family.
+
+### Session arc 2026-05-27 evening — Lane 5 Walkthrough 3 landed
 
 *Where we started today (commit `4d77d75` on `docs/consolidate-roadmaps-
 and-sigma-skepticism-2026-05-26`, post-#123):* the consolidation branch

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/bridge-status.md

@@ -23,13 +23,19 @@ This document strictly tracks the status of experimental extensions and bridges
 - **Core Affect:** NO
 
 ## 4. Buchholz / Veblen Ordinals
-- **Status:** BLOCKED
+- **Status:** PARTIAL (11/13 constructors closed under WfCNF; 1 in flight)
 - **Dependencies:** Standard Agda
-- **Blockers:** Well-foundedness of shared-binder cases is blocked by the failure of the self-lift.
+- **Blockers:** `<ᵇ-+1` joint-bplus is the single remaining open constructor. The head-Ω domination route (option A) has its abstraction + per-marker dominances at both branches + the option-(b) head-Ω inversion lemmas all landed across 2026-05-27 (PRs #124 / #130 / #131); only the WfCNF-carrier structural recursion (Slice 2-bplus) remains. The earlier shared-binder-self-lift blocker is resolved (`RankAdm` + `RankLex` slices, 2026-05-26/27). Live tracker: `docs/echo-types/buchholz-rank-obstruction.adoc`.
 - **Core Affect:** NO
 
 ## 5. JanusKey / Categorical
 - **Status:** EXPLORATORY
 - **Dependencies:** Categorical foundations
 - **Blockers:** Higher-level abstractions (monads, adjunctions) are still evolving; core functors are stable.
 - **Core Affect:** NO
+
+## 6. Decoration bridge (conceptual, not cross-repo)
+- **Status:** EXPLORATORY (R5 deferred-research; cleanly abandonable)
+- **Dependencies:** `EchoIntegration`, `EchoChoreo`, `EchoGraded` (import only)
+- **Blockers:** Bridge is bounded by construction. Closes under any of the documented termination criteria: Track A/B/C failure, all candidate analogies retired, redundancy with retracted-prose graded-comonad framing, forbidden-rebrandings register addition, retraction-watch trip. Companion: `docs/echo-types/explorations/decoration-bridge/README.adoc`; module: `proofs/agda/EchoDecorationBridge.agda` (deliberately not in `All.agda`).
+- **Core Affect:** NO

docs/bridges/buchholz-plan.adoc

@@ -4,6 +4,21 @@
 :sectnums:
 :sectnumlevels: 2
 
+[CAUTION]
+====
+*Historical spec.*  This document is the original phased plan for the
+ordinal-notation / collapsing-function workstream as written when E1–E7
+were ahead of us.  The "PLANNED" tags below are dated; many phases have
+since landed under different module names (E1–E7 closed; the WfCNF
+restriction +  `RankPow` / `RankAdm` / `RankLex` slices replace the
+generic `Phase 2.2 rank-mono`; the WF-0/WF-1 well-foundedness is in
+`Ordinal.Buchholz.WellFounded`).  *Live per-constructor verdict*:
+`docs/echo-types/buchholz-rank-obstruction.adoc`.  *Live lane status*:
+`roadmap.adoc` § Lane 3.  *Per-session ledger*: `CLAUDE.md` § "Current
+rung state".  This file is retained for provenance and design context;
+treat its concrete "PLANNED" items as superseded.
+====
+
 [.lead]
 This document scopes the ordinal-notation / collapsing-function workstream
 (Workstream E in `roadmap.adoc`). It is a spec, not a theorem file.

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