# Reproduction — Linear Kalman tracker (constant velocity)

A constant-velocity Kalman filter tracking a 1-D position from noisy position-only measurements, built from the kalman2d_predict + kalman2d_update kernels. Regenerate with `make kalman-demo`.

| stage | artifact | tier |
|---|---|---|
| emit | `kalman2d_predict.eml`, `kalman2d_update.eml` → 32 targets | LOCAL |
| proof | `kalman2d_cov_predict_psd` — the predicted covariance F·P·Fᵀ+Q stays positive-semidefinite | TOOLCHAIN — Lean (proven sorryAx-free in the test suite) |
| proof | `kalman2d_joseph_psd` — the Joseph covariance update preserves PSD for any gain | TOOLCHAIN — Lean (proven sorryAx-free in the test suite) |
| simulate | filter RMS vs measurement RMS = 0.525 / 0.934 ratio 0.56 < 0.6 | LOCAL |
| simulate | recovered velocity (never measured) = 0.516 ≈ 0.5 | LOCAL |
| simulate | max |filter − NumPy-KF| = 1.1e-16 < 1e-9 | LOCAL |
| silicon | `kalman2d_predict.cov_predict` — Verilog + Verilator bit-exact | TOOLCHAIN (Verilator) |

**Proved, simulated, on silicon.** The covariance stays PSD (proven); the filter cuts noise to RMS 0.52 (from 0.93) and recovers the unmeasured velocity (0.52) while matching NumPy to 1e-16; and cov_predict runs bit-exact on RTL.