docs: record echo-types typesystem-integration sweep (4 downstream consumers)

cross-repo-bridge-status.md gains four rows: nextgen-typing (EchoTyping —
affine subtyping = weaken; erasure = fiber), phronesis (PhronesisEcho —
verdict-provenance = Echo), nextgen-languages/kitchenspeak (EchoBridge
hand-verified → machine-checked), invariant-path (Rust application example).
First three are content bridges importing echo-types under --safe; the
fourth is citation-level. CHANGELOG updated. No proof source changed.

https://claude.ai/code/session_01DQACj3RFmAPZaBPgR9SAaS

Author: claude

CHANGELOG.md

@@ -8,6 +8,26 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
 
 ## [Unreleased]
 
+### Added (2026-06-12)
+
+- *Cross-repo typesystem-integration sweep recorded in
+  `docs/bridges/cross-repo-bridge-status.md`.* echo-types is now
+  integrated into the hyperpolymath type systems (all merged to the
+  consumers' `main`), with four new ledger rows:
+  - **nextgen-typing** — `EchoTyping.agda` imports `EchoLinear`/`Echo`:
+    AffineScript `linear ⊑ affine` subtyping IS `weaken` (irreversible,
+    distinction-forgetting, proof-irrelevant at affine); refinement
+    erasure IS a fiber. Content bridge, `agda --safe` 3/3.
+  - **phronesis** — `PhronesisEcho.agda`: an ethical verdict's
+    provenance IS `Echo verdict v`. Content bridge.
+  - **nextgen-languages/kitchenspeak** — `EchoBridge.agda` status
+    upgraded hand-verified → machine-checked against the real `Echo`.
+  - **invariant-path** — Rust application example
+    (`classify_candidate` non-injective; retained candidate + `losses`
+    IS the echo). Citation-level.
+  No echo-types proof source changed; this is a documentation/ledger
+  sweep recording downstream adoption.
+
 ### Added (2026-05-30)
 
 - *Lane 3 ordinal track — Slice 3+4 Route A 6-PR arc + doc sweep.*

docs/bridges/cross-repo-bridge-status.md

@@ -2,7 +2,7 @@
 <!-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
 # Cross-Repo Bridge Status
 
-Last updated: 2026-06-02.
+Last updated: 2026-06-12.
 
 This file is the single status ledger for echo-type bridge work that
 touches other repositories.
@@ -18,6 +18,10 @@ touches other repositories.
 | EchoTypes.jl executable mirror | Tier-1+Tier-2 spine + unconditional F5 OFS fragment (modules: `Echo`, `EchoResidue`, `EchoFiberCount`, `EchoThermodynamics`, plus 2026-05-27 v0.2.0 additions: `EchoTotalCompletion`, `EchoOrthogonalFactorizationSystem`, `EchoImageFactorization`, `EchoNoSectionGeneric`, `EchoLossTaxonomy`, `EchoEntropy`, `EchoObservationalEquivalence`) | [`hyperpolymath/EchoTypes.jl`](https://github.com/hyperpolymath/EchoTypes.jl) v0.2.0 (pinned to `e7dded6`); registered in `julia-professional-registry` | **Executable companion shipped.** Mirrors run the finite-domain shadow of the upstream theorems on concrete data and falsify-by-counterexample; the companion makes no proof claims, the Agda here remains the source of truth. R-2026-05-18 retraction surface NOT mirrored; F5 funext-qualified clauses (uniqueness up to iso, diagonal lifting) NOT mirrored — Julia has no funext, the claims would be vacuous. UIP- and truncation-strength upgrades likewise honestly not mirrored. | — (shipped; honest scope holds verbatim from upstream). Future advances on the Tier-1+Tier-2 spine are candidates for new shadows in subsequent EchoTypes.jl releases, but no in-repo CI dependency exists in either direction. |
 | Ephapax L3 bridge (Agda↔Coq) | `proofs/agda/EchoEphapaxBridge.agda` | `ephapax/formal/Echo.v` (Coq, 584 lines, 24 `Qed`, zero `Admitted` / zero `Axiom`) — explicit port of `EchoLinear.agda` + `EchoResidue.agda` under a K-free / zero-axiom discipline equivalent to `--safe --without-K` | **Navigability bridge done; content bridge NARROW** (2026-05-30). Two definitional `refl`-renames: `ephapax-L3-weaken = EchoLinear.weaken` and `ephapax-L3-no-section-collapse = EchoResidue.no-section-collapse-to-residue`. Coq headlines `mode_le_prop`, `weaken_collapses_distinction`, `affine_canonical`, `degrade_mode_comp`, `no_section_collapse_to_residue` (line 502-517) each match an Agda counterpart pinned in `Smoke.agda`. Scope: **L3 only** — ephapax-affine has Rust checkers only; L1 has 5 `Axiom` + 11 `Admitted`; L4 has no mechanised theorems yet (cf. ephapax `formal/PRESERVATION-DESIGN.md`, `docs/echo-types/paper.adoc` §"Threats to validity"). | Per-bridge docs `docs/bridges/ECHO-EPHAPAX-BRIDGE.adoc` (CNO-equivalent) not yet authored; tracked as follow-up issue. Full content bridge (round-trip CI between Agda + Coq) would require an Agda mirror of ephapax `formal/Echo.v` and is **not foreclosed** by the NARROW stub. |
 | Valence Shell / Ochránce accountable-shell bridge (exploratory, downstream) | Structured-loss vocabulary only — `EchoResidue` / `EchoResidueTaxonomy` / `EchoLossTaxonomy` / `EchoObservationalEquivalence` / `EchoNoSectionGeneric` cited at the reading-aid level. **No bridge module**; nothing added to `All.agda`, `Smoke.agda`, or `EchoCanonicalIdentitySuite.agda`. | Valence Shell (`hyperpolymath/valence-shell`) — shell state transitions, undo/redo, checkpoints, diff/replay. Ochránce (`hyperpolymath/ochrance`) — A2ML manifests, Merkle state commitments, repair/attestation surfaces. | **Exploratory — candidate downstream consumer. Core Affect: NO.** Echo Types' structured-loss semantics may *classify* shell state transitions by residue / loss form (recoverable / constrained / residue-bearing / observationally equivalent / genuinely lost); Ochránce may supply concrete receipt evidence. Downstream application evidence only — not a new foundation. No mechanised cross-repo theorem currently exists. Companion: `docs/bridge-status.md` §7 and `docs/echo-types/explorations/accountable-shell/README.adoc`. | No shared schema and no Agda↔Idris2 / Agda↔Rust import path; the relationship is citation-level only. Echo Types makes **no** claim about Valence Shell / Ochránce implementation correctness, and **no** claim about POSIX, Rust, the Lean→Rust correspondence, secure deletion, GDPR, cryptographic integrity, or attestation. Valence Shell's RMR/RMO vocabulary, if referenced, is downstream application vocabulary and is not adopted into the Echo Types core. |
+| **Typesystem integration (nextgen-typing)** | `EchoLinear` (`weaken`, `no-section-weaken`, `affine-canonical`), `Echo` | `nextgen-typing/verification/proofs/agda/EchoTyping.agda` (imports echo-types directly via `depend: echo-types`) | **Content bridge done (2026-06-12).** AffineScript `linear ⊑ affine` subtyping IS `EchoLinear.weaken` (irreversible — `no-section-weaken`; distinction-forgetting; proof-irrelevant at affine via `affine-canonical`); refinement erasure IS a fiber of `erase`. Headlines `TP-ECHO-1/2/3`. `agda --safe` 3/3 pass (Agda 2.6.3 + stdlib v2.3 + echo-types). | — (closed at content-bridge level; the hyperpolymath type-theory pipeline reuses echo-types' structured-loss notion directly rather than a parallel definition). |
+| **Verdict-provenance (phronesis)** | `Echo`, `echo-intro` | `phronesis/academic/formal-verification/agda/PhronesisEcho.agda` (imports echo-types directly) | **Content bridge done (2026-06-12).** An ethical verdict's provenance IS `Echo verdict v`: `eval` is non-injective, so the fiber retains *which* expressions justify a verdict the bare `Bool` forgets (`verdict-forgets-provenance`); `proj₁` is the recovering section. Machine-checked vs real echo-types. (Also fixed 4 pre-existing bugs making `Phronesis.agda` compile.) | — (closed; downstream consumer in the agentic-ethics language). |
+| **KitchenSpeak `@` witness (nextgen-languages)** | `Echo` | `nextgen-languages/kitchenspeak/proofs/agda/EchoBridge.agda` | **Status upgraded to MACHINE-CHECKED (2026-06-12).** Previously "hand-verified, not machine-checked"; now typechecks against the real `Echo`. The `@` sensor witness IS `Echo (fired sensor thr) true` (`witness⇒echo` / `echo⇒witness`). PoachedEgg stdlib-v2.3 drift (`toWitness {Q=}`→`{a?=}`) fixed so the suite type-checks. | — (the `--` comments in `kitchenspeak.agda-lib` need Agda ≥ 2.6.4; on the 2.6.3 CI toolchain use the explicit `-i` form, documented in the module). |
+| **Invariant Path application (invariant-path)** | Structured-loss vocabulary (the `Echo` fiber concept) — citation-level | `invariant-path` (Rust): `classify_candidate` + `docs/ECHO-TYPES.md` + `crates/invariant-path-core/{examples,tests}/echo_structured_loss.rs` | **Application example (2026-06-12).** `classify_candidate` is a non-injective classifier; the retained `ClaimCandidate` + `ClassificationOutcome.losses` IS the echo (fiber) over a `Classification`. Invariant Path is "a claim-path debugger, not a truth engine" precisely because it retains echoes. Runnable example + 2 CI-covered tests. | No Agda↔Rust import path; citation-level — the application *uses* the echo principle; no mechanised cross-repo theorem. |
 
 ## Immediate next actions
 
@@ -67,6 +71,17 @@ precisely to paper over this in the relational model.
 
 ## Revision history
 
+- 2026-06-12: **Typesystem-integration sweep.** Added four downstream
+  consumer rows recording that echo-types is now integrated into the
+  hyperpolymath type systems, all merged to the consumers' `main`:
+  nextgen-typing (`EchoTyping.agda` — affine subtyping = `weaken`;
+  refinement erasure = fiber), phronesis (`PhronesisEcho.agda` —
+  verdict-provenance = `Echo`), nextgen-languages/kitchenspeak
+  (`EchoBridge.agda` status upgraded hand-verified → machine-checked;
+  PoachedEgg stdlib drift fixed), and invariant-path (Rust application
+  example, citation-level). First three are content bridges that
+  `import` echo-types directly under `--safe`; the fourth is
+  citation-level (no Agda↔Rust path).
 - 2026-06-02: Added the Valence Shell / Ochránce accountable-shell
   bridge row as an exploratory downstream-consumer entry (Core Affect:
   NO; citation-level only, no bridge module, nothing wired into