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

[avrabe]

[hygiene sweep — progress, with an honest correction to what "P04/P05 done" means]

Two of the three layers have shipped on tagged releases, but not in the exact shape this umbrella's checkboxes describe — so recording precisely rather than ticking them clean.

item	status	evidence
MATHF32-P03 rounding, sine	✅ done	falcon-v1.127.0
MATHF32-P04 approximation, sine	⚠️ ingredient shipped, composition NOT	falcon-v1.128.0 (#307 impl, #308 verify)
MATHF32-P05 cosine pair	⚠️ both ingredients shipped, composition NOT	falcon-v1.129.0 (#320 impl, #322 verify)
MATHF32-P06 argument reduction	❌ open	deferred v1.130 → v1.131 → v1.132

The correction: this umbrella's P04 line says "…composed with P03's rounding bound → machine-checked reduced-range accuracy of sinf". What actually shipped is the approximation bound alone:

|P(r) − sin r| ≤ 1e-8   over [-0.8, 0.8]   (Coq-Interval, coqc-checked)
|Q(r) − cos r| ≤ 1e-9   over [-0.8, 0.8]   (cosine, v1.129)

both non-vacuous (sine fails at 8e-9 @ i_degree 18; cosine fails at 1e-10 @ i_degree 20), both gated by rocq.yml, both using coefficients byte-identical to the Gappa proofs so the layers can compose by triangle inequality — but assembling that composition into one coqc-checked lemma was deliberately deferred, and the rivet artifacts say so explicitly. Two proven halves are not a composition.

Cosine also came out ~10× more accurate than sine (1e-9 vs 1e-8), because cos_poly carries the exact 1 − 0.5·z terms and only fits the residual.

remaining:

1. MATHF32-P06 — the Cody-Waite argument-reduction bound (the hardest of the four), now scoped to falcon-v1.132.0.
2. The reduced-range composition for both sine and cosine — folded into the P06 step, since that is where the reduced-range pieces meet the reduction bound for full-range accuracy.

Staying open on both counts. Not ticking the P04/P05 boxes, because their text promises the composition and the composition is not done.