diff --git a/.gitignore b/.gitignore
index 5f72477..20518bd 100644
--- a/.gitignore
+++ b/.gitignore
@@ -87,3 +87,10 @@ dist/
 
 # TLA+ model-checker jar cache (fetched by `just proof-tla`)
 .tlacache/
+
+# Dafny release cache (fetched by `just proof-dafny`)
+.dafnycache/
+
+# Lean/Lake build cache and vendored Mathlib checkout (fetched/built by
+# `just proof-lean`); see proofs/lean/.gitignore.
+proofs/lean/.lake/
diff --git a/.machine_readable/contractiles/trust/Trustfile.a2ml b/.machine_readable/contractiles/trust/Trustfile.a2ml
index f3f1cc4..638b2c8 100644
--- a/.machine_readable/contractiles/trust/Trustfile.a2ml
+++ b/.machine_readable/contractiles/trust/Trustfile.a2ml
@@ -225,8 +225,8 @@ artifacts:
   - id: "0.1" ; name: "Panic-freedom (operational paths)" ; system: "proptest" ; file: "crates/*/tests/proptest_*.rs, neurophone-core/tests/proptest_core.rs" ; status: "TESTED"
   - id: "0.2" ; name: "Numeric containment (no NaN/Inf)"   ; system: "proptest" ; file: "crates/*/tests/proptest_numeric.rs, proptest_core.rs"                  ; status: "TESTED"
   - id: "0.3" ; name: "unsafe discipline"                  ; system: "rustc"    ; file: "forbid/deny(unsafe_code) across crates"                                ; status: "PROVEN"
-  - id: "1.1" ; name: "Echo State Property"                ; system: "Lean/TLA" ; file: "proofs/lean/, proofs/tla/"                                             ; status: "DESIGNED"
-  - id: "1.2" ; name: "LSM bounded dynamics"               ; system: "proptest/Dafny" ; file: "crates/lsm/tests/proptest_bounds.rs"                             ; status: "TESTED"
+  - id: "1.1" ; name: "Echo State Property (contraction, ‖W‖∞ hypothesis)" ; system: "Lean 4 + Mathlib" ; file: "proofs/lean/EsnEcho.lean" ; status: "PROVEN"
+  - id: "1.2" ; name: "LSM bounded dynamics (membrane-potential ceiling)" ; system: "proptest + Dafny" ; file: "crates/lsm/tests/proptest_bounds.rs, proofs/dafny/LsmBoundedDynamics.dfy" ; status: "PROVEN"
   - id: "1.3" ; name: "Bridge soundness"                   ; system: "proptest" ; file: "crates/bridge/tests/proptest_soundness.rs"                             ; status: "TESTED"
   - id: "2.1" ; name: "Lifecycle state-machine safety"     ; system: "TLA+ (TLC)" ; file: "proofs/tla/Lifecycle.{tla,cfg}"                                      ; status: "PROVEN"
   - id: "2.2" ; name: "Concurrency safety"                 ; system: "TLA+"     ; file: "(deferred: single-owner design, no shared concurrency)"                ; status: "DESIGNED"
@@ -234,12 +234,13 @@ artifacts:
   - id: "3.1" ; name: "Data-egress / privacy"              ; system: "proptest + conative-gating" ; file: "crates/claude-client/src/egress_gate.rs (wired into create_message), egress_integration_tests" ; status: "TESTED"
   - id: "3.2" ; name: "Bounded external interaction"       ; system: "proptest/contract" ; file: "claude-client: capped backoff + bounded retries (backoff_is_bounded_and_monotonic, total_retry_budget_is_finite)" ; status: "TESTED"
 open_obligations:
-  - "1.1 formal contraction proof (precondition holds; theorem pending)"
-  - "1.2 formal Dafny bound (property evidence exists)"
+  - "1.1 bridge lemma: spectral_radius(W) < 1 (what esn::scale_to_spectral_radius actually enforces) does NOT in general imply ‖W‖∞ < 1 (the Lean theorem's hypothesis) for non-normal matrices — the contraction theorem itself is proven (proofs/lean/EsnEcho.lean), but this connecting lemma is a separate, harder, unattempted result (would need a Gelfand's-formula-style construction)."
+  - "1.2 the two-sided [reset, threshold] membrane-potential bound is FALSE in general (see the LowerBoundFails counterexample in proofs/dafny/LsmBoundedDynamics.dfy) — only the one-sided ceiling bound is provable and is now proven; the exact-real-vs-f32 gap and the spike-history-length bound (crates/lsm/tests/proptest_bounds.rs's third invariant) remain open, not attempted in Dafny this pass."
   - "2.2 concurrency spec (N/A until shared concurrency exists)"
   - "3.1 caller-declared classification honesty (EgressClass is asserted by the caller, not derived from an independent sensor-provenance tracker); no formal (non-property) proof yet"
 non_claims:
-  - "neurophone does NOT yet claim a machine-checked Echo State Property (1.1)."
+  - "neurophone's 1.1 Lean proof (proofs/lean/EsnEcho.lean) establishes the classical reservoir contraction / echo-state theorem under a ‖W‖∞ < 1 hypothesis; it does NOT claim — and this is false in general for non-normal matrices — that the code's actual spectral-radius scaling implies that hypothesis. The code-to-theorem bridge is a separate, still-open lemma."
+  - "neurophone's 1.2 Dafny proof (proofs/dafny/LsmBoundedDynamics.dfy) establishes only a one-sided (ceiling) bound on membrane potential; it does NOT claim a lower (floor) bound (a Dafny counterexample refutes one), and it does not model f32 floating-point rounding, subnormals, or overflow."
   - "neurophone's egress veto (3.1) enforces policy on a caller-declared payload classification; it does NOT independently verify that classification against real sensor provenance, and it is NOT a formally-proven (only property-tested) guarantee."
 
 ---
diff --git a/Justfile b/Justfile
index 76b3038..fe818c8 100644
--- a/Justfile
+++ b/Justfile
@@ -81,10 +81,55 @@ proof-tla:
     cd proofs/tla
     java -XX:+UseParallelGC -cp "$jar" tlc2.TLC -config Lifecycle.cfg Lifecycle.tla
 
+# Type-check the Lean 4 Echo State Property proof (obligation 1.1, issue
+# #84, `proofs/lean/EsnEcho.lean`). Self-skips (non-fatal) if `lake` (elan)
+# isn't on PATH. First run needs network access to fetch the pinned Mathlib
+# revision (see `proofs/lean/lake-manifest.json`); later runs reuse the
+# local `.lake/` cache.
+proof-lean:
+    #!/usr/bin/env bash
+    set -euo pipefail
+    if ! command -v lake >/dev/null 2>&1; then
+        echo "proof-lean: lake not found — skipping Lean check (spec unchanged)"; exit 0
+    fi
+    cd proofs/lean && lake build
+
+# Verify the Dafny LSM-bounded-dynamics proof (obligation 1.2, issue #84,
+# `proofs/dafny/LsmBoundedDynamics.dfy`). Uses a system `dafny` if present;
+# otherwise fetches a pinned, checksum-verified, self-contained release into
+# `.dafnycache/` on first run. Self-skips (non-fatal) if no system `dafny`
+# is found and the download isn't possible (offline / no permissions), so
+# it degrades gracefully in minimal/offline environments.
+proof-dafny:
+    #!/usr/bin/env bash
+    set -euo pipefail
+    if command -v dafny >/dev/null 2>&1; then
+        dafny verify proofs/dafny/LsmBoundedDynamics.dfy
+        exit 0
+    fi
+    version=4.11.0
+    sha256=a46a9ff7cdd720f7955854c78e95df13f4cfe6b80691b05f8654fe19e8267179
+    dir="$(pwd)/.dafnycache/dafny-${version}"
+    bin="${dir}/dafny/dafny"
+    if [ ! -x "$bin" ]; then
+        zip="$(pwd)/.dafnycache/dafny-${version}.zip"
+        mkdir -p "$dir"
+        if ! curl -fsSL -o "$zip" \
+          "https://github.com/dafny-lang/dafny/releases/download/v${version}/dafny-${version}-x64-ubuntu-22.04.zip"; then
+            echo "proof-dafny: could not download Dafny (offline?) — skipping"; exit 0
+        fi
+        echo "${sha256}  ${zip}" | sha256sum -c - || {
+            echo "proof-dafny: checksum mismatch on downloaded release, aborting"; exit 1
+        }
+        unzip -q "$zip" -d "$dir"
+    fi
+    "$bin" verify proofs/dafny/LsmBoundedDynamics.dfy
+
 # Run the full proof surface: property tests + compile-fail typestate doc-tests
-# (via `cargo test`) plus the TLA+ model check.
-proof: test proof-tla
-    @echo "Proof surface checked (properties, typestate compile-fails, TLC)."
+# (via `cargo test`) plus the TLA+ model check, the Lean type-check, and the
+# Dafny verification.
+proof: test proof-tla proof-lean proof-dafny
+    @echo "Proof surface checked (properties, typestate compile-fails, TLC, Lean, Dafny)."
 
 # Quality gates (RSR golden path `just test && just quality`).
 quality: fmt-check lint audit
diff --git a/proofs/README.adoc b/proofs/README.adoc
index 1f3aae0..a2e6ab2 100644
--- a/proofs/README.adoc
+++ b/proofs/README.adoc
@@ -18,8 +18,8 @@ the index from each obligation to the artefact that discharges it.
 |===
 | Tool | Directory | Obligations
 | TLA+ (TLC)        | `proofs/tla/`   | 2.1 lifecycle *(checked)*; 2.2/3.1 specs deferred
-| Lean / Coq        | `proofs/lean/`  | 1.1 echo state property, 1.3 bridge soundness (spec)
-| Dafny / F*        | `proofs/dafny/` | 1.2 LSM bounded dynamics, 0.2 numeric containment (spec)
+| Lean / Coq        | `proofs/lean/`  | 1.1 echo state property *(checked, `‖W‖∞` hypothesis — see NOTE)*; 1.3 bridge soundness (spec)
+| Dafny / F*        | `proofs/dafny/` | 1.2 LSM bounded dynamics *(checked, ceiling half — see NOTE)*; 0.2 numeric containment (spec)
 | proptest          | (in `crates/`)  | executable evidence for 0.1, 0.2, 1.2, 1.3, 3.1 (veto enforcement), 3.2
 | compile-fail tests| `neurophone-core` doc-tests | 2.1 (type level) + 2.3 release-once
 |===
@@ -39,8 +39,8 @@ by property tests over the operational paths; *open* = honest gap, never faked.
 | 0.1 | Panic-freedom on operational paths              | *property* — `esn`/`sensors`/`lsm` numeric suites + `neurophone-core/tests/proptest_core.rs`
 | 0.2 | Numeric containment (no NaN/Inf, no overflow)   | *property* — `*/tests/proptest_numeric.rs` (#87) + `proptest_core.rs`
 | 0.3 | `unsafe` discipline (`deny`/`forbid` all crates) | *done*
-| 1.1 | Echo State Property (reservoir is a contraction)| *open* — the implementation prerequisite holds (see the `spectral_radius` NOTE); the formal contraction proof is pending.
-| 1.2 | LSM bounded dynamics                            | *property* — `lsm/tests/proptest_bounds.rs`; formal Dafny bound *open*
+| 1.1 | Echo State Property (reservoir is a contraction)| *checked* (Lean, sorry-free) — `proofs/lean/EsnEcho.lean` proves `update` is a contraction (constant `(1-a)+a·ρ<1`) and that iterating it forgets the initial state, under the classical `‖W‖∞ < 1` hypothesis. *Open*: the bridge from the code's actual invariant (spectral radius, via `estimate_spectral_radius`) to this hypothesis — see NOTE.
+| 1.2 | LSM bounded dynamics                            | *checked* (Dafny, no assume/axiom) + *property* — `proofs/dafny/LsmBoundedDynamics.dfy` proves the membrane potential never exceeds threshold over an arbitrary-length run; `lsm/tests/proptest_bounds.rs` checks this empirically over `f32`. *Corrected*: the two-sided `[reset, threshold]` bound this table previously implied is **false** in general (Dafny counterexample `LowerBoundFails`) — only the ceiling half is provable. *Open*: exact-real-vs-`f32` gap; spike-history-length bound not attempted in Dafny.
 | 1.3 | Bridge soundness (neural→symbolic)              | *property* — `bridge/tests/proptest_soundness.rs` (#90); salience-ordering semantics *open*
 | 2.1 | Lifecycle state-machine safety                  | *checked* — TLC on `tla/Lifecycle.{tla,cfg}` (no error; 13 states) + 3 compile-fail typestate doc-tests
 | 2.2 | Concurrency safety (no deadlock)                | *open* — N/A under the current single-owner (`&mut`) design; TLA+ spec deferred until shared concurrency exists
@@ -51,16 +51,47 @@ by property tests over the operational paths; *open* = honest gap, never faked.
 
 [NOTE]
 ====
-*`spectral_radius` realisation (1.1).* An earlier version applied
-`EsnConfig.spectral_radius` as a plain scale factor (matrix infinity-norm), which
-only *bounds* the true spectral radius from above — so the configured value was
-never actually realised. That is now fixed: `esn::EchoStateNetwork` estimates the
-true spectral radius by power iteration (`estimate_spectral_radius`) and scales
-the reservoir to hit the target (`scale_to_spectral_radius`), covered by a unit
-test. The Echo State Property's *precondition* (spectral radius `< 1`) therefore
-holds in code; what remains *open* for 1.1 is the formal proof that this
-precondition implies the contraction / echo-forgetting property. Tracked under
-issue #84 / #88.
+*`spectral_radius` realisation and the Lean proof (1.1).* An earlier version
+applied `EsnConfig.spectral_radius` as a plain scale factor (matrix
+infinity-norm), which only *bounds* the true spectral radius from above — so
+the configured value was never actually realised. That is now fixed:
+`esn::EchoStateNetwork` estimates the true spectral radius by power iteration
+(`estimate_spectral_radius`) and scales the reservoir to hit the target
+(`scale_to_spectral_radius`), covered by a unit test (issue #88, closed).
+
+`proofs/lean/EsnEcho.lean` now formally proves (Lean 4 + Mathlib, no `sorry`)
+that the reservoir update is a contraction — *given* the classical sufficient
+condition `‖W‖∞ < 1` (max absolute row sum), which is also what the field
+generally uses. What remains genuinely *open* is a **different, harder**
+statement: that the code's actual invariant (`spectral_radius(W) < 1`, via
+power iteration) implies `‖W‖∞ < 1`. For a general (non-normal) matrix the
+spectral radius can be strictly smaller than every induced operator norm —
+e.g. a nilpotent matrix has spectral radius `0` but arbitrary infinity norm —
+so this bridge is **not true in full generality**, and is a known subtlety in
+reservoir computing (spectral radius `< 1` is the field's standard
+*heuristic*, not, by itself, a sufficient condition for every non-normal
+reservoir — see Yildiz, Jaeger & Kiebel 2012). Proving a correct (necessarily
+weaker/asymptotic — Gelfand's-formula-flavoured) version of this bridge is
+future work; the Lean file's header comment gives the precise mathematical
+reason it was not attempted this pass. Tracked under issue #84 / #88.
+====
+
+[NOTE]
+====
+*The membrane-potential bound is one-sided, not two-sided (1.2).* An earlier
+version of this corpus's obligation text (in `proofs/dafny/README.adoc`)
+described the LSM membrane-potential invariant as a *two-sided* bound,
+`v ∈ [reset, threshold + ε]`. `proofs/dafny/LsmBoundedDynamics.dfy` shows this
+was an overclaim: the Rust `total_current` (input- and recurrent-weighted
+sum) is never clamped, so a sufficiently negative current drives the updated
+potential arbitrarily far *below* `v_reset` in one step — there is a ceiling
+(the threshold-crossing reset) but no floor. The Dafny file's
+`LowerBoundFails` lemma proves this with a concrete counterexample rather
+than merely asserting it. The corrected, honestly-provable (and now
+Dafny-*proven*) claim is one-sided: the potential never exceeds `v_thresh`,
+for any run of any length and any (unrestricted) input-current sequence —
+which is also all that `crates/lsm/tests/proptest_bounds.rs` actually checks
+(it never asserts a lower bound). Tracked under issue #84 / #89.
 ====
 
 == Reproducing
@@ -69,6 +100,14 @@ issue #84 / #88.
 * TLA+ model check: `just proof-tla` (fetches `tla2tools.jar` into `.tlacache/`
   on first run; self-skips if `java` is absent). Direct form:
   `java -cp tla2tools.jar tlc2.TLC -config proofs/tla/Lifecycle.cfg proofs/tla/Lifecycle.tla`.
+* Lean check (obligation 1.1): `just proof-lean` (or `cd proofs/lean && lake
+  build`; self-skips if `lake`/elan is absent). First run needs network
+  access to fetch the pinned Mathlib revision in
+  `proofs/lean/lake-manifest.json`.
+* Dafny check (obligation 1.2): `just proof-dafny` (uses a system `dafny` if
+  present, else fetches a pinned, checksum-verified, self-contained Dafny
+  4.11.0 release into `.dafnycache/`; self-skips if neither is available).
+  Direct form: `dafny verify proofs/dafny/LsmBoundedDynamics.dfy`.
 
 == Ground rules
 
diff --git a/proofs/dafny/LsmBoundedDynamics.dfy b/proofs/dafny/LsmBoundedDynamics.dfy
new file mode 100644
index 0000000..171fecc
--- /dev/null
+++ b/proofs/dafny/LsmBoundedDynamics.dfy
@@ -0,0 +1,200 @@
+// SPDX-License-Identifier: MPL-2.0
+// NeuroPhone - High-Assurance Hardware Orchestration
+// Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+//
+// Obligation 1.2 (LSM bounded dynamics), issue #84 / #89.
+//
+// Models exactly the per-neuron Leaky Integrate-and-Fire (LIF) update in
+// `crates/lsm/src/lib.rs::LiquidStateMachine::step`:
+//
+//   if refrac_remaining > 0.0 {
+//       refrac_remaining -= dt;                      // v unchanged
+//   } else {
+//       dv = dt / tau_m * (-(v - v_rest) + r_m * total_current);
+//       v  = v + dv;
+//       if v >= v_thresh {
+//           v = v_reset;
+//           refrac_remaining = t_refrac;
+//       }
+//   }
+//
+// `LifStep` below is that same two-branch update (as a pure Dafny
+// `function`, so its defining equations are transparent to the verifier),
+// and `LifRun` folds it over an arbitrary finite sequence of per-step input
+// currents (modelling an arbitrary-length simulation run, matching the
+// property test's "long runs of arbitrary input" framing in
+// `crates/lsm/tests/proptest_bounds.rs`).
+//
+// ## What is proven (the half of 1.2 that is actually true of the code)
+//
+// `LifRunKeepsBelowThreshold` proves, by induction over the input-current
+// sequence (a loop-invariant argument mirrored by the recursive structure
+// of `LifRun`), that a membrane potential which starts `<= v_thresh` *never*
+// exceeds `v_thresh` at the end of any subsequent step, for *any* sequence
+// of (unrestricted, not merely bounded) input currents. This holds because
+// `LifStep` is a two-branch invariant-preserving map: the refractory branch
+// passes `v` through unchanged (so the invariant is inherited), and the
+// non-refractory branch either resets to `v_reset < v_thresh` or leaves the
+// updated potential strictly below `v_thresh` (that's exactly the negation
+// of the reset condition) — regardless of how large `total_current` is.
+// Because Dafny's `real` is exact, this is a genuine `<=`, not the `+ 1e-3`
+// slack the Rust proptest needs to accommodate `f32` rounding.
+//
+// ## Honest scope note — the lower bound is NOT provable (corrects an
+// overclaim in the *original* `proofs/dafny/README.adoc`)
+//
+// The original `proofs/dafny/README.adoc` text (written before this file
+// existed) claimed the membrane potential stays within `[reset, threshold +
+// ε]` — a *two*-sided bound. That is false in general for the code as
+// written: `total_current` (`input_weights.dot(input) + recurrent
+// weights^T . spike_indicators`) is not clamped anywhere, so a sufficiently
+// negative `total_current` drives `dv` (and hence the updated `v`)
+// arbitrarily far *below* `v_reset` in a single step — there is a ceiling
+// (the threshold-crossing reset) but no floor. `LowerBoundFails` below is a
+// concrete Dafny counterexample: valid LIF parameters, a valid pre-state,
+// and one step with a large negative current produce a post-step potential
+// strictly below `v_reset`, refuting the general two-sided claim. This file
+// (and the corrected `proofs/README.adoc` / `proofs/dafny/README.adoc`
+// entries) now honestly state a *one-sided* (ceiling-only) bound, which is
+// also all that `crates/lsm/tests/proptest_bounds.rs` actually asserts (it
+// checks finiteness and the upper bound; it never asserts a lower bound).
+//
+// Similarly, the refractory countdown (`refrac_remaining -= dt`, taken
+// verbatim from the Rust code) is *not* clamped at `0` either — it can dip
+// slightly negative for exactly one step (harmless, since the next step's
+// guard is `> 0.0`, which a small negative value also fails, so it is
+// treated identically to `0`). This file does not claim
+// `refracNext >= 0.0` for that reason: it would be a false, unrequested
+// invariant, not something `LiquidStateMachine::step` actually maintains.
+//
+// ## Honest scope note — exact reals vs. `f32`
+//
+// Dafny's `real` is an exact, unbounded-precision numeric domain: it has no
+// NaN, no `Inf`, no overflow, no rounding. This file therefore proves the
+// bound for the *idealised* exact-arithmetic recurrence. It does not, by
+// itself, model IEEE-754 `f32` rounding, subnormal behaviour, or
+// overflow-to-infinity — that empirical side (over the real `f32`
+// execution) is exactly what `crates/lsm/tests/proptest_bounds.rs` and
+// `crates/lsm/tests/proptest_numeric.rs` check. A Dafny/SMT
+// floating-point-theory model (or a Kani harness) bridging exact reals to
+// `f32` remains open — tracked under issue #84.
+//
+// ## Honest scope note — spike-history bound not attempted here
+//
+// `crates/lsm/tests/proptest_bounds.rs` also property-tests a *third*
+// invariant: retained spike-history length per neuron stays within
+// `ceil(history_window / t_refrac) + 2`. This file does not attempt that
+// (it is a separate combinatorial argument over spike *timing*, not the
+// membrane-potential recurrence) — left open, see `proofs/README.adoc`.
+
+module LsmBoundedDynamics {
+
+  // LIF parameters, named exactly as the fields of
+  // `crates/lsm/src/lib.rs::LifParameters` (`tau_m`, `v_rest`, `v_thresh`,
+  // `v_reset`, `t_refrac`, `r_m`).
+  datatype LifParams = LifParams(
+    tauM: real,
+    vRest: real,
+    vThresh: real,
+    vReset: real,
+    tRefrac: real,
+    rM: real)
+
+  // The configuration invariants the Rust code relies on (positive time
+  // constant; the reset potential is strictly below the firing threshold —
+  // true of `LifParameters::default()`: -70.0 < -50.0).
+  predicate ValidParams(p: LifParams)
+  {
+    p.tauM > 0.0 && p.vReset < p.vThresh
+  }
+
+  /// One LIF step for a single neuron, exactly mirroring the per-neuron
+  /// branch of `LiquidStateMachine::step`. A transparent `function` (not an
+  /// opaque `method`) so its defining equations are directly available to
+  /// the verifier at call sites. Returns `(nextV, nextRefracRemaining)`.
+  function LifStep(p: LifParams, dt: real, v: real, refracRemaining: real, totalCurrent: real)
+      : (real, real)
+    requires ValidParams(p)
+  {
+    if refracRemaining > 0.0 then
+      (v, refracRemaining - dt)
+    else
+      var dv := dt / p.tauM * (-(v - p.vRest) + p.rM * totalCurrent);
+      var vUpdated := v + dv;
+      if vUpdated >= p.vThresh then (p.vReset, p.tRefrac) else (vUpdated, 0.0)
+  }
+
+  /// **Obligation 1.2 (single-step ceiling).** If the potential entering
+  /// the step already respects the threshold, it still does after the
+  /// step — regardless of the magnitude of `totalCurrent`.
+  lemma LifStepKeepsBelowThreshold(p: LifParams, dt: real, v: real, refracRemaining: real, totalCurrent: real)
+    requires ValidParams(p)
+    requires v <= p.vThresh
+    ensures LifStep(p, dt, v, refracRemaining, totalCurrent).0 <= p.vThresh
+  {
+    // `LifStep` is a transparent function, so Dafny unfolds it here: in the
+    // refractory branch the result is literally `v`, which is `<= vThresh`
+    // by hypothesis; in the other branch it is either `vReset` (`< vThresh`
+    // by `ValidParams`) or `vUpdated` (`< vThresh` by the negation of the
+    // reset guard). No further hints are needed.
+  }
+
+  /// **Obligation 1.2 (membrane-potential ceiling, whole-run version).**
+  /// Folding `LifStep` over *any* finite sequence of per-step input
+  /// currents (arbitrary reals — a fortiori covering the property test's
+  /// bounded `-10.0..10.0` input range) never lets the membrane potential
+  /// exceed `v_thresh`, given a valid starting state. Proved by induction
+  /// over the sequence length via a loop invariant.
+  lemma LifRunKeepsBelowThreshold(p: LifParams, dt: real, v0: real, refrac0: real, currents: seq<real>)
+    requires ValidParams(p)
+    requires v0 <= p.vThresh
+    ensures LifRun(p, dt, v0, refrac0, currents).0 <= p.vThresh
+  {
+    var v := v0;
+    var refrac := refrac0;
+    var i := 0;
+    while i < |currents|
+      invariant 0 <= i <= |currents|
+      invariant v <= p.vThresh
+      invariant (v, refrac) == LifRunUpTo(p, dt, v0, refrac0, currents, i)
+    {
+      LifStepKeepsBelowThreshold(p, dt, v, refrac, currents[i]);
+      var next := LifStep(p, dt, v, refrac, currents[i]);
+      v, refrac := next.0, next.1;
+      i := i + 1;
+    }
+  }
+
+  /// Fold `LifStep` over the first `i` elements of `currents`.
+  function LifRunUpTo(p: LifParams, dt: real, v0: real, refrac0: real, currents: seq<real>, i: nat)
+      : (real, real)
+    requires ValidParams(p)
+    requires i <= |currents|
+  {
+    if i == 0 then (v0, refrac0)
+    else
+      var (v, refrac) := LifRunUpTo(p, dt, v0, refrac0, currents, i - 1);
+      LifStep(p, dt, v, refrac, currents[i - 1])
+  }
+
+  /// Fold `LifStep` over an entire (arbitrary-length) input sequence.
+  function LifRun(p: LifParams, dt: real, v0: real, refrac0: real, currents: seq<real>): (real, real)
+    requires ValidParams(p)
+  {
+    LifRunUpTo(p, dt, v0, refrac0, currents, |currents|)
+  }
+
+  /// **Honest counterexample.** Refutes the two-sided `[v_reset, v_thresh]`
+  /// bound the *original* `proofs/dafny/README.adoc` claimed: with
+  /// `LifParameters::default()`-shaped parameters, starting at `v_rest`,
+  /// one step with a large negative `total_current` produces a post-step
+  /// potential strictly below `v_reset`. (Arithmetic: `dv = 1/20 * (-(−65 −
+  /// (−65)) + 10 * (−1000)) = -500`, so `v' = -65 + (-500) = -565 <
+  /// v_reset = -70`.)
+  lemma LowerBoundFails()
+    ensures
+      var p := LifParams(20.0, -65.0, -50.0, -70.0, 2.0, 10.0);
+      LifStep(p, 1.0, -65.0, 0.0, -1000.0).0 < p.vReset
+  {
+  }
+}
diff --git a/proofs/dafny/README.adoc b/proofs/dafny/README.adoc
index 7403d38..ef710fd 100644
--- a/proofs/dafny/README.adoc
+++ b/proofs/dafny/README.adoc
@@ -3,12 +3,48 @@
 
 Obligations discharged here (see issue #84):
 
-* *1.2 LSM bounded dynamics* — the discretised Leaky Integrate-and-Fire update
-  keeps the membrane potential within `[reset, threshold + ε]`, respects the
-  refractory period, bounds the firing rate given bounded input, and keeps the
-  spike-history ring buffers within capacity.
+* *1.2 LSM bounded dynamics* — `proofs/dafny/LsmBoundedDynamics.dfy`.
+  **Proven, no `assume`/axiom**: the discretised Leaky Integrate-and-Fire
+  update (`LifStep`, mirroring the per-neuron branch of
+  `LiquidStateMachine::step` in `crates/lsm/src/lib.rs` exactly) never lets
+  the membrane potential exceed `v_thresh`, for *any* finite run and *any*
+  (unrestricted) sequence of input currents, given a valid starting state
+  (`LifRunKeepsBelowThreshold`, proved by induction over the run length).
++
+**Honest correction versus the *original* text of this file.** The
+  original wording (below, superseded) claimed the potential stays within a
+  *two-sided* `[reset, threshold + ε]` interval. That is false in general:
+  `total_current` is not clamped anywhere in the Rust code, so a
+  sufficiently negative current drives the updated potential arbitrarily far
+  *below* `v_reset` in a single step — there is a ceiling (the
+  threshold-crossing reset) but no floor. `LowerBoundFails` in the same file
+  is a concrete Dafny counterexample proving this (not just asserting it).
+  This matches `crates/lsm/tests/proptest_bounds.rs`, which likewise only
+  ever asserts the upper bound plus finiteness, never a lower bound. The
+  refractory-period respect, firing-rate bound, and spike-history-capacity
+  parts of the original claim remain as before: the spike-history length
+  bound is property-tested (`proptest_bounds.rs`) but not attempted in
+  Dafny (a separate combinatorial argument over spike timing, not the
+  membrane-potential recurrence) — open, tracked under issue #84.
++
+**Honest scope note — exact reals vs. `f32`.** Dafny's `real` is exact
+  (no NaN/Inf/overflow/rounding); this proof is over the *idealised*
+  exact-arithmetic recurrence, and does not by itself model IEEE-754 `f32`
+  rounding or overflow-to-infinity — that empirical side is exactly what
+  `crates/lsm/tests/proptest_bounds.rs` / `proptest_numeric.rs` check.
+  Bridging exact reals to `f32` (Dafny/SMT floating-point theory, or a Kani
+  harness) remains open.
 * *0.2 Numeric containment* — the sensor and reservoir kernels neither produce
   nor propagate NaN/Inf, and integer indexing/accumulation does not overflow.
+  *(Spec only — no `.dfy` file yet; property-tested in
+  `crates/*/tests/proptest_numeric.rs`.)*
 
 Models are written against the algorithm; the Rust implementation is tied back
-to them with Kani harnesses and `proptest` properties in the respective crates.
+to them with `proptest` properties in the respective crates (Kani is not
+currently wired — see `proofs/README.adoc`). Reproduce with
+`just proof-dafny` (or a system `dafny verify
+proofs/dafny/LsmBoundedDynamics.dfy`); fetches a pinned, checksum-verified,
+self-contained Dafny 4.11.0 release into `.dafnycache/` on first run if no
+system `dafny` is found, and self-skips (non-fatal) if that download isn't
+possible (offline / no permissions). Verified in this pass with Dafny 4.11.0
+(self-contained Linux x64 release; no system `dotnet` required).
diff --git a/proofs/lean/.gitignore b/proofs/lean/.gitignore
new file mode 100644
index 0000000..ba8e4af
--- /dev/null
+++ b/proofs/lean/.gitignore
@@ -0,0 +1,5 @@
+# SPDX-License-Identifier: MPL-2.0
+# Lake build cache and vendored dependencies (Mathlib + transitive deps).
+# Not committed — reproducible from `lakefile.lean` / `lake-manifest.json`
+# (pinned Mathlib revision) via `lake build`.
+.lake/
diff --git a/proofs/lean/EsnEcho.lean b/proofs/lean/EsnEcho.lean
new file mode 100644
index 0000000..301d833
--- /dev/null
+++ b/proofs/lean/EsnEcho.lean
@@ -0,0 +1,292 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- NeuroPhone - High-Assurance Hardware Orchestration
+-- Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+--
+-- Obligation 1.1 (Echo State Property), issue #84 / #88.
+--
+-- This file formalises and *proves* (no `sorry`/`admit`) that the Echo State
+-- Network reservoir update implemented in `crates/esn/src/lib.rs`
+-- (`EchoStateNetwork::step`) is a contraction in the state variable whenever
+-- the recurrent weight matrix's infinity-operator-norm (max absolute row
+-- sum) is below `1`, and derives the classical Echo State (fading-memory)
+-- Property as a corollary: iterating the update under an arbitrary shared
+-- input sequence forgets the initial reservoir state exponentially fast.
+--
+-- ## Exact correspondence with the Rust implementation
+--
+-- `crates/esn/src/lib.rs::EchoStateNetwork::step` computes
+-- ```
+-- total_activation   = input_weights.dot(input) + recurrent_weights.dot(state)
+-- new_state          = (1 - leaking_rate) * state
+--                       + leaking_rate * total_activation.mapv(tanh)
+-- ```
+-- i.e. (writing `a` for `leaking_rate`, `W` for `recurrent_weights`, and
+-- collecting `input_weights.dot(input)` into a single vector `b` that is
+-- *constant* across the two trajectories being compared — it depends only on
+-- the shared input at that step, not on the reservoir state):
+-- `x' = (1 - a) • x + a • tanh(W *ᵥ x + b)`.
+-- `update` below is exactly this map.
+--
+-- ## Honest scope note — spectral radius vs. operator norm (the actual gap)
+--
+-- The theorem's hypothesis is `‖W‖∞ < 1` (`rowAbsSum W i ≤ ρ < 1` for every
+-- row `i`), matching the classical sufficient condition for the Echo State
+-- Property (tanh is 1-Lipschitz; a convex combination with a `< 1`-operator-norm
+-- linear map is a strict contraction). This is also what the *original*
+-- `proofs/lean/README.adoc` text described before this file existed.
+--
+-- `crates/esn/src/lib.rs::scale_to_spectral_radius` scales the reservoir by
+-- the matrix's *true spectral radius* (via power iteration,
+-- `estimate_spectral_radius`), **not** by the infinity norm. For a general
+-- (non-normal) real matrix the spectral radius can be *strictly smaller* than
+-- every induced operator norm — e.g. a nilpotent matrix has spectral radius
+-- `0` but can have an arbitrarily large infinity norm — so
+-- "`spectral_radius(W) < 1`" does **not**, in general, imply "`‖W‖∞ < 1`".
+-- This is a known subtlety in the reservoir-computing literature (spectral
+-- radius `< 1` is the classical *heuristic* used in practice, but is not by
+-- itself a sufficient condition for the fading-memory property for
+-- non-normal reservoirs — see e.g. Yildiz, Jaeger & Kiebel 2012,
+-- "Re-visiting the echo state property").
+--
+-- So: **this file fully and honestly discharges the contraction theorem
+-- under the classical `‖W‖∞ < 1` hypothesis** (a complete, `sorry`-free proof
+-- — see `update_isContraction` / `update_iterate_isContraction` below). What
+-- remains genuinely open (tracked in `proofs/README.adoc` / issue #84) is the
+-- *separate* bridge lemma "`spectral_radius(W) < 1` (what the Rust code
+-- actually enforces) implies `‖W‖∞ < ρ'` for some `ρ' < 1`" — this is false in
+-- full generality for non-normal matrices (as above), and the true general
+-- fact (Gelfand's formula: for every `ε > 0` there is *some* submultiplicative
+-- norm with `‖W‖ ≤ spectralRadius W + ε`) is a substantially harder theorem
+-- (needs a real Schur/Jordan-form construction) that has not been attempted
+-- here. Do not read this file as closing that gap — it does not.
+
+import Mathlib.Analysis.Calculus.MeanValue
+import Mathlib.Analysis.SpecificLimits.Basic
+import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
+import Mathlib.Data.Complex.Trigonometric
+import Mathlib.Data.Matrix.Mul
+import Mathlib.Analysis.Normed.Group.Constructions
+
+open scoped Matrix
+open Finset
+
+namespace NeuroPhone.EsnEcho
+
+/-! ### Vectors and matrices
+
+Reservoir states live in `Fin n → ℝ`; Mathlib's `Pi.normedAddCommGroup`
+instance equips this with the **sup norm** `‖x‖ = ⨆ i, |x i|`
+(`Finset.univ.sup` on `Fin n`, `0` when `n = 0`), i.e. exactly `‖x‖∞`. -/
+
+variable {n : ℕ}
+
+/-- The max-absolute-row-sum ("infinity operator norm") of a real square
+matrix, row `i`. -/
+def rowAbsSum (W : Matrix (Fin n) (Fin n) ℝ) (i : Fin n) : ℝ :=
+  ∑ j, |W i j|
+
+theorem rowAbsSum_def (W : Matrix (Fin n) (Fin n) ℝ) (i : Fin n) :
+    rowAbsSum W i = ∑ j, |W i j| :=
+  rfl
+
+/-- `Matrix.mulVec` unfolds to the expected finite sum. -/
+theorem mulVec_apply (W : Matrix (Fin n) (Fin n) ℝ) (x : Fin n → ℝ) (i : Fin n) :
+    (W *ᵥ x) i = ∑ j, W i j * x j :=
+  rfl
+
+/-- Each component of `W *ᵥ x` is bounded by `(rowAbsSum W i) * ‖x‖`. -/
+theorem abs_mulVec_apply_le (W : Matrix (Fin n) (Fin n) ℝ) (x : Fin n → ℝ) (i : Fin n) :
+    |(W *ᵥ x) i| ≤ rowAbsSum W i * ‖x‖ := by
+  rw [mulVec_apply]
+  calc
+    |∑ j, W i j * x j| ≤ ∑ j, |W i j * x j| := Finset.abs_sum_le_sum_abs _ _
+    _ = ∑ j, |W i j| * |x j| := by simp [abs_mul]
+    _ ≤ ∑ j, |W i j| * ‖x‖ := by
+        apply Finset.sum_le_sum
+        intro j _
+        have hxj : |x j| ≤ ‖x‖ := by
+          have := norm_le_pi_norm x j
+          rwa [Real.norm_eq_abs] at this
+        exact mul_le_mul_of_nonneg_left hxj (abs_nonneg _)
+    _ = rowAbsSum W i * ‖x‖ := by rw [rowAbsSum_def, Finset.sum_mul]
+
+/-- If every row of `W` has absolute-sum `≤ ρ`, then `W` is `ρ`-Lipschitz
+(as a linear map) with respect to the sup norm: `‖W *ᵥ x‖ ≤ ρ * ‖x‖`. -/
+theorem norm_mulVec_le {W : Matrix (Fin n) (Fin n) ℝ} {ρ : ℝ} (hρ0 : 0 ≤ ρ)
+    (hW : ∀ i, rowAbsSum W i ≤ ρ) (x : Fin n → ℝ) : ‖W *ᵥ x‖ ≤ ρ * ‖x‖ := by
+  have hb : 0 ≤ ρ * ‖x‖ := mul_nonneg hρ0 (norm_nonneg _)
+  refine (pi_norm_le_iff_of_nonneg hb).2 fun i => ?_
+  rw [Real.norm_eq_abs]
+  exact (abs_mulVec_apply_le W x i).trans (mul_le_mul_of_nonneg_right (hW i) (norm_nonneg _))
+
+/-! ### `tanh` is `1`-Lipschitz
+
+Classical fact: `tanh' x = 1 / (cosh x)^2 ∈ (0, 1]` since `cosh x ≥ 1`
+everywhere, so the mean-value theorem gives a global `1`-Lipschitz bound. -/
+
+theorem hasDerivAt_tanh (x : ℝ) : HasDerivAt Real.tanh (1 / Real.cosh x ^ 2) x := by
+  have hc : Real.cosh x ≠ 0 := (Real.cosh_pos x).ne'
+  have h := (Real.hasDerivAt_sinh x).div (Real.hasDerivAt_cosh x) hc
+  have hnum : Real.cosh x * Real.cosh x - Real.sinh x * Real.sinh x = 1 := by
+    linear_combination Real.cosh_sq_sub_sinh_sq x
+  rw [hnum] at h
+  have hfun : (fun y => Real.sinh y / Real.cosh y) = Real.tanh :=
+    funext fun y => (Real.tanh_eq_sinh_div_cosh y).symm
+  rwa [hfun] at h
+
+theorem deriv_tanh_le_one (x : ℝ) : |deriv Real.tanh x| ≤ 1 := by
+  rw [(hasDerivAt_tanh x).deriv]
+  have hc1 : (1 : ℝ) ≤ Real.cosh x := Real.one_le_cosh x
+  have hsq : (1 : ℝ) ≤ Real.cosh x ^ 2 := by nlinarith
+  rw [abs_of_pos (by positivity), div_le_one (by positivity)]
+  linarith
+
+/-- `Real.tanh` is `1`-Lipschitz: `|tanh a - tanh b| ≤ |a - b|`. -/
+theorem tanh_lipschitz (a b : ℝ) : |Real.tanh a - Real.tanh b| ≤ |a - b| := by
+  have hdiff : ∀ x ∈ (Set.univ : Set ℝ), DifferentiableAt ℝ Real.tanh x :=
+    fun x _ => (hasDerivAt_tanh x).differentiableAt
+  have hbound : ∀ x ∈ (Set.univ : Set ℝ), ‖deriv Real.tanh x‖ ≤ 1 := by
+    intro x _
+    simpa [Real.norm_eq_abs] using deriv_tanh_le_one x
+  have hmvt := convex_univ.norm_image_sub_le_of_norm_deriv_le hdiff hbound
+    (Set.mem_univ b) (Set.mem_univ a)
+  simpa [Real.norm_eq_abs] using hmvt
+
+/-- Elementwise `tanh` on reservoir-sized vectors. -/
+noncomputable def vtanh (x : Fin n → ℝ) : Fin n → ℝ := fun i => Real.tanh (x i)
+
+/-- `vtanh` is `1`-Lipschitz for the sup norm: `‖vtanh x - vtanh y‖ ≤ ‖x - y‖`. -/
+theorem norm_vtanh_sub_le (x y : Fin n → ℝ) : ‖vtanh x - vtanh y‖ ≤ ‖x - y‖ := by
+  refine (pi_norm_le_iff_of_nonneg (norm_nonneg _)).2 fun i => ?_
+  have hi : ‖(vtanh x - vtanh y) i‖ = |Real.tanh (x i) - Real.tanh (y i)| := by
+    simp [vtanh, Real.norm_eq_abs]
+  rw [hi]
+  refine (tanh_lipschitz (x i) (y i)).trans ?_
+  have : |x i - y i| = ‖(x - y) i‖ := by simp [Real.norm_eq_abs]
+  rw [this]
+  exact norm_le_pi_norm (x - y) i
+
+/-! ### The reservoir update map and its contraction constant -/
+
+/-- The Echo State Network reservoir update, exactly as implemented by
+`EchoStateNetwork::step`: `x' = (1 - a) • x + a • tanh(W *ᵥ x + b)`, where `a`
+is the leaking rate, `W` the recurrent weight matrix, and `b` the (per-step,
+trajectory-independent) driven-input contribution `input_weights.dot(input)`. -/
+noncomputable def update (a : ℝ) (W : Matrix (Fin n) (Fin n) ℝ) (b x : Fin n → ℝ) : Fin n → ℝ :=
+  (1 - a) • x + a • vtanh (W *ᵥ x + b)
+
+/-- **Obligation 1.1 (single step).** If the leaking rate `a ∈ [0, 1]` and the
+recurrent matrix satisfies `‖W‖∞ ≤ ρ`, then `update a W b` is Lipschitz in the
+state with constant `(1 - a) + a * ρ`, uniformly in the (shared, per-step)
+input contribution `b`. -/
+theorem update_lipschitz {a ρ : ℝ} (ha0 : 0 ≤ a) (ha1 : a ≤ 1) (hρ0 : 0 ≤ ρ)
+    {W : Matrix (Fin n) (Fin n) ℝ} (hW : ∀ i, rowAbsSum W i ≤ ρ) (b x y : Fin n → ℝ) :
+    ‖update a W b x - update a W b y‖ ≤ ((1 - a) + a * ρ) * ‖x - y‖ := by
+  have hstep :
+      update a W b x - update a W b y
+        = (1 - a) • (x - y) + a • (vtanh (W *ᵥ x + b) - vtanh (W *ᵥ y + b)) := by
+    funext i
+    simp only [update, Pi.sub_apply, Pi.add_apply, Pi.smul_apply, smul_eq_mul]
+    ring
+  rw [hstep]
+  refine (norm_add_le _ _).trans ?_
+  have h1 : ‖(1 - a) • (x - y)‖ ≤ (1 - a) * ‖x - y‖ := by
+    rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg (by linarith)]
+  have h2 : ‖a • (vtanh (W *ᵥ x + b) - vtanh (W *ᵥ y + b))‖ ≤ a * (ρ * ‖x - y‖) := by
+    rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg ha0]
+    have hlin : W *ᵥ x + b - (W *ᵥ y + b) = W *ᵥ (x - y) := by
+      rw [Matrix.mulVec_sub]; abel
+    have := norm_vtanh_sub_le (W *ᵥ x + b) (W *ᵥ y + b)
+    rw [hlin] at this
+    have hWxy := norm_mulVec_le hρ0 hW (x - y)
+    calc
+      a * ‖vtanh (W *ᵥ x + b) - vtanh (W *ᵥ y + b)‖ ≤ a * ‖W *ᵥ (x - y)‖ :=
+        mul_le_mul_of_nonneg_left this ha0
+      _ ≤ a * (ρ * ‖x - y‖) := mul_le_mul_of_nonneg_left hWxy ha0
+  calc
+    ‖(1 - a) • (x - y)‖ + ‖a • (vtanh (W *ᵥ x + b) - vtanh (W *ᵥ y + b))‖
+        ≤ (1 - a) * ‖x - y‖ + a * (ρ * ‖x - y‖) := add_le_add h1 h2
+    _ = ((1 - a) + a * ρ) * ‖x - y‖ := by ring
+
+/-- The single-step contraction constant is strictly below `1` exactly when
+the leaking rate is strictly positive and `ρ < 1` — i.e. `update` is a
+genuine (strict) contraction, not merely non-expansive. A leaking rate of
+exactly `0` is a real, if degenerate, edge case allowed by
+`EsnConfig`'s validation (`leaking_rate ∈ [0.0, 1.0]`): with `a = 0` the
+update never changes the state (`x' = x`) regardless of input, so the Echo
+State Property genuinely fails at that boundary — this is not a proof gap,
+it is a correct fact about the map. -/
+theorem contraction_constant_lt_one {a ρ : ℝ} (ha0 : 0 < a) (hρ1 : ρ < 1) :
+    (1 - a) + a * ρ < 1 := by nlinarith
+
+/-- Iterating `update` over a (finite, arbitrary-length) shared input
+sequence `bs`, one additive contribution per step, oldest first. This models
+running the same driven input sequence into two different initial reservoir
+states. -/
+noncomputable def iterateUpdate (a : ℝ) (W : Matrix (Fin n) (Fin n) ℝ)
+    (bs : List (Fin n → ℝ)) (x : Fin n → ℝ) : Fin n → ℝ :=
+  bs.foldl (fun acc b => update a W b acc) x
+
+/-- **Obligation 1.1 (Echo State / fading-memory property).** Driving two
+different reservoir states `x0`, `y0` with the *same* input sequence `bs`
+(any finite length) shrinks their distance by the single-step contraction
+constant raised to the `bs.length`-th power. Since `(1 - a) + a * ρ < 1`
+whenever `0 < a` and `ρ < 1` (`contraction_constant_lt_one`), this distance
+→ 0 as the sequence length → ∞ — the reservoir *forgets its initial state*
+independently of what that initial state was, which is precisely the Echo
+State (fading-memory) Property. -/
+theorem iterateUpdate_lipschitz {a ρ : ℝ} (ha0 : 0 ≤ a) (ha1 : a ≤ 1) (hρ0 : 0 ≤ ρ)
+    {W : Matrix (Fin n) (Fin n) ℝ} (hW : ∀ i, rowAbsSum W i ≤ ρ) :
+    ∀ (bs : List (Fin n → ℝ)) (x0 y0 : Fin n → ℝ),
+      ‖iterateUpdate a W bs x0 - iterateUpdate a W bs y0‖
+        ≤ ((1 - a) + a * ρ) ^ bs.length * ‖x0 - y0‖ := by
+  have hL0 : 0 ≤ (1 - a) + a * ρ := by nlinarith
+  intro bs
+  induction bs with
+  | nil =>
+      intro x0 y0
+      simp [iterateUpdate]
+  | cons b bs' ih =>
+      intro x0 y0
+      have hunfold : ∀ z : Fin n → ℝ,
+          iterateUpdate a W (b :: bs') z = iterateUpdate a W bs' (update a W b z) := fun z => rfl
+      rw [hunfold x0, hunfold y0]
+      calc
+        ‖iterateUpdate a W bs' (update a W b x0) - iterateUpdate a W bs' (update a W b y0)‖
+            ≤ ((1 - a) + a * ρ) ^ bs'.length * ‖update a W b x0 - update a W b y0‖ :=
+          ih (update a W b x0) (update a W b y0)
+        _ ≤ ((1 - a) + a * ρ) ^ bs'.length * (((1 - a) + a * ρ) * ‖x0 - y0‖) := by
+              apply mul_le_mul_of_nonneg_left (update_lipschitz ha0 ha1 hρ0 hW b x0 y0)
+              exact pow_nonneg hL0 _
+        _ = ((1 - a) + a * ρ) ^ (b :: bs').length * ‖x0 - y0‖ := by
+              rw [List.length_cons]; ring
+
+/-- **Obligation 1.1 (closing the loop).** Corollary of `iterateUpdate_lipschitz`:
+for a strict contraction (`0 < a`, `ρ < 1`) and *any* way of extending the
+shared input sequence over time (`bs : ℕ → List (Fin n → ℝ)` with
+`(bs k).length = k`), two reservoirs started from different initial states
+`x0`, `y0` and driven by that same growing input sequence converge to each
+other — `iterateUpdate a W (bs k) x0 - iterateUpdate a W (bs k) y0 → 0` as
+`k → ∞`. This is the formal statement of "fading memory" / "echo state"
+independence from initial conditions: the reservoir state is asymptotically
+determined entirely by the (shared) input history, not by where it started. -/
+theorem iterateUpdate_forgets_initial_state {a ρ : ℝ} (ha0 : 0 < a) (ha1 : a ≤ 1)
+    (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) {W : Matrix (Fin n) (Fin n) ℝ}
+    (hW : ∀ i, rowAbsSum W i ≤ ρ) (bs : ℕ → List (Fin n → ℝ))
+    (hbs : ∀ k, (bs k).length = k) (x0 y0 : Fin n → ℝ) :
+    Filter.Tendsto
+      (fun k => iterateUpdate a W (bs k) x0 - iterateUpdate a W (bs k) y0)
+      Filter.atTop (nhds 0) := by
+  have hL0 : 0 ≤ (1 - a) + a * ρ := by nlinarith
+  have hL1 : (1 - a) + a * ρ < 1 := contraction_constant_lt_one ha0 hρ1
+  have hbound : ∀ k, ‖iterateUpdate a W (bs k) x0 - iterateUpdate a W (bs k) y0‖
+      ≤ ((1 - a) + a * ρ) ^ k * ‖x0 - y0‖ := by
+    intro k
+    have hik := iterateUpdate_lipschitz ha0.le ha1 hρ0 hW (bs k) x0 y0
+    rwa [hbs k] at hik
+  have htends :
+      Filter.Tendsto (fun k => ((1 - a) + a * ρ) ^ k * ‖x0 - y0‖) Filter.atTop (nhds 0) := by
+    simpa using (tendsto_pow_atTop_nhds_zero_of_lt_one hL0 hL1).mul_const (‖x0 - y0‖)
+  exact squeeze_zero_norm hbound htends
+
+end NeuroPhone.EsnEcho
diff --git a/proofs/lean/README.adoc b/proofs/lean/README.adoc
index 26c8dc0..e2a83de 100644
--- a/proofs/lean/README.adoc
+++ b/proofs/lean/README.adoc
@@ -3,14 +3,37 @@
 
 Obligations discharged here (see issue #84):
 
-* *1.1 Echo State Property* — the ESN update map
-  `x' = (1-a)·x + a·tanh(W·x + W_in·u)` is a contraction whenever the
-  recurrent matrix satisfies `‖W‖∞ < 1` (the sufficient condition the code
-  currently enforces via `scale_to_spectral_radius`). tanh is 1-Lipschitz and
-  the leaking-rate convex combination is non-expansive, so the composite map is
-  a contraction in the ∞-norm ⇒ the Echo State (fading-memory) Property holds.
+* *1.1 Echo State Property* — `proofs/lean/EsnEcho.lean` (Lean 4 + Mathlib,
+  toolchain pinned in `proofs/lean/lean-toolchain`). **Proven, no `sorry`**:
+  the ESN update map `x' = (1-a)·x + a·tanh(W·x + b)` (exactly
+  `EchoStateNetwork::step` in `crates/esn/src/lib.rs`, with `b` the
+  per-step input contribution shared by both trajectories being compared) is
+  a contraction whenever the recurrent matrix satisfies `‖W‖∞ < 1` (max
+  absolute row sum). `tanh` is 1-Lipschitz (proved from its derivative,
+  `1/cosh²`, being in `(0, 1]`, via the mean-value theorem) and the
+  leaking-rate convex combination is non-expansive, so the composite map has
+  Lipschitz constant `(1-a) + a·ρ < 1` whenever `0 < a ≤ 1` and `ρ < 1`.
+  Iterating over an arbitrary shared input sequence therefore forgets the
+  initial state exponentially fast — the Echo State (fading-memory)
+  Property (`iterateUpdate_forgets_initial_state`).
++
+**Honest scope note.** The proof's hypothesis is `‖W‖∞ < 1`, matching the
+  classical sufficient condition. `crates/esn/src/lib.rs::scale_to_spectral_radius`
+  scales the reservoir by the matrix's *true spectral radius*
+  (`estimate_spectral_radius`, power iteration) — **not** the infinity norm.
+  For a general (non-normal) real matrix the spectral radius can be
+  *strictly smaller* than every induced operator norm, so
+  `spectral_radius(W) < 1` does **not**, in general, imply `‖W‖∞ < 1` (a
+  known subtlety in the reservoir-computing literature — see e.g. Yildiz,
+  Jaeger & Kiebel 2012, "Re-visiting the echo state property"). That bridge
+  lemma is a separate, harder, unattempted theorem (see the file's header
+  comment and `proofs/README.adoc`); this file does not close it, and does
+  not claim to.
 * *1.3 Bridge soundness* — the neural→symbolic encoding in `crates/bridge` is
-  total and deterministic, and round-trips within tolerance.
+  total and deterministic, and round-trips within tolerance. *(Spec only —
+  no `.lean` file yet; property-tested in `crates/bridge/tests/proptest_soundness.rs`.)*
 
 No `sorry` / `admit` is permitted (enforced by `MUST.contractile`); a file lands
-here only when its theorems are fully proved.
+here only when its theorems are fully proved. Reproduce with
+`just proof-lean` (or `cd proofs/lean && lake build`); self-skips if `lake`
+isn't on `PATH`.
diff --git a/proofs/lean/lake-manifest.json b/proofs/lean/lake-manifest.json
new file mode 100644
index 0000000..2845b1a
--- /dev/null
+++ b/proofs/lean/lake-manifest.json
@@ -0,0 +1,116 @@
+{
+ "version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages": [
+  {
+   "url": "https://github.com/leanprover-community/mathlib4.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "a6276f4c6097675b1cf5ebd49b1146b735f38c02",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.16.0",
+   "inherited": false,
+   "configFile": "lakefile.lean"
+  },
+  {
+   "url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "1622a8693b31523c8f82db48e01b14c74bc1f155",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.16.0-rc1",
+   "inherited": true,
+   "configFile": "lakefile.toml"
+  },
+  {
+   "url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "003ff459cdd85de551f4dcf95cdfeefe10f20531",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"
+  },
+  {
+   "url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "1a6613663c3eb08c401ce0fd1a408412f2c2321e",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"
+  },
+  {
+   "url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "07f60e90998dfd6592688a14cd67bd4e384b77b2",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.50",
+   "inherited": true,
+   "configFile": "lakefile.lean"
+  },
+  {
+   "url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "79402ad9ab4be9a2286701a9880697e2351e4955",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.16.0-rc1",
+   "inherited": true,
+   "configFile": "lakefile.toml"
+  },
+  {
+   "url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "f0c584bcb14c5adfb53079781eeea75b26ebbd32",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.15.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"
+  },
+  {
+   "url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "01006c9e86bf9e397c026fef4190478dd1fd897e",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"
+  },
+  {
+   "url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"
+  }
+ ],
+ "name": "neurophone_proofs",
+ "lakeDir": ".lake"
+}
diff --git a/proofs/lean/lakefile.lean b/proofs/lean/lakefile.lean
new file mode 100644
index 0000000..a0fdb6a
--- /dev/null
+++ b/proofs/lean/lakefile.lean
@@ -0,0 +1,20 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Obligation 1.1 (Echo State Property) — see issue #84 / #88 and
+-- proofs/README.adoc. Toolchain pinned in `lean-toolchain`
+-- (`leanprover/lean4:v4.16.0`, matching the mathlib revision below).
+import Lake
+open Lake DSL
+
+package neurophone_proofs where
+
+require mathlib from git
+  "https://github.com/leanprover-community/mathlib4.git" @ "v4.16.0"
+
+/-- Obligation 1.1: the ESN reservoir state-update map is a contraction
+    (Echo State / fading-memory Property) whenever the recurrent weight
+    matrix's operator norm is `< 1`. See `EsnEcho/Contraction.lean` for the
+    exact statement and honest scope notes. -/
+@[default_target]
+lean_lib EsnEcho where
+  srcDir := "."
+  roots := #[`EsnEcho]
diff --git a/proofs/lean/lean-toolchain b/proofs/lean/lean-toolchain
new file mode 100644
index 0000000..2586f88
--- /dev/null
+++ b/proofs/lean/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.16.0