diff --git a/compiler/lib/typecheck.ml b/compiler/lib/typecheck.ml
index 9895256..74812fd 100644
--- a/compiler/lib/typecheck.ml
+++ b/compiler/lib/typecheck.ml
@@ -622,6 +622,66 @@ let rec infer_expr (gamma : env) (sigma : strand_ctx) (e : expr) : ty =
   | EchoEq (e1, e2) ->
     infer_echo_eq (infer_expr gamma sigma e1) (infer_expr gamma sigma e2)
 
+  (* ---- Echo types (structured loss) ----
+   * Mirror the HasType rules in proofs/Tangle.lean:
+   *   [T-Echo-Close] echoClose e : Echo[Word[n], Word[0]]   when e : Word[n]
+   *   [T-Lower]      lower e      : τ                        when e : Echo[ρ, τ]
+   *   [T-Residue]    residue e    : ρ                        when e : Echo[ρ, τ]
+   *   [T-Pair]/[T-Fst]/[T-Snd]    product intro + projections
+   *   [T-Echo-Add]   echoAdd a b  : Echo[Num × Num, Num]
+   *   [T-Echo-Eq]    echoEq a b   : Echo[ρ × ρ, Bool]        for ρ ∈ {Num, Str, Word[n]}
+   *)
+  | EchoClose e1 ->
+    begin match infer_expr gamma sigma e1 with
+    | TWord n -> TEcho (TWord n, TWord 0)
+    | t -> type_error "echoClose requires Word[n], got %s" (pp_ty t)
+    end
+
+  | Lower e1 ->
+    begin match infer_expr gamma sigma e1 with
+    | TEcho (_, t) -> t
+    | t -> type_error "lower requires Echo[_, _], got %s" (pp_ty t)
+    end
+
+  | Residue e1 ->
+    begin match infer_expr gamma sigma e1 with
+    | TEcho (r, _) -> r
+    | t -> type_error "residue requires Echo[_, _], got %s" (pp_ty t)
+    end
+
+  | Pair (e1, e2) ->
+    let t1 = infer_expr gamma sigma e1 in
+    let t2 = infer_expr gamma sigma e2 in
+    TProd (t1, t2)
+
+  | Fst e1 ->
+    begin match infer_expr gamma sigma e1 with
+    | TProd (a, _) -> a
+    | t -> type_error "fst requires a product, got %s" (pp_ty t)
+    end
+
+  | Snd e1 ->
+    begin match infer_expr gamma sigma e1 with
+    | TProd (_, b) -> b
+    | t -> type_error "snd requires a product, got %s" (pp_ty t)
+    end
+
+  | EchoAdd (e1, e2) ->
+    begin match infer_expr gamma sigma e1, infer_expr gamma sigma e2 with
+    | TNum, TNum -> TEcho (TProd (TNum, TNum), TNum)
+    | t1, t2 -> type_error "echoAdd requires Num, Num, got %s, %s" (pp_ty t1) (pp_ty t2)
+    end
+
+  | EchoEq (e1, e2) ->
+    begin match infer_expr gamma sigma e1, infer_expr gamma sigma e2 with
+    | TNum, TNum -> TEcho (TProd (TNum, TNum), TBool)
+    | TStr, TStr -> TEcho (TProd (TStr, TStr), TBool)
+    | TWord n, TWord m when n = m -> TEcho (TProd (TWord n, TWord n), TBool)
+    | t1, t2 ->
+      type_error "echoEq requires matching Num/Str/Word[n] operands, got %s, %s"
+        (pp_ty t1) (pp_ty t2)
+    end
+
 (** Infer the type of a binary operation given operand types.
  *  Implements rules from sections 3.4, 3.5, 3.6.
  *)
diff --git a/docs/spec/ECHO-TANGLEIR-THREADING.md b/docs/spec/ECHO-TANGLEIR-THREADING.md
index 171543d..f7cb057 100644
--- a/docs/spec/ECHO-TANGLEIR-THREADING.md
+++ b/docs/spec/ECHO-TANGLEIR-THREADING.md
@@ -1,4 +1,5 @@
 <!--
+SPDX-License-Identifier: MPL-2.0
 SPDX-License-Identifier: CC-BY-SA-4.0
 Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -->
@@ -26,6 +27,10 @@ The seam with QuandleDB is exact, not incidental:
 > object `quandle_presentation(ir::TangleIR)::QuandlePresentation` derives the
 > quandle from.
 
+`echo_distinguishes_collapsed` (Lean) says distinct braids can close to the
+same diagram while keeping distinct residues. Threading the residue therefore
+gives QuandleDB **provenance**: which braid produced a given closed diagram,
+disambiguating cases that plain `close` would conflate.
 **A note on what the Lean model proves.** The mechanized `close`/`lower`
 (`proofs/Tangle.lean`) is a *type-level* collapse: every braid reduces to the
 single `Word[0]` value `.identity` (a collapse to one point), **not** to a knot
@@ -83,6 +88,9 @@ The invariant to preserve: for any braid `b`,
 `quandle_presentation(EchoClosed(b, close(b)))` ≡
 `quandle_presentation(Close(close(b)))` whenever the closed diagram alone
 suffices — the residue path must agree with the diagram path on the quandle,
+and additionally retains `b` for provenance. This mirrors
+`echo_roundtrip_typed` (the residue/result projections are well-typed) and the
+`lower`/`residue` agreement in the Lean model.
 and additionally retains `b` for provenance.
 
 **This quandle invariant is an unproven knot-theoretic obligation** that