feat+docs: Lane 5 walkthrough 1 + Lane 3 ψα slice + N5 sharpened + Pillar E offline prep + packaging (#122)

## Summary

Four follow-on workstreams from the four design decisions on 2026-05-26.
Stacked onto PR #118's consolidation branch (lands with #118 on the
final squash to main).

**Lane 5 [UNPARKED] — Walkthrough 1 landed**
- `tutorial/region_exit_audit/RegionExitAudit.agda`: ephapax-L3-style
region exit. `LEcho linear` = LiveHandle, `LEcho affine` = AuditReceipt,
`exit = weaken`, `audit-no-recovery = no-section-weaken` aliased
per-region. Honest-bound disclosure (NOT a byte-zeroing claim) opens the
file; matched-negative block at bottom names the four properties NOT
proved.
- Per-walkthrough Smoke + All; tutorial-track aggregator;
`tutorial/README.adoc` unpark status updated.

**Lane 3 [ACTIVE PUSH] — ψ-admissibility rank refinement slice**
- `proofs/agda/Ordinal/Buchholz/RankAdm.agda`: admissibility-aware rank
with α-discriminating bpsi shape `ω-rank-pow ν ⊕ rank-pow α`. Closes 1
of 2 deferred ψ constructors via `rank-mono-<ᵇ⁺-ψα-from-pow`. The
`<ᵇ-ψΩ≤` ν=μ boundary case is *re-classified* from "admissibility" to
"encoding mismatch" (a real structural gap surfaced by the slice); two
design follow-ups documented inline.
- Score in `buchholz-rank-obstruction.adoc`: 9/13 → 10/13.

**Gate 2 N5 falsifier — sharpened & resolved**
- `characteristic/N5Falsifier.agda`: unsolved metas resolved by pinning
the implicit role+grade params at the four `applyRole`/`applyGrade` call
sites. The 2026-05-18 broken status was *inference*, not content (Agda
cannot recover the role from `RoleGEcho r keep = Echo (obs r) true`
because `obs` is not injective). Now in `characteristic/All.agda` CI
green closure.
- `docs/characteristic.adoc` Rev 5b: N5-not-adopted decision UNCHANGED
on the cosmetic-only-marginal-evidence logic.

**Pillar E offline prep — all three sub-tasks**
- `docs/echo-types/pillar-e-offline.adoc`: venue matrix (TYPES first
recommended), Zenodo DOI mint plan, library packaging update, three
outreach drafts (Granule/QTT, choreographic, Linear Haskell).
- `echo-types.agda-lib`: include path extended to repo root (for
tutorial tree).
- `CITATION.cff` + `.zenodo.json`: pre-staged with placeholder DOIs and
ORCID fields left blank (not invented) for author to add post-mint.

## Test plan

- [x] `agda --library=echo-types proofs/agda/All.agda` → exit 0
- [x] `agda --library=echo-types proofs/agda/Smoke.agda` → exit 0
- [x] `agda --library=echo-types proofs/agda/characteristic/All.agda` →
exit 0 (N5Falsifier now included)
- [x] `agda --library=echo-types tutorial/All.agda` → exit 0
- [x] All under `--safe --without-K`, zero postulates / escape pragmas /
funext
- [x] GPG-signed
- [ ] CI: governance + Hypatia + agda jobs green
- [ ] Auto-merge enabled (squash, delete branch)

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

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

Author: hyperpolymath

.zenodo.json

@@ -0,0 +1,30 @@
+{
+  "title": "echo-types: a definitionally-grounded, loss-graded reindexing modality (Agda)",
+  "upload_type": "software",
+  "description": "Constructive Agda formalisation of fibre-based \"structured loss\" types. Defines Echo f y := Σ (x : A) , (f x ≡ y), shows it is definitionally the homotopy fibre (echo↔fib), and develops a loss-graded reindexing modality on top with a pointwise (funext-relative) mediator property, a separating model, and a carrier-parametric abstraction over a fixed grade poset. Under --safe --without-K throughout with zero postulates and a falsifiable retraction discipline.",
+  "creators": [
+    {
+      "name": "Jewell, Jonathan"
+    }
+  ],
+  "keywords": [
+    "agda",
+    "graded modality",
+    "homotopy fibre",
+    "structured loss",
+    "reindexing modality",
+    "formal methods",
+    "mechanised metatheory",
+    "echo types"
+  ],
+  "access_right": "open",
+  "license": "MPL-2.0",
+  "related_identifiers": [
+    {
+      "relation": "isSupplementTo",
+      "identifier": "https://github.com/hyperpolymath/echo-types",
+      "resource_type": "software"
+    }
+  ],
+  "communities": []
+}

CITATION.cff

@@ -0,0 +1,43 @@
+cff-version: 1.2.0
+title: "echo-types: a definitionally-grounded, loss-graded reindexing modality (Agda)"
+message: "If you cite this software, please cite the Zenodo DOI."
+type: software
+authors:
+  - given-names: Jonathan
+    family-names: Jewell
+    email: jonathan.jewell@gmail.com
+    # PLACEHOLDER: insert ORCID once registered, e.g.
+    # orcid: "https://orcid.org/0000-0000-0000-0000"
+repository-code: "https://github.com/hyperpolymath/echo-types"
+url: "https://github.com/hyperpolymath/echo-types"
+abstract: >
+  Constructive Agda formalisation of fibre-based "structured loss"
+  types. Defines Echo f y := Σ (x : A) , (f x ≡ y), shows it is
+  definitionally the homotopy fibre (echo↔fib), and develops a
+  loss-graded reindexing modality on top with a pointwise
+  (funext-relative) mediator property, a separating model, and a
+  carrier-parametric abstraction over a fixed grade poset. Under
+  --safe --without-K throughout with zero postulates and a
+  falsifiable retraction discipline. See paper.adoc and
+  types-abstract.adoc for the mechanised metatheory write-up.
+keywords:
+  - agda
+  - graded modality
+  - homotopy fibre
+  - structured loss
+  - reindexing modality
+  - formal methods
+  - mechanised metatheory
+license: MPL-2.0
+# === PLACEHOLDER: paste concept DOI here after first Zenodo mint ===
+doi: 10.5281/zenodo.0000000
+# === END PLACEHOLDER ===
+preferred-citation:
+  type: software
+  title: "echo-types: a definitionally-grounded, loss-graded reindexing modality (Agda)"
+  authors:
+    - given-names: Jonathan
+      family-names: Jewell
+  url: "https://github.com/hyperpolymath/echo-types"
+  doi: 10.5281/zenodo.0000000
+  year: 2026

docs/characteristic.adoc

@@ -524,6 +524,8 @@ withdrawn lemma can be left in place as a historical signpost.
 | 4 | Added `EchoLinear.degradeMode-compose` as N4 (per the Revision-3 recommendation; user-explicit). Built `characteristic.RoleGraded` and `choreo-grade-commute` (closes handoff Observation E). 4/4 surviving across three modules. Proposed adding `choreo-grade-commute` as N5 (left to integrator's discretion).
 
 | 5 (2026-05-26) | Close-out re-audit per `roadmap.adoc` §Lane 2: re-checks the Revision-4 nominee table against everything that has landed since (EI-2 terminated negative; `characteristic.NonTruncatable` for Q2.1 received-`y` form is PARTIALLY REDUCIBLE; the broken `characteristic.N5Falsifier` is ledgered, not silently dropped). Verdict: 4/4 still surviving, *comfortable* threshold (≥3/4) met by margin of one. Candidate N5 (`choreo-grade-commute`) remains unadopted: the post-Rev-4 EI-2 termination shows its non-trivial content is the same single `(c⊑s, keep≤keep)` cell as before, so nominating it would not strengthen the count beyond cosmetic.
+
+| 5b (2026-05-27) | Within-Rev-5 follow-up: `characteristic.N5Falsifier` *no longer broken* — unsolved metas around `EchoChoreo.obs` were resolved by pinning the implicit role and grade parameters at the four `applyRole`/`applyGrade` call sites (the blocker was inference, not content). The module is now in `characteristic/All.agda`'s CI green closure. Audit consequences are *recorded in-line in §"Evidence reviewed" item 3 above*: the SURVIVES verdict for the falsifier exhibit is now mechanised, but the N5-not-adopted decision is unchanged on the same Rev-4/Rev-5 cosmetic-only-marginal-evidence logic.
 |===
 
 [[revision-5]]
@@ -568,16 +570,24 @@ comfortable bar?
   bare non-injectivity, carries echo-specific content but is not on
   the Revision-4 nominee table — it is closer to a Gate-3 example
   obligation than a Gate-2 nominee.
-. *`characteristic.N5Falsifier` — KNOWN BROKEN, DELIBERATELY EXCLUDED*
-  from `characteristic/All.agda` and from any CI green closure
-  (`UnsolvedConstraints` + `UnsolvedMetaVariables`). Status disclosed
-  in the module's own broken banner and at
-  `docs/echo-types/earn-back-plan.adoc` item C/N5; monitored by an
-  expected-failure CI gate. *Crucially: nothing in N5Falsifier is
-  cited as evidence in this audit, and its broken status does not
-  count against any nominee. The fact that an attempted falsifier
-  for N5 (= `choreo-grade-commute`) is not mechanised is exactly why
-  N5 itself is not adopted in this revision.*
+. *`characteristic.N5Falsifier` — RESOLVED 2026-05-27, NOW GREEN AND IN CI CLOSURE.*
+  Originally KNOWN BROKEN, deliberately excluded
+  (`UnsolvedConstraints` + `UnsolvedMetaVariables`). The Lane-2
+  N5-sharpening pass on 2026-05-27 closed the unsolved metas by
+  making the implicit `r1`/`r2`/`g` parameters of `applyRole` /
+  `applyGrade` explicit at the four call sites; the obstacle was
+  *inference*, not *content* (Agda cannot recover the role from
+  `RoleGEcho r keep = Echo (obs r) true` because `obs` is not
+  injective, but supplying the role explicitly resolves it). The
+  module is now imported in `characteristic/All.agda` and the
+  broken-banner has been updated with the resolution record.
+  *Crucially: the resolution does not change the Rev-4 conclusion
+  about candidate N5* — the only non-trivial cell is still the
+  `(c⊑s, keep≤keep)` Choreo content already credited to N3, so
+  adoption would still be cosmetic. The cleaned-up green falsifier
+  exhibit *does* tighten the audit story (the SURVIVES verdict is
+  now mechanised instead of being a not-mechanised attempt-of-record)
+  without changing the N5-not-adopted decision.
 
 === Per-nominee re-check
 

docs/echo-types/buchholz-rank-obstruction.adoc

@@ -303,22 +303,30 @@ constructors discharge by additive-principal closure.
 | `<ᵇ-ψ+`    | ✓ closed  | `rank-pow-via-left` plus the IH.
 | `<ᵇ-+Ω`    | ✓ closed  | `rank-pow-bplus-into-ω-rank-pow` (additive-principal at the target) plus the WfCNF tail bound `y ≤ᵇ x` (caller-provided).
 | `<ᵇ-+ψ`    | ✓ closed  | Same as `<ᵇ-+Ω` since `rank-pow (bpsi ν _) = ω-rank-pow ν`.
-| `<ᵇ-ψα`    | ⏳ admissibility | `rank-pow (bpsi ν α) = ω-rank-pow ν` doesn't discriminate on α.  Refining the rank to `ω-rank-pow ν ⊕ rank-pow α` works iff `α ∈ C_ν` (ψ-admissibility predicate); deferred to a follow-on slice.
-| `<ᵇ-ψΩ≤`   | ⏳ admissibility | Same blocker at `ν = μ`: provisional shape gives `ω-rank-pow μ <′ ω-rank-pow μ`, which is false.
+| `<ᵇ⁺-ψα`   | ✓ closed (Lane 3, 2026-05-26) | `rank-adm (bpsi ν α) = ω-rank-pow ν ⊕ rank-pow α`; `⊕-mono-<-right` closes the shared-Ω-index lex case from `rank-pow α <′ rank-pow β` (which the existing `_<ᵇ⁰_` umbrella discharges).  Primitive `rank-mono-<ᵇ⁺-ψα-from-pow` in `Ordinal.Buchholz.RankAdm`.
+| `<ᵇ-ψΩ≤`   | ⏳ encoding mismatch | `ν <Ω μ` (strict) case closes by `additive-principal-ω-rank-pow {μ}`.  `ν = μ` case STILL OPEN: `ω-rank-pow μ ⊕ rank-pow α <′ ω-rank-pow μ` is impossible under any rank shape with `ω-rank-pow ν ≤ rank-adm (bpsi ν α)`.  The classical Buchholz gap `[Ω_μ, Ω_{μ+1})` that admissible ψ_μ(α) lives in is not modelled by `ω-rank-pow ν ⊕ rank-pow α`.  Two design follow-ups (lex pair, multiplicative ordinal) documented in `RankAdm.agda` §"<ᵇ-ψΩ≤-still-open"; option A (lex pair) recommended.
 | `<ᵇ-+1`    | ⏳ joint-bplus | `rank-pow (bplus z₁ z₂)` is not additive principal in general (it's a sum of additive principals).  Discharging requires a coarser bound (e.g., dominate by `ω-rank-pow` of the leading subterm's Ω-index) or a structurally richer rank.
 | `<ᵇ-0-+`   | ✓ closed* | `rank-pow bzero = oz`, and `rank-pow (bplus x y) ≥′ oz` strictly when *either* `x` or `y` is non-`bzero` and the term is WfCNF.  The degenerate `bplus bzero bzero` is excluded by WfCNF (atomic-right ≤ left forces both `bzero` and then the sum reduces to a `bzero`-shaped equivalent that doesn't pattern-match as a `bplus` under CNF normalisation — covered as a side-condition).
 |===
 
-*Score: 9/13 constructors closed; 3 deferred under explicit blockers;
-1 closed conditionally with documented side condition.*
+*Score: 10/13 constructors closed (9 under the original `rank-pow`
+umbrella + 1 under the new `rank-adm` slice); 2 deferred under
+explicit blockers; 1 closed conditionally with documented side
+condition. The Lane-3 active-push slice on 2026-05-26 advanced the
+score by 1 (`<ᵇ⁺-ψα`) and re-classified `<ᵇ-ψΩ≤` from "admissibility"
+to "encoding mismatch" with two named follow-up routes.*
 
 === What remains open
 
-* *ψ-admissibility predicate* (`WellFormedAdmissible.agda`, ~80 lines).
-  Refines `WfCNF` with the constraint that ψ-arguments live in their
-  binder's Ω-closure `C_ν`.  Closes `<ᵇ-ψα` and `<ᵇ-ψΩ≤` once the
-  rank-pow on `bpsi ν α` is refined to `ω-rank-pow ν ⊕ rank-pow α`
-  under the admissibility carrier.
+* *ψ-admissibility predicate* (`WellFormedAdmissible.agda`, landed
+  earlier; `RankAdm.agda` landed 2026-05-26 in the Lane 3 active-push
+  slice). Refines `WfCNF` with the rank-bound on ψ-arguments.
+  *Status*: `<ᵇ⁺-ψα` *closed* via `rank-mono-<ᵇ⁺-ψα-from-pow` in
+  `RankAdm.agda`. `<ᵇ-ψΩ≤` ν=μ boundary case re-classified as
+  *encoding mismatch* — needs a richer rank target (two-component
+  lex or multiplicative ordinal), not just the admissibility
+  carrier. See `RankAdm.agda` §"<ᵇ-ψΩ≤-still-open" for the two
+  design options; option A (lex pair) recommended.
 * *`<ᵇ-+1` joint-bplus*.  Needs either a coarser dominator (e.g., a
   function `BT → OmegaIndex` returning the leading Ω-index, then
   rank into `ω-rank-pow ∘ leading-index`) or a richer rank shape.