proof: discharge proof-obligation map Tiers 0–3 (#84) (#106)

## Proof-obligation map (#84) — Tiers 0–3, batched

Full lowest-tier-first. Entire workspace: `cargo clippy --workspace
--all-targets` clean, `cargo test --workspace` all green.

### Tier 0 — foundations
- **0.1 panic-freedom (#86)** — 6 operational `unwrap`/`expect` removed;
`cfg_attr(not(test), deny(clippy::unwrap_used, expect_used))` on every
crate.
- **0.2 numeric containment (#87)** — proptest no-NaN/Inf for
`esn::step`, `lsm::step`, sensors IIR.
- **0.3 unsafe discipline** — `deny`/`forbid` (on main).

### Tier 1 — core algorithmic correctness
- **1.1 Echo State Property (#88)** — true spectral radius via power
iteration (merged in #101).
- **1.2 LSM bounded dynamics (#89)** — same spectral-radius fix in lsm +
membrane/spike-history bounds proptest.
- **1.3 bridge soundness (#90)** — totality / determinism /
bounded-output proptest.

### Tier 2 — system orchestration
- **2.1 lifecycle (#91)** — compile-time **typestate**
(`Created→Active→Down`, terminal shutdown); illegal transitions don't
compile. Matches `proofs/tla/Lifecycle.tla`.
- **2.2 concurrency (#92)** — no-lost-updates stress test (8×250);
data-race & deadlock freedom argued from safe-Rust + single-lock.
- **2.3 resource/affine (#93)** — design spec (`proofs/affine/`); Rust
ownership gives acquire-release-once today, AffineScript linear handles
deferred.

### Tier 3 — trust boundary
- **3.1 data-egress (#94)** — egress allow-list test (API key stays a
header; no device/sensor fields in body) +
neural-context-not-sent-when-disabled.
- **3.2 bounded external interaction (#95)** — saturating/capped backoff
(fixes a latent `pow` overflow); injection-safety via typed JSON.

Closes #86 #87 #89 #90 #91 #92 #94 #95 (1.1/#88 already merged via #101;
2.3/#93 remains a tracked spec).

_The two Kotlin banned-language CI checks are red from `main`'s
`android/` app (tracked in #83), not from this PR._

https://claude.ai/code/session_01Gu1JFCZHuBtBhAWPr4sMQw

---------

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

.machine_readable/agent_instructions/methodology.a2ml

@@ -25,6 +25,19 @@ ring-ceiling = 2              # Hard ceiling for ring expansion (0-3)
 wave-cap = 2                  # Max waves before requiring user "keep going"
 spike-required = true         # Every session must ship code, not just designs
 
+# ============================================================================
+# WORK ORDERING (ALWAYS)
+# ============================================================================
+# Complete the FULL lowest tier before moving up. General precedence:
+#   lowest-tier (complete) -> proximal seam -> distal themes -> current focus -> other
+# For tiered backlogs (e.g. proof obligations): finish all of Tier 0, then all of
+# Tier 1, then Tier 2, then Tier 3, then other work. Never open a higher tier
+# while a lower tier still has open items.
+
+[methodology.work-ordering]
+rule = "full-lowest-tier-first"
+order = ["lowest-tier-complete", "proximal-seam", "distal-themes", "current-focus", "other"]
+
 # ============================================================================
 # PRIORITY WEIGHTS
 # ============================================================================

Cargo.lock

@@ -6,6 +6,7 @@
 //! natural-language description suitable for prompt injection into an LLM.
 
 #![forbid(unsafe_code)]
+#![cfg_attr(not(test), deny(clippy::unwrap_used, clippy::expect_used))]
 
 use ndarray::{Array1, ArrayView1};
 use serde::{Deserialize, Serialize};

crates/bridge/src/lib.rs

@@ -0,0 +1,47 @@
+// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell
+//! Property tests — bridge soundness (obligation 1.3, #90).
+//!
+//! The neural->symbolic encoder must be:
+//!   * total — defined on all finite inputs (any/empty/mismatched lengths), no panic;
+//!   * deterministic — identical input sequences yield identical outputs (incl. the
+//!     history-dependent urgency term);
+//!   * well-formed — salience, urgency in [0,1] and finite; active counts never
+//!     exceed the input lengths; description never empty.
+
+use bridge::{Bridge, BridgeConfig};
+use ndarray::Array1;
+use proptest::prelude::*;
+
+proptest! {
+    #[test]
+    fn bridge_encode_deterministic_and_bounded(
+        seq in proptest::collection::vec(
+            (
+                proptest::collection::vec(-1.0e3f32..1.0e3f32, 0..48),
+                proptest::collection::vec(-1.0e3f32..1.0e3f32, 0..48),
+            ),
+            1..40)
+    ) {
+        let mut b1 = Bridge::new(BridgeConfig::default()).unwrap();
+        let mut b2 = Bridge::new(BridgeConfig::default()).unwrap();
+
+        for (lv, ev) in seq {
+            let lsm = Array1::from_vec(lv);
+            let esn = Array1::from_vec(ev);
+
+            let c1 = b1.encode(lsm.view(), esn.view());
+            let c2 = b2.encode(lsm.view(), esn.view());
+
+            // Determinism (including the last_lsm-dependent urgency).
+            prop_assert_eq!(&c1, &c2);
+
+            // Well-formed, bounded outputs.
+            prop_assert!(c1.salience.is_finite() && (0.0..=1.0).contains(&c1.salience));
+            prop_assert!(c1.urgency.is_finite() && (0.0..=1.0).contains(&c1.urgency));
+            prop_assert!(c1.lsm_active <= lsm.len());
+            prop_assert!(c1.esn_active <= esn.len());
+            prop_assert!(!c1.description.is_empty());
+        }
+    }
+}