From 6847b6fd47e1c5e34e4f5e135130b79f2c8c7264 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 30 May 2026 14:13:01 +0100 Subject: [PATCH 1/2] docs+proofs: EchoEphapaxBridge NARROW stub (closes #126) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit NARROW per /tmp/ephapax-bridge-proposal.md §4 (bg-agent verdict): import-time documentation + two definitional refl-renames pinning the load-bearing Agda symbols under ephapax-L3- prefixed names. 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. Adds: * `proofs/agda/EchoEphapaxBridge.agda` (~45 lines including preamble): - `ephapax-L3-weaken = weaken` (from `EchoLinear`) - `ephapax-L3-no-section-collapse = no-section-collapse-to-residue` (from `EchoResidue`) Module docstring catalogues the five Coq headlines (`mode_le_prop`, `weaken_collapses_distinction`, `affine_canonical`, `degrade_mode_comp`, `no_section_collapse_to_residue`) as same-shape cross-repo counterparts. * `proofs/agda/All.agda`: wires `EchoEphapaxBridge` between `EchoJanusBridge` and `Dyadic` (Cross-repo bridges neighbourhood). * `proofs/agda/Smoke.agda`: pins `ephapax-L3-weaken` and `ephapax-L3-no-section-collapse` so a silent upstream rename in `EchoLinear` / `EchoResidue` trips CI fast. * `docs/echo-types/MAP.adoc` §Directions: new `=== Ephapax L3 — linear/affine modality bridge` subsection between JanusKey and Tropical/Dyadic. Scope explicit: L3 only — ephapax-affine and L1/L2/L4 are NOT mechanised to the same standard (cf. ephapax `formal/PRESERVATION-DESIGN.md`, MEMORY hook `feedback_ephapax_affine_proofs_not_done.md`). Local typecheck: * `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. Companion to #161 (closes #125 + #127 + #132). Closes #126; #128 umbrella ready to close once both PRs merge. Co-Authored-By: Claude Opus 4.7 (1M context) --- docs/echo-types/MAP.adoc | 27 ++++++++++++++++++ proofs/agda/All.agda | 1 + proofs/agda/EchoEphapaxBridge.agda | 45 ++++++++++++++++++++++++++++++ proofs/agda/Smoke.agda | 11 ++++++++ 4 files changed, 84 insertions(+) create mode 100644 proofs/agda/EchoEphapaxBridge.agda 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/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 From a700af5bec68a16b45a53321f5537109d5dc1b5d Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 30 May 2026 14:26:52 +0100 Subject: [PATCH 2/2] ci: classify EchoEphapaxBridge in echo-kernel-note (kernel-guard fix) Pre-existing CI invariant (`scripts/kernel-guard.sh` step B): every `Echo*.agda` module must be classified somewhere in `docs/echo-types/echo-kernel-note.adoc`. The initial #126 stub commit landed the module but missed the classification, failing the kernel- guard step before Agda's typecheck started. Adds `EchoEphapaxBridge` to the Tier-2 list adjacent to `EchoCNOBridge` (both are cross-repo bridges depending on Tier-2 `EchoLinear` / `EchoResidue`). No semantic change. Local: `sh scripts/kernel-guard.sh` PASS. Co-Authored-By: Claude Opus 4.7 (1M context) --- docs/echo-types/echo-kernel-note.adoc | 1 + 1 file changed, 1 insertion(+) 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`,