# Reproduction — Recursive 2-D Kalman filter — whole filter, 32 DSPs, 100 MHz on silicon

The capstone: measurement update + Joseph covariance update, looped with (x,P) state feedback, all through shared MACs + one reciprocal. It tracks a target with the covariance shrinking, and the WHOLE recursive filter closes 100 MHz on a real Arty A7-100T in 32 DSP48s — 13% of the device, less than a third of what the unrolled measurement update alone cost. Scope (graded honestly): the two halves are machine-checked (forward-error bound + MMSE-optimality + Joseph PSD); the composition into 'implemented ≈ optimal' is ARGUED, not yet a Lean theorem; and the shared scheduler/control is verified BIT-EXACT (301 silicon frames, Verilator shared==unrolled), not proven.

| stage | artifact | tier |
|---|---|---|
| emit | 15 compiled targets | LOCAL |
| proof | `kalman2_state_update_fxerr` — the fixed-point measurement update x'=x+K(z-x) is forward-error bounded through the inverse (sorryAx-free) | TOOLCHAIN — Lean axiom trail |
| proof | `matrix2_posterior_mean_mmse` — the posterior-mean estimate is MMSE-optimal (trace loss, per-component) (sorryAx-free) | TOOLCHAIN — Lean axiom trail |
| proof | `kalman2_joseph_psd` — the Joseph covariance step keeps P symmetric PSD for any gain — so recursing it is safe (sorryAx-free) | TOOLCHAIN — Lean axiom trail |
| simulate | estimate converges to target = |err| = 0.0532 < 0.10 (✓) | LOCAL — Q16.16 model, bit-exact to the emitted RTL |
| simulate | covariance trace shrinks monotonically = 0.4000 → 0.0244 monotone ↓ yes (✓) | LOCAL — Q16.16 model, bit-exact to the emitted RTL |
| simulate | final trace(P) vs initial = 0.0244 / 0.4000 < 0.1000 (✓) | LOCAL — Q16.16 model, bit-exact to the emitted RTL |
| silicon | `kalman2d_filter` — WNS +0.715 ns @ 100 MHz on Arty A7-100T | REPLAY |

**Proved, simulated, and on silicon — graded honestly.** The pieces are machine-checked (forward-error bound `kalman2_state_update_fxerr` + MMSE-optimality `matrix2_posterior_mean_mmse` + Joseph PSD `kalman2_joseph_psd`, all sorryAx-free); the fixed-point bounds apply because the emitted per-product arithmetic is bit-identical (TESTED) to the unrolled dataflow they were proven for. Two links are honestly graded, not proven: the composition into 'implemented ≈ optimal' is ARGUED (needs a gain=posterior-mean bridge lemma), and the shared scheduler/control is verified BIT-EXACT (301 silicon frames + Verilator), not proven. See docs/streaming_kalman_filter.md §4b.

Silicon evidence (REPLAY): `monogate-research/electronics_intake/kalman_filter_streaming_arty/evidence/FINDINGS.md`.