3 filters — linear Kalman, matrix EKF, quaternion AHRS — each proven (Lean, sorryAx-free), simulated as a working filter on the real Forge-emitted kernels, and run on silicon (Verilog/Verilator bit-exact). One math source per kernel; no numpy in any estimator.
A textbook predict→update Kalman filter — cuts position noise and recovers the unmeasured velocity from position measurements alone.
32 compiled targets
kalman2d_cov_predict_psd ✓ clean — the predicted covariance F·P·Fᵀ+Q stays positive-semidefinite axiom trailkalman2d_joseph_psd ✓ clean — the Joseph covariance update preserves PSD for any gain axiom trail| quantity | result | |
|---|---|---|
| filter RMS vs measurement RMS | 0.525 / 0.934 ratio 0.56 < 0.6 | ✓ |
| recovered velocity (never measured) | 0.516 ≈ 0.5 | ✓ |
| max |filter − NumPy-KF| | 1.1e-16 < 1e-9 | ✓ |
kalman2d_predict.cov_predict — Verilog/Verilator bit-exact
A nonlinear Extended Kalman Filter — range-only trilateration to two beacons; the gain K = P·Hᵀ·(H·P·Hᵀ+R)⁻¹ exercises the matrix-inverse operator.
100 compiled targets
ekf_range_nonneg ✓ clean — the range measurement √((lx-x)²+(ly-y)²) is ≥ 0 axiom trailkalman2d_innovation_cov_psd ✓ clean — the innovation covariance H·P·Hᵀ+R stays positive-semidefinite axiom trailkalman2d_matrix_joseph_psd ✓ clean — the Joseph covariance update A·P·Aᵀ+W preserves PSD for any gain axiom trail| quantity | result | |
|---|---|---|
| EKF position RMSE vs dead-reckoning | 0.479 / 2.993 ratio 0.16 < 0.6 | ✓ |
| max |EKF − NumPy-EKF| | 4.2e-15 < 1e-9 | ✓ |
complementary_filter.fuse, weighted_fusion.fuse3, kalman2d_update_matrix.update_cov — Verilog/Verilator bit-exact
A complementary attitude filter fusing a biased gyroscope with an accelerometer; every quaternion op is a shipped kernel and the state is re-normalised onto the unit sphere each step.
18 compiled targets
quat_normalize_unit ✓ clean — ‖normalize(q)‖² = 1 — the state stays a unit quaternion (sorryAx-free) axiom trail| quantity | result | |
|---|---|---|
| Mahony attitude error vs gyro-only | 2.38° / 18.44° ratio 0.13 < 0.3 | ✓ |
| max |‖q‖ − 1| over the run | 2.2e-16 < 1e-12 | ✓ |
quat_mul, quat_rotate_vec — Verilog/Verilator bit-exact