Lane-4 bridge candidate: EchoEphapaxBridge.agda (content bridge to hyperpolymath/ephapax L3)

[hyperpolymath]

Proposal

Add `proofs/agda/EchoEphapaxBridge.agda` as a Lane-4 content bridge — mirroring `EchoCNOBridge.agda` (issue #21) and `EchoJanusBridge.agda` — to formalise the cross-repo correspondence between echo-types' `EchoLinear`/`LEcho` family and ephapax's L3 layer.

This is a scope question + dependency surface, not a ready-to-merge proposal. Filing to get owner direction on whether the bridge is wanted, and (if so) whether the ephapax side prerequisite work is in scope.

Why this is sensible to formalise

The conceptual coupling already exists in echo-types' own docs:

• `tutorial/region_exit_audit/RegionExitAudit.agda` — "models an ephapax-L3-style region as a Mode-indexed `LEcho`."
• `roadmap.adoc` — "region-exit audit, modelled on ephapax L3's region-based memory."
• `docs/echo-types/decisions/lane-4-bridges-ci-scope.adoc` — mentions submodule pinning `hyperpolymath/ephapax`.
• `tutorial/README.adoc` — "first because it ties to an active adjacent project (ephapax L3)."

Ephapax's L3 file (`formal/Echo.v`, landed via PR #166 + #167 on its design branch) is already an explicit Coq port of `EchoLinear.agda` + `EchoResidue.agda`. The bridge would formalise the round-trip: from echo-types' `LEcho Mode` upstream → ephapax `formal/Echo.v` → back to Agda as a content-bridge module that imports the ephapax content directly (the same way `EchoCNOBridge.agda` imports `IsCNO` directly from `absolute-zero/proofs/agda/CNO.agda`).

The dependency surface

The blocker is real and worth surfacing before any bridge work begins:

Ephapax has no Agda content today. Its formal layer is Coq (`formal/*.v`) + Idris2 (`idris2/src/Ephapax/`). `formal/Echo.v` is a Coq file. A content bridge in echo-types vocabulary (Agda `import` clause) requires either:

1. Port `formal/Echo.v` back to Agda in ephapax as `proofs/agda/L3/Echo.agda` (or similar). One-session move; the file is small and structurally close to the Agda upstream. Adds an Agda dependency to ephapax, which currently has none.
2. Bridge via interface declaration, not direct content: write `EchoEphapaxBridge.agda` with a `postulate`-free abstract interface that ephapax's Coq Echo file satisfies on inspection, but isn't imported by Agda. Weaker than the CNO content-bridge model but doesn't require ephapax-Agda.
3. Bridge against ephapax's Idris2: not a content bridge in the strict sense, but an extensional correspondence statement. Idris2 `Refs` for Coq's `Echo.v` invariants. Probably the worst option — neither end is Agda.

`docs/echo-types/decisions/lane-4-bridges-ci-scope.adoc` mentions "submodule pinning hyperpolymath/ephapax" which suggests intent for option 1 (proper content bridge), but I haven't audited the doc fully.

What the bridge would prove

Echoing `EchoCNOBridge`'s shape: for every ephapax `LEcho Linear` or `LEcho Affine` term as defined in ephapax `formal/Echo.v` (with the Linear → Affine `weaken` map), exhibit a constructive correspondence with echo-types' `LEcho` family + `degrade` map. The headline lemma in the echo-types direction: ephapax's `no_section_collapse_to_residue` (`Qed` under the global context, zero axioms — landed in ephapax PR #167) corresponds literally to echo-types' `no-section-collapse-to-residue` in `EchoResidue.agda:33–73`.

The constructive content is the same theorem stated twice — once in Agda, once in Coq, with a content bridge proving the correspondence is faithful.

What this would help

• Identity claim, criterion 3 ("canonical examples"): ephapax becomes a machine-checked canonical example of `LEcho`, not just a tutorial-referenced one.
• Pillar E (paper): provides a concrete cross-language reproducibility case for the fiber + thin-poset template.
• Cross-repo CI (Lane 4): if echo-types' content changes break ephapax's L3, the CI catches it.

Owner direction needed

Before any work happens:

1. Is the bridge wanted enough to justify ephapax adding Agda content (option 1)?
2. If not, is the abstract-interface bridge (option 2) acceptable?
3. Should this be filed against ephapax (as "add Agda L3 mirror") or stay echo-types-side (as "add bridge module" with the dependency noted)?

Filed without code. No PR is offered until direction is given.

References

• ephapax `formal/Echo.v` (PR proof(Slice 3+4 Route A): (c) trichotomy + consumer-side first-eq derivation #166, proof(Path-3 prototype): same-left joint-bplus rank-mono extension #167): proof(L3): formal/Echo.v scaffold — Mode + LEcho + decoration-commuting weakening ephapax#166 / proof(L3 Phase 2): EchoR residue + no-section irreversibility headline ephapax#167
• ephapax `formal/PRESERVATION-DESIGN.md` §6 (L3 layer, citing `EchoLinear.agda` as upstream).
• echo-types `EchoCNOBridge.agda` — content-bridge template.
• echo-types `docs/echo-types/decisions/lane-4-bridges-ci-scope.adoc` — pre-existing intent.

🤖 Generated with Claude Code

[hyperpolymath]

Now tracked under parent #128.