docs: ephapax bridge adjacency cleanup (3-file follow-up to #161 + #162) (#163)

## Summary

Seam-analyst follow-up to the ephapax bridge package (#161 + #162).
Three doc surfaces enumerate the bridges and were missing Ephapax-L3:

| File | Change |
|---|---|
| `docs/bridges/EchoBridges.md` | New §5 "EchoEphapaxBridge
\`[NARROW]\`" — purpose, components, 5-row cross-repo theorem
correspondence table, scope discipline (L3 ONLY), main entry. Overview
line now includes "Ephapax-L3". |
| `docs/bridges/cross-repo-bridge-status.md` | New 6th Tracks row
"Ephapax L3 bridge (Agda↔Coq)" after the EchoTypes.jl row landed in
#161. References the two \`refl\`-renames, the upstream Coq headlines,
the L3-only honest scope, and the per-bridge-doc follow-up. |
| `roadmap.adoc` | §Lane 4 module-list appended with
\`EchoEphapaxBridge.agda\`; added a sentence noting it's NARROW (no Lane
4 CI dependency). |

## Why

Per the seam-analyst sweep (background agent verdict captured in the
umbrella #128 closure comment): the bridge package shipped the **core**
Ephapax surfacing (#161 Agda stub + #162 doc paragraphs) but didn't
update three documents that **enumerate** bridges across the repo. A
reader navigating via \`EchoBridges.md\` overview, the bridges-status
Tracks table, or the roadmap Lane 4 module list would not have found
Ephapax-L3 catalogued.

## Honest-scope discipline (preserved across all three surfaces)

The corroboration claim is scoped **to L3 only**:

- Ephapax-affine has Rust checkers only — NOT mirrored as proof-bearing.
- L1 has 5 \`Axiom\` + 11 \`Admitted\` in \`Semantics_L1.v\`.
- L2 has 1 \`Admitted\` in \`TypingL2.v\` (post-hybrid
\`weaken_modality\` is \`Qed\`).
- L4 has no mechanised theorems yet (5 \`Qed\`-style obligations only).
- L3 (\`formal/Echo.v\`, 584 lines, 24 \`Qed\`, zero \`Admitted\` / zero
\`Axiom\`) is the **single** layer where the upstream-Agda
correspondence is both literal and fully discharged.

Cf. MEMORY hooks \`feedback_ephapax_affine_proofs_not_done.md\` +
\`feedback_ephapax_no_patching_legacy_preservation.md\`.

## Pre-existing tech-debt NOT touched

\`EchoBridges.md\` §1 (EchoJanusBridge) still describes the OLD
4-variant \`JanusOp\` enum (Create/Delete/Modify/Move); the canonical
surface in \`EchoJanusBridge.agda\` is now 8-variant \`OpKind\`
(Copy/Move/Delete/Modify/Obliterate/KeyGen/KeyRotate/KeyRevoke). This
drift is already tracked in \`cross-repo-bridge-status.md\` §JanusKey
row + §"Immediate next actions" — out of scope here.

## Follow-up filed

Per-bridge documentation \`docs/bridges/ECHO-EPHAPAX-BRIDGE.adoc\`
(analogous to the existing 461-line \`ECHO-CNO-BRIDGE.adoc\`) is filed
as a separate issue, not blocking this PR.

## Test plan

- [x] No code changes — docs-only diff.
- [x] No \`Echo*.agda\` modules added — kernel-guard not affected.
- [x] Foundation guardrail not affected.
- [ ] CI: governance + Agda lanes pass on this branch.
- [ ] Auto-merge on green.

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

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

Author: hyperpolymath

docs/bridges/EchoBridges.md

@@ -4,7 +4,7 @@
 
 ## Overview
 
-This document provides comprehensive documentation for the echo types bridge modules, which extend the core echo type theory to various domains including JanusKey, CNO, Tropical, and Dyadic systems.
+This document provides comprehensive documentation for the echo types bridge modules, which extend the core echo type theory to various domains including JanusKey, CNO, Tropical, Dyadic, and Ephapax-L3 systems.
 
 ## Bridge Modules
 
@@ -116,6 +116,37 @@ DyadicEchoBridgeTheorem :
   Σ (Session Alice) (λ S → Σ (Session Bob) (λ T → EchoSafe S × EchoSafe T × EchoDual S T))
 ```
 
+### 5. EchoEphapaxBridge `[NARROW]`
+
+**Location**: `proofs/agda/EchoEphapaxBridge.agda`
+
+**Purpose**: Cross-repo navigability marker for the `hyperpolymath/ephapax` programming-language project, whose L3 layer (`formal/Echo.v`, 584 lines, 24 `Qed`, zero `Admitted` / zero `Axiom`) is an explicit Coq port of `EchoLinear.agda` + `EchoResidue.agda` under a K-free / zero-axiom discipline equivalent to `--safe --without-K`.
+
+**Scope** (intentionally NARROW, per `/tmp/ephapax-bridge-proposal.md` §4): import-time documentation + two definitional `refl`-renames pinning load-bearing Agda symbols under `ephapax-L3-`-prefixed names. The cross-repo content correspondence is already discharged by `coqc` on the ephapax side; **no Lane 4 CI dependency**.
+
+**Key Components**:
+
+- **`ephapax-L3-weaken`**: definitional alias for `EchoLinear.weaken` (Coq counterpart: ephapax `formal/Echo.v` `weaken`)
+- **`ephapax-L3-no-section-collapse`**: definitional alias for `EchoResidue.no-section-collapse-to-residue` (Coq counterpart: ephapax `formal/Echo.v:502-517` `no_section_collapse_to_residue`)
+
+**Cross-repo theorem table** (correspondence catalogued in the module docstring):
+
+| Agda (echo-types) | Coq (ephapax `formal/Echo.v`) |
+|---|---|
+| `EchoLinear` mode order (linear ≤ affine) | `mode_le_prop` |
+| `EchoLinear.weaken-collapses-distinction` | `weaken_collapses_distinction` |
+| Affine canonicality on `LEcho affine` | `affine_canonical`, `affine_all_equal` |
+| `EchoLinear.degradeMode-comp` | `degrade_mode_comp` |
+| `EchoResidue.no-section-collapse-to-residue` | `no_section_collapse_to_residue` |
+
+**Scope discipline (honest)**: corroboration claim is **L3 only**. Ephapax-affine has Rust checkers only (no Coq mechanisation); L1 has 5 `Axiom` + 11 `Admitted`; L4 has no mechanised theorems yet. See `docs/echo-types/paper.adoc` §"Threats to validity" for the full honest-scope statement.
+
+**Main entry**:
+```agda
+ephapax-L3-weaken : LEcho linear → LEcho affine
+ephapax-L3-weaken = weaken
+```
+
 ## Integration Patterns
 
 ### JanusKey Integration

docs/bridges/cross-repo-bridge-status.md

@@ -16,6 +16,7 @@ touches other repositories.
 | JanusKey bridge | `proofs/agda/EchoJanusBridge.agda` | `januskey/src/abi/Types.idr` (`OpKind`, `IsFileOp`, `IsKeyOp`); `januskey/PROOF-NEEDS.md` | Name-bridge only — Agda side has a *local* 4-variant `JanusOp = Create \| Delete \| Modify \| Move`; canonical Idris2 ABI defines 8-variant `OpKind = Copy \| Move \| Delete \| Modify \| Obliterate \| KeyGen \| KeyRotate \| KeyRevoke` plus `IsFileOp`/`IsKeyOp` predicates. Already drifted (Create vs Copy; missing Obliterate + 3 key ops). | Decision recorded: structural-mirror the Agda enum to januskey's Idris2 `OpKind`; content-bridge deferred until januskey's `PROOF-NEEDS.md` lands content-bearing semantics. Agda↔Idris2 has no FFI, so any content-bridge must run via shared schema or trusted extraction. |
 | Tropical alignment | `proofs/agda/EchoTropical.agda` | `tropical-resource-typing/Tropical.thy`, `tropical-resource-typing/TropicalSessionTypes.lean` (and 8 other `.thy` files) | Adjacent repo audit complete (2026-05-20). Repo present at `repos-monorepo/verification-ecosystem/tropical-resource-typing`; remote `hyperpolymath/tropical-resource-typing` active (last push 2026-05-18, language=Isabelle). First alignable theorem pair identified: Agda `⊕-idem` ↔ Isabelle `trop_add_idem` ↔ Lean `add_comm_trop`+`add_assoc_trop`. | Agda cannot import `.thy` or `.lean` directly; alignment is citation-level (statement correspondence with build-side independent proof per language), not import-level. Long-game target: `Tropical_Ordinal_Bridge.thy` ↔ echo-types ordinal track. |
 | EchoTypes.jl executable mirror | Tier-1+Tier-2 spine + unconditional F5 OFS fragment (modules: `Echo`, `EchoResidue`, `EchoFiberCount`, `EchoThermodynamics`, plus 2026-05-27 v0.2.0 additions: `EchoTotalCompletion`, `EchoOrthogonalFactorizationSystem`, `EchoImageFactorization`, `EchoNoSectionGeneric`, `EchoLossTaxonomy`, `EchoEntropy`, `EchoObservationalEquivalence`) | [`hyperpolymath/EchoTypes.jl`](https://github.com/hyperpolymath/EchoTypes.jl) v0.2.0 (pinned to `e7dded6`); registered in `julia-professional-registry` | **Executable companion shipped.** Mirrors run the finite-domain shadow of the upstream theorems on concrete data and falsify-by-counterexample; the companion makes no proof claims, the Agda here remains the source of truth. R-2026-05-18 retraction surface NOT mirrored; F5 funext-qualified clauses (uniqueness up to iso, diagonal lifting) NOT mirrored — Julia has no funext, the claims would be vacuous. UIP- and truncation-strength upgrades likewise honestly not mirrored. | — (shipped; honest scope holds verbatim from upstream). Future advances on the Tier-1+Tier-2 spine are candidates for new shadows in subsequent EchoTypes.jl releases, but no in-repo CI dependency exists in either direction. |
+| Ephapax L3 bridge (Agda↔Coq) | `proofs/agda/EchoEphapaxBridge.agda` | `ephapax/formal/Echo.v` (Coq, 584 lines, 24 `Qed`, zero `Admitted` / zero `Axiom`) — explicit port of `EchoLinear.agda` + `EchoResidue.agda` under a K-free / zero-axiom discipline equivalent to `--safe --without-K` | **Navigability bridge done; content bridge NARROW** (2026-05-30). Two definitional `refl`-renames: `ephapax-L3-weaken = EchoLinear.weaken` and `ephapax-L3-no-section-collapse = EchoResidue.no-section-collapse-to-residue`. Coq headlines `mode_le_prop`, `weaken_collapses_distinction`, `affine_canonical`, `degrade_mode_comp`, `no_section_collapse_to_residue` (line 502-517) each match an Agda counterpart pinned in `Smoke.agda`. Scope: **L3 only** — ephapax-affine has Rust checkers only; L1 has 5 `Axiom` + 11 `Admitted`; L4 has no mechanised theorems yet (cf. ephapax `formal/PRESERVATION-DESIGN.md`, `docs/echo-types/paper.adoc` §"Threats to validity"). | Per-bridge docs `docs/bridges/ECHO-EPHAPAX-BRIDGE.adoc` (CNO-equivalent) not yet authored; tracked as follow-up issue. Full content bridge (round-trip CI between Agda + Coq) would require an Agda mirror of ephapax `formal/Echo.v` and is **not foreclosed** by the NARROW stub. |
 
 ## Immediate next actions
 

roadmap.adoc

@@ -375,10 +375,15 @@ 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`,
-`DyadicEchoBridge.agda`) without CI-verified round-trips against the
-target codebases. Two architectural options when unparking:
+bridges to Janus, Tropical, CNO, Ephapax-L3, etc. currently sit as
+in-tree modules (`EchoJanusBridge.agda`, `EchoTropical.agda`,
+`EchoCNOBridge.agda`, `DyadicEchoBridge.agda`,
+`EchoEphapaxBridge.agda`) without CI-verified round-trips against
+the target codebases. `EchoEphapaxBridge` is intentionally NARROW
+(definitional `refl`-renames only, no content claim — the cross-repo
+content correspondence is discharged by `coqc` on the ephapax side;
+see `docs/echo-types/MAP.adoc` §"Ephapax L3 — linear/affine modality
+bridge"). Two architectural options when unparking:
 
 * A separate `echo-bridges-ci` repository pulling echo-types and each
   target as submodules; runs the verified-translation lemmas in its