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

## Summary

**Closes #126** with the NARROW recommendation from the bg-agent
proposal at `/tmp/ephapax-bridge-proposal.md` §4:

- **Companion** to #161 (which closes #125 + #127 + #132).
- **Sets up** #128 umbrella close: once this and #161 merge, every
  child issue (#125 / #126 / #127 / #132) is discharged.

Ships a thin import-time documentation module that catalogues the
ephapax↔echo-types L3 correspondence without re-mechanising it. Two
definitional `refl`-renames pin the load-bearing Agda symbols under
`ephapax-L3-` prefixed names so `MAP.adoc`'s "Directions" navigation
has an ephapax row and a silent upstream rename trips `Smoke.agda`.

The cross-repo content correspondence is already discharged by
`coqc` on the ephapax side (`formal/Echo.v`, 584 lines, 24 `Qed`,
zero `Admitted` / zero `Axiom` — explicit Coq port of
`EchoLinear.agda` + `EchoResidue.agda` under a K-free / zero-axiom
discipline equivalent to `--safe --without-K`). **No Lane 4 CI
dependency.**

## Files

| File | Change |
|---|---|
| `proofs/agda/EchoEphapaxBridge.agda` | **NEW** ~45 lines. Module
docstring catalogues 5 Coq headlines (`mode_le_prop`,
`weaken_collapses_distinction`, `affine_canonical`, `degrade_mode_comp`,
`no_section_collapse_to_residue`); two definitional `refl`-renames
`ephapax-L3-weaken = weaken` + `ephapax-L3-no-section-collapse =
no-section-collapse-to-residue`. |
| `proofs/agda/All.agda` | One line: wires `EchoEphapaxBridge` between
`EchoJanusBridge` and `Dyadic`. |
| `proofs/agda/Smoke.agda` | Pins `ephapax-L3-weaken` +
`ephapax-L3-no-section-collapse` so silent upstream renames in
`EchoLinear` / `EchoResidue` trip CI fast. Comment block flags ephapax
cross-repo nature. |
| `docs/echo-types/MAP.adoc` | New `=== Ephapax L3 — linear/affine
modality bridge \`[REAL]\`` subsection in §Directions between JanusKey
and Tropical/Dyadic. Scope explicit: **L3 only** — ephapax-affine and
L1/L2/L4 are NOT mechanised to the same standard. |

## Why NARROW (not YES or NO)

Per the bg-agent verdict:

- **YES (full content bridge)** would require ephapax to add an Agda
  dependency it doesn't currently have (ephapax's stack is Coq +
  Idris2 + Rust). Definitional redundancy: by construction the
  bridge collapses to `Echo f y := Σ A (f x ≡ y), QED`.
- **NO (decline)** is right about content but wrong about
  navigability. `EchoCNOBridge.agda` + `EchoJanusBridge.agda` both
  exist for navigability reasons independent of content depth.
  Declining would mean `MAP.adoc` has no ephapax row, despite
  ephapax being more tightly mechanised than several already-bridged
  targets.
- **NARROW** captures the trade-off: ship a thin pointer without
  re-mechanising. Maintenance cost is near-zero (renames are `refl`;
  upstream renames break `Smoke.agda` and surface immediately). The
  stub does not foreclose a future full content bridge.

## Local verification

- `agda -i proofs/agda proofs/agda/EchoEphapaxBridge.agda` — clean.
- `agda -i proofs/agda proofs/agda/Smoke.agda` — clean, exit 0.
- `agda -i proofs/agda proofs/agda/All.agda` — clean, exit 0.
- `bash tools/check-guardrails.sh proofs/agda` — 160 modules pass
  (`--safe --without-K`, no escape pragmas, no postulates, with the
  two existing exploratory exemptions).

## Honest-scope discipline

The module docstring + MAP.adoc subsection both scope the
corroboration claim **to L3 only** per the MEMORY hook
`feedback_ephapax_affine_proofs_not_done.md` and the R-2026-05-18
retraction surface. Ephapax-affine has Rust checkers only; L1 has 5
`Axiom` + 11 `Admitted`; L4 has no mechanised theorems yet. L3 is
the single layer where the upstream-Agda correspondence is both
literal (file mirrors files) and fully discharged.

## Test plan

- [x] New file typechecks under `--safe --without-K` locally.
- [x] `Smoke.agda` typechecks with new pins, exit 0.
- [x] `All.agda` typechecks with new module wired in, exit 0.
- [x] Foundation guardrail passes (160 modules, no new exemptions).
- [ ] CI: Agda + cold-check + characteristic + examples lanes all
  green 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/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