docs: Pillar E in-repo close-out + Gate 2 Rev 5 + Lane 4/5 scope/scaffold (#121)

## Summary

In-repo close-out work across all four currently-open lanes per
`roadmap.adoc`. Stacked on PR #118 (consolidation); merges into that
branch and will land on `main` together when #118 squashes.

- **Lane 1 (Pillar E in-repo).** Status NOTE in `paper.adoc` +
`types-abstract.adoc` declaring tags 1/2/3 cleared; tag 4 (ordinal
appendix) is gated on Bachmann–Howard per `roadmap.adoc` §Lane 3 — not a
missing deliverable for the in-repo half of Pillar E. Honest about the
offline boundary (venue choice, Zenodo DOI, library packaging,
outreach).
- **Lane 2 (Gate 2 re-audit).** `docs/characteristic.adoc` Revision 5:
re-checks 4/4 surviving against everything post-Rev-4 (EI-2 termination
via PATH B, `characteristic.NonTruncatable` Q2.1 PARTIALLY REDUCIBLE
caveat, deliberately-broken `characteristic.N5Falsifier`). Comfortable
threshold (≥3/4) met by margin of one. Candidate N5 remains unadopted on
the same logic as Rev 4. Closes the Lane 2 close-out criterion (3).
- **Lane 4 [PARKED] (bridges-CI scope).**
`docs/echo-types/decisions/lane-4-bridges-ci-scope.adoc` adopts option A
(separate `echo-bridges-ci` repo with submodules) over option B (in-tree
submodules). Three load-bearing reasons; three override triggers;
unpark-time playbook. Lane stays PARKED.
- **Lane 5 [PARKED] (tutorial track).** `tutorial/README.adoc` scaffolds
three walkthroughs at design-doc level: (1) certified region-exit audit
tied to ephapax L3 = killer-app candidate; (2) epistemic erasure with
the in-memory-bytes-vs-type-level disclosure as the opening sentence;
(3) provenance/debugging echo. No Agda lands. Lane stays PARKED.
- **`roadmap.adoc`**: Lane 2 close-out item (3) marked LANDED; Lane 4 +
Lane 5 sections gain pre-resolved-decision/scaffold pointers.

Build invariant held: `agda All.agda` + `agda Smoke.agda` both exit 0
under `--safe --without-K`, zero postulates / escape pragmas / funext
(no Agda touched in this commit).

## Test plan

- [x] `agda --library-file=/tmp/agda-libs -i proofs/agda
proofs/agda/All.agda` → exit 0
- [x] `agda --library-file=/tmp/agda-libs -i proofs/agda
proofs/agda/Smoke.agda` → exit 0
- [x] No new postulates / escape pragmas (docs-only commit)
- [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

docs/characteristic.adoc

@@ -11,11 +11,15 @@ Gate 2 of the identity claim. It audits the nominees against the gate's
 falsifier — "naturally echo-shaped, not reducible to generic sigma/fiber
 lemmas" — and reports the threshold outcome.
 
-This is *Revision 4*. It adds a fourth nominee (`EchoLinear.degradeMode-compose`),
-introduces a new construction in this lane (`characteristic.RoleGraded`)
-that closes the open recommendation from the handoff's Observation E,
-and proposes a candidate fifth nominee. See §<<revision,Revision notes>>
-for the diff.
+This is *Revision 5* (2026-05-26). It is the close-out re-audit
+required by `roadmap.adoc` §Lane 2: it re-checks that the
+Revision-4 nominee table still clears the *comfortable* threshold
+(≥ 3 of 4 surviving) under everything that has landed in this
+lane since then. Verdict: still 4/4 surviving; comfortable
+threshold met by margin of one. The Revision-5 substance is in
+§<<revision-5,Revision-5 re-audit (2026-05-26)>>; the per-nominee
+audits below are unchanged from Revision 4. See §<<revision,Revision
+notes>> for the full diff.
 
 toc::[]
 
@@ -518,7 +522,117 @@ withdrawn lemma can be left in place as a historical signpost.
 | 3 | Amendment to `roadmap-gates.adoc` adopted. Nominee list: `degrade-via-join`, `degrade-compose`, `applyChoreo-compose`. 3/3 surviving across two modules. Recommended further work: genuine integration theorem; fourth nominee for diversification.
 
 | 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.
+|===
+
+[[revision-5]]
+== Revision-5 re-audit (2026-05-26)
+
+This section is the close-out audit named in `roadmap.adoc` §Lane 2
+close-out criterion (3). It re-checks the Revision-4 nominee table
+against everything that has landed in the characteristic / Gate-2
+lane since Revision 4. Three categories of evidence were considered;
+none weakens the Revision-4 verdict.
+
+=== Bar being checked
+
+`roadmap.adoc` §Lane 2 distinguishes two thresholds (taken from
+`roadmap-gates.adoc` Gate 2): the *honest minimum* (≥ 2 of 4
+surviving) and the *comfortable* threshold (≥ 3 of 4 surviving).
+Revision 4 reported 4/4. Lane 2 close-out asks: under everything
+this lane has produced since, does that still hold by the
+comfortable bar?
+
+=== Evidence reviewed since Revision 4
+
+. *EI-2 terminated — negative verdict, PATH B* (`docs/EI2_REPORT.adoc`,
+  authoritative). Eight investigation phases, seven data points
+  (sibling 2D constructions `characteristic.RoleMode`,
+  `characteristic.ModeGraded`, 3D `characteristic.RoleModeGrade`
+  with three pairwise commutations + a triple, self-pairing
+  `characteristic.RoleRole`), plus the formal exhibit
+  `characteristic.ChoreoInjective` for the non-loss-only criterion
+  and the partial generic `characteristic.RecipeTheorem`. The
+  termination finding is that the integration recipe with the
+  existing five named axes does *not* carry substantive simultaneous
+  cross-axis content — every "non-trivial" cell carries one-axis-at-
+  a-time content. The five doc locations enumerated in EI2_REPORT
+  §"Documentation cascade" have all been updated accordingly.
+. *Q2.1 / `characteristic.NonTruncatable`.* The general statement of
+  `echo-not-prop` for `(f, y)` with two distinct preimages is
+  re-exported under the Q2.1 name; the received-`y` form is
+  *PARTIALLY REDUCIBLE* per the module's own Gate-2 falsifier audit
+  (proof factors through generic Σ; echo-specific content is in the
+  statement only). The constructed-`y` form, which builds `y` from
+  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.*
+
+=== Per-nominee re-check
+
+[cols="1,2,2,3", options="header"]
 |===
+| Nominee | Module | Status as of Rev 5 | Reason
+
+| N1 | `EchoGraded.degrade-via-join` | SURVIVES (unchanged from Rev 4) | The lemma is on the loss-grade lattice's join, not on any integration claim. EI-2 termination does not touch it. No falsifier attempted since Rev 4.
+| N2 | `EchoGraded.degrade-compose` | SURVIVES (unchanged from Rev 4) | As N1: single-decoration lemma; EI-2 termination is orthogonal. No falsifier attempted since Rev 4.
+| N3 | `EchoChoreo.applyChoreo-compose` | SURVIVES (unchanged from Rev 4) | Single-decoration role-reachability lemma; the `client-to-server` content this lemma factors through is the very content EI-2 traced as the one load-bearing non-trivial cell across 2D pairings — that is independent evidence the lemma is non-vacuous, not a weakening.
+| N4 | `EchoLinear.degradeMode-compose` | SURVIVES (unchanged from Rev 4) | Single-decoration mode lemma with the specific `weaken` content (`no-section-collapse-to-residue` attached); EI-2 termination is orthogonal.
+|===
+
+=== Verdict
+
+Survivors: N1, N2, N3, N4. Count: 4. Honest threshold (≥ 2): met.
+Comfortable threshold (≥ 3): met by margin of one. The Lane 2
+close-out criterion in `roadmap.adoc` is satisfied.
+
+=== What the re-audit explicitly does NOT do
+
+. *Does not nominate N5.* The candidate fifth nominee
+  (`characteristic.RoleGraded.choreo-grade-commute`) remains a
+  candidate. EI-2's termination shows the protocol-pass-but-narrow
+  reading from Rev 4 was correct: the only non-trivial cell of the
+  2D family's commutation is `(c⊑s, keep≤keep)`, reducing to
+  `client-to-server e` — the same Choreo content N3 already carries.
+  Nominating it would push the count to 5/5, but the marginal
+  evidence is the same `client-to-server` content already credited
+  to N3, so nominating it would be cosmetic. Left unadopted on the
+  same logic as Rev 4.
+. *Does not retroactively retract any Rev-4 verdict.* No nominee's
+  falsifier was attempted and *failed*; the absence of attempts is
+  carried forward as a Rev-4 honest qualification (§<<qualifications,
+  Honest qualifications>> item 3), not a Rev-5 finding.
+. *Does not promote `characteristic.NonTruncatable.Q2-1` to the
+  nominee table.* Its own broken-Gate-2 audit (PARTIALLY REDUCIBLE)
+  was applied honestly; the lemma remains useful as a Gate-3
+  signpost, not as a Gate-2 survivor.
+
+=== Pointer additions since Rev 4
+
+* `proofs/agda/characteristic/RoleMode.agda`,
+  `RoleModeGrade.agda`, `RoleRole.agda`, `ModeGraded.agda`,
+  `ChoreoInjective.agda`, `RecipeNonTriviality.agda`,
+  `RecipeSpec.agda`, `RecipeTheorem.agda`, `InteractionTest.agda` —
+  EI-2 investigation lane. Not Gate-2 nominees; supply the
+  EI-2-termination evidence the §"Evidence reviewed" item 1 cites.
+* `proofs/agda/characteristic/NonTruncatable.agda` — Q2.1, see
+  §"Evidence reviewed" item 2.
+* `proofs/agda/characteristic/N5Falsifier.agda` —
+  *KNOWN BROKEN, NOT IN CI CLOSURE*; see §"Evidence reviewed"
+  item 3.
+* `docs/EI2_REPORT.adoc` — authoritative EI-2 verdict.
+* `proofs/agda/characteristic/All.agda` — the lane-local CI seam.
 
 == Cross-lane observations
 

docs/echo-types/decisions/lane-4-bridges-ci-scope.adoc

@@ -0,0 +1,165 @@
+= Lane 4 scope decision: bridges-CI architecture
+:toc: macro
+:toclevels: 2
+:sectnums:
+:icons: font
+
+[.lead]
+Decision document for `roadmap.adoc` §"Lane 4 [PARKED] — Bridges-CI".
+This file resolves the scope question that the parked-lane line
+asked, while keeping the lane formally parked until its unblocking
+condition (Lane 1 close-out) is met. Author: Claude session,
+2026-05-26.
+
+toc::[]
+
+== The question this document answers
+
+`roadmap.adoc` §"Lane 4 [PARKED]" records:
+
+[quote]
+End-to-end verified bridges to Janus, Tropical, CNO, etc.
+currently sit as in-tree modules (`EchoJanusBridge.agda`,
+`EchoTropical.agda`, `EchoCNOBridge.agda`, `DyadicEchoBridge.agda`)
+without CI-verified round-trips against the target codebases. Two
+architectural options when unparking: …
+
+This document picks one of those two architectures and pins the
+choice so a future session unparking Lane 4 does not re-litigate it.
+It does *not* re-open Lane 4 — the unblocking condition (Lane 1
+closes) still gates activation.
+
+== Decision
+
+*Adopt option A: a separate `echo-bridges-ci` repository pulling
+echo-types and each target as submodules.*
+
+The roadmap line already states this is preferred unless broader
+research-plan priorities favour tighter integration. As of
+2026-05-26 there is no such preference on file; this document
+ratifies the preferred reading as the *decision* rather than the
+default.
+
+== Why option A
+
+Three load-bearing reasons, in priority order.
+
+. *`--safe --without-K` discipline stays inside echo-types.* Every
+  in-tree bridge module today (`EchoJanusBridge`, `EchoTropical`,
+  `EchoCNOBridge`, `DyadicEchoBridge`) typechecks under
+  `--safe --without-K` with zero postulates because the target
+  codebase's content is *encoded structurally* (e.g. `EchoJanusBridge`
+  mirrors januskey's eight-variant `OpKind` as a local Agda
+  inductive). Pulling the actual target codebases in-tree would
+  drag their build invariants into this repo's CI, several of which
+  (Rust / SPARK / Idris2 / TypeScript) cannot be `--safe --without-K`
+  by construction. Option B silently degrades the single invariant
+  this repo is currently strict about.
+. *Bridge instability does not propagate.* The targets evolve on
+  their own cadence; a verified-translation lemma that breaks
+  because the target's API moved should land as a *bridge-CI
+  failure*, not as a red echo-types build. The blast radius of
+  bridge churn must stay outside the load-bearing repo (Lane 1).
+. *Lane 1 is the load-bearing lane.* `roadmap.adoc` §Lanes lists
+  Lane 1 first by priority for a reason: the paper / external
+  recognition. Anything that risks Lane 1's CI cleanliness for
+  Lane 4's content is the wrong trade-off as long as Lane 1 is
+  load-bearing.
+
+== When option B (in-tree submodules) would override
+
+Three concrete triggers, all of which must hold simultaneously,
+would re-open this decision:
+
+. The user's stated priorities shift to favour tighter integration
+  with one specific target codebase to the extent that bridge churn
+  *should* fail the echo-types build.
+. The target codebase in question is itself `--safe --without-K`
+  compatible (in practice: Agda or Idris2-with-totality-checked
+  modules), so option B does not degrade the invariant.
+. Lane 1 has *fully closed* (not merely close-out-met) — i.e. the
+  paper is published or accepted, and external-recognition pressure
+  on CI cleanliness has lifted.
+
+Absent all three, option A stands.
+
+== What option A looks like at unpark time
+
+When Lane 1 closes and Lane 4 is unparked, the work expands to:
+
+. *New repository `hyperpolymath/echo-bridges-ci`* under the same
+  org. Same licence policy (MPL-2.0 per the recent estate sweep).
+. *Submodule layout* under `bridges/`:
++
+[source,text]
+----
+bridges/
+  echo-types/      → submodule pinning hyperpolymath/echo-types
+  januskey/        → submodule pinning hyperpolymath/januskey
+  cno/             → submodule pinning hyperpolymath/cnocode (or wherever absolute-zero lives)
+  ephapax/         → submodule pinning hyperpolymath/ephapax
+  ...
+----
+. *Per-bridge verified-translation lemmas* land in
+  `bridges/<target>/verify.agda` (or `.idr`/`.lean` as the target's
+  proof assistant requires). Each lemma states the round-trip
+  property between the echo-types in-tree mirror (e.g.
+  `EchoJanusBridge.OpKind`) and the live target type (e.g.
+  januskey's `src/abi/Types.idr` `OpKind`). The CI seam is *this
+  lemma typechecking*, not the targets themselves typechecking
+  against echo-types.
+. *CI matrix* per bridge: a build job that bumps the submodule
+  pin, runs the verify lemma, and reports green/red. Red is a
+  bridge-CI signal, not a target-repo signal — neither this repo
+  nor any target is gated on bridge-CI green.
+
+== What stays in echo-types after option A is built
+
+The current in-tree bridge modules
+(`EchoJanusBridge.agda`, `EchoTropical.agda`, `EchoCNOBridge.agda`,
+`DyadicEchoBridge.agda`) *stay where they are*. They are the local
+structural mirrors that the bridge-CI verified-translation lemmas
+target on the echo-types side. Deleting them would break the
+bridge-CI lemmas without strengthening this repo. The roadmap
+should reflect: "in-tree mirrors are the canonical Agda statement
+of the bridge interface; round-trip verification against the live
+target is in `echo-bridges-ci`."
+
+== Open question this decision deliberately leaves
+
+The Tropical bridge does not point at a single canonical target
+repo today (the tropical decoration is a mathematical pattern, not
+a codebase). When Lane 4 unparks, the Tropical bridge either (a)
+finds a concrete consumer to verify against, or (b) stays as the
+in-tree `EchoTropical.agda` plus `AntiEchoTropical.agda` /
+`AntiEchoTropicalGeneric.agda` and is *not* migrated into
+`echo-bridges-ci`. Option (b) is the honest default; option (a)
+requires a named consumer.
+
+== Status
+
+Decision: *option A adopted as of 2026-05-26*.
+
+Lane 4 status: still *PARKED*. This document does not unpark it.
+The unblocking condition (Lane 1 closes per `roadmap.adoc` Lane 1
+close-out criterion) is unchanged.
+
+When Lane 4 unparks, the first three actions are:
+
+. Create `hyperpolymath/echo-bridges-ci` per §"What option A looks
+  like at unpark time".
+. Migrate the JanusBridge round-trip from a structural mirror to a
+  verified-translation lemma against the live januskey
+  `src/abi/Types.idr` `OpKind`.
+. Migrate the CNO bridge analogously.
+
+That sequence is *not* started in this session; recording it here
+saves the next session from re-deriving the unpark plan.
+
+== References
+
+* `roadmap.adoc` §"Lane 4 [PARKED] — Bridges-CI"
+* `docs/bridges/cross-repo-bridge-status.md` — current per-bridge status
+* `proofs/agda/EchoJanusBridge.agda`, `EchoTropical.agda`,
+  `EchoCNOBridge.agda`, `DyadicEchoBridge.agda` — in-tree mirrors
+* `CLAUDE.md` §"Ecosystem context" — list of adjacent target repos

docs/echo-types/paper.adoc

@@ -19,6 +19,21 @@ abstract
 (`types-abstract.adoc`) is the short, already-submission-ready
 companion; this is the full CPP/ITP-style mechanised-metatheory
 paper it grows into.
+
+*Pillar E in-repo close-out (2026-05-26).* Of the four `[EXPAND]`
+tags originally on this paper: tag 1 (background / notation primer)
+cleared in PR #73; tag 2 (related work — Granule / QTT,
+Uustalu–Vene comonads, coeffects, lens/optic vs witness-transport
+leg) cleared in PR #120, with the single-page reviewer companion at
+`docs/echo-types/comparators.adoc` shipping the axis-by-axis
+summary; tag 3 (evaluation — proof-size / cost table, honest
+account of the common-upper-bound idiom) cleared earlier in PR #84
+(see §"Evaluation and discussion"). Tag 4 (ordinal consumer-evidence
+appendix) is the only one remaining open, and it is *gated* on the
+ordinal-track milestone per `roadmap.adoc` §Lane 3 — not a missing
+deliverable for the in-repo half of Pillar E. Everything else
+(venue choice, Zenodo DOI, library packaging, outreach) is
+author-driven and is flagged but not auto-run.
 ====
 
 toc::[]

docs/echo-types/types-abstract.adoc

@@ -185,3 +185,14 @@ Submission logistics (venue deadline, TYPES-template formatting,
 author metadata, Zenodo DOI, arXiv cross-post) remain offline and
 author-driven; they are downstream of, not a substitute for, the
 re-review.
+
+NOTE: *In-repo Pillar E status (2026-05-26).* The full `paper.adoc`
+has cleared all `[EXPAND]` tags except the ordinal consumer-evidence
+appendix (gated on Bachmann–Howard per `roadmap.adoc` §Lane 3). Any
+further re-review of this abstract should treat the full paper as
+the canonical reference for narrowed claims; this abstract is the
+2-page condensation of it. The single-page reviewer companion
+`docs/echo-types/comparators.adoc` carries the axis-by-axis
+comparison against Granule, QTT, choreographic types, and Linear
+Haskell. See `roadmap.adoc` §"Pillar status" for the lane-level
+view.

roadmap.adoc

@@ -169,9 +169,14 @@ gate cross-links) landed in-session. Tracks B + C remain.
   headline example (parser, provenance, abs-int) with the small
   Σ-misuse it blocks. Builds clean under `--safe --without-K`;
   pinned in `Smoke.agda` under own `using` block.
-. The Gate 2 nominee list is re-audited and crosses the *comfortable*
-  threshold (≥ 3 of 4 surviving), not merely the honest minimum.
-  *(Remaining open item for Lane 2 close-out.)*
+. *LANDED 2026-05-26.* The Gate 2 nominee list is re-audited (Rev 5,
+  `docs/characteristic.adoc` §"Revision-5 re-audit (2026-05-26)") and
+  still crosses the *comfortable* threshold: 4/4 surviving, margin of
+  one above the comfortable bar (≥ 3 of 4). The re-audit explicitly
+  re-checks the post-Rev-4 evidence (EI-2 termination,
+  `characteristic.NonTruncatable` Q2.1, the deliberately broken
+  `characteristic.N5Falsifier`) and finds none of it weakens any
+  surviving nominee.
 
 *Artefacts (landed today).* `core/skepticisms/is-this-just-sigma-types.md`
 (canonical answer doc, 5-section structure mirroring the demands);
@@ -218,6 +223,16 @@ subtree. Per-session ledger in CLAUDE.md §"Session arc 2026-05-20".
 
 *Unblocking condition.* Lane 1 closes.
 
+*Scope decision (pre-resolved 2026-05-26).*
+`docs/echo-types/decisions/lane-4-bridges-ci-scope.adoc` adopts
+**option A** (separate `echo-bridges-ci` repository pulling
+echo-types and each target as submodules) per the recommendation
+this section already carried. The decision document also names the
+three triggers that would override the choice (all three must hold
+simultaneously) and lays out what option A looks like at unpark
+time, so an unparking session does not re-derive the architecture.
+Lane 4 itself remains PARKED.
+
 *Scope question to resolve when unparking.* End-to-end verified
 bridges to Janus, Tropical, CNO, etc. currently sit as in-tree
 modules (`EchoJanusBridge.agda`, `EchoTropical.agda`, `EchoCNOBridge.agda`,
@@ -253,6 +268,14 @@ in-memory bytes are zeroed — conflating these is a category error a
 sceptic will catch); (3) provenance / debugging echo over a small
 state-reconstruction example.
 
+*Scaffold (pre-resolved 2026-05-26).* `tutorial/README.adoc` lands
+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.
+
 == Closed lanes
 
 (none yet — populated when a lane closes per its close-out criterion).