docs: ResidueForm count 6→8 + Slice 3 closure (#142 + #143) (#145)

## Summary

Two corrections to PR #144's narrative refresh.

## ResidueForm instance count: 6 → 8

PR #144 stated the post-#139 ResidueForm count as six. The actual count
is eight. The pre-#139 baseline was already six (not four): the
2026-05-27 audit-follow-on landed \`indexed-residue\` + \`cost-residue\`
(lines 181–234 of EchoResidueTaxonomy.agda). PR #139 then added
\`search-residue\` + \`epistemic-residue\`, for a total of 8.

## Slice 3 closure: PRs #142 + #143

PR #144 framed the Slice 3 umbrella case-split as remaining work and the
\`bpsi=bpsi at equal markers\` sub-case as still needing α's rank via
rank-adm / rank-lex. Both landed in PRs #142 + #143:

- **PR #142** — \`_<ᵇ¹_\` extension with joint-bplus + strict-head
dispatch wires the headline (from #141) into the umbrella.
- **PR #143** — \`bpsi-source-at-equality\` ψ-rank discharge closes the
last sub-case via rank-lex.

CHANGELOG + EXPLAINME updated to acknowledge both.

## Files

- CHANGELOG.md — count fix + new Slice 3 follow-on bullet (#142 + #143)
- EXPLAINME.adoc — Slice 3 narrative refreshed
- docs/echo-types/MAP.adoc — 8 instances enumerated with landing dates
- README.md — Tier 2 mermaid label
- readme.adoc — Tier 2 list mirror

## Verification

\`scripts/kernel-guard.sh\` PASS. No Agda code changed.

## Test plan

- [x] kernel-guard.sh PASS
- [ ] Admin-merge if budget permits

Refs: echo-types#142, echo-types#143, echo-types#144.

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

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

Author: hyperpolymath

CHANGELOG.md

@@ -47,10 +47,22 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
 - *Classification grid — Search + Epistemic ResidueForm instances.*
   PR #139: `EchoResidueTaxonomy.agda` gains two further `ResidueForm
   f R` instances (`Search` and `Epistemic`) alongside the existing
-  four (trivial, identity, generic Σ-cert, linear-affine). Brings
-  the total to six instances, with the other four decoration
+  six (trivial, identity, generic Σ-cert, linear-affine, indexed,
+  cost; the 2026-05-27 audit-follow-on lands of `indexed-residue` +
+  `cost-residue` are what made the pre-#139 count six). Brings the
+  total to **eight instances**, with the remaining two decoration
   modules documented as structurally compatible.
 
+- *Lane 3 ordinal track — Slice 3 umbrella + lex-rank companion.*
+  PR #142 extends `_<ᵇ¹_` with the joint-bplus constructor + the
+  strict-head dispatch that wires the Slice 3 headline
+  (`rank-mono-<ᵇ-+1-via-head-Ω` from PR #141) into the umbrella
+  case-split. PR #143 adds the lex-rank companion: the
+  `bpsi-source-at-equality` ψ-rank discharge — the very sub-case
+  PR #144's CHANGELOG described as still requiring `α`'s rank via
+  rank-adm or rank-lex. The `<ᵇ-+1` joint-bplus rank-mono closure
+  is now substantively complete via the head-Ω+lex-rank composition.
+
 - *Visual identity — banner kit ("Diagrammatic Hush").* PR #140:
   `docs/assets/banner.{png,svg}`, `docs/assets/banner-philosophy.md`,
   `tools/banner/build-banner.mjs`. The `README.md` and `readme.adoc`

EXPLAINME.adoc

@@ -34,8 +34,8 @@ Ongoing tracks at a glance (point-in-time, see `roadmap.adoc` for the live statu
 
 * *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. The remaining `<ᵇ-+1` joint-bplus case is now FULLY CLOSED (2026-05-27) via 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`) + the WfCNF-carrier structural recursion (Slice 2-bplus, `Ordinal.Buchholz.RankPowDomination.rank-pow-dominated-by-head-Ω`). See `docs/echo-types/buchholz-rank-obstruction.adoc`.
-* *Ordinal / Buchholz track — Slice 3 (2026-05-28).* `Ordinal.Buchholz.RankPowSlice3` lands three primitives — `NonBzero` (left-spine non-bzero predicate), `ω-rank-pow-succ-≤-via-<Ω` (strict-jump bridge), and `head-Ω-lower-bound` (dual of `rank-pow-dominated-by-head-Ω`). On top of those, `Ordinal.Buchholz.RankPowSlice3Headline` closes the Slice 3 headline `rank-mono-<ᵇ-+1-via-head-Ω` via Route A — a clean chain through the four prerequisites with no structural recursion, taking the strict-head premise `head-Ω x₁ <Ω head-Ω y₁` as an *external hypothesis*. The umbrella case-split is the remaining wiring; the `bpsi = bpsi at equal markers` sub-case still needs `α`'s rank via rank-adm or rank-lex.
-* *Canonical identity layer (Tier 1 + Tier 2 extensions, 2026-05-28).* `EchoImageFactorizationProp` lands the (epi, mono) earn-back module, module-parameterised in a truncation interface (Tier 2, adjacent to `EchoImageFactorization`). `EchoResidueTaxonomy`'s `ResidueForm f R` record gains `Search` and `Epistemic` instances alongside the existing four (trivial, identity, generic Σ-cert, linear-affine).
+* *Ordinal / Buchholz track — Slice 3 (2026-05-28).* `Ordinal.Buchholz.RankPowSlice3` lands three primitives — `NonBzero` (left-spine non-bzero predicate), `ω-rank-pow-succ-≤-via-<Ω` (strict-jump bridge), and `head-Ω-lower-bound` (dual of `rank-pow-dominated-by-head-Ω`). On top of those, `Ordinal.Buchholz.RankPowSlice3Headline` closes the Slice 3 headline `rank-mono-<ᵇ-+1-via-head-Ω` via Route A — a clean chain through the four prerequisites with no structural recursion, taking the strict-head premise `head-Ω x₁ <Ω head-Ω y₁` as an *external hypothesis*. PR #142 wired the umbrella case-split (`_<ᵇ¹_` extension with joint-bplus + strict-head dispatch). PR #143 added the lex-rank companion: the `bpsi-source-at-equality` ψ-rank discharge — closing the last remaining sub-case via rank-lex. The `<ᵇ-+1` joint-bplus rank-mono closure is now substantively complete via the head-Ω + lex-rank composition.
+* *Canonical identity layer (Tier 1 + Tier 2 extensions, 2026-05-28).* `EchoImageFactorizationProp` lands the (epi, mono) earn-back module, module-parameterised in a truncation interface (Tier 2, adjacent to `EchoImageFactorization`). `EchoResidueTaxonomy`'s `ResidueForm f R` record gains `Search` and `Epistemic` instances bringing the total to eight (alongside the existing trivial, identity, generic Σ-cert, linear-affine, indexed, cost — the latter two landed 2026-05-27 as audit follow-ons).
 * *CI / foundational hygiene (2026-05-28).* Kernel-guard discipline scaled to the canonical-identity cohort: 18 previously-unclassified `Echo*.agda` modules (the canonical-identity / OFS cohort plus the application/extension modules — `EchoEntropy`, `EchoLLEncoding`, `EchoProvenance`, `EchoSecurity`, `EchoProbabilisticSupport`, `EchoDifferential`) are now classified in `docs/echo-types/echo-kernel-note.adoc`. The (now-stale) `N5Falsifier` xfail gate was removed from `.github/workflows/agda.yml` following the 2026-05-27 resolution of `proofs/agda/characteristic/N5Falsifier.agda` (the unsolved-metas were an inference blocker, not a content blocker; four `applyRole` / `applyGrade` call sites had their implicit `r` / `grade` pinned). This is infrastructure honesty, not a proof-content advance.
 * *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).

README.md

@@ -33,7 +33,7 @@ flowchart TD
     AD["<b>Pillars A–D</b> (establishment plan, LANDED 2026-05-17)<br/>A: echo↔fib · B: pullback UP · C: separating model · D: carrier-parametric"]
     PF["<b>Pillar F gates</b> (earn-back, ALL PASSED)<br/>F1: graded-comonad witness · F2: 2nd Echo-functor model<br/>F3: 2nd non-iso grade-monoid · F4: funext-qualified pullback UP<br/>F5: funext-qualified full OFS"]
     T1["<b>Tier 1 · Canonical identity layer</b> (2026-05-27, extended 2026-05-28)<br/>EchoTotalCompletion (A ≃ Σ B Echo f) · OFS-witness · Image · no-section-of-collapsing-map · ImageFactorizationProp (epi,mono earn-back)"]
-    T2["<b>Tier 2 · Classification grid</b><br/>LossTaxonomy (function-side) · ResidueTaxonomy (residue-side, 6 instances incl. Search + Epistemic) · DecorationStructure · _≡m_"]
+    T2["<b>Tier 2 · Classification grid</b><br/>LossTaxonomy (function-side) · ResidueTaxonomy (residue-side, 8 instances incl. Indexed, Cost, Search, Epistemic) · DecorationStructure · _≡m_"]
     T3["<b>Tier 3 · Qualified universal property</b> (Gate F5)<br/>echo-factorisation-strict · diagonal lifting · factorisation uniqueness up to iso"]
     AUD["<b>Audience surfaces</b><br/>EchoProvenance · EchoSecurity · EchoProbabilisticSupport · EchoDifferential"]
     SUITE["<b>EchoCanonicalIdentitySuite</b><br/>(curated single-file entry point)"]

docs/echo-types/MAP.adoc

@@ -98,11 +98,13 @@ in the Pillar F4 template style.
   `proofs/agda/EchoLossTaxonomy.agda`.
 * *Residue taxonomy* (residue-side) — `record ResidueForm f R`
   packaging the per-output residue carrier + lowering shared by the
-  eight decoration modules. Six instances (as of 2026-05-28): trivial
-  (⊤), identity (`Echo f`), generic Σ-cert (`echoR-residue`),
-  `linear-affine-residue`, and the newer `Search` + `Epistemic`
-  forms. The other four decoration modules documented as structurally
-  compatible.
+  eight decoration modules. Eight instances (as of 2026-05-28):
+  the original endpoint pair (trivial (⊤), identity (`Echo f`)),
+  the generic Σ-cert (`echoR-residue`), `linear-affine-residue`,
+  the 2026-05-27 audit-follow-ons `indexed-residue` +
+  `cost-residue`, and the 2026-05-28 additions `search-residue` +
+  `epistemic-residue`. The remaining two decoration modules
+  documented as structurally compatible.
   `proofs/agda/EchoResidueTaxonomy.agda`.
 * *Decoration structure* (observation-side) — `record
   DecorationStructure G` packaging the seven-field decoration

readme.adoc

@@ -74,7 +74,7 @@ Tier 1 (the canonical identity layer itself):
 Tier 2 (the classification grid):
 
 * `EchoLossTaxonomy.agda` — function-side four-axis (EQUIV / INJ / SURJ / CONST)
-* `EchoResidueTaxonomy.agda` — `ResidueForm` record + 6 instances (trivial, identity, generic Σ-cert, linear-affine, Search, Epistemic; the last two added 2026-05-28)
+* `EchoResidueTaxonomy.agda` — `ResidueForm` record + 8 instances (trivial, identity, generic Σ-cert, linear-affine, indexed, cost, search, epistemic; indexed+cost from 2026-05-27 audit-follow-on, search+epistemic from 2026-05-28 PR #139)
 * `EchoDecorationStructure.agda` — `DecorationStructure` record + abstract degrade-compose
 * `EchoObservationalEquivalence.agda` — mode-indexed `_≡m_` on `LEcho`