docs: author docs/bridges/ECHO-EPHAPAX-BRIDGE.adoc (per-bridge doc, CNO-equivalent)

[hyperpolymath]

Follow-up to #128 / #126 (Ephapax bridge package)

The other cross-repo bridges have detailed per-bridge documentation:

Bridge	Per-bridge doc	Length
CNO	`docs/bridges/ECHO-CNO-BRIDGE.adoc`	461 lines
JanusKey	`docs/EchoJanusBridge.md`	(auxiliary, plus content in EchoBridges.md)
Tropical	—	(status doc only)
Dyadic	—	(status doc only)
Ephapax-L3	— (this issue)	(status doc + MAP entry + EchoBridges.md §5 only)

What's already shipped

• Module: `proofs/agda/EchoEphapaxBridge.agda` (PR docs+proofs: EchoEphapaxBridge.agda NARROW stub (closes #126) #162, MERGED 2026-05-30).
• MAP entry: `docs/echo-types/MAP.adoc` §"Ephapax L3 — linear/affine modality bridge" (PR docs+proofs: EchoEphapaxBridge.agda NARROW stub (closes #126) #162).
• Bridges-status row: `docs/bridges/cross-repo-bridge-status.md` Tracks table 6th row (PR docs: ephapax bridge adjacency cleanup (3-file follow-up to #161 + #162) #163, pending).
• EchoBridges.md §5: enumeration entry with cross-repo theorem table (PR docs: ephapax bridge adjacency cleanup (3-file follow-up to #161 + #162) #163, pending).
• roadmap.adoc: Lane 4 module list entry (PR docs: ephapax bridge adjacency cleanup (3-file follow-up to #161 + #162) #163, pending).

What this issue asks for

Author `docs/bridges/ECHO-EPHAPAX-BRIDGE.adoc` matching the structure of `ECHO-CNO-BRIDGE.adoc` (or a thinner subset if NARROW-stub status makes the full pattern oversized). Plausible sections:

1. Cross-repo correspondence map — exhaustive Agda↔Coq theorem table (vs. the 5-row summary that's already in EchoBridges.md §5 / bridges-status). Cover at least the 24 `Qed` results in `formal/Echo.v` and their Agda counterparts in `EchoLinear.agda` + `EchoResidue.agda`.
2. K-free / zero-axiom discipline correspondence — how ephapax's K-avoidance (no `dependent destruction`, raw dependent match + motive trick) maps to echo-types' `--safe --without-K` discipline.
3. The mode-join structure — `formal/Echo.v:548-584` is the mode-join cohort; `EchoLinear` has its `⊔m` family. Document the correspondence.
4. Honest scope (R-2026-05-18 + L3-only) — restated for the per-bridge doc audience, with explicit pointers to the layers (L1/L2/L4 + ephapax-affine) that are NOT corroborated by this bridge.
5. Failure modes — what would have to break for the NARROW stub to no longer hold (upstream symbol renames in either repo, `Smoke.agda` integration drift, etc.).
6. Open paths to full content bridge — what an Agda mirror of `formal/Echo.v` would look like and what proof-debt return / maintenance cost it would carry; ties back to the YES/NO/NARROW analysis from the original `/tmp/ephapax-bridge-proposal.md` §4 verdict.

Not blocking

The NARROW stub is operational without this doc. This issue tracks completing the per-bridge documentation pattern across all bridges for symmetry.

Out of scope

This is not a request to upgrade Ephapax to a content bridge. The NARROW decision was deliberate (per the bg-agent verdict in the umbrella #128 closure); upgrading is a separate, larger decision and would need ephapax to add an Agda dependency it currently does not have.

🤖 Generated with Claude Code