docs: mark axis-2 approximate echoes as formalised in EchoApprox

roadmap.md: flip [unblocked] → [landed] with the three headline lemmas
listed. taxonomy.md §2: retire the "not yet formalised" / "conjecture"
language; the additive-composition statement is now the theorem
echo-approx-compose under non-expansive outer leg.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

docs/echo-types/roadmap.md

@@ -75,8 +75,14 @@ Paths marked **[unblocked]** can proceed today. Paths marked
   concrete ordinal-track milestone. Pushing that result back into
   `Ordinal/Buchholz/Order.agda`'s main `_<ᵇ_` package is the step
   after that.
-- **[unblocked]** `EchoApprox.agda`: new module for ε-indexed echoes
+- **[landed]** `EchoApprox.agda`: new module for ε-indexed echoes
   over a metric codomain. First-class taxonomy axis 2 artifact.
+  Ships `EchoR ε f y = Σ A (λ x → dist (f x) y ≤ ε)` parametric over
+  a `Tolerance` monoid and a `PseudoMetric`, with three headline
+  lemmas: `echo-approx-intro` (exact ⇒ zero-ε), `echo-approx-relax`
+  (monotone in ε), and `echo-approx-compose` (additive composition
+  under a non-expansive outer leg, realising the taxonomy §2
+  conjecture). Wired into `All.agda` and `Smoke.agda`.
 - **[unblocked]** Per-decoration composition lemmas in `EchoGraded`,
   `EchoLinear`, `EchoIndexed`, `EchoChoreo`, `EchoEpistemic`: check
   each commutes with basic composition.

docs/echo-types/taxonomy.md

@@ -47,18 +47,20 @@ and ask whether the theory still names the residue coherently.
 
 *Example.*
 - Exact: `Echo f y = Σ A (λ x → f x ≡ y)`.
-- Approximate (new, not yet in Agda):
-  `EchoR ε f y = Σ A (λ x → dist (f x) y ≤ ε)` for some metric on `B`.
+- Approximate: `EchoR ε f y = Σ A (λ x → dist (f x) y ≤ ε)` for a
+  pseudo-metric on `B`. **Formalised** in `proofs/agda/EchoApprox.agda`,
+  parametric over a `Tolerance` monoid and a `PseudoMetric`.
 
 The approximate version appears implicitly in numerical
-computation, sensor-fusion pipelines, and lossy compression. It is
-**not yet formalised** in this repo. Open question: what is the
-right universal formulation of an "ε-echo" and what do its
-composition laws look like?
-
-*Conjecture.* Approximate echoes compose with an additive error:
-`ε₁-echo(f) + ε₂-echo(g) ⊑ (ε₁ + ε₂)-echo(g ∘ f)` — roughly, tolerances
-accumulate along composition. Requires careful statement.
+computation, sensor-fusion pipelines, and lossy compression.
+
+*Conjecture (now a theorem).* Approximate echoes compose with an
+additive error under a non-expansive outer leg:
+`ε₁-echo(f) + ε₂-echo(g) ⊑ (ε₁ + ε₂)-echo(g ∘ f)`. Realised in
+`EchoApprox.Approx.echo-approx-compose`. The non-expansiveness
+hypothesis on the outer leg is the minimal extra assumption — without
+it an amplifying second leg can blow ε₁ up arbitrarily on the way
+through.
 
 ---