feat(math): machine-checked rounding bound for the f32 cosine kernel (MATHF32-P05 rounding half) - #304
Merged
Merged
Conversation
…(MATHF32-P05, rounding half)
The cosine analogue of the shipped sin proof (MATHF32-P03): the f32 Horner
evaluation of cos_poly is faithful to within 2^-23 of the exact real value
of the same polynomial over the reduced range r ∈ [-0.8, 0.8]. Gappa
(gappa -Bcoq) emits a Flocq/Rocq term; coqc KERNEL-CHECKS it — never
trusting Gappa's own success (rules_rocq_rust gappa_proof, rivet CC-002).
2^-23 (not 2^-24 like sin): cos_poly carries the extra `1 - 0.5*z`
subtraction, which contributes an additional rounding step. Verified
green + NON-VACUOUS in a clean run — an impossible bound (2^-28) fails to
build ("some properties were not satisfied"), so the pass has teeth.
Auto-enforced by the required rocq.yml gate (//proofs/gappa:all).
Drafted in parallel by a subagent and INDEPENDENTLY re-verified here (its
own claim of the bound was not taken on trust — I re-ran the kernel-check
and the negative test myself).
This is the ROUNDING half of MATHF32-P05. The APPROXIMATION half
(|Q(r)-cos r|, Coq-Interval) is BLOCKED on a toolchain gap: Coq-Interval
won't load without mathcomp (rules_rocq_rust#43). P05 stays proposed
until that half lands.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The cosine analogue of the shipped sin rounding proof (MATHF32-P03) — the second machine-checked FP-kernel proof, landed this session.
What lands
proofs/gappa/cos_poly_rounding.gappa: the f32 Horner evaluation ofcos_polyis within 2⁻²³ of the exact real value of the same polynomial over r ∈ [−0.8, 0.8]. Gappa → Flocq → coqc kernel-check (Gappa's own success never trusted).cos_polycarries the extra1 − 0.5·zsubtraction — one more rounding step.2⁻²⁸fails to build ("some properties were not satisfied");2⁻²³builds green. Teeth confirmed.rocq.ymlgate (//proofs/gappa:all).Provenance
Drafted in parallel by a Fable subagent, then independently re-verified here — I re-ran the kernel-check and the negative test myself rather than trust the agent's reported bound (the first ambiguous "cached PASSED" was rejected; the marginal 2⁻²⁴ was set aside for a clean 2⁻²⁸ refutation).
Honest scope
This is the rounding half of MATHF32-P05. The approximation half (
|Q(r) − cos r|, Coq-Interval) is blocked on a toolchain gap — Coq-Interval won't load without mathcomp, filed as rules_rocq_rust#43. P05 staysproposeduntil that half lands; nothing over-claimed.🤖 Generated with Claude Code
https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG