diff --git a/docs/echo-residue-integration.adoc b/docs/echo-residue-integration.adoc
index df235f1..ad16eb3 100644
--- a/docs/echo-residue-integration.adoc
+++ b/docs/echo-residue-integration.adoc
@@ -248,12 +248,30 @@ The replay uses a *per-variable delta*: `reversible as <name>` captures the
 before-image of only the fields its body mutates (a static scan of the body),
 and `reverse <name>` writes just those back — so unrelated state, including
 intervening `set`s by other handlers, survives the reversal. The proof-side
-bridge lemma against echo-types remains the natural next step.
+bridge lemma against echo-types has now landed — see the next section.
 
 == Cross-repo bridge (echo-types)
 
 `Type::Echo<T>` corresponds to echo-types' `Echo f y`, and 007's CNO layer
 (`proofs/agda/CNO.agda`) already bridges to `echo-types/EchoCNOBridge`. A
 direct Agda bridge from the 007 reversibility model to echo-types'
-`EchoTotalCompletion` / `EchoLinear` is the natural place to discharge the
-phase-2 proof obligations against the upstream library of record.
+`EchoTotalCompletion` / `EchoLinear` discharges the phase-2 proof obligations
+against the upstream library of record. It has *landed* as
+`echo-types/proofs/agda/EchoReversibilityBridge.agda` (`--safe --without-K`,
+zero postulates):
+
+* `ReversibleCompletion` re-states the interface this model needs — arm a
+  residue (`hold`), take-it-for-reverse (`takeForReverse`), and the once-only
+  correctness that replay recovers the input (`reverse-recovers`);
+* `echo-reversible` proves `Echo f` satisfies it (its `takeForReverse` is
+  `reverseLinear`'s witness extraction, the `Just`-branch of this model's
+  `takeForReverse : … → Maybe`);
+* `reversibility-via-totality : Σ B (Echo f) ↔ A` is the slogan iso
+  ("irreversible f + residue = reversible representation");
+* `capability-can-be-dropped` / `no-recovery-once-dropped` pin the phase-2
+  "affine capability, linear consumption" discipline via `EchoLinear.weaken`
+  / `no-section-weaken`.
+
+Honest scope: this is the type-level totality + recovery + linear→affine
+no-section content. 007's linear `(1 e : Echo f y)` quantity is not re-proved
+in Agda — the full quantity-semantics port is the documented next slice.