# Reproduction — EKF localization (range-only, two beacons)

A nonlinear Extended Kalman Filter built entirely from eml-stdlib estimation kernels. A robot under noisy, biased odometry measures its range to two fixed beacons (a nonlinear observation) and localizes. Regenerate with `make ekf-demo`.

| stage | artifact | tier |
|---|---|---|
| emit | `ekf_range_bearing.eml` → 22 targets | LOCAL |
| emit | `kalman2d_update_matrix.eml` → 16 targets | LOCAL |
| emit | `complementary_filter.eml` → 31 targets | LOCAL |
| emit | `weighted_fusion.eml` → 31 targets | LOCAL |
| proof | `ekf_range_nonneg` — the range measurement √((lx-x)²+(ly-y)²) is ≥ 0 (`ekf_range_bearing.eml`) | TOOLCHAIN — Lean (proven sorryAx-free in the test suite) |
| proof | `kalman2d_innovation_cov_psd` — the innovation covariance H·P·Hᵀ+R stays positive-semidefinite (`kalman2d_update_matrix.eml`) | TOOLCHAIN — Lean (proven sorryAx-free in the test suite) |
| proof | `kalman2d_matrix_joseph_psd` — the Joseph covariance update A·P·Aᵀ+W preserves PSD for any gain (`kalman2d_update_matrix.eml`) | TOOLCHAIN — Lean (proven sorryAx-free in the test suite) |
| simulate | `out/ekf/trace.csv` — EKF RMSE 0.479 < 0.6 × dead-reckoning 2.993 (ratio 0.16) | LOCAL |
| simulate | max \|EKF − NumPy-EKF\| = 4.2e-15 < 1e-9 (bit-for-bit the textbook EKF) | LOCAL |
| silicon | `complementary_filter.fuse` — Verilog + Verilator bit-exact | TOOLCHAIN (Verilator) |
| silicon | `weighted_fusion.fuse3` — Verilog + Verilator bit-exact | TOOLCHAIN (Verilator) |
| silicon | `kalman2d_update_matrix.update_cov` — Verilog + Verilator bit-exact | TOOLCHAIN (Verilator) |

**The same estimation library, four ways.** Its contract theorems close sorryAx-free (range ≥ 0, covariance PSD); the filter it builds localizes (RMSE 0.479, 16% of dead-reckoning) and is bit-for-bit the NumPy EKF (4e-15); and its pure-MAC kernels run bit-exact on RTL. The gain K = P·Hᵀ·(H·P·Hᵀ+R)⁻¹ exercises the matrix-inverse operator; every estimator kernel in the loop is Forge-emitted.