Machine-checked FP kernel proof — remaining layers (approximation + argument reduction)

[avrabe]

Umbrella tracker for completing the machine-checked floating-point proof of the relay-math f32 sin/cos kernels. The rounding layer is done and gated (MATHF32-P03, falcon-v1.127.0: Gappa→Flocq→coqc, |computed − P(r)| ≤ 2⁻²⁴, non-vacuous). What remains, planned in rivet:

• MATHF32-P04 (falcon-v1.128.0) — approximation layer, sine. Coq-Interval (wired via rules_rocq_rust#41) proof of |P(r) − sin r| ≤ ε over the reduced range, composed with P03's rounding bound → machine-checked reduced-range accuracy of sinf. Tractable — the next slice.
• MATHF32-P05 (falcon-v1.129.0) — same treatment for cos_poly → reduced-range cosf. Small extension after P04.
• MATHF32-P06 (falcon-v1.130.0) — argument-reduction cancellation (Gappa) over |x| ≤ 128, composed with P04/P05 → full-range accuracy. The hard one (weeks; the crlibm/CORE-MATH-heavy part); sequenced last so the reduced-range proof lands first.

Each lands the same way as P03: kernel-checked, negative-tested (teeth), enforced under the required rocq.yml gate, cross-checked against the exhaustive empirical bound (MATHF32-P02). Source of truth is rivet (SWREQ-FALCON-MATHF32-P04/P05/P06); this issue is the human-facing view.

🤖 Generated with Claude Code

https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG