docs+proofs: EchoEphapaxBridge.agda NARROW stub (closes #126)

docs/echo-types/MAP.adoc

@@ -289,6 +289,33 @@ loss".
 * Proofs: `proofs/agda/EchoJanusBridge.agda`.
 * Docs: `docs/EchoJanusBridge.md`, `docs/EchoBridges.md`.
 
+=== Ephapax L3 — linear/affine modality bridge `[REAL]`
+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`. The Coq
+headlines (`mode_le_prop`, `weaken_collapses_distinction`,
+`affine_canonical`, `degrade_mode_comp`,
+`no_section_collapse_to_residue`) each carry the same theorem as the
+Agda counterpart.
+
+Scope is intentionally NARROW: this is import-time documentation +
+two definitional `refl`-renames of the load-bearing Agda symbols
+under `ephapax-L3-`-prefixed names, so a silent upstream rename
+trips `Smoke.agda`. The cross-repo content correspondence is already
+discharged by `coqc` on the ephapax side; no Lane 4 CI dependency.
+
+* Proofs: `proofs/agda/EchoEphapaxBridge.agda` (`ephapax-L3-weaken` ↔
+  `EchoLinear.weaken` ↔ ephapax `formal/Echo.v` `weaken`;
+  `ephapax-L3-no-section-collapse` ↔
+  `EchoResidue.no-section-collapse-to-residue` ↔ ephapax
+  `formal/Echo.v:502-517` `no_section_collapse_to_residue`).
+* External corroboration scope: L3 only — ephapax-affine and L1/L2/L4
+  are NOT mechanised to the same standard (see ephapax
+  `formal/PRESERVATION-DESIGN.md` + `docs/echo-types/paper.adoc`
+  §"Threats to validity").
+
 === Tropical / Dyadic `[REAL*]`
 Bridge domains enumerated in `docs/EchoBridges.md` (JanusKey / CNO /
 Tropical / Dyadic). Dyadic is mechanised; Tropical is named/early.

docs/echo-types/echo-kernel-note.adoc

@@ -79,6 +79,7 @@ kernel** — the boundary is real and lives outside this core.
   `EchoEpistemicResidue`, `EchoExamples`, `EchoGraded`,
   `EchoLinear`, `EchoPullback`, `EchoRelModel`, `EchoScope`,
   `EchoStabilityTests`, `EchoThermodynamics`, `EchoCNOBridge`,
+  `EchoEphapaxBridge`,
   `EchoThermodynamicsFinite`, `EchoIntegration`, `EchoAccess`,
   `EchoCost`, `EchoCostInstance`, `EchoSearch`, `EchoSearchInstance`,
   `EchoExampleAbsInt`, `EchoExampleParser`, `EchoExampleProvenance`,

proofs/agda/All.agda

@@ -51,6 +51,7 @@ open import EchoCategorical
 open import EchoScope
 open import EchoOrdinal
 open import EchoJanusBridge
+open import EchoEphapaxBridge
 open import Dyadic
 open import DyadicEchoBridge
 open import EchoThermodynamics

proofs/agda/EchoEphapaxBridge.agda

@@ -0,0 +1,45 @@
+{-# OPTIONS --safe --without-K #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+-- Echo↔Ephapax L3 Bridge (NARROW — navigability + cross-repo cataloguing).
+--
+-- The ephapax programming-language project (hyperpolymath/ephapax)
+-- carries a four-layer typing redesign 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`.  The Coq
+-- headlines `mode_le_prop`, `weaken_collapses_distinction`,
+-- `affine_canonical`, `degrade_mode_comp`, and
+-- `no_section_collapse_to_residue` each carry the same theorem as the
+-- Agda counterpart pinned here.
+--
+-- Scope (NARROW, per `/tmp/ephapax-bridge-proposal.md` §4): this
+-- module is import-time documentation.  The cross-repo content
+-- correspondence is already discharged by `coqc` on the ephapax side
+-- (no Lane 4 CI dependency).  The two definitional `refl`-renames
+-- below pin the load-bearing Agda symbols under `ephapax-`-prefixed
+-- names so `MAP.adoc`'s "Directions" navigation has an ephapax row,
+-- and so a silent upstream rename trips `Smoke.agda`.  A future
+-- content bridge would require an Agda mirror of ephapax's
+-- `formal/Echo.v` and is not foreclosed by this stub.
+--
+-- References:
+--   * `docs/bridges/cross-repo-bridge-status.md` (when extended).
+--   * `docs/echo-types/MAP.adoc` §"Directions" / "Ephapax L3".
+--   * ephapax `formal/Echo.v:502-517` ↔
+--     `EchoResidue.no-section-collapse-to-residue`.
+--   * ephapax `formal/Echo.v` `weaken` ↔ `EchoLinear.weaken`.
+
+module EchoEphapaxBridge where
+
+open import EchoLinear  using (linear; affine; LEcho; weaken)
+open import EchoResidue using (no-section-collapse-to-residue)
+
+-- ephapax `formal/Echo.v` `weaken` — Coq port of this Agda symbol.
+ephapax-L3-weaken : LEcho linear → LEcho affine
+ephapax-L3-weaken = weaken
+
+-- ephapax `formal/Echo.v` `no_section_collapse_to_residue`
+-- (line 502-517, `Qed`, zero axioms) — Coq port of this Agda symbol.
+ephapax-L3-no-section-collapse = no-section-collapse-to-residue

proofs/agda/Smoke.agda

@@ -956,6 +956,17 @@ open import EchoJanusBridge using
   ; keyrevoke-echo
   )
 
+-- Cross-repo bridges (NARROW): ephapax `formal/Echo.v` is a Coq port
+-- of `EchoLinear.agda` + `EchoResidue.agda` under a K-free / zero-axiom
+-- discipline.  `ephapax-L3-weaken` and `ephapax-L3-no-section-collapse`
+-- are definitional `refl`-renames of the load-bearing Agda symbols,
+-- pinned so a silent upstream rename trips CI fast.  See
+-- `EchoEphapaxBridge.agda` preamble.
+open import EchoEphapaxBridge using
+  ( ephapax-L3-weaken
+  ; ephapax-L3-no-section-collapse
+  )
+
 open import Ordinal.Base using
   ( OT
   ; zero