feat(math): machine-checked approximation bound for the f32 sin kernel (MATHF32-P04)

[avrabe]

What

Proves the approximation layer of the f32 sine kernel — the minimax remainder |P(r) − sin r| — the "not yet proven" half from the One ulp of doubt story. Complements the P03 Gappa rounding bound (|Msin − Esin| ≤ 2⁻²⁴, shipped v1.127).

proofs/rocq/sin_approx.v, kernel-checked by coqc via Coq-Interval:

|P(r) − sin r| ≤ 1e-8   for all r ∈ [-0.8, 0.8]

Unblocked by rules_rocq_rust#43 (merged today), which wired the coq_9_0.withPackages(flocq interval coquelicot) env resolving Interval's full transitive closure (mathcomp-boot/fingroup, hierarchy-builder, coq-elpi). Empirically confirmed the interval tactic runs end-to-end — the smoke test //examples/interval_proof:smoke_test and this proof both pass, not just "the package fetches."

Why it's honest

• Coefficients byte-identical to the Gappa proof (S1 = -0x1.5555460p-3, S2 = 0x1.11073c0p-7, S3 = -0x1.9943f20p-13) → P equals Gappa's exact-arithmetic Esin. This is the correctness gate for composition: the rounding and approximation bounds chain by triangle inequality only because they reference the same real function. With different coefficients they don't compose.
• Non-vacuous (teeth): interval proves 1e-8 at i_degree 15 but fails to prove 8e-9 even at i_degree 18 (5e-9 fails at i_degree 22). The pass isn't achievable at an arbitrary bound — mirrors P03's "coqc rejects 2⁻²⁵".
• Range = the actual clamp. reduce() clamps to [-0.8, 0.8]; the kernel's doc comment says π/4 ≈ 0.785. We prove the wider clamp range (and note the comment/clamp mismatch in the file header).
• Sanity: approximation error 1e-8 ≪ the exhaustive total 1.19e-7 (MATHF32-P02) — as expected, since the total is dominated by f32 rounding, not the minimax polynomial.

Scope (two-commit rule)

Status set to implemented, not verified — promotion is the separate code-free verify PR. Scope narrowed honestly: this delivers the approximation ingredient. The reduced-range composition into one |computed − sin r| ≤ 1e-8 + 2⁻²⁴ lemma (integrating the Gappa-emitted term with the Interval term) is deferred to the P06 composition step; the P04 artifact no longer claims the composition is done.

Changes

• proofs/rocq/sin_approx.v — the proof (new).
• proofs/rocq/BUILD.bazel — rocq_interval_proof + rocq_proof_test targets; auto-included in //proofs/rocq:all (the required rocq.yml gate).
• MODULE.bazel — use_repo rocq_interval_env (the rocq_interval_proof rule defaults to @rocq_interval_env//:coqc).
• artifacts/swreq/SWREQ-FALCON-MATHF32-P04.yaml — proposed → implemented, scope narrowed to the approximation bound.

Gate builds against rules_rocq_rust main (rocq.yml checks it out unpinned), which has #43. bazel test //proofs/rocq:sin_approx_test PASSED locally in relay's own bazel.

🤖 Generated with Claude Code