docs(readme): note echo types + decidability in the mechanised-proofs summary

The proofs list predated the echo-types feature (TG-10) and decidability (TG-2);
README now reflects the current verified surface and points at proofs/README.md.

https://claude.ai/code/session_01PgHpCFzwYB7Qy9L6kmR8CE

Author: Jonathan D.A. Jewell

README.adoc

@@ -108,11 +108,18 @@ This includes:
   * preservation
   * determinism
   * type safety
+  * decidability of type checking (`infer` ≡ `HasType`)
+
+* *echo types* — structured loss as a type-system feature: `close` (braid
+  closure) is the canonical lossy map, and `echoClose`/`lower`/`residue` make
+  that loss recoverable at the type level (a simply-typed shadow of
+  hyperpolymath/echo-types). All four safety theorems cover them.
 
 See:
 
-* `Tangle.lean`
+* `proofs/Tangle.lean` (and `proofs/README.md` to build/verify)
 * `docs/spec/FORMAL-SEMANTICS.md`
+* `PROOF-NARRATIVE.md` / `PROOF-NEEDS.md`
 
 This formal core covers the *structural heart of the language*, though not all surface features.