docs(echo): re-center on retained-loss lineage; refine echo decisions

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

Author: claude

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)
 

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

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`).

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.
 

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`.