docs: classify EchoAbstractionBarrier + reflect Lane 5 triplet + Lane 3 head-Ω slice in README/W2-README

Cleanup pass before PR #118 merge.

* docs/echo-types/echo-kernel-note.adoc — adds EchoAbstractionBarrier
  (Lane 1 / Lane 2 Track B artefact, landed 2026-05-26 via PR #119) to
  the Tier-2 derived-modules list with a note pointing at its load
  and import set.  Was previously missing; the kernel-guard.sh CI gate
  (`scripts/kernel-guard.sh` step B) was failing with "unclassified
  Echo* module(s): EchoAbstractionBarrier".  Now passes.

* README.md — adds two one-line status updates:
  * Lane 5 tutorial triplet LANDED 2026-05-27 under tutorial/
    (region-exit audit, epistemic erasure, provenance / debugging),
    with build command.
  * Buchholz rank-monotonicity matrix at 11/13 closed via the WfCNF-
    restricted `_<ᵇ⁻_` umbrella; the last open `<ᵇ-+1` joint-bplus
    case opens via Ordinal.Buchholz.HeadOmega's first slice landed
    2026-05-27.

* tutorial/epistemic_erasure/README.adoc — fixes the stale "W3 remains
  at scaffold/design-doc level" claim; W3 also landed 2026-05-27.

Local verification: kernel-guard.sh, tools/check-guardrails.sh, and
the full agda sequence (All / Smoke / characteristic/All / examples/
All / tutorial/All) all exit 0 under --safe --without-K, zero
postulates, no funext.  This is the canonical CI sequence per
.github/workflows/agda.yml.

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

Author: hyperpolymath

README.md

@@ -97,6 +97,7 @@ On `main`, the following are true:
 - distinct-witness and retained-constraint exemplars are present (`echo-true≢echo-false`, `stateA≢stateB`, `visible-constraint`)
 - degrade-law family lands across decoration layers (graded, linear/affine, choreographic, access, cost, search); see `docs/theorem-index.md` for the aggregate
 - Pillars A–D of the establishment plan are LANDED (with R-2026-05-18 narrowings; see `docs/retractions.adoc`); Pillar E (paper) is in progress
+- Lane 5 tutorial triplet LANDED 2026-05-27 under `tutorial/`: region-exit audit, epistemic erasure, and provenance / debugging — each with honest-bound + matched-negative disclosure discipline; build via `agda --library-file=/tmp/agda-libs -i . -i proofs/agda tutorial/All.agda`
 
 Per-lane status, close-out criteria, and the identity-claim verdict
 per tag are in `roadmap.adoc`.
@@ -137,6 +138,7 @@ CLAUDE.md):
 - the new budgeted layer on `ℕ × BT` isolates the missing global step: the recursive surface route is now well-founded once explicit budget is carried, and the remaining task is to discharge or eliminate that budget in the unbudgeted theorem
 - this still does not internalize the historically blocked shared-binder shapes as actual constructors of `_ <ᵇ _`; the full intended Buchholz order remains open at that step
 - remaining live mathematical work is therefore not the current-core WF route, but the mediated internalization of the shared-binder cases back into the real order package
+- as of 2026-05-27: the Buchholz rank-monotonicity matrix closes 11/13 constructor cases via the WfCNF-restricted `_<ᵇ⁻_` umbrella (9 via `RankPow` + `<ᵇ⁺-ψα` via `RankAdm` 2026-05-26 + `<ᵇ-ψΩ≤` via `RankLex` 2026-05-27); the last open case is `<ᵇ-+1` joint-bplus, with the `Ordinal.Buchholz.HeadOmega` first slice (leading-Ω-index head function + 4 definitional sanity lemmas) landed 2026-05-27 as the structural opening of option (A) per the obstruction doc
 
 ## External Bridge Targets (local workspace)
 

docs/echo-types/echo-kernel-note.adoc

@@ -81,12 +81,17 @@ kernel** — the boundary is real and lives outside this core.
   `EchoExampleAbsInt`, `EchoExampleParser`, `EchoExampleProvenance`,
   `EchoExampleSignAnalysis`, `EchoExampleTruncation`,
   `EchoSearchExample`, `EchoThermodynamicsArbitrary`,
-  `EchoThermoCollapseImpossible`
+  `EchoThermoCollapseImpossible`, `EchoAbstractionBarrier`
 | Multi-hop. `EchoThermodynamics` reaches the kernel via
   `EchoFiberCount` (no direct `Echo` import);
   `EchoThermodynamicsFinite` is its Bishop-finite transport layer.
   `EchoSearch` / `EchoCost` / `EchoAccess` are Axis 8 witness-search
-  and cost-model extensions. `EchoExample*` are derived domain
+  and cost-model extensions.  `EchoAbstractionBarrier` is the
+  Lane 1 / Lane 2 consumer-side free-theorem artefact (Track B —
+  `affine-consumer-cannot-distinguish` plus raw-Σ counter-program
+  `sigma-distinguishes`); imports `Echo` + `EchoCharacteristic` +
+  `EchoLinear`, landed 2026-05-26 via PR #119.  `EchoExample*` are
+  derived domain
   applications.
 
 | *Earn-back gate modules* +

tutorial/epistemic_erasure/README.adoc

@@ -138,5 +138,6 @@ Both exit 0 under `--safe --without-K` with zero postulates.
 == Status
 
 LANDED 2026-05-27 as the second Lane 5 walkthrough. Walkthrough 3
-(provenance / debugging) remains at scaffold/design-doc level per
-`tutorial/README.adoc`.
+(provenance / debugging) also LANDED 2026-05-27 — see
+`tutorial/provenance_debugging/README.adoc`. The originally-
+scaffolded Lane 5 triplet is complete in Agda.