# Reproduction — Mahony AHRS (quaternion attitude estimation)

A Mahony complementary filter fusing a biased gyroscope with an accelerometer, built entirely from eml-stdlib quaternion kernels. Regenerate with `make ahrs-demo`.

| stage | artifact | tier |
|---|---|---|
| emit | `attitude_quaternion.eml` → 18 targets | LOCAL |
| proof | `quat_normalize_unit` — ‖normalize(q)‖² = 1, the state stays a unit quaternion (`attitude_quaternion.eml`) | TOOLCHAIN — Lean (proven sorryAx-free in the test suite) |
| simulate | `out/ahrs/trace.csv` — Mahony error 2.38° < 0.3 × gyro-only 18.44° (ratio 0.13) | LOCAL |
| simulate | max \|‖q‖ − 1\| = 2.2e-16 over the run (state never leaves the unit sphere) | LOCAL |
| silicon | `quat_mul`, `quat_rotate_vec` — Verilog + Verilator bit-exact | TOOLCHAIN (Verilator) |

**The same attitude kernels, four ways.** quat_normalize is proven to keep the state a unit quaternion; the Mahony filter it anchors tracks orientation to 2.4° (13% of gyro-only drift) while ‖q‖ holds at 1 to 2e-16; and the composition / rotation kernels run bit-exact on RTL. Gravity prediction is quat_rotate_vec(quat_conjugate(q), g); integration is quat_mul; re-projection is quat_normalize — every quaternion op is Forge-emitted.