# Reproduction — Scalar Kalman filter — proven optimal, on silicon at 100 MHz

The scalar Kalman filter behind the whole proof→silicon arc: state carried across measurements, the variance update `P ← P·r/(P+r)` a division in the feedback path. Regenerate with `make scalar-kalman-demo`.

| stage | artifact | tier |
|---|---|---|
| emit | `kalman_update_1d.eml`, `kalman_filter.eml` → 32 targets | LOCAL |
| proof | `kalman_recursive_mmse` — each recursive step's posterior mean is MMSE-optimal (conjugacy self-composition) (sorryAx-free) | TOOLCHAIN — Lean, axiom trail re-derivable |
| proof | `kalman_variance_recursion_fixed_point` — the Q16.16 variance recursion stays within a proven bound of the exact recursion over N steps (sorryAx-free) | TOOLCHAIN — Lean, axiom trail re-derivable |
| proof | `kalman_estimate_recursion_coupled` — the estimate recursion's fixed-point error is bounded — the gain error derived from the variance error (sorryAx-free) | TOOLCHAIN — Lean, axiom trail re-derivable |
| simulate | filter RMS vs measurement RMS = 0.071 / 0.325 ratio 0.22 < 1 (✓) | LOCAL — real emitted update kernel |
| simulate | estimate converges to truth = |2.4812 − 2.5| = 0.0188 < 0.10 (✓) | LOCAL — real emitted update kernel |
| simulate | posterior variance shrinks = 1.000 → 0.01538 < 0.05 (✓) | LOCAL — real emitted update kernel |
| silicon | `eml_reciprocal` — WNS +1.102 ns @ 100 MHz on Arty A7-100T | REPLAY |
| silicon | `kalman_update_1d` — WNS +0.587 ns @ 100 MHz on Arty A7-100T | REPLAY |
| silicon | `kalman_filter_step` — WNS +0.866 ns @ 100 MHz on Arty A7-100T | REPLAY |

**Proved, simulated, and on silicon.** Each recursive step is MMSE-optimal and the Q16.16 recursion's fixed-point error is bounded in both state components (all sorryAx-free); the emitted update, driven over the stream, beats the raw measurements (filter RMS 0.071 vs 0.325) and converges to 2.4812 (truth 2.5, |err| 0.0188) as the variance shrinks to 0.01538; and all three anchors close 100 MHz WHOLE-DESIGN (0 failing endpoints, DRC clean); 170 passes bit-exact to the golden recursion, the estimate tracks and P shrinks 1.0 → 0.015

Silicon evidence (REPLAY): `monogate-research/electronics_intake/KALMAN_SILICON_FLAGSHIP.md` — the three anchors' post-route timing, DRC, and bit-exact UART captures.