docs: post-PR-136 narrative refresh (CHANGELOG + EXPLAINME + MAP + README) (#144)

## Summary

Surgical narrative refresh across the five canonical doc surfaces
(CHANGELOG.md, EXPLAINME.adoc, docs/echo-types/MAP.adoc, README.md,
readme.adoc) to catch up with the six PRs that landed 2026-05-28: #136
(kernel-guard fix), #137 (Slice 3 prerequisites), #138
(EchoImageFactorizationProp), #139 (ResidueTaxonomy Search + Epistemic),
#140 (banner kit), #141 (Slice 3 headline).

## Changes per file

- **CHANGELOG.md** (+78 lines) — new \`### Added (2026-05-28)\` + \`###
Fixed (2026-05-28)\` blocks covering all six PRs with honest framing
(Slice 3 headline closure described as "under a strict-head premise";
bpsi=bpsi-at-equal-markers caller-burden sub-case explicitly NOT
closed).
- **EXPLAINME.adoc** (+4 lines) — status-snapshot bullets for Slice 3,
canonical identity layer extensions, and CI / foundational hygiene; new
\`docs/echo-types/echo-kernel-note.adoc\` entry in "Where to look
first".
- **docs/echo-types/MAP.adoc** (+14 / -9 net) — new (epi, mono) bullet
adjacent to image factorisation; ResidueForm instance count 4 → 6 with
Search + Epistemic named; Buchholz proofs list gains RankPowSlice3 +
RankPowSlice3Headline with strict-head-premise framing.
- **README.md** (+2 / -2) — Tier 1 + Tier 2 mermaid node labels updated
for ImageFactorizationProp + Search/Epistemic.
- **readme.adoc** (+2 / -1) — Tier 1 + Tier 2 list mirror updated.

## Verification

- \`scripts/kernel-guard.sh\` PASS (both Check A funext-free + Check B
classification-drift).
- No Agda code touched; docs-only refresh.

## Honesty constraints preserved

- Slice 3 headline framed as closed *under a strict-head premise*, not
unconditionally.
- bpsi=bpsi-at-equal-markers caller-burden sub-case explicitly named as
NOT closed (rank-adm / rank-lex remaining work).
- PR #136 framed as "infrastructure honesty, not a proof-content
advance".
- 11/13 per-constructor rank-mono count unchanged.

## Test plan

- [x] kernel-guard.sh PASS locally
- [ ] CI green on this PR
- [ ] Admin-merge once green or budget permits

🤖 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

@@ -6,6 +6,84 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
 
 ## [Unreleased]
 
+### Added (2026-05-28)
+
+- *Lane 3 ordinal track — Slice 3 prerequisites.* PR #137 added
+  `proofs/agda/Ordinal/Buchholz/RankPowSlice3.agda` (220 lines) —
+  three primitives toward the Slice 3 headline:
+  - `NonBzero` — left-spine non-bzero predicate excluding the
+    degenerate `bplus bzero bzero` chains that WfCNF technically
+    allows but CNF normalisation excludes.
+  - `ω-rank-pow-succ-≤-via-<Ω` — strict-jump bridge from `μ <Ω ν`
+    to `ω-rank-pow-succ μ ≤′ ω-rank-pow ν`. Closes the gap between
+    Slice 2-bplus's upper bound on the source's rank and the lower
+    bound on the target's rank.
+  - `head-Ω-lower-bound` — head-Ω LOWER bound under WfCNF +
+    NonBzero. Dual of `rank-pow-dominated-by-head-Ω`.
+
+- *Lane 3 ordinal track — Slice 3 headline closed under a strict-head
+  premise.* PR #141 added
+  `proofs/agda/Ordinal/Buchholz/RankPowSlice3Headline.agda` (155
+  lines). The headline `rank-mono-<ᵇ-+1-via-head-Ω` closes the
+  joint-bplus rank-mono case for `_<ᵇ-+1_` via Route A from the
+  Slice 3 design note. The proof composes the four Slice 3
+  prerequisites in a clean chain (no structural recursion):
+  Slice 2-bplus + head-Ω-bplus → strict-jump bridge → head-Ω lower
+  bound → `⊕-left-≤-sum`, all via `≤′-trans`. The headline takes
+  the strict-head premise `head-Ω x₁ <Ω head-Ω y₁` as an EXTERNAL
+  HYPOTHESIS; the umbrella's case-split is the remaining wiring
+  (the `bpsi=bpsi` at equal markers sub-case still needs `α`'s
+  rank via rank-adm or rank-lex). Compiles standalone under
+  `--safe --without-K`, zero postulates. Smoke green.
+
+- *Canonical identity layer — (epi, mono) earn-back form.* PR #138:
+  `proofs/agda/EchoImageFactorizationProp.agda` lands the
+  (epi, mono) factorisation module-parameterised in a truncation
+  interface — the long-pending earn-back gate previously referenced
+  as "next" in `docs/echo-types/MAP.adoc`. Companion to
+  `EchoImageFactorization`. Classification: Tier 2 in
+  `docs/echo-types/echo-kernel-note.adoc`.
+
+- *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
+  modules documented as structurally compatible.
+
+- *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`
+  both gained the banner image at the top. No content impact; purely
+  visual identity for the project's public surface.
+
+### Fixed (2026-05-28)
+
+- *CI hygiene: kernel-guard classification-drift unblocked.* PR #136:
+  18 previously-unclassified `Echo*.agda` modules (the canonical-
+  identity / OFS cohort plus the application/extension modules:
+  `EchoTotalCompletion`, `EchoOrthogonalFactorizationSystem`,
+  `EchoImageFactorization`, `EchoNoSectionGeneric`,
+  `EchoLossTaxonomy`, `EchoResidueTaxonomy`,
+  `EchoDecorationStructure`, `EchoObservationalEquivalence`,
+  `EchoOFSUnivF5`/`Diag`/`Iso`, `EchoCanonicalIdentitySuite`,
+  `EchoEntropy`, `EchoLLEncoding`, `EchoProvenance`, `EchoSecurity`,
+  `EchoProbabilisticSupport`, `EchoDifferential`) are now classified
+  in `docs/echo-types/echo-kernel-note.adoc`, unblocking
+  `scripts/kernel-guard.sh` Check B (classification-drift lint).
+
+- *CI hygiene: N5Falsifier xfail gate removed.* PR #136 also dropped
+  the `Expected-failure gate (N5Falsifier is known-broken)` step
+  from `.github/workflows/agda.yml`. `proofs/agda/characteristic/
+  N5Falsifier.agda` was resolved on 2026-05-27 by pinning the
+  implicit `r` / `grade` at four `applyRole` / `applyGrade` call
+  sites — the unsolved-metas were an inference blocker, not a
+  content blocker. The module is now imported by
+  `proofs/agda/characteristic/All.agda` (line 33). The xfail gate's
+  own self-disclosed instructions (`"register it in
+  characteristic/All.agda and remove this xfail gate"`) fired on
+  the previous CI run; this PR completed those instructions.
+
 ### Added (2026-05-27)
 
 - *Lane 3 ordinal track — 11/13 Buchholz constructors closed under

EXPLAINME.adoc

@@ -34,12 +34,16 @@ 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).
+* *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).
 
 == Where to look first
 
 * `docs/echo-types/MAP.adoc` — the master map (every direction, status-tagged).
+* `docs/echo-types/echo-kernel-note.adoc` — kernel-vs-derived classification; status SoT for the `Echo*.agda` dependency cone.
 * `roadmap.adoc` + `roadmap-gates.adoc` — lane structure + identity-claim gates.
 * `tutorial/README.adoc` — the pedagogy track if you want to read worked examples first.
 * `docs/retractions.adoc` — read before citing any claim above as final.

README.md

@@ -32,8 +32,8 @@ flowchart TD
     F["<b>Foundation</b><br/>Echo f y := Σ (x : A) , (f x ≡ y)<br/>= homotopy fibre"]
     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)<br/>EchoTotalCompletion (A ≃ Σ B Echo f) · OFS-witness · Image · no-section-of-collapsing-map"]
-    T2["<b>Tier 2 · Classification grid</b><br/>LossTaxonomy (function-side) · ResidueTaxonomy (residue-side) · DecorationStructure · _≡m_"]
+    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_"]
     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

@@ -78,8 +78,13 @@ in the Pillar F4 template style.
 * *Image factorisation* — `Image f := Σ B (Echo f)`; the proof-
   relevant image IS the total Echo space. Three classifications
   (Surjective, Injective, projection-uniqueness under injectivity).
-  The (epi, mono) truncation form is the next earn-back gate.
   `proofs/agda/EchoImageFactorization.agda`.
+* *Image factorisation, (epi, mono) form (2026-05-28)* — the
+  (epi, mono) earn-back module, module-parameterised in a
+  truncation interface. Companion to `EchoImageFactorization`;
+  the previously-pending (epi, mono) form now lands without
+  committing the kernel to a specific truncation primitive.
+  `proofs/agda/EchoImageFactorizationProp.agda`.
 * *Generic no-section* — `no-section-of-collapsing-map`: for ANY
   collapsing map with two distinct elements landing on the same
   image, no section exists. Lifts the previous single-instance
@@ -93,10 +98,11 @@ 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. Four instances: trivial (⊤), identity
-  (`Echo f`), generic Σ-cert (`echoR-residue`), and the worked
-  `linear-affine-residue`. The other six decoration modules
-  documented as structurally compatible.
+  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.
   `proofs/agda/EchoResidueTaxonomy.agda`.
 * *Decoration structure* (observation-side) — `record
   DecorationStructure G` packaging the seven-field decoration
@@ -228,7 +234,12 @@ Staged Buchholz-style collapsing in `--safe --without-K`.
 
 * Proofs: `proofs/agda/Ordinal/` (`Buchholz/`, `Brouwer`, `CNF`,
   `Closure`, `Psi…`, `ExtendedOrder`, `RankPow`, `RankAdm`,
-  `RankLex`, `HeadOmega`, `HeadOmegaInversion`, `RankPowDomination`).
+  `RankLex`, `HeadOmega`, `HeadOmegaInversion`, `RankPowDomination`,
+  `RankPowSlice3` (2026-05-28 — `NonBzero` + strict-jump bridge +
+  head-Ω lower bound), `RankPowSlice3Headline` (2026-05-28 — Slice 3
+  headline `rank-mono-<ᵇ-+1-via-head-Ω` closed under a strict-head
+  premise; umbrella case-split bumps `bpsi=bpsi at equal markers`
+  to rank-adm / rank-lex)).
 * Docs: `docs/buchholz-plan.adoc`,
   `docs/echo-types/buchholz-extended-wf.md`,
   `docs/echo-types/buchholz-rank-obstruction.adoc` (per-constructor

readme.adoc

@@ -68,12 +68,13 @@ Tier 1 (the canonical identity layer itself):
 * `EchoTotalCompletion.agda` — `A ≃ Σ B (Echo f)`
 * `EchoOrthogonalFactorizationSystem.agda` — `ofs-witness`
 * `EchoImageFactorization.agda` — `Image f := Σ B (Echo f)`
+* `EchoImageFactorizationProp.agda` — (epi, mono) earn-back form, module-parameterised in a truncation interface (2026-05-28)
 * `EchoNoSectionGeneric.agda` — `no-section-of-collapsing-map`
 
 Tier 2 (the classification grid):
 
 * `EchoLossTaxonomy.agda` — function-side four-axis (EQUIV / INJ / SURJ / CONST)
-* `EchoResidueTaxonomy.agda` — `ResidueForm` record + instances
+* `EchoResidueTaxonomy.agda` — `ResidueForm` record + 6 instances (trivial, identity, generic Σ-cert, linear-affine, Search, Epistemic; the last two added 2026-05-28)
 * `EchoDecorationStructure.agda` — `DecorationStructure` record + abstract degrade-compose
 * `EchoObservationalEquivalence.agda` — mode-indexed `_≡m_` on `LEcho`