proof(#84): 1.1 Echo State Property (Lean) + 1.2 LSM bounded dynamics (Dafny)

.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/

.machine_readable/contractiles/trust/Trustfile.a2ml

@@ -225,21 +225,22 @@ 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"
   - id: "2.3" ; name: "Resource/affine lifecycle"          ; system: "rustc (compile-fail)" ; file: "neurophone-core compile-fail doc-tests + android reset"       ; status: "PROVEN"
   - 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."
 
 ---

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

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