docs: refresh CHANGELOG / MAP / EXPLAINME / roadmap for 2026-05-27 work

CHANGELOG.md gains 2026-05-27 Added + Changed entries covering the
Lane 3 ordinal track (RankAdm + RankLex + HeadOmega slices, 11/13
constructor closure), the Lane 5 tutorial track (Walkthroughs 1+2+3
landed), Pillar E packaging pre-staging (CITATION.cff, .zenodo.json,
echo-types.agda-lib, README sections, pillar-e-offline.adoc), Gate 2
audit Rev 5+5b, roadmap consolidation, N5Falsifier promotion, and
the per-constructor verdict score bump.

docs/echo-types/MAP.adoc: Buchholz entry gains the new module
list (RankPow / RankAdm / RankLex / HeadOmega) and an obstruction-doc
pointer; new top-level "Tutorial / pedagogy [REAL]" section lists
the three walkthroughs and their build command.

EXPLAINME.adoc: status snapshot gains "Ongoing tracks at a glance"
covering identity claim narrowings, the 11/13 Buchholz closure, the
tutorial track, and the Pillar E split (in-repo close-out vs
author-driven offline half); new "Where to look first" section
points readers at MAP / roadmap / tutorial / retractions.

roadmap.adoc Lane 3: bottleneck line bumped 10/13 → 11/13, naming
RankAdm + RankLex + HeadOmega; close-out criterion narrowed to the
head-Ω domination route (Slices 2/3/4); per-session ledger pointer
updated.  Lane 5: "Walkthroughs landed (2026-05-26/27)" subsection
records all three walkthroughs landed while the lane stays PARKED
at the lane-policy level pending user unpark decision.  Pillar E
status row updated with pre-staging detail + owner-action list.

Wiki Home.md refreshed in a parallel commit
(hyperpolymath/echo-types.wiki @ 3798dc9): adds Tutorial track
line, Buchholz 11/13 ledger pointer, Pillar E offline pointer.

CLAUDE.md was already refreshed by a parallel session with 2026-05-27
session arcs for Walkthrough 3 and the head-Ω first slice; this
slice leaves CLAUDE.md unchanged.

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

Author: hyperpolymath

CHANGELOG.md

@@ -6,12 +6,78 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
 
 ## [Unreleased]
 
-### Added
+### Added (2026-05-27)
 
+- *Lane 3 ordinal track — 11/13 Buchholz constructors closed under
+  WfCNF restriction.* Three slices land on top of the existing
+  `RankPow` 9-constructor umbrella:
+  - `Ordinal.Buchholz.RankAdm` (admissibility-aware rank
+    `rank-adm (bpsi ν α) = ω-rank-pow ν ⊕ rank-pow α`) closing
+    `<ᵇ⁺-ψα` via `rank-mono-<ᵇ⁺-ψα-from-pow`.
+  - `Ordinal.Buchholz.RankLex` (lex-pair rank `RankLex` over
+    `Ord × Ord` with shared-implicit second-strict constructor)
+    closing `<ᵇ-ψΩ≤` at both `ν<μ` (first-strict) and the
+    `ν=μ` boundary (second-strict via the admissibility bound).
+  - `Ordinal.Buchholz.HeadOmega` (leading-Ω-index head function
+    `head-Ω : BT → OmegaIndex` plus definitional sanity lemmas and
+    a two-level compositional convenience) — first slice of option
+    (A) for the remaining `<ᵇ-+1` joint-bplus discharge; no
+    rank-mono yet.
+- *Lane 5 tutorial track — the originally-scaffolded triplet is
+  complete.* `tutorial/` ships three worked walkthroughs with
+  honest-bound disclosure at top + matched-negative `NotProved-*`
+  `⊤`-aliases at bottom:
+  - `tutorial/region_exit_audit/` (Walkthrough 1, killer-app
+    candidate per `roadmap.adoc` §Lane 5) — ephapax-L3-style
+    region exit modelled type-level via
+    `EchoLinear.no-section-weaken`.
+  - `tutorial/epistemic_erasure/` (Walkthrough 2) — 4-seed →
+    2-key KDF with no-section-via-residue lifted from
+    `EchoResidue.no-section-collapse-to-residue`.
+  - `tutorial/provenance_debugging/` (Walkthrough 3) — 4-element
+    `State` with two orthogonal sign bits walked through 3 residue
+    layers; new pedagogical shape ships *both* a section (Layer 1
+    `recover-section-at-layer-1`) and its absence (Layer 2
+    `no-recovery-from-trivial`), exhibiting the boundary at which
+    the type-level recovery property flips.
+- *Establishment-track Pillar E — packaging pre-staged.*
+  `CITATION.cff` and `.zenodo.json` at the repo root (placeholder
+  DOI + ORCID-commented until author setup), `echo-types.agda-lib`
+  with dual `include: proofs/agda .` covering the tutorial track,
+  and README §Citation + §"Installing as a library" sections. CI
+  install-self + GitHub→Zenodo workflows intentionally deferred
+  until the author authorises the Zenodo integration (avoids
+  transient CI red).
+- *Establishment-track Pillar E — venue + outreach.*
+  `docs/echo-types/pillar-e-offline.adoc` lands the venue matrix
+  (TYPES → CPP → ITP → MSCS), Zenodo DOI mint plan, library
+  packaging plan, and three pre-written outreach cover letters
+  (Granule/QTT, choreographic types, Linear Haskell). Author-driven
+  for submission, sending, and Zenodo flip.
+- *Gate 2 audit — Revision 5 + 5b.* `docs/characteristic.adoc`
+  carries the close-out re-audit (4/4 surviving theorems, N5
+  resolved within Rev 5 follow-up).
 - Initial RSR template floor (CHANGELOG/SECURITY/CONTRIBUTING/QUICKSTART set + contractiles + 4 mandatory workflows + dotfiles + 0-AI-MANIFEST). Scaffolded 2026-04-30.
 
-### Changed
+### Changed (2026-05-27)
 
+- *Roadmap consolidation.* Five overlapping roadmap docs
+  (`docs/echo-types/roadmap.md`, `docs/PRIORITIZED_PROOF_ROADMAP.md`,
+  `docs/ProofRoadmap.md`, `docs/WORK_PLAN.md`, plus stragglers)
+  consolidated into the single canonical `roadmap.adoc` at repo
+  root.
+- *Per-constructor verdict on `_<ᵇ_`.*
+  `docs/echo-types/buchholz-rank-obstruction.adoc` score bumped
+  10/13 → 11/13; `<ᵇ-ψΩ≤` flipped from "encoding mismatch" to
+  "closed (Lane 3 follow-on, lex pair)". Only `<ᵇ-+1` joint-bplus
+  remains in the per-constructor matrix.
+- *N5Falsifier promoted into characteristic CI green closure.*
+  `proofs/agda/characteristic/N5Falsifier.agda` no longer carries
+  the "broken" banner; the unsolved metas were diagnosed as an
+  inference blocker (Agda cannot recover the role from
+  `RoleGEcho r keep = Echo (obs r) true` because `obs` is not
+  injective), resolved by making the `applyRole` / `applyGrade`
+  Role + Grade parameters explicit at the four call sites.
 - 6a2 metadata files migrated from `*.scm` at repo root to `.machine_readable/6a2/*.a2ml` per the canonical hyperpolymath rule (`.a2ml` is the canonical extension; `.scm` is reserved for Guix). 2026-04-30.
 
 ## [0.1.0+integration-pending]

EXPLAINME.adoc

@@ -29,3 +29,17 @@ Per `.machine_readable/6a2/STATE.a2ml`:
 * Bridges: linear, graded, tropical, choreographic, epistemic, CNO, Janus, Dyadic, Ordinal, Indexed, Relational, Categorical, Scope.
 * Investigation EI-2 (integration-recipe distinctness) terminated negatively via PATH B.
 * `.machine_readable/6a2/STATE.a2ml § ei-2` is the authoritative record; do not reopen.
+
+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`.
+* *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).
+* `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.

docs/echo-types/MAP.adoc

@@ -91,9 +91,12 @@ the standing B- freeze lifted because O-THERMO-∞ is now discharged
 Staged Buchholz-style collapsing in `--safe --without-K`.
 
 * Proofs: `proofs/agda/Ordinal/` (`Buchholz/`, `Brouwer`, `CNF`,
-  `Closure`, `Psi…`, `ExtendedOrder`).
+  `Closure`, `Psi…`, `ExtendedOrder`, `RankPow`, `RankAdm`,
+  `RankLex`, `HeadOmega`).
 * Docs: `docs/buchholz-plan.adoc`,
-  `docs/echo-types/buchholz-extended-wf.md`.
+  `docs/echo-types/buchholz-extended-wf.md`,
+  `docs/echo-types/buchholz-rank-obstruction.adoc` (per-constructor
+  verdict table — see ledger for live count).
 * Direct-constructor `_<ᵇ_` same-binder cases (Buchholz item B):
   status tracked solely in the earn-back ledger
   (`docs/echo-types/earn-back-plan.adoc`, row B) and
@@ -153,6 +156,33 @@ mutual-information formalisation is open.
   `docs/adjacency/information-flow.adoc`,
   `docs/gate-3-canonical.adoc`, `docs/gate-3-transport-handoff.adoc`.
 
+== Tutorial / pedagogy `[REAL]`
+
+Three worked walkthroughs landing 2026-05-26/27 under `tutorial/`,
+each following the honest-bound + matched-negative discipline
+(disclosure at top + `NotProved-*` ⊤-aliases at bottom). Build with
+`agda --library-file=/tmp/agda-libs -i . -i proofs/agda tutorial/All.agda`.
+
+* *Walkthrough 1 — certified region-exit audit*
+  (`tutorial/region_exit_audit/`). ephapax-L3-style region exit
+  modelled type-level via `EchoLinear.no-section-weaken`. Killer-app
+  candidate per `roadmap.adoc` §Lane 5 second unblocking condition.
+* *Walkthrough 2 — epistemic erasure*
+  (`tutorial/epistemic_erasure/`). 4-seed → 2-key KDF with
+  no-section-via-residue lifted from
+  `EchoResidue.no-section-collapse-to-residue`. Heads off the
+  "does echo-types prove key zeroing?" category-error question.
+* *Walkthrough 3 — provenance / debugging*
+  (`tutorial/provenance_debugging/`). 4-element `State` with two
+  orthogonal sign bits walked through 3 residue layers. Ships
+  *both* a section (Layer 1) and its absence (Layer 2),
+  exhibiting the boundary at which type-level recovery flips.
+
+Track-level docs: `tutorial/README.adoc`, plus per-walkthrough
+`README.adoc` files. Lane policy status: see `roadmap.adoc` §Lane 5
+(currently [PARKED] at lane-policy level pending user unpark
+decision; all three walkthroughs landed regardless).
+
 == Tooling
 
 === ArghDA — proof-ladder workspace manager `[REAL*]`

roadmap.adoc

@@ -198,24 +198,31 @@ repository. Treat as parallel-independent; Lane 1 progress is never
 gated on Lane 3 progress, and the README + roadmap surface the two as
 separate branches.
 
-*Bottleneck.* Unbudgeted `_<ᵇʳᶠ_` global well-foundedness; 10/13
-constructors closed via the budgeted route + `_<ᵇ⁰_` umbrella per the
-2026-05-20 evening session; 3 constructor cases (`<ᵇ-ψα`, `<ᵇ-ψΩ≤`,
-`<ᵇ-+1` joint-bplus) remain open under documented structural blockers
-(see `docs/echo-types/buchholz-rank-obstruction.adoc`).
+*Bottleneck.* Unbudgeted `_<ᵇʳᶠ_` global well-foundedness; 11/13
+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.
 
 *Close-out criterion.* Either:
 
-* the three open constructor cases close via ψ-admissibility rank
-  refinement + leading-Ω-index domination (planned closure work; ~3
-  follow-on slices), unblocking full `rank-pow-mono-<ᵇ⁻` umbrella and
-  thereby `wf-<ᵇʳᶠ`; OR
+* 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
 * 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.
 
-*Artefacts.* See `docs/buchholz-plan.adoc` and the `Ordinal/Buchholz/`
-subtree. Per-session ledger in CLAUDE.md §"Session arc 2026-05-20".
+*Artefacts.* See `docs/buchholz-plan.adoc`,
+`docs/echo-types/buchholz-rank-obstruction.adoc` (live per-constructor
+verdict), and the `Ordinal/Buchholz/` subtree. Per-session ledger in
+CLAUDE.md §"Session arc 2026-05-20" and §"Session arc 2026-05-27 late
+evening".
 
 *Status.* Continue on parallel branches. Lane 1 does not wait.
 
@@ -272,9 +279,25 @@ state-reconstruction example.
 the three walkthroughs at design-doc level with their target file
 layouts, honest-bound disclosures, the per-walkthrough Smoke pin
 discipline, and the killer-app-candidate close-out check on
-Walkthrough 1. No Agda lands at this stage; the scaffold exists so
-an unparking session lands Agda directly rather than re-deriving
-the pedagogy. Lane 5 itself remains PARKED.
+Walkthrough 1.
+
+*Walkthroughs landed (2026-05-26/27).* The originally-scaffolded
+Lane 5 triplet is now complete in Agda — Walkthrough 1
+(`tutorial/region_exit_audit/`) landed 2026-05-26 as the killer-app
+candidate; Walkthrough 2 (`tutorial/epistemic_erasure/`) landed
+2026-05-27 with the KDF / no-section-via-residue framing;
+Walkthrough 3 (`tutorial/provenance_debugging/`) landed 2026-05-27
+with the section/no-section contrast across three residue layers.
+Each carries an honest-bound disclosure at the top and a
+matched-negative `NotProved-*` ⊤-aliases block at the bottom. The
+tutorial tree builds under `--safe --without-K` with zero postulates
+via `tutorial/All.agda`.
+
+Lane 5 itself remains PARKED at the lane-policy level pending the
+user's unpark decision (per §"Unblocking condition" above —
+either Lane 1 closes or Walkthrough 1's killer-app status is
+formally accepted). The walkthroughs landing did not auto-unpark
+the lane.
 
 == Closed lanes
 
@@ -321,8 +344,8 @@ narrowings.
 | `EchoRelModel.GradedLossModel` + generic `GCLaws` — *carrier-parametricity over a fixed grade poset* (not model-independence; see R-2026-05-18). `conservativity.adoc` — evidence-for, not proof-of, conservativity.
 
 | E — External validation (paper + outreach)
-| IN PROGRESS
-| `docs/echo-types/paper.adoc` LIVING DRAFT with `[EXPAND]` tags; `types-abstract.adoc` submission-ready. Lane 1's close-out criterion governs.
+| IN PROGRESS (in-repo half close-out; offline half author-driven)
+| `docs/echo-types/paper.adoc` LIVING DRAFT with `[EXPAND]` tags; `types-abstract.adoc` submission-ready. `docs/echo-types/pillar-e-offline.adoc` carries the venue matrix (TYPES → CPP → ITP → MSCS), Zenodo DOI mint plan, library packaging plan, and three pre-written outreach drafts. Pre-staged: `CITATION.cff`, `.zenodo.json` (placeholder DOI + ORCID-commented), `echo-types.agda-lib`, README §Citation + §"Installing as a library". Owner-action items: ORCID + Zenodo authorisation + TYPES/CPP submissions + outreach send. Lane 1's close-out criterion still governs the in-repo half.
 |===
 
 == Historical milestone log (M1–M13)