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

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