docs: ResidueForm instance count correction (6 → 8) + Slice 3 closure update

hyperpolymath · claude · hyperpolymath · commit 0bf9778a3163 · 2026-05-28T10:21:49.000+01:00
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 added `indexed-residue` + `cost-residue` (lines 181-234 of EchoResidueTaxonomy.agda) on top of the original endpoint pair + generic Σ-cert + linear-affine. PR #139 then added `search-residue` + `epistemic-residue`, taking the total to eight. Files updated: - CHANGELOG.md — PR #139 entry rephrased: six → eight, with the pre-#139 six explicitly attributed to the 2026-05-27 audit follow-on. - docs/echo-types/MAP.adoc — eight instances enumerated, grouped by landing date. - README.md — Tier 2 mermaid label updated to "8 instances incl. Indexed, Cost, Search, Epistemic". - readme.adoc — Tier 2 list line updated to 8 with the same enumeration. ## Slice 3 closure: PRs #142 + #143 PR #144 said the Slice 3 umbrella case-split was the remaining wiring and the `bpsi=bpsi at equal markers` sub-case still needed `α`'s rank via rank-adm / rank-lex. Both have now landed: - PR #142 — Slice 3 umbrella extension: `_<ᵇ¹_` extension with joint-bplus constructor + strict-head dispatch wires the Slice 3 headline (from #141) into the umbrella. - PR #143 — Slice 3 lex-rank companion: the `bpsi-source-at- equality` ψ-rank discharge closes the last remaining sub-case via rank-lex (exactly the path #144 named as remaining work). Files updated: - CHANGELOG.md — new Slice 3 follow-on bullet covering #142 + #143; framed as "substantively complete via head-Ω + lex-rank composition" rather than hard-claiming full closure (the wider paper-critical-path claims live in `roadmap.adoc` not the CHANGELOG). - EXPLAINME.adoc — Slice 3 line revised to acknowledge umbrella + lex-rank closures. ## Verification scripts/kernel-guard.sh PASS — both checks green. No Agda code changed. Refs: echo-types#142 (umbrella), echo-types#143 (lex-rank companion), echo-types#144 (the now-corrected narrative refresh). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
diff --git a/CHANGELOG.md b/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`
diff --git a/EXPLAINME.adoc b/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).
diff --git a/README.md b/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)"]
diff --git a/docs/echo-types/MAP.adoc b/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
diff --git a/readme.adoc b/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`
 
