feat(falcon): v1.122 — RPM-tracked harmonic notches + pre-arm check table (NOTCH-P01 + PREARM-P03)

[avrabe]

Verify-Filter: (has-tag "v1.122")

Implements NOTCH-P01 + PREARM-P03 (→ implemented; verify PR follows per the two-commit rule) — the final rung of the v1.117–v1.122 infra ladder.

NOTCH-P01 — relay-notch

The PX4 IMU_GYRO_DNF / ArduPilot INS_HNTCH / Betaflight RPM-filter role: per-motor biquad notches (fundamental + 2nd harmonic) tracking achieved eRPM through the same read_motor_rpm seam the rotor-out FDI consumes (jess DD-024: bidir-DShot primary, DroneCAN alternate).

• Safety posture: absent RPM ⇒ bit-exact unity bypass (Kani-proven — no filtering is safer than a mistracked notch); per-notch Nyquist clamp (at the 250 Hz loop the 2nd harmonic self-limits; proven never to engage outside the band).
• Measured criteria: ≥ 20 dB at the tracked fundamental across hover-to-full, stepped sweep within 3 dB, < 10° added phase at the rate-loop crossover with the full 4-motor bank engaged — DFT-measured, not asserted from arithmetic.
• Kani drove two real fixes: proptest/CBMC found +∞ riding through a fully-Nyquist-clamped bank (fixed: bank-boundary sanitize); the NaN side-conditions forced operand sanitization so a poisoned state can't even compute a NaN; and symbolic trig hit libm's rem_pio2_large (>1500-iteration unwinding) — solved with the trig-free band_ok split, unit-pinned to set's engagement.
• Closed loop: SimBackend gained rotor-line vibration (narrowband at each motor's rotation frequency — broadband can't exercise a notch) + an rpm_telemetry switch; the tracking notch cuts hover motor thrash to < 60% of the bypass baseline (gz plant hovers with an attitude limit-cycle (~1 rad/s roll/pitch, motor thrash 0.1↔1.0) #270's regression-metric shape; the full limit-cycle root-cause stays open in gz plant hovers with an attitude limit-cycle (~1 rad/s roll/pitch, motor thrash 0.1↔1.0) #270).

PREARM-P03 — the check table

"Most crashes are prevented on the ground", as data: 19 rows (estimator/nav integrity incl. the GNSS-P02 divergence flag, config consistency incl. params-from-NVM and geofence sanity, hardware consistency incl. ESC-telemetry-alive and battery takeoff margin, safety state), each with a distinct operator STATUSTEXT reason.

• Legacy six = rows 0..=5, always required; breadth rows gate once declared (a bench without RC isn't blocked by a link check it can't satisfy; a declared row that fails always blocks).
• Kani PREFLIGHT-K03/K04: gate exactness + monotonicity (failing any row of an Allowed table can never remain Allowed).
• Per-row pair tests are table-driven — coverage equals table length by construction; reason-text distinctness asserted.
• Cold-boot criterion on the real seam: a defaults-fallback parameter load (blank NVM through PARAM-P03's two-slot image) cannot arm, with its distinct reason; after a save + genuine reload it arms.

Gates

cargo test: relay-notch 8 + relay-preflight 6 + falcon-core 56, 0 fail · cargo kani: notch 3/3, preflight 4/4 (incl. the two new) · clippy -D warnings clean · rivet validate PASS · relay-notch enrolled in kani.yml + CI clippy at birth.

🤖 Generated with Claude Code

https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG