From 4f32f8a361850dcf9f8c38cc4e40ebbe96ac4d0b Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Tue, 2 Jun 2026 13:46:51 +0000
Subject: [PATCH 1/4] =?UTF-8?q?feat(echo):=20commence=20AffineScript=20ali?=
 =?UTF-8?q?gnment=20=E2=80=94=20Echo=20Types,=20proofs-first?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Begins moving JtV to AffineScript's maturity/governance position, starting
with proofs, and accommodates the echo-types loss taxonomy in the checker.

Proofs (first):
- jtv_proofs/JtvEcho.lean: formalise JtV's Echo system (spec v2 §8-9) as a
  bounded join-semilattice (Safe ⊑ Neutral ⊑ Breaking) with the reverse-block
  admissibility contract (blockEcho_admissible) and the fibre correspondence
  with the echo-types Agda library (Echo f y := Σ x, f x = y). Wired into
  lakefile.lean / proof-regression CI. sorry-free.

Type checker (accommodate echo-types):
- crates/jtv-core/src/echo.rs: executable image of JtvEcho.lean — Echo lattice,
  join, admissibility, statement classifier (validated against AST stubs).
- typechecker.rs: reverse blocks rejected when aggregate echo is Breaking
  (JtvError::EchoViolation) — realises blockEcho_admissible. + tests.

Governance (adopt the AffineScript matrix discipline):
- ALIGNMENT-AFFINESCRIPT.adoc: gap analysis + phased roadmap (proofs first).
- verification/PROOF-CAPABILITY-MATRIX.adoc: authoritative proof-status matrix.
- academic/TODO_GAPS.md: doc-truthing — proofs are sorry-free (PROOF-5 stale).
- spec: anchor §8 Echo System to echo-types / JtvEcho.lean / echo.rs.

Findings recorded for later phases: jtv-core does not currently compile
(ast.rs ControlStmt lacks ReversibleBlock/ReverseToken/AbandonToken used by
interpreter/typechecker/cli; unvendored patacl-core path dep) — contradicting
STATUS.md "100% complete".

https://claude.ai/code/session_01EJLZKDtcF1RGdKx6TcUTQG
---
 ALIGNMENT-AFFINESCRIPT.adoc               | 172 ++++++++++++++++
 academic/TODO_GAPS.md                     |  28 +--
 crates/jtv-core/src/echo.rs               | 201 +++++++++++++++++++
 crates/jtv-core/src/error.rs              |   3 +
 crates/jtv-core/src/lib.rs                |   1 +
 crates/jtv-core/src/typechecker.rs        |  52 +++++
 jtv_proofs/JtvEcho.lean                   | 226 ++++++++++++++++++++++
 jtv_proofs/lakefile.lean                  |   7 +-
 spec/jtv_v2_type_system_corrected.adoc    |  12 ++
 verification/PROOF-CAPABILITY-MATRIX.adoc | 102 ++++++++++
 10 files changed, 790 insertions(+), 14 deletions(-)
 create mode 100644 ALIGNMENT-AFFINESCRIPT.adoc
 create mode 100644 crates/jtv-core/src/echo.rs
 create mode 100644 jtv_proofs/JtvEcho.lean
 create mode 100644 verification/PROOF-CAPABILITY-MATRIX.adoc

diff --git a/ALIGNMENT-AFFINESCRIPT.adoc b/ALIGNMENT-AFFINESCRIPT.adoc
new file mode 100644
index 0000000..6146f90
--- /dev/null
+++ b/ALIGNMENT-AFFINESCRIPT.adoc
@@ -0,0 +1,172 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+= Julia the Viper → AffineScript Alignment Plan
+:toc:
+:toclevels: 3
+:revdate: 2026-06-02
+
+Bring *Julia the Viper* (JtV) from its current position to the same level of
+*maturity and governance discipline* that `hyperpolymath/affinescript` has
+reached — *starting with proofs*. This document is the master plan; it is
+deliberately conservative and honest, in the spirit of `ROADMAP.adoc`.
+
+== 1. What "AffineScript's position" means
+
+AffineScript is an alpha-stage but disciplined language project. Its distinctive
+strength is not (only) the compiler — it is the *governance model* that keeps
+claims honest:
+
+[cols="1,3"]
+|===
+| Asset | Description
+
+| Compiler pipeline
+| `face syntax → core AST → type / effect / ownership checks → backend`
+  (OCaml; sedlex + Menhir; WASM / typed-wasm backends).
+
+| `docs/CAPABILITY-MATRIX.adoc`
+| The *single authoritative source* of feature status, using a precise
+  six-term vocabulary: `enforced`, `works`, `partial`, `declared-but-unwired`,
+  `parse-only`, `absent`.
+
+| Doc-truthing
+| `tools/check-doc-truthing.sh` mechanically blocks over-claims in docs against
+  the compiler-as-oracle test gate.
+
+| `docs/TECH-DEBT.adoc`
+| A coordination ledger with domain prefixes (DOC / CORE / STDLIB / INT / SAT).
+
+| Honest posture
+| Self-describes as alpha; its one known base-language soundness gap is tracked
+  as an issue (CORE-01 / #177), not hidden.
+
+| Verification locus
+| Verification lives at the *typed-wasm target layer*. AffineScript does **not**
+  use a proof assistant.
+|===
+
+== 2. Where JtV is today (honest snapshot, 2026-06-02)
+
+[cols="1,3"]
+|===
+| Area | Reality
+
+| Mechanized proofs
+| *Ahead of AffineScript.* `jtv_proofs/` has 7 Lean 4 libraries (~2,300 LOC)
+  with *zero* `sorry` / `admit` / `axiom`, plus an Idris2 ABI (`src/abi/`) and a
+  `proof-regression.yml` CI gate. This is JtV's strongest asset.
+
+| Paper proofs
+| `academic/proofs/` — 7 documents (type theory, security, algebra, quantum,
+  etc.).
+
+| Rust core
+| `crates/{jtv-core,jtv-cli,jtv-lsp,jtv-debug}`. *Does not currently compile*
+  (see TECH-DEBT below): `ast.rs::ControlStmt` lacks the `ReversibleBlock` /
+  `ReverseToken` / `AbandonToken` variants that `interpreter.rs`,
+  `typechecker.rs`, and `jtv-cli` already match on; and the workspace has an
+  unvendored sibling path-dependency `patacl-core` (`../patacl`).
+
+| Conformance
+| `conformance/{valid,invalid,coproc}` exists; not yet a compiler-as-oracle
+  gate.
+
+| Spec
+| `spec/` has `grammar.ebnf`, a v2 type system (`jtv_v2_type_system_corrected.adoc`)
+  that *declares* an Echo system (§8–9, §12) but the checker implements none of it.
+
+| Governance / truthing
+| *The main gap.* `STATUS.md` claims "100% Complete – Production Ready" while
+  `ROADMAP.adoc` honestly says "Phase 0 Alpha", and `academic/TODO_GAPS.md`
+  claims Lean proofs still use `sorry` when they do not. Docs contradict reality
+  in *both* directions.
+|===
+
+== 3. Gap analysis
+
+The proofs are not the weak point — *governance and build-truth* are. To reach
+AffineScript's position JtV must:
+
+. *G1 — Authoritative status.* Adopt a single capability matrix with a precise
+  status vocabulary; reconcile `STATUS.md` ⇄ `ROADMAP.adoc` ⇄ `TODO_GAPS.md`.
+. *G2 — Doc-truthing.* A mechanical check that docs cannot over-claim past the
+  test/proof gates.
+. *G3 — Build truth.* The Rust core must actually compile, and CI must prove it.
+. *G4 — Conformance-as-oracle.* Promote `conformance/` to a gate.
+. *G5 — Verification locus.* Keep JtV's proof-assistant advantage *and* add the
+  target-layer (WASM) verification story AffineScript has.
+
+== 4. Phased roadmap (starts with proofs)
+
+=== Phase 1 — Proofs & proof-governance (THIS effort)
+
+Rationale: proofs are JtV's strongest asset and the right place to establish the
+truthing discipline, because a mechanized proof cannot lie.
+
+* [x] Inventory every Lean theorem and its status (see
+  `verification/PROOF-CAPABILITY-MATRIX.adoc`).
+* [x] Adopt the AffineScript status vocabulary, specialised for proofs
+  (`verified` / `partial` / `stated-unproven` / `absent`).
+* [x] Doc-truthing pass on the proof layer: correct the stale `sorry` claims in
+  `academic/TODO_GAPS.md` (the proofs are `sorry`-free).
+* [x] *Echo Types alignment (proofs first):* formalise JtV's Echo system in
+  `jtv_proofs/JtvEcho.lean`, aligned with the `echo-types` Agda library and
+  `EchoTypes.jl`. This is the formal contract for the type checker.
+* [ ] Wire `JtvEcho` into the `proof-regression.yml` gate (already covered by
+  the `lakefile.lean` default target).
+
+=== Phase 2 — Echo Types in the checker (commenced here)
+
+* [x] Implement the Echo effect lattice in `crates/jtv-core/src/echo.rs`
+  (`Safe ⊑ Neutral ⊑ Breaking`, join, admissibility) — the executable image of
+  `JtvEcho.lean`.
+* [x] Enforce spec §9 in the type checker: a `reverse` block is rejected when
+  its aggregate echo is `Breaking` (`JtvError::EchoViolation`).
+* [ ] Propagate echo through Data inference as a second effect dimension
+  (alongside `Purity`); surface `@echo(...)` annotations.
+* [ ] Bridge value-level fibres (`echo-types`) to the effect classes for
+  function calls.
+
+=== Phase 3 — Build truth & governance parity
+
+* [ ] *G3:* repair the `ast.rs ⇄ interpreter/typechecker/cli` drift so
+  `jtv-core` compiles; vendor or feature-gate `patacl-core`; make
+  `rust-ci.yml` prove the build.
+* [ ] *G1/G2:* create `docs/CAPABILITY-MATRIX.adoc` for the whole project and a
+  `hooks/check-doc-truthing.sh`; reconcile `STATUS.md`.
+* [ ] *G4:* promote `conformance/` to a compiler-as-oracle gate.
+
+=== Phase 4 — Backend / verification locus
+
+* [ ] *G5:* document and test the WASM target-layer verification story to match
+  AffineScript's typed-wasm contract, while retaining the Lean/Idris assets.
+
+== 5. Echo Types — why this workstream sits in Phase 1
+
+The `echo-types` library (`hyperpolymath/echo-types`, Agda) formalises
+*structured loss / non-total erasure*: the echo of `f` at `y` is the fibre
+`Echo f y := Σ x, f x ≡ y` — irreversible computation that nonetheless *retains
+proof-relevant witnesses* of what was lost. `EchoTypes.jl` is its finite,
+executable companion.
+
+This maps exactly onto JtV's already-declared (but unimplemented) Echo system:
+
+[cols="1,1,2"]
+|===
+| JtV Echo | echo-types | Meaning
+
+| `EchoSafe`     | injective `f` (singleton fibre) | no loss; reversible (`+`↔`-`)
+| `EchoNeutral`  | non-injective, residue retained | structured loss; not invertible
+| `EchoBreaking` | total erasure                   | information destroyed
+|===
+
+Because the construct is *itself proof-defined*, the faithful way to "make the
+type checker accommodate it" is proofs-first: state the lattice and the
+reverse-block contract in Lean (`JtvEcho.lean`), then implement that exact
+contract in Rust (`echo.rs`). Both are delivered in this effort.
+
+== 6. Out of scope here
+
+Full echo propagation through inference, the project-wide capability matrix, the
+Rust build repair, and the WASM verification locus are *named and sequenced*
+above but deferred to their phases to keep this change reviewable.
diff --git a/academic/TODO_GAPS.md b/academic/TODO_GAPS.md
index 2c07a69..a96e96b 100644
--- a/academic/TODO_GAPS.md
+++ b/academic/TODO_GAPS.md
@@ -29,10 +29,14 @@ This document tracks all items marked as TODO in the academic documentation and
 | PROOF-2 | Interpreter correctness partial | High | 🔶 Partial |
 | PROOF-3 | WASM compilation not verified | Medium | ❌ Not Started |
 | PROOF-4 | End-to-end verification chain incomplete | High | 🔶 Partial |
-| PROOF-5 | Some Lean proofs use `sorry` | High | 🔶 Partial |
+| ~~PROOF-5~~ | ~~Some Lean proofs use `sorry`~~ — **RESOLVED 2026-06-02**: `grep -rc 'sorry\|admit\|axiom' jtv_proofs/*.lean` ⇒ 0. The proof layer is `sorry`-free. | — | ✅ Done |
 
 **Impact:** While core theorems are proven, full verification chain is incomplete.
 
+> **Doc-truthing note (2026-06-02):** This section previously overstated proof
+> incompleteness. The authoritative, continuously-checked status now lives in
+> [`verification/PROOF-CAPABILITY-MATRIX.adoc`](../verification/PROOF-CAPABILITY-MATRIX.adoc).
+
 ### 1.3 Security
 
 | Gap | Description | Priority | Status |
@@ -123,21 +127,19 @@ Line ~460: TODO: Uncertainty quantification
 
 ## 3. Lean Proof Gaps
 
-### 3.1 Proofs Using `sorry`
+### 3.1 Proofs Using `sorry` — RESOLVED (2026-06-02)
 
-The following proofs in `jtv_proofs/` use `sorry` and need completion:
+**No proof in `jtv_proofs/` uses `sorry`, `admit`, or an added `axiom`.** The
+claims previously listed here are stale:
 
-```lean
--- JtvOperational.lean:307
-theorem data_terminates (e : DataExpr) (σ : State) :
-    ∃ (n : Int), DataStepStar ⟨e, σ⟩ ⟨DataExpr.lit n, σ⟩ := by
-  -- ... cases use sorry for step composition
+* `data_terminates` (now `JtvOperational.lean:~341`) is a *complete* structural
+  induction over `DataExpr` (lit / var / add / neg), discharged via
+  `dataStepStar_trans` and the `dataStepStar_*` congruence lemmas. No `sorry`.
+* The Control-divergence fact is shown by the fully-proved
+  `infinite_loop_steps`, not a `sorry`-d example.
 
--- JtvOperational.lean:362
-example (σ : State) :
-    ∃ σ', σ' ≠ σ ∧ CtrlStep ... := by
-  -- Uses sorry for σ "x" ≠ 42 case
-```
+Verification: `grep -rc 'sorry\|admit\|axiom' jtv_proofs/*.lean` ⇒ all zero.
+See `verification/PROOF-CAPABILITY-MATRIX.adoc` for the authoritative inventory.
 
 ### 3.2 Missing Theorems
 
diff --git a/crates/jtv-core/src/echo.rs b/crates/jtv-core/src/echo.rs
new file mode 100644
index 0000000..b7e03f6
--- /dev/null
+++ b/crates/jtv-core/src/echo.rs
@@ -0,0 +1,201 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+//
+// Echo: the structured-loss (non-total-erasure) effect lattice for JtV.
+//
+// This implements the type-checker side of JtV's Echo system (spec v2 §8–9,
+// §12) and is the executable counterpart of the formal model in
+// `jtv_proofs/JtvEcho.lean`. The taxonomy aligns with the `echo-types` Agda
+// library (hyperpolymath/echo-types) and its companion `EchoTypes.jl`:
+//
+//   * `Safe`     — no loss: the operation is injective / reversible
+//                  (`+` ↔ `-`). Its fibre over any output is a subsingleton.
+//   * `Neutral`  — structured loss (non-total erasure): information is lost
+//                  but a residue witness is retained.
+//   * `Breaking` — total erasure: information is destroyed; not invertible.
+//
+// Lattice order: `Safe ⊑ Neutral ⊑ Breaking` (join loses guarantees). The
+// headline rule, proved as `blockEcho_admissible` in Lean, is that a reverse
+// block is admissible iff *no* constituent statement is `Breaking`.
+//
+// NOTE (spec v2 §12): Echo is an *effect* dimension, independent of value
+// typing — it lives alongside `Purity`, not inside `Type`.
+
+use crate::ast::*;
+
+/// The three loss classes of the Echo taxonomy.
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub enum Echo {
+    /// No loss — injective / reversible.
+    Safe,
+    /// Structured loss — non-total erasure, residue retained.
+    Neutral,
+    /// Total erasure — irreversible.
+    Breaking,
+}
+
+impl Echo {
+    /// Least upper bound. `Breaking` is absorbing; `Safe` is the unit.
+    /// Matches `Echo.join` in `JtvEcho.lean`.
+    pub fn join(self, other: Echo) -> Echo {
+        use Echo::*;
+        match (self, other) {
+            (Breaking, _) | (_, Breaking) => Breaking,
+            (Neutral, _) | (_, Neutral) => Neutral,
+            (Safe, Safe) => Safe,
+        }
+    }
+
+    /// Lattice order `a ≤ b ↔ a ⊔ b = b`.
+    pub fn leq(self, other: Echo) -> bool {
+        self.join(other) == other
+    }
+
+    /// Whether this echo may appear inside a reverse block.
+    /// Spec v2 §9: reverse blocks forbid `Breaking` (information-destroying)
+    /// statements. Corresponds to `Echo.admissible` in `JtvEcho.lean`.
+    pub fn admissible_in_reverse(self) -> bool {
+        self != Echo::Breaking
+    }
+}
+
+impl std::fmt::Display for Echo {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        match self {
+            Echo::Safe => write!(f, "EchoSafe"),
+            Echo::Neutral => write!(f, "EchoNeutral"),
+            Echo::Breaking => write!(f, "EchoBreaking"),
+        }
+    }
+}
+
+/// Does `expr` reference variable `var`? Self-reference in a reversible
+/// assignment destroys the original value (e.g. `x += x` cannot be inverted),
+/// which is exactly a `Breaking` echo.
+fn data_expr_uses(expr: &DataExpr, var: &str) -> bool {
+    match expr {
+        DataExpr::Number(_) | DataExpr::StringLit(_) => false,
+        DataExpr::Identifier(name) => name == var,
+        DataExpr::Add(l, r) => data_expr_uses(l, var) || data_expr_uses(r, var),
+        DataExpr::Negate(inner) => data_expr_uses(inner, var),
+        DataExpr::FunctionCall(call) => call.args.iter().any(|a| data_expr_uses(a, var)),
+        DataExpr::List(elems) | DataExpr::Tuple(elems) => {
+            elems.iter().any(|e| data_expr_uses(e, var))
+        }
+    }
+}
+
+/// Classify the echo of a single reversible statement.
+pub fn classify_reversible_stmt(stmt: &ReversibleStmt) -> Echo {
+    match stmt {
+        // `x += e` / `x -= e` is reversible (Safe) unless the target appears
+        // in `e`, in which case the original value is destroyed (Breaking).
+        ReversibleStmt::AddAssign(target, expr) | ReversibleStmt::SubAssign(target, expr) => {
+            if data_expr_uses(expr, target) {
+                Echo::Breaking
+            } else {
+                Echo::Safe
+            }
+        }
+        // A reversible `if` is as lossy as its lossiest branch. The Data guard
+        // is pure (Safe); branches are classified conservatively.
+        ReversibleStmt::If(if_stmt) => {
+            let then_echo = classify_control_stmts(&if_stmt.then_branch);
+            let else_echo = if_stmt
+                .else_branch
+                .as_ref()
+                .map(|b| classify_control_stmts(b))
+                .unwrap_or(Echo::Safe);
+            then_echo.join(else_echo)
+        }
+    }
+}
+
+/// Aggregate echo of a list of reversible statements: the join of their
+/// echoes (starting from `Safe`). Matches `blockEcho` in `JtvEcho.lean`.
+pub fn classify_stmts(stmts: &[ReversibleStmt]) -> Echo {
+    stmts
+        .iter()
+        .map(classify_reversible_stmt)
+        .fold(Echo::Safe, Echo::join)
+}
+
+/// Classify control statements appearing inside a reversible `if` branch.
+/// Plain assignments are reversible (Safe); nested reverse blocks recurse;
+/// anything else is treated conservatively as `Neutral` (structured loss we
+/// cannot yet prove reversible).
+fn classify_control_stmts(stmts: &[ControlStmt]) -> Echo {
+    stmts
+        .iter()
+        .map(|s| match s {
+            ControlStmt::Assignment(_) => Echo::Safe,
+            ControlStmt::ReverseBlock(b) => classify_stmts(&b.body),
+            _ => Echo::Neutral,
+        })
+        .fold(Echo::Safe, Echo::join)
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn join_is_lattice() {
+        use Echo::*;
+        // breaking is absorbing, safe is the unit, idempotent.
+        assert_eq!(Safe.join(Safe), Safe);
+        assert_eq!(Safe.join(Neutral), Neutral);
+        assert_eq!(Neutral.join(Breaking), Breaking);
+        assert_eq!(Breaking.join(Safe), Breaking);
+        assert_eq!(Neutral.join(Neutral), Neutral);
+        // commutativity on a sample
+        assert_eq!(Safe.join(Breaking), Breaking.join(Safe));
+    }
+
+    #[test]
+    fn order_and_admissibility() {
+        use Echo::*;
+        assert!(Safe.leq(Neutral));
+        assert!(Neutral.leq(Breaking));
+        assert!(Safe.leq(Breaking));
+        assert!(!Breaking.leq(Safe));
+        assert!(Safe.admissible_in_reverse());
+        assert!(Neutral.admissible_in_reverse());
+        assert!(!Breaking.admissible_in_reverse());
+    }
+
+    #[test]
+    fn add_assign_independent_is_safe() {
+        // x += y  (y independent of x)  ->  Safe
+        let stmt = ReversibleStmt::AddAssign(
+            "x".to_string(),
+            DataExpr::Identifier("y".to_string()),
+        );
+        assert_eq!(classify_reversible_stmt(&stmt), Echo::Safe);
+    }
+
+    #[test]
+    fn self_reference_is_breaking() {
+        // x += x  destroys the original x  ->  Breaking
+        let stmt = ReversibleStmt::AddAssign(
+            "x".to_string(),
+            DataExpr::Identifier("x".to_string()),
+        );
+        assert_eq!(classify_reversible_stmt(&stmt), Echo::Breaking);
+    }
+
+    #[test]
+    fn block_breaking_iff_any_breaking() {
+        // [Safe, Safe] -> Safe ; one Breaking poisons the block.
+        let safe = ReversibleStmt::AddAssign(
+            "x".to_string(),
+            DataExpr::Number(Number::Int(5)),
+        );
+        let breaking = ReversibleStmt::AddAssign(
+            "y".to_string(),
+            DataExpr::Identifier("y".to_string()),
+        );
+        assert_eq!(classify_stmts(&[safe.clone()]), Echo::Safe);
+        assert_eq!(classify_stmts(&[safe.clone(), breaking]), Echo::Breaking);
+    }
+}
diff --git a/crates/jtv-core/src/error.rs b/crates/jtv-core/src/error.rs
index 6845a24..e801523 100644
--- a/crates/jtv-core/src/error.rs
+++ b/crates/jtv-core/src/error.rs
@@ -17,6 +17,9 @@ pub enum JtvError {
     #[error("Purity violation: {0}")]
     PurityViolation(String),
 
+    #[error("Echo violation: {0}")]
+    EchoViolation(String),
+
     #[error("Totality violation: {0}")]
     TotalityViolation(String),
 
diff --git a/crates/jtv-core/src/lib.rs b/crates/jtv-core/src/lib.rs
index cb734ea..05576e1 100644
--- a/crates/jtv-core/src/lib.rs
+++ b/crates/jtv-core/src/lib.rs
@@ -14,6 +14,7 @@
 pub mod ast;
 pub mod coproc;
 pub mod coproc_lower;
+pub mod echo;
 pub mod error;
 pub mod formatter;
 pub mod interpreter;
diff --git a/crates/jtv-core/src/typechecker.rs b/crates/jtv-core/src/typechecker.rs
index e8f66fd..9fb73e6 100644
--- a/crates/jtv-core/src/typechecker.rs
+++ b/crates/jtv-core/src/typechecker.rs
@@ -2,6 +2,7 @@
 // Implements static type checking for the 7 number systems and compound types
 
 use crate::ast::*;
+use crate::echo::{self, Echo};
 use crate::error::{JtvError, Result};
 use std::collections::HashMap;
 
@@ -371,6 +372,7 @@ impl TypeChecker {
                 for stmt in &block.body {
                     self.check_reversible_stmt(stmt)?;
                 }
+                self.check_echo_admissible(&block.body)?;
                 Ok(())
             }
             ControlStmt::ReversibleBlock(rb) => {
@@ -399,6 +401,24 @@ impl TypeChecker {
         }
     }
 
+    /// Enforce the Echo admissibility rule for a reverse block (spec v2 §9):
+    /// a reverse block is well-typed iff no constituent statement is
+    /// `EchoBreaking` (information-destroying). This is the type-checker
+    /// realisation of `blockEcho_admissible` in `jtv_proofs/JtvEcho.lean`.
+    fn check_echo_admissible(&self, body: &[ReversibleStmt]) -> Result<()> {
+        let aggregate = echo::classify_stmts(body);
+        if !aggregate.admissible_in_reverse() {
+            return Err(JtvError::EchoViolation(format!(
+                "reverse block has echo {aggregate}: it destroys information \
+                 and cannot be inverted. Reverse blocks may only contain \
+                 {} or {} statements (no total erasure).",
+                Echo::Safe,
+                Echo::Neutral
+            )));
+        }
+        Ok(())
+    }
+
     fn check_reversible_stmt(&mut self, stmt: &ReversibleStmt) -> Result<()> {
         match stmt {
             ReversibleStmt::AddAssign(target, expr) | ReversibleStmt::SubAssign(target, expr) => {
@@ -605,6 +625,38 @@ mod tests {
         assert!(checker.check_program(&program).is_ok());
     }
 
+    #[test]
+    fn test_reverse_block_rejects_breaking_echo() {
+        // A reverse block whose statement destroys information (self-reference,
+        // EchoBreaking) must be rejected by the type checker (spec v2 §9).
+        use crate::ast::*;
+        let mut checker = TypeChecker::new();
+        let block = ReverseBlock {
+            body: vec![ReversibleStmt::AddAssign(
+                "x".to_string(),
+                DataExpr::Identifier("x".to_string()),
+            )],
+        };
+        let stmt = ControlStmt::ReverseBlock(block);
+        let result = checker.check_control_stmt(&stmt);
+        assert!(matches!(result, Err(JtvError::EchoViolation(_))));
+    }
+
+    #[test]
+    fn test_reverse_block_accepts_safe_echo() {
+        use crate::ast::*;
+        let mut checker = TypeChecker::new();
+        checker.env.set_var("x".to_string(), Type::Int);
+        let block = ReverseBlock {
+            body: vec![ReversibleStmt::AddAssign(
+                "x".to_string(),
+                DataExpr::Number(Number::Int(5)),
+            )],
+        };
+        let stmt = ControlStmt::ReverseBlock(block);
+        assert!(checker.check_control_stmt(&stmt).is_ok());
+    }
+
     #[test]
     fn test_coercion() {
         let code = r#"
diff --git a/jtv_proofs/JtvEcho.lean b/jtv_proofs/JtvEcho.lean
new file mode 100644
index 0000000..f1f5976
--- /dev/null
+++ b/jtv_proofs/JtvEcho.lean
@@ -0,0 +1,226 @@
+/-
+  Julia the Viper — Echo Types: Structured Loss / Non-Total Erasure
+
+  This module formalises JtV's *Echo system* (spec v2, §8–9, §12) and aligns it
+  with the `echo-types` Agda library (hyperpolymath/echo-types) and its
+  executable companion `EchoTypes.jl`.
+
+  An **Echo** classifies the information-loss behaviour of an operation:
+
+    * `safe`     — no loss. The operation is injective / reversible
+                   (its fibre over any output is a subsingleton).
+    * `neutral`  — *structured loss* (non-total erasure). Information is lost,
+                   but a residue witness is retained: the fibre
+                   `Echo f y := Σ x, f x = y` is non-trivial yet bounded.
+    * `breaking` — *total erasure*. Information is destroyed and cannot be
+                   recovered or inverted.
+
+  Lattice order:  `safe ⊑ neutral ⊑ breaking`  (join moves rightward, losing
+  guarantees — mirroring the effect lattice `Total ⊑ Pure ⊑ Impure`).
+
+  The headline result for the type checker is `blockEcho_admissible`: a reverse
+  block is admissible iff *no* constituent statement is `breaking`. This is the
+  formal contract enforced by `crates/jtv-core/src/echo.rs`.
+
+  Proofs are deliberately Mathlib-free (Lean core only) and discharge every
+  goal by finite case analysis, matching the style of the other JtV proofs.
+-/
+
+namespace Jtv.Echo
+
+-- ============================================================================
+-- SECTION 1: THE ECHO LATTICE
+-- ============================================================================
+
+/-- The three loss classes of the Echo taxonomy. -/
+inductive Echo where
+  | safe
+  | neutral
+  | breaking
+  deriving Repr, DecidableEq
+
+/-- Numeric rank, giving the lattice order `safe < neutral < breaking`. -/
+def Echo.rank : Echo → Nat
+  | .safe     => 0
+  | .neutral  => 1
+  | .breaking => 2
+
+/-- Join (least upper bound). Defined by direct pattern match so that every
+    law below reduces by `rfl`. `breaking` is absorbing; `safe` is the unit. -/
+def Echo.join : Echo → Echo → Echo
+  | .breaking, _        => .breaking
+  | _,        .breaking => .breaking
+  | .neutral, _         => .neutral
+  | _,        .neutral  => .neutral
+  | .safe,    .safe     => .safe
+
+@[inherit_doc] infixl:65 " ⊔ " => Echo.join
+
+-- Lattice laws (finite case analysis).
+
+theorem join_comm (a b : Echo) : a ⊔ b = b ⊔ a := by
+  cases a <;> cases b <;> rfl
+
+theorem join_assoc (a b c : Echo) : (a ⊔ b) ⊔ c = a ⊔ (b ⊔ c) := by
+  cases a <;> cases b <;> cases c <;> rfl
+
+theorem join_idem (a : Echo) : a ⊔ a = a := by
+  cases a <;> rfl
+
+/-- `safe` is the bottom element (identity of join): no loss adds nothing. -/
+theorem join_safe_left (a : Echo) : Echo.safe ⊔ a = a := by
+  cases a <;> rfl
+
+theorem join_safe_right (a : Echo) : a ⊔ Echo.safe = a := by
+  cases a <;> rfl
+
+/-- `breaking` is the top element (absorbing): once destroyed, always destroyed. -/
+theorem join_breaking_left (a : Echo) : Echo.breaking ⊔ a = Echo.breaking := by
+  cases a <;> rfl
+
+theorem join_breaking_right (a : Echo) : a ⊔ Echo.breaking = Echo.breaking := by
+  cases a <;> rfl
+
+/-- Partial order induced by the join: `a ≤ b ↔ a ⊔ b = b`. -/
+def Echo.le (a b : Echo) : Prop := a ⊔ b = b
+
+instance : LE Echo := ⟨Echo.le⟩
+
+theorem le_refl (a : Echo) : a ≤ a := join_idem a
+
+theorem le_trans (a b c : Echo) : a ≤ b → b ≤ c → a ≤ c := by
+  cases a <;> cases b <;> cases c <;> intro hab hbc <;>
+    simp_all [LE.le, Echo.le, Echo.join]
+
+/-- `safe` is below everything, `breaking` above everything. -/
+theorem safe_le (a : Echo) : Echo.safe ≤ a := by
+  cases a <;> rfl
+
+theorem le_breaking (a : Echo) : a ≤ Echo.breaking := by
+  cases a <;> rfl
+
+-- ============================================================================
+-- SECTION 2: REVERSE-BLOCK ADMISSIBILITY (the type-checker contract)
+-- ============================================================================
+
+/-- Boolean admissibility: an Echo may appear in a reverse block iff it does
+    not totally erase information (spec v2 §9 forbids `EchoBreaking`). -/
+def Echo.admissible : Echo → Bool
+  | .breaking => false
+  | _         => true
+
+theorem admissible_iff (e : Echo) : e.admissible = true ↔ e ≠ Echo.breaking := by
+  cases e <;> simp [Echo.admissible]
+
+/-- **Key compositional law.** The echo of a composite operation `a ⊔ b` is
+    admissible iff *both* parts are. A single `breaking` sub-operation makes
+    the whole composite inadmissible. -/
+theorem join_admissible (a b : Echo) :
+    (a ⊔ b).admissible = (a.admissible && b.admissible) := by
+  cases a <;> cases b <;> rfl
+
+/-- Admissibility is downward-closed under the lattice order: weakening the
+    loss class of an admissible operation keeps it admissible. -/
+theorem admissible_downward_closed (a b : Echo) :
+    a ≤ b → b.admissible = true → a.admissible = true := by
+  cases a <;> cases b <;> intro hle hb <;>
+    simp_all [LE.le, Echo.le, Echo.join, Echo.admissible]
+
+-- ============================================================================
+-- SECTION 3: REVERSE BLOCKS AS LISTS OF ECHOES
+-- ============================================================================
+
+/-- Aggregate echo of a sequence of statements: the join of their echoes,
+    starting from `safe`. -/
+def blockEcho : List Echo → Echo
+  | []      => .safe
+  | e :: es => e ⊔ blockEcho es
+
+/-- Explicit "all admissible" predicate over a statement list. -/
+def allAdmissible : List Echo → Bool
+  | []      => true
+  | e :: es => e.admissible && allAdmissible es
+
+/-- **Reverse-block soundness.** A block's aggregate echo is admissible iff
+    every statement in it is admissible — i.e. a reverse block is well-typed
+    exactly when it contains no `breaking` (information-destroying) statement.
+
+    This is the property `echo::classify_stmts` / the reverse-block gate in
+    `crates/jtv-core/src/echo.rs` must implement. -/
+theorem blockEcho_admissible (es : List Echo) :
+    (blockEcho es).admissible = allAdmissible es := by
+  induction es with
+  | nil => rfl
+  | cons e es ih =>
+      show (e ⊔ blockEcho es).admissible = (e.admissible && allAdmissible es)
+      rw [join_admissible, ih]
+
+/-- Corollary: if any statement is `breaking`, the whole block is inadmissible. -/
+theorem breaking_blocks_reversal (pre post : List Echo) :
+    (blockEcho (pre ++ Echo.breaking :: post)).admissible = false := by
+  rw [blockEcho_admissible]
+  induction pre with
+  | nil => rfl
+  | cons e pre ih =>
+      show (e.admissible && allAdmissible (pre ++ Echo.breaking :: post)) = false
+      rw [ih]; exact Bool.and_false _
+
+-- ============================================================================
+-- SECTION 4: FIBRES — THE echo-types CORRESPONDENCE
+-- ============================================================================
+
+/-
+  The `echo-types` library defines the echo of `f : A → B` at `y : B` as the
+  fibre `Echo f y := Σ (x : A), f x ≡ y`. We reproduce that definition and
+  prove the bridge between the *value-level* fibre and the *effect-level*
+  Echo class above:
+
+    * injective `f`            ↔  every fibre is a subsingleton   ↔  `safe`
+    * non-injective, retained  ↔  fibre has ≥2 witnesses, bounded ↔  `neutral`
+    * residue weakening        ↔  witnesses forgotten             ↔  loss is
+                                                                     one-way
+-/
+
+/-- The fibre ("echo") of `f` at `y`: inputs mapping to `y`, paired with proof.
+    This is the `echo-types` `Echo f y := Σ x, f x ≡ y`. -/
+def Fibre {A B : Type} (f : A → B) (y : B) : Type := { x : A // f x = y }
+
+/-- `echo-intro`: every input lives in the fibre over its own image. -/
+def echoIntro {A B : Type} (f : A → B) (x : A) : Fibre f (f x) := ⟨x, rfl⟩
+
+/-- `map-over`: a fibre of `g ∘ f` over `z` projects to a fibre of `g` over `z`. -/
+def mapOver {A B C : Type} (f : A → B) (g : B → C) (z : C) :
+    Fibre (g ∘ f) z → Fibre g z
+  | ⟨x, h⟩ => ⟨f x, h⟩
+
+/-- Injectivity, stated without Mathlib. -/
+def Injective {A B : Type} (f : A → B) : Prop :=
+  ∀ x₁ x₂ : A, f x₁ = f x₂ → x₁ = x₂
+
+/-- **Safe ⇔ no loss.** If `f` is injective, every fibre is a subsingleton:
+    the witness is uniquely recoverable, so the operation is reversible. -/
+theorem injective_fibre_subsingleton {A B : Type} (f : A → B)
+    (hf : Injective f) (y : B) (p q : Fibre f y) : p.val = q.val :=
+  hf p.val q.val (p.property.trans q.property.symm)
+
+/-- The residue map: weaken an echo to its observed output, forgetting the
+    witness. This is `echo_to_residue` in `EchoTypes.jl`. -/
+def toResidue {A B : Type} (f : A → B) (y : B) : Fibre f y → B := fun _ => y
+
+/-- **Structured loss is real and one-way.** There is a (non-injective) `f`
+    whose fibre carries two distinct witnesses that the residue cannot tell
+    apart — information genuinely lost, justifying the `neutral`/`breaking`
+    classes rather than `safe`. -/
+theorem residue_lossy :
+    ∃ (f : Bool → Unit) (y : Unit) (p q : Fibre f y), p.val ≠ q.val := by
+  refine ⟨fun _ => (), (), ⟨true, rfl⟩, ⟨false, rfl⟩, ?_⟩
+  decide
+
+/-- Sanity check: the canonical reversible primitive (negation) is injective,
+    hence `safe` — the value-level justification for `reverse { x += v }`. -/
+theorem neg_injective : Injective (fun n : Int => -n) := by
+  intro a b h
+  have : - -a = - -b := by rw [h]
+  simpa using this
+
+end Jtv.Echo
diff --git a/jtv_proofs/lakefile.lean b/jtv_proofs/lakefile.lean
index 7479d0c..ba190ad 100644
--- a/jtv_proofs/lakefile.lean
+++ b/jtv_proofs/lakefile.lean
@@ -29,7 +29,12 @@ lean_lib JtvSecurity where
   -- Security properties: injection impossibility, sandboxing
   roots := #[`JtvSecurity]
 
+lean_lib JtvEcho where
+  -- Echo Types: structured-loss lattice + fibre correspondence
+  -- (aligns with the echo-types Agda library / EchoTypes.jl)
+  roots := #[`JtvEcho]
+
 -- Build all proofs
 @[default_target]
 lean_lib JtvAll where
-  roots := #[`JtvCore, `JtvTheorems, `JtvOperational, `JtvTypes, `JtvSecurity]
+  roots := #[`JtvCore, `JtvTheorems, `JtvOperational, `JtvTypes, `JtvSecurity, `JtvEcho]
diff --git a/spec/jtv_v2_type_system_corrected.adoc b/spec/jtv_v2_type_system_corrected.adoc
index b3b2665..d409f9a 100644
--- a/spec/jtv_v2_type_system_corrected.adoc
+++ b/spec/jtv_v2_type_system_corrected.adoc
@@ -91,6 +91,18 @@ Note: termination is per-input, not bounded.
 
 == 8. Echo System
 
+The Echo system tracks *structured loss (non-total erasure)*. Its canonical
+formal model is the `echo-types` Agda library (`hyperpolymath/echo-types`),
+where the echo of `f` at `y` is the fibre `Echo f y := Σ x, f x ≡ y`; the finite
+executable companion is `EchoTypes.jl`. JtV's three classes correspond to:
+
+* `EchoSafe`     — injective `f` (singleton fibre): no loss, reversible.
+* `EchoNeutral`  — non-injective, residue retained: structured loss.
+* `EchoBreaking` — total erasure: information destroyed.
+
+Mechanized model: `jtv_proofs/JtvEcho.lean` (`verified`).
+Implementation: `crates/jtv-core/src/echo.rs` (lattice + reverse-block gate).
+
 Echo ::= EchoSafe | EchoNeutral | EchoBreaking
 
 Join:
diff --git a/verification/PROOF-CAPABILITY-MATRIX.adoc b/verification/PROOF-CAPABILITY-MATRIX.adoc
new file mode 100644
index 0000000..4f816c8
--- /dev/null
+++ b/verification/PROOF-CAPABILITY-MATRIX.adoc
@@ -0,0 +1,102 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+= JtV Proof Capability Matrix
+:toc:
+:revdate: 2026-06-02
+
+*Authoritative status of JtV's formal proofs.* Modelled on AffineScript's
+`docs/CAPABILITY-MATRIX.adoc` discipline: this file overrides prose claims
+elsewhere. If another document disagrees with this matrix, this matrix is right
+and the other document is a bug.
+
+== Status vocabulary (proof-specialised)
+
+[cols="1,4"]
+|===
+| Term | Meaning
+
+| `verified`
+| Mechanized in Lean 4 and compiles under `lake build` with *no* `sorry`,
+  `admit`, or added `axiom`.
+
+| `partial`
+| Mechanized for the core cases; documented gaps remain (e.g. only the Data
+  fragment, not full Control).
+
+| `stated-unproven`
+| Stated in a paper proof (`academic/proofs/`) but *not* mechanized.
+
+| `absent`
+| Claimed somewhere but neither mechanized nor written down rigorously.
+|===
+
+== Mechanization invariant (checked, 2026-06-02)
+
+`grep -rc 'sorry\|admit\|axiom' jtv_proofs/*.lean` ⇒ *0* across all seven (now
+eight) libraries. The proof layer is `sorry`-free. The `proof-regression.yml`
+workflow runs `lake build` on every change to `jtv_proofs/**`.
+
+NOTE: `academic/TODO_GAPS.md` previously listed PROOF-5 ("Some Lean proofs use
+`sorry`") and a `data_terminates` `sorry` at `JtvOperational.lean:307`. *Both are
+stale* — `data_terminates` (now at line ~341) is a complete structural
+induction. Corrected as part of the Phase-1 doc-truthing pass.
+
+== Lean libraries
+
+[cols="1,1,3"]
+|===
+| Library | Status | Notes
+
+| `JtvCore` | `verified` | Semantic domains, `evalDataExpr`, AST, substitution, free vars.
+| `JtvTheorems` | `verified` | Totality + determinism for Term / Expr / DataExpr.
+| `JtvOperational` | `verified` | Small/big-step equivalence, progress, `data_terminates`, `data_is_pure`; Control non-termination shown by example.
+| `JtvTypes` | `verified` | Typing/purity rules, algebraic cancellation, semantic equivalence congruences.
+| `JtvSecurity` | `verified` | Injection impossibility, no Control→Data flow, OWASP mitigation, sandboxing.
+| `JtvExtended` | `verified` | Strong normalization, confluence, non-interference, reversibility composition.
+| `JtvEcho` | `verified` | *New.* Echo lattice + reverse-block admissibility + fibre correspondence with `echo-types`.
+|===
+
+== Key theorems
+
+[cols="2,1,1,2"]
+|===
+| Theorem | Library | Status | Property
+
+| `dataExpr_totality` | JtvTheorems | `verified` | Every Data expression evaluates (Totality).
+| `dataExpr_determinism` | JtvTheorems | `verified` | Data evaluation is a function.
+| `data_terminates` | JtvOperational | `verified` | Data reduction reaches a literal.
+| `data_is_pure` | JtvOperational | `verified` | Data steps preserve state (Harvard invariant).
+| `no_control_to_data_flow` | JtvSecurity | `verified` | Control cannot flow into Data.
+| `string_not_executable` | JtvSecurity | `verified` | User strings are never code (injection impossibility).
+| `strong_normalization` | JtvExtended | `verified` | Data fragment strongly normalizing.
+| `confluence` | JtvExtended | `verified` | Data reduction confluent.
+| `blockEcho_admissible` | JtvEcho | `verified` | Reverse block admissible ⇔ no `Breaking` statement (the checker contract).
+| `injective_fibre_subsingleton` | JtvEcho | `verified` | `EchoSafe` ⇔ injective ⇔ recoverable.
+| `residue_lossy` | JtvEcho | `verified` | Structured loss is genuine and one-way.
+| `parser_correctness` | — | `absent` | Parser produces a valid AST. (PROOF-1, High.)
+| `interpreter_correctness` | — | `partial` | Interpreter matches denotational semantics. (PROOF-2.)
+| `wasm_compilation_correctness` | — | `absent` | WASM output matches semantics. (PROOF-3, Medium.)
+|===
+
+== Echo Types ↔ implementation correspondence
+
+[cols="2,2"]
+|===
+| `jtv_proofs/JtvEcho.lean` | `crates/jtv-core/src/echo.rs`
+
+| `Echo.join` (absorbing `breaking`, unit `safe`) | `Echo::join`
+| `Echo.admissible` | `Echo::admissible_in_reverse`
+| `Echo.le` (`a ⊔ b = b`) | `Echo::leq`
+| `blockEcho` / `blockEcho_admissible` | `classify_stmts` + reverse-block gate
+| `Fibre f y := { x // f x = y }` | (value-level; effect classes implemented)
+|===
+
+The Rust gate (`TypeChecker::check_echo_admissible`) raises
+`JtvError::EchoViolation` exactly when `blockEcho_admissible` returns `false`.
+
+== Outstanding proof work (sequenced in ALIGNMENT-AFFINESCRIPT.adoc)
+
+* PROOF-1 `parser_correctness` (High) — `absent`.
+* PROOF-2 `interpreter_correctness` (High) — `partial`.
+* PROOF-3 `wasm_compilation_correctness` (Medium) — `absent`.
+* Echo: bridge value-level fibre classification to function-call echo (Phase 2).

From daade4aac1858c8965fee96fe5b0dce84fc34417 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Tue, 2 Jun 2026 14:03:51 +0000
Subject: [PATCH 2/4] refactor(echo): Safe-only reverse-block policy + rustfmt
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Per design decision: reverse blocks accept only EchoSafe; EchoNeutral and
EchoBreaking are both rejected (stricter than spec §9, which permits Neutral
via residue reversal — deferred until that runtime mechanism exists).

- echo.rs: admissible_in_reverse ⇔ Safe; tests + docs updated; rustfmt-clean.
- typechecker.rs: EchoViolation message reflects Safe-only policy.
- JtvEcho.lean: Echo.admissible is Safe-only; admissible_iff ↔ e = safe.
  join_admissible / blockEcho_admissible still hold (join is safe ⇔ both safe).
- spec §9, ALIGNMENT, PROOF matrix: record the Safe-only policy + the four
  Echo design decisions (effect-only; Safe-only; infer+@echo; bridge deferred).

https://claude.ai/code/session_01EJLZKDtcF1RGdKx6TcUTQG
---
 ALIGNMENT-AFFINESCRIPT.adoc               | 19 +++++++++--
 crates/jtv-core/src/echo.rs               | 39 +++++++++++------------
 crates/jtv-core/src/typechecker.rs        |  9 +++---
 jtv_proofs/JtvEcho.lean                   | 25 +++++++++------
 spec/jtv_v2_type_system_corrected.adoc    |  6 ++++
 verification/PROOF-CAPABILITY-MATRIX.adoc |  2 +-
 6 files changed, 63 insertions(+), 37 deletions(-)

diff --git a/ALIGNMENT-AFFINESCRIPT.adoc b/ALIGNMENT-AFFINESCRIPT.adoc
index 6146f90..ecc95b5 100644
--- a/ALIGNMENT-AFFINESCRIPT.adoc
+++ b/ALIGNMENT-AFFINESCRIPT.adoc
@@ -115,13 +115,28 @@ truthing discipline, because a mechanized proof cannot lie.
 * [ ] Wire `JtvEcho` into the `proof-regression.yml` gate (already covered by
   the `lakefile.lean` default target).
 
+==== Design decisions (2026-06-02)
+
+. *Echo is effect-only* — a static dimension alongside `Purity`, not a value
+  type (spec §12). A first-class `Echo<T>` value type is reserved for a later
+  phase.
+. *Safe-only reversal* — reverse blocks accept only `EchoSafe`; `Neutral` and
+  `Breaking` are rejected (see §9 implementation note).
+. *Echo source = infer + `@echo(...)` override* — inferred from operation shape,
+  with an optional annotation mirroring `@pure`/`@total`. Lossy numeric widening
+  (e.g. `Float→Int`) is to carry `Neutral` echo.
+. *Agda↔Lean proof bridge deferred* — `JtvEcho.lean` re-mechanizes the model
+  independently for now; `echo-types` remains the Agda source of truth.
+
 === Phase 2 — Echo Types in the checker (commenced here)
 
 * [x] Implement the Echo effect lattice in `crates/jtv-core/src/echo.rs`
   (`Safe ⊑ Neutral ⊑ Breaking`, join, admissibility) — the executable image of
   `JtvEcho.lean`.
-* [x] Enforce spec §9 in the type checker: a `reverse` block is rejected when
-  its aggregate echo is `Breaking` (`JtvError::EchoViolation`).
+* [x] Enforce reversibility in the type checker (Safe-only policy): a `reverse`
+  block is rejected unless every statement is `EchoSafe` — `Neutral` and
+  `Breaking` both raise `JtvError::EchoViolation`. (Spec §9 permits `Neutral` via
+  residue reversal; deferred until that runtime mechanism exists.)
 * [ ] Propagate echo through Data inference as a second effect dimension
   (alongside `Purity`); surface `@echo(...)` annotations.
 * [ ] Bridge value-level fibres (`echo-types`) to the effect classes for
diff --git a/crates/jtv-core/src/echo.rs b/crates/jtv-core/src/echo.rs
index b7e03f6..35961fc 100644
--- a/crates/jtv-core/src/echo.rs
+++ b/crates/jtv-core/src/echo.rs
@@ -52,10 +52,17 @@ impl Echo {
     }
 
     /// Whether this echo may appear inside a reverse block.
-    /// Spec v2 §9: reverse blocks forbid `Breaking` (information-destroying)
-    /// statements. Corresponds to `Echo.admissible` in `JtvEcho.lean`.
+    ///
+    /// Policy: **Safe-only.** A reverse block must be fully reversible, so only
+    /// `EchoSafe` (bijective `+`/`-`) statements are admissible. `EchoNeutral`
+    /// is rejected too: although spec v2 §9 permits it *in principle*
+    /// (reversal via a retained residue, Bennett-style), that runtime mechanism
+    /// is not implemented, so the checker conservatively requires `Safe`.
+    /// `EchoBreaking` is of course always rejected.
+    ///
+    /// Corresponds to `Echo.admissible` in `JtvEcho.lean`.
     pub fn admissible_in_reverse(self) -> bool {
-        self != Echo::Breaking
+        self == Echo::Safe
     }
 }
 
@@ -159,42 +166,34 @@ mod tests {
         assert!(Neutral.leq(Breaking));
         assert!(Safe.leq(Breaking));
         assert!(!Breaking.leq(Safe));
+        // Safe-only reversal policy: only Safe is admissible in a reverse block.
         assert!(Safe.admissible_in_reverse());
-        assert!(Neutral.admissible_in_reverse());
+        assert!(!Neutral.admissible_in_reverse());
         assert!(!Breaking.admissible_in_reverse());
     }
 
     #[test]
     fn add_assign_independent_is_safe() {
         // x += y  (y independent of x)  ->  Safe
-        let stmt = ReversibleStmt::AddAssign(
-            "x".to_string(),
-            DataExpr::Identifier("y".to_string()),
-        );
+        let stmt =
+            ReversibleStmt::AddAssign("x".to_string(), DataExpr::Identifier("y".to_string()));
         assert_eq!(classify_reversible_stmt(&stmt), Echo::Safe);
     }
 
     #[test]
     fn self_reference_is_breaking() {
         // x += x  destroys the original x  ->  Breaking
-        let stmt = ReversibleStmt::AddAssign(
-            "x".to_string(),
-            DataExpr::Identifier("x".to_string()),
-        );
+        let stmt =
+            ReversibleStmt::AddAssign("x".to_string(), DataExpr::Identifier("x".to_string()));
         assert_eq!(classify_reversible_stmt(&stmt), Echo::Breaking);
     }
 
     #[test]
     fn block_breaking_iff_any_breaking() {
         // [Safe, Safe] -> Safe ; one Breaking poisons the block.
-        let safe = ReversibleStmt::AddAssign(
-            "x".to_string(),
-            DataExpr::Number(Number::Int(5)),
-        );
-        let breaking = ReversibleStmt::AddAssign(
-            "y".to_string(),
-            DataExpr::Identifier("y".to_string()),
-        );
+        let safe = ReversibleStmt::AddAssign("x".to_string(), DataExpr::Number(Number::Int(5)));
+        let breaking =
+            ReversibleStmt::AddAssign("y".to_string(), DataExpr::Identifier("y".to_string()));
         assert_eq!(classify_stmts(&[safe.clone()]), Echo::Safe);
         assert_eq!(classify_stmts(&[safe.clone(), breaking]), Echo::Breaking);
     }
diff --git a/crates/jtv-core/src/typechecker.rs b/crates/jtv-core/src/typechecker.rs
index 9fb73e6..c9905e4 100644
--- a/crates/jtv-core/src/typechecker.rs
+++ b/crates/jtv-core/src/typechecker.rs
@@ -409,11 +409,12 @@ impl TypeChecker {
         let aggregate = echo::classify_stmts(body);
         if !aggregate.admissible_in_reverse() {
             return Err(JtvError::EchoViolation(format!(
-                "reverse block has echo {aggregate}: it destroys information \
-                 and cannot be inverted. Reverse blocks may only contain \
-                 {} or {} statements (no total erasure).",
+                "reverse block has echo {aggregate}: it is not fully reversible. \
+                 Reverse blocks may only contain {} statements (bijective +/-); \
+                 lossy ({} / {}) operations are not invertible here.",
                 Echo::Safe,
-                Echo::Neutral
+                Echo::Neutral,
+                Echo::Breaking
             )));
         }
         Ok(())
diff --git a/jtv_proofs/JtvEcho.lean b/jtv_proofs/JtvEcho.lean
index f1f5976..08e7b69 100644
--- a/jtv_proofs/JtvEcho.lean
+++ b/jtv_proofs/JtvEcho.lean
@@ -18,9 +18,11 @@
   Lattice order:  `safe ⊑ neutral ⊑ breaking`  (join moves rightward, losing
   guarantees — mirroring the effect lattice `Total ⊑ Pure ⊑ Impure`).
 
-  The headline result for the type checker is `blockEcho_admissible`: a reverse
-  block is admissible iff *no* constituent statement is `breaking`. This is the
-  formal contract enforced by `crates/jtv-core/src/echo.rs`.
+  The headline result for the type checker is `blockEcho_admissible`: under the
+  **Safe-only** reversal policy, a reverse block is admissible iff *every*
+  constituent statement is `safe` (fully reversible). `neutral` (lossy but
+  residue-retaining) and `breaking` are both rejected. This is the formal
+  contract enforced by `crates/jtv-core/src/echo.rs`.
 
   Proofs are deliberately Mathlib-free (Lean core only) and discharge every
   goal by finite case analysis, matching the style of the other JtV proofs.
@@ -103,13 +105,16 @@ theorem le_breaking (a : Echo) : a ≤ Echo.breaking := by
 -- SECTION 2: REVERSE-BLOCK ADMISSIBILITY (the type-checker contract)
 -- ============================================================================
 
-/-- Boolean admissibility: an Echo may appear in a reverse block iff it does
-    not totally erase information (spec v2 §9 forbids `EchoBreaking`). -/
+/-- Boolean admissibility: an Echo may appear in a reverse block iff it is
+    `safe`. This is the **Safe-only** policy: a reverse block must be fully
+    reversible, so lossy `neutral` operations (whose Bennett-style residue
+    reversal is not yet implemented) are rejected alongside `breaking`. Spec v2
+    §9 permits `neutral` in principle; the checker is conservatively stricter. -/
 def Echo.admissible : Echo → Bool
-  | .breaking => false
-  | _         => true
+  | .safe => true
+  | _     => false
 
-theorem admissible_iff (e : Echo) : e.admissible = true ↔ e ≠ Echo.breaking := by
+theorem admissible_iff (e : Echo) : e.admissible = true ↔ e = Echo.safe := by
   cases e <;> simp [Echo.admissible]
 
 /-- **Key compositional law.** The echo of a composite operation `a ⊔ b` is
@@ -142,8 +147,8 @@ def allAdmissible : List Echo → Bool
   | e :: es => e.admissible && allAdmissible es
 
 /-- **Reverse-block soundness.** A block's aggregate echo is admissible iff
-    every statement in it is admissible — i.e. a reverse block is well-typed
-    exactly when it contains no `breaking` (information-destroying) statement.
+    every statement in it is admissible — i.e. (under the Safe-only policy) a
+    reverse block is well-typed exactly when every statement is `safe`.
 
     This is the property `echo::classify_stmts` / the reverse-block gate in
     `crates/jtv-core/src/echo.rs` must implement. -/
diff --git a/spec/jtv_v2_type_system_corrected.adoc b/spec/jtv_v2_type_system_corrected.adoc
index d409f9a..e59e4de 100644
--- a/spec/jtv_v2_type_system_corrected.adoc
+++ b/spec/jtv_v2_type_system_corrected.adoc
@@ -127,6 +127,12 @@ Allowed only if:
 - no EchoBreaking statements
 - no loops in V2
 
+Implementation note (2026-06-02): the checker enforces a *stricter, Safe-only*
+policy — every statement must be `EchoSafe`. `EchoNeutral` is permitted by this
+spec in principle (reversal via a retained residue, Bennett-style), but that
+runtime mechanism is unimplemented, so the checker conservatively rejects it.
+See `crates/jtv-core/src/echo.rs` and `jtv_proofs/JtvEcho.lean`.
+
 == 10. Soundness Theorem
 
 Theorem (Safe Fragment Termination):
diff --git a/verification/PROOF-CAPABILITY-MATRIX.adoc b/verification/PROOF-CAPABILITY-MATRIX.adoc
index 4f816c8..631f7c0 100644
--- a/verification/PROOF-CAPABILITY-MATRIX.adoc
+++ b/verification/PROOF-CAPABILITY-MATRIX.adoc
@@ -70,7 +70,7 @@ induction. Corrected as part of the Phase-1 doc-truthing pass.
 | `string_not_executable` | JtvSecurity | `verified` | User strings are never code (injection impossibility).
 | `strong_normalization` | JtvExtended | `verified` | Data fragment strongly normalizing.
 | `confluence` | JtvExtended | `verified` | Data reduction confluent.
-| `blockEcho_admissible` | JtvEcho | `verified` | Reverse block admissible ⇔ no `Breaking` statement (the checker contract).
+| `blockEcho_admissible` | JtvEcho | `verified` | Reverse block admissible ⇔ every statement `Safe` (Safe-only policy; the checker contract).
 | `injective_fibre_subsingleton` | JtvEcho | `verified` | `EchoSafe` ⇔ injective ⇔ recoverable.
 | `residue_lossy` | JtvEcho | `verified` | Structured loss is genuine and one-way.
 | `parser_correctness` | — | `absent` | Parser produces a valid AST. (PROOF-1, High.)

From 6bf4f057c7ef79b48c796c25510f324eee98ce27 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Tue, 2 Jun 2026 14:08:29 +0000
Subject: [PATCH 3/4] =?UTF-8?q?docs(echo):=20record=20refined=20design=20d?=
 =?UTF-8?q?ecisions=20+=20revise=20=C2=A712=20widening/echo?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

- Echo source is inference-only (no @echo annotation); lossy numeric widening
  (Float→Int) carries EchoNeutral. Revises spec §12's "widening independent of
  echo" — widening may raise the echo dimension but never the value type.
- Echo value type (Echo<T>) deferred; AST/Type to be designed so it can be
  added without rework.
- Confirms Safe-only reversal and independent-Lean (no Agda bridge) decisions.

https://claude.ai/code/session_01EJLZKDtcF1RGdKx6TcUTQG
---
 ALIGNMENT-AFFINESCRIPT.adoc            | 19 +++++++++++--------
 spec/jtv_v2_type_system_corrected.adoc |  6 ++++--
 2 files changed, 15 insertions(+), 10 deletions(-)

diff --git a/ALIGNMENT-AFFINESCRIPT.adoc b/ALIGNMENT-AFFINESCRIPT.adoc
index ecc95b5..dc63bdc 100644
--- a/ALIGNMENT-AFFINESCRIPT.adoc
+++ b/ALIGNMENT-AFFINESCRIPT.adoc
@@ -117,16 +117,19 @@ truthing discipline, because a mechanized proof cannot lie.
 
 ==== Design decisions (2026-06-02)
 
-. *Echo is effect-only* — a static dimension alongside `Purity`, not a value
-  type (spec §12). A first-class `Echo<T>` value type is reserved for a later
-  phase.
+. *Echo is effect-only (value type later)* — a static dimension alongside
+  `Purity`, not a value type (spec §12). A first-class `Echo<T>` value type is
+  deferred; the AST/`Type` are to be designed so it can be added *without
+  rework*.
 . *Safe-only reversal* — reverse blocks accept only `EchoSafe`; `Neutral` and
   `Breaking` are rejected (see §9 implementation note).
-. *Echo source = infer + `@echo(...)` override* — inferred from operation shape,
-  with an optional annotation mirroring `@pure`/`@total`. Lossy numeric widening
-  (e.g. `Float→Int`) is to carry `Neutral` echo.
-. *Agda↔Lean proof bridge deferred* — `JtvEcho.lean` re-mechanizes the model
-  independently for now; `echo-types` remains the Agda source of truth.
+. *Echo source = inference only (no annotation)* — echo is inferred from
+  operation shape; there is no `@echo` annotation. *Lossy numeric widening*
+  (e.g. `Float→Int`) carries `EchoNeutral`, which revises spec §12's "widening
+  independent of echo" (the value type is still unaffected — echo is a separate
+  dimension). [Phase-2 implementation: wire echo through `infer_data_expr`.]
+. *Agda↔Lean proof bridge: independent* — `JtvEcho.lean` re-mechanizes the
+  model; `echo-types` remains the sibling Agda source of truth, cited not linked.
 
 === Phase 2 — Echo Types in the checker (commenced here)
 
diff --git a/spec/jtv_v2_type_system_corrected.adoc b/spec/jtv_v2_type_system_corrected.adoc
index e59e4de..f290fa5 100644
--- a/spec/jtv_v2_type_system_corrected.adoc
+++ b/spec/jtv_v2_type_system_corrected.adoc
@@ -170,6 +170,8 @@ Future:
 - Data totality holds
 - Safe fragment termination holds
 - Halting boundary is syntactic
-- Echo does not affect value typing
-- Widening may be lossy and is independent of echo
+- Echo does not affect value typing (Echo is a separate effect dimension)
+- Lossy widening (e.g. Float→Int) raises echo to EchoNeutral; lossless widening
+  stays EchoSafe. (Revises the earlier "widening independent of echo": widening
+  may raise the echo dimension, though it still never changes the value type.)
 

From 824dadabd61a58c3beba30b2b04a35277e025439 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Tue, 2 Jun 2026 14:14:45 +0000
Subject: [PATCH 4/4] docs(echo): re-center on retained-loss lineage; refine
 echo decisions
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Per authoritative Echo design decisions:
- Principle: Echo = structured, proof-relevant loss; the semantic object is
  retained-loss lineage/provenance, not a generic Σ-type or decorative effect.
  Reframed echo.rs + JtvEcho.lean accordingly (fibre = lineage carrier).
- Echo source: infer-by-default + @echo(safe|neutral|breaking) checked
  annotations (not infer-only; needed at boundaries/foreign/audited APIs).
  Added @echo to spec §7.
- Numeric conversions carry echo (3-way): exact⇒Safe, lossy+residue⇒Neutral,
  lossy-no-residue⇒Breaking; Float→Int per residue retention. Revised spec §12.
- Effect-now/value-later: reserve AST/grammar for value-level Echo<T>.
- Formal: JtvEcho.lean authoritative for JtV semantics; Agda↔Lean bridge
  deferred to Phase 4; grammar v2 not blocked on it.

https://claude.ai/code/session_01EJLZKDtcF1RGdKx6TcUTQG
---
 ALIGNMENT-AFFINESCRIPT.adoc               | 37 +++++++++++++++--------
 crates/jtv-core/src/echo.rs               | 17 ++++++++---
 jtv_proofs/JtvEcho.lean                   | 22 ++++++++------
 spec/jtv_v2_type_system_corrected.adoc    | 16 ++++++++--
 verification/PROOF-CAPABILITY-MATRIX.adoc |  4 +++
 5 files changed, 67 insertions(+), 29 deletions(-)

diff --git a/ALIGNMENT-AFFINESCRIPT.adoc b/ALIGNMENT-AFFINESCRIPT.adoc
index dc63bdc..f791555 100644
--- a/ALIGNMENT-AFFINESCRIPT.adoc
+++ b/ALIGNMENT-AFFINESCRIPT.adoc
@@ -117,19 +117,32 @@ truthing discipline, because a mechanized proof cannot lie.
 
 ==== Design decisions (2026-06-02)
 
-. *Echo is effect-only (value type later)* — a static dimension alongside
-  `Purity`, not a value type (spec §12). A first-class `Echo<T>` value type is
-  deferred; the AST/`Type` are to be designed so it can be added *without
-  rework*.
+Echo's semantic object is *retained-loss lineage* — proof-relevant provenance of
+collapsed/weakened/sampled/projected/degraded information. It is **not** a
+generic wrapper, a generic Σ-type, or a decorative effect.
+
+. *Echo is effect-only (value type later)* — for grammar v2, Echo is an effect
+  *classification dimension* alongside `Purity`, not a first-class runtime
+  residue type. The AST/grammar shape is reserved so a value-level `Echo<T>`
+  (carrying the residue) can be added later *without redesign*.
 . *Safe-only reversal* — reverse blocks accept only `EchoSafe`; `Neutral` and
-  `Breaking` are rejected (see §9 implementation note).
-. *Echo source = inference only (no annotation)* — echo is inferred from
-  operation shape; there is no `@echo` annotation. *Lossy numeric widening*
-  (e.g. `Float→Int`) carries `EchoNeutral`, which revises spec §12's "widening
-  independent of echo" (the value type is still unaffected — echo is a separate
-  dimension). [Phase-2 implementation: wire echo through `infer_data_expr`.]
-. *Agda↔Lean proof bridge: independent* — `JtvEcho.lean` re-mechanizes the
-  model; `echo-types` remains the sibling Agda source of truth, cited not linked.
+  `Breaking` are rejected (see §9 implementation note). This is stricter than the
+  earlier spec but matches current interpreter reality. Later, `EchoNeutral` may
+  be admitted *only* with an explicit carried Bennett residue / residue inversion.
+. *Echo source = infer + `@echo` annotations* — inferred from operation shape by
+  default, with `@echo(safe|neutral|breaking)` accepted as *checked*
+  declarations/overrides. Not infer-only (boundaries, foreign calls, and audited
+  APIs need declarations) and not annotation-everywhere. [Phase-2: wire echo
+  through `infer_data_expr` + parse `@echo`.]
+. *Numeric conversions carry echo* (revises spec §12 "independent of echo"):
+  exact/injective representation-preserving ⇒ `EchoSafe`; lossy but
+  residue-retained ⇒ `EchoNeutral`; lossy without usable residue ⇒ `EchoBreaking`.
+  `Float→Int` is `Neutral` or `Breaking` per residue retention. The *value* type
+  is still unaffected — echo is a separate dimension.
+. *Formal layer: independent Lean for Phase 2* — `JtvEcho.lean` is authoritative
+  for JtV implementation semantics now; `echo-types` Agda remains the conceptual
+  source/reference. The Agda↔Lean bridge is deferred to Phase 4; grammar v2 is
+  *not* blocked on a cross-prover bridge.
 
 === Phase 2 — Echo Types in the checker (commenced here)
 
diff --git a/crates/jtv-core/src/echo.rs b/crates/jtv-core/src/echo.rs
index 35961fc..e79760e 100644
--- a/crates/jtv-core/src/echo.rs
+++ b/crates/jtv-core/src/echo.rs
@@ -6,13 +6,20 @@
 // This implements the type-checker side of JtV's Echo system (spec v2 §8–9,
 // §12) and is the executable counterpart of the formal model in
 // `jtv_proofs/JtvEcho.lean`. The taxonomy aligns with the `echo-types` Agda
-// library (hyperpolymath/echo-types) and its companion `EchoTypes.jl`:
+// library (hyperpolymath/echo-types) and its companion `EchoTypes.jl`.
+//
+// PRINCIPLE: Echo is about *structured, proof-relevant loss* — information may
+// be collapsed, weakened, sampled, projected, or degraded, but the
+// residue / provenance / lineage of that loss is still representable. Echo is
+// NOT a generic wrapper, a generic Σ-type, or a decorative effect; the object
+// of interest is *retained-loss lineage*.
 //
 //   * `Safe`     — no loss: the operation is injective / reversible
-//                  (`+` ↔ `-`). Its fibre over any output is a subsingleton.
-//   * `Neutral`  — structured loss (non-total erasure): information is lost
-//                  but a residue witness is retained.
-//   * `Breaking` — total erasure: information is destroyed; not invertible.
+//                  (`+` ↔ `-`). Its fibre over any output is a subsingleton,
+//                  so the lineage is trivial.
+//   * `Neutral`  — structured loss: information is collapsed, but a residue
+//                  carrying the loss lineage/provenance is retained.
+//   * `Breaking` — total erasure: lineage is destroyed; not invertible.
 //
 // Lattice order: `Safe ⊑ Neutral ⊑ Breaking` (join loses guarantees). The
 // headline rule, proved as `blockEcho_admissible` in Lean, is that a reverse
diff --git a/jtv_proofs/JtvEcho.lean b/jtv_proofs/JtvEcho.lean
index 08e7b69..f251650 100644
--- a/jtv_proofs/JtvEcho.lean
+++ b/jtv_proofs/JtvEcho.lean
@@ -5,15 +5,19 @@
   with the `echo-types` Agda library (hyperpolymath/echo-types) and its
   executable companion `EchoTypes.jl`.
 
-  An **Echo** classifies the information-loss behaviour of an operation:
-
-    * `safe`     — no loss. The operation is injective / reversible
-                   (its fibre over any output is a subsingleton).
-    * `neutral`  — *structured loss* (non-total erasure). Information is lost,
-                   but a residue witness is retained: the fibre
-                   `Echo f y := Σ x, f x = y` is non-trivial yet bounded.
-    * `breaking` — *total erasure*. Information is destroyed and cannot be
-                   recovered or inverted.
+  PRINCIPLE: Echo is about *structured, proof-relevant loss* — information may
+  be collapsed, weakened, sampled, projected, or degraded, but the
+  residue / provenance / lineage of that loss is still representable. The fibre
+  `Echo f y := Σ x, f x = y` is used not as a generic Σ-type but as the carrier
+  of *retained-loss lineage*: it records which inputs were collapsed into `y`.
+
+  An **Echo** classifies the loss behaviour of an operation:
+
+    * `safe`     — no loss. The operation is injective / reversible; its fibre
+                   over any output is a subsingleton, so lineage is trivial.
+    * `neutral`  — *structured loss*. Information is collapsed, but the fibre
+                   retains the loss lineage (non-trivial yet bounded).
+    * `breaking` — *total erasure*. Lineage is destroyed; cannot be inverted.
 
   Lattice order:  `safe ⊑ neutral ⊑ breaking`  (join moves rightward, losing
   guarantees — mirroring the effect lattice `Total ⊑ Pure ⊑ Impure`).
diff --git a/spec/jtv_v2_type_system_corrected.adoc b/spec/jtv_v2_type_system_corrected.adoc
index f290fa5..c2b019a 100644
--- a/spec/jtv_v2_type_system_corrected.adoc
+++ b/spec/jtv_v2_type_system_corrected.adoc
@@ -89,6 +89,13 @@ Note: termination is per-input, not bounded.
 @impure:
 - unrestricted
 
+Echo annotations (orthogonal to purity):
+
+@echo(safe|neutral|breaking):
+- checked declaration/override of an operation's loss class
+- inferred from operation shape when absent
+- required at boundaries, foreign calls, and audited APIs (not inferred there)
+
 == 8. Echo System
 
 The Echo system tracks *structured loss (non-total erasure)*. Its canonical
@@ -171,7 +178,10 @@ Future:
 - Safe fragment termination holds
 - Halting boundary is syntactic
 - Echo does not affect value typing (Echo is a separate effect dimension)
-- Lossy widening (e.g. Float→Int) raises echo to EchoNeutral; lossless widening
-  stays EchoSafe. (Revises the earlier "widening independent of echo": widening
-  may raise the echo dimension, though it still never changes the value type.)
+- Numeric conversions carry echo (revises "widening independent of echo"):
+  * exact / injective representation-preserving conversion ⇒ EchoSafe
+  * lossy but residue-retained conversion ⇒ EchoNeutral
+  * lossy without usable residue ⇒ EchoBreaking
+  (e.g. Float→Int is EchoNeutral or EchoBreaking per residue retention.)
+  The conversion still never changes the *value* type — echo is separate.
 
diff --git a/verification/PROOF-CAPABILITY-MATRIX.adoc b/verification/PROOF-CAPABILITY-MATRIX.adoc
index 631f7c0..3faa736 100644
--- a/verification/PROOF-CAPABILITY-MATRIX.adoc
+++ b/verification/PROOF-CAPABILITY-MATRIX.adoc
@@ -94,6 +94,10 @@ induction. Corrected as part of the Phase-1 doc-truthing pass.
 The Rust gate (`TypeChecker::check_echo_admissible`) raises
 `JtvError::EchoViolation` exactly when `blockEcho_admissible` returns `false`.
 
+*Authority:* `JtvEcho.lean` is authoritative for JtV implementation semantics;
+the `echo-types` Agda library is the conceptual source/reference. The Agda↔Lean
+bridge is deferred to Phase 4 — grammar v2 is not blocked on a cross-prover bridge.
+
 == Outstanding proof work (sequenced in ALIGNMENT-AFFINESCRIPT.adoc)
 
 * PROOF-1 `parser_correctness` (High) — `absent`.