Add cross-repo bridge status ledger and canonical links

Author: hyperpolymath

README.md

@@ -92,6 +92,7 @@ Cross-repo status:
 - bridge formalisms live in this repo (`EchoCNOBridge`, `EchoJanusBridge`, tropical-collapse witness work in `EchoTropical`)
 - Agda-side adapter slot now exists in `maa-framework/absolute-zero` at `absolute-zero/proofs/agda/EchoBridgeScaffold.agda`
 - end-to-end conformance against upstream codebases is a separate track and is not yet fully machine-checked here
+- current bridge ledger: `docs/echo-types/cross-repo-bridge-status.md`
 - see `docs/echo-types/roadmap.md` for staged cross-repo verification gates
 
 ## What Echo Types Are For

docs/echo-types/cross-repo-bridge-status.md

@@ -0,0 +1,22 @@
+# Cross-Repo Bridge Status
+
+Last updated: 2026-04-23
+
+This file is the single status ledger for echo-type bridge work that touches
+other repositories.
+
+## Tracks
+
+| Track | echo-types side | Adjacent side | Current status | Main blocker |
+|---|---|---|---|---|
+| CNO bridge (Agda) | `proofs/agda/EchoCNOBridge.agda` | `maa-framework/absolute-zero/proofs/agda/EchoBridgeScaffold.agda` | Adapter slot landed on both sides | `absolute-zero/proofs/agda/CNO.agda` still has unfinished holes, so direct import-level instantiation is deferred |
+| CNO core theorem alignment | `EchoCNOBridge` theorem family | `absolute-zero/proofs/coq/common/CNO.v`, `absolute-zero/proofs/lean4/CNO.lean` | Paths identified; theorem-by-theorem alignment not yet done | Cross-prover statement normalization not written |
+| JanusKey bridge (reversibility/category/thermo context) | `proofs/agda/EchoJanusBridge.agda`, `EchoThermodynamics.agda` | `januskey/src/abi/*.idr`, `januskey/docs/wiki/theory/*.adoc` | Conceptual relation present; no formal checker bridge yet | JanusKey formal artifacts are mostly Idris + docs, not a synchronized Coq/Lean theorem surface |
+| Tropical alignment | `proofs/agda/EchoTropical.agda` | `tropical-resource-typing/*.thy`, `TropicalSessionTypes.lean` | Repo inventory complete; no theorem alignment yet | Adjacent repo not recently audited for this integration path |
+
+## Immediate next actions
+
+1. Close holes in `absolute-zero/proofs/agda/CNO.agda`.
+2. Add `EchoCNOBridgeConcrete.agda` in `absolute-zero/proofs/agda/` that instantiates `EchoBridgeScaffold.CNOModel` from concrete CNO semantics.
+3. Write a theorem correspondence table (name-by-name) for `EchoCNOBridge` vs Coq/Lean CNO statements.
+4. Decide JanusKey formal target layer (Idris ABI vs another prover) before writing an automated bridge.

docs/echo-types/roadmap.md

@@ -3,6 +3,9 @@
 **Status:** planning document. Partitions work by dependency on the
 two identified bottlenecks:
 
+For current cross-repo progress snapshots, see
+`cross-repo-bridge-status.md`.
+
 - **Bottleneck B1.** The `--without-K` shared-binder constructor
   block in the Buchholz `_<ᵇ_` order. `wf-<ᵇ` is landed for the
   currently admitted core, but full totality + full-constructor

readme.adoc

@@ -98,6 +98,7 @@ Cross-repo status:
 * Bridge formalisms live in this repo (`EchoCNOBridge`, `EchoJanusBridge`, tropical-collapse witness work in `EchoTropical`).
 * Agda-side adapter slot now exists in `maa-framework/absolute-zero` at `absolute-zero/proofs/agda/EchoBridgeScaffold.agda`.
 * End-to-end conformance against upstream codebases is a separate track and is not yet fully machine-checked here.
+* Current bridge ledger: `docs/echo-types/cross-repo-bridge-status.md`.
 * See `docs/echo-types/roadmap.md` for staged cross-repo verification gates.
 
 == What Echo Types Are For