diff --git a/docs/echo-types/MAP.adoc b/docs/echo-types/MAP.adoc index 51a817c..8a4c1c6 100644 --- a/docs/echo-types/MAP.adoc +++ b/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. diff --git a/docs/echo-types/echo-kernel-note.adoc b/docs/echo-types/echo-kernel-note.adoc index 857e345..60ea2dc 100644 --- a/docs/echo-types/echo-kernel-note.adoc +++ b/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`, diff --git a/proofs/agda/All.agda b/proofs/agda/All.agda index c04e071..d76de3e 100644 --- a/proofs/agda/All.agda +++ b/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 diff --git a/proofs/agda/EchoEphapaxBridge.agda b/proofs/agda/EchoEphapaxBridge.agda new file mode 100644 index 0000000..e61250d --- /dev/null +++ b/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 + +-- 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 diff --git a/proofs/agda/Smoke.agda b/proofs/agda/Smoke.agda index 482f1d4..725c09b 100644 --- a/proofs/agda/Smoke.agda +++ b/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