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

MODULE.bazel

@@ -85,6 +85,13 @@ use_repo(
     "rocq_gappalib",
     "rocq_interval",
     "rocq_coquelicot",
+    # Coq-Interval approximation-bound env (rules_rocq_rust#43, DD-003): a
+    # coq_9_0.withPackages(...) composition resolving Interval's full closure
+    # (mathcomp-boot/fingroup, hierarchy-builder, coq-elpi). The
+    # rocq_interval_proof rule defaults to @rocq_interval_env//:coqc — without
+    # this use_repo, proofs/rocq/sin_approx.v (MATHF32-P04) can't resolve
+    # `Require Import Interval.Tactic`.
+    "rocq_interval_env",
 )
 register_toolchains("@rocq_toolchains//:all")
 

artifacts/swreq/SWREQ-FALCON-MATHF32-P04.yaml

@@ -1,34 +1,51 @@
 artifacts:
   - id: SWREQ-FALCON-MATHF32-P04
     type: sw-req
-    title: "MATHF32-P04 — machine-checked APPROXIMATION bound for the sin polynomial (Coq-Interval) + reduced-range composition"
-    status: proposed
+    title: "MATHF32-P04 — machine-checked APPROXIMATION bound for the f32 sin polynomial (Coq-Interval)"
+    status: implemented
     release: falcon-v1.128.0
     description: >
-      Establish the second (approximation) half of the sine-kernel proof and
-      COMPOSE it with the rounding half (MATHF32-P03) to give a machine-checked
-      bound on the reduced-range accuracy of the f32 sine kernel. Two parts:
-      (a) using Coq-Interval (now wired via rules_rocq_rust #41), prove the
-      minimax remainder |P(r) - sin r| <= eps over the reduced range r in
-      [-0.8, 0.8] (containing [-pi/4, pi/4]), where P is the exact real value
-      of the kernel's f32-coefficient polynomial; (b) compose it with the
-      P03 Gappa rounding bound |computed - P(r)| <= 2^-24 via the triangle
-      inequality to obtain a kernel-checked |computed - sin r| <= (eps +
-      2^-24) for the REDUCED range. This turns "rounding proven" into
-      "reduced-range sine kernel proven." It does NOT cover the full input
-      range — the Cody-Waite argument-reduction cancellation (MATHF32-P06) is
-      the remaining ingredient for that.
+      Establish the second (approximation) half of the sine-kernel proof: the
+      minimax remainder between the kernel polynomial and true sine. Using
+      Coq-Interval (wired via rules_rocq_rust #41/#43 — the withPackages env
+      that resolves Interval's full closure, DD-003), prove
+      |P(r) - sin r| <= 1e-8 over the reduced range r in [-0.8, 0.8] (the
+      interval the Cody-Waite reduction clamps to, containing [-pi/4, pi/4]),
+      where P is the EXACT real value of the kernel's f32-coefficient
+      polynomial. The coefficients are byte-identical to those in the P03
+      Gappa proof (S1 = -0x1.5555460p-3, S2 = 0x1.11073c0p-7,
+      S3 = -0x1.9943f20p-13), so P equals Gappa's exact-arithmetic polynomial
+      Esin — the two layers reference the SAME real function. This is the
+      OTHER ingredient (with the P03 rounding bound) behind the exhaustive
+      1.19e-7 (~2^-23) absolute-error bound (MATHF32-P02), now proven by
+      construction rather than by enumeration.
+
+      SCOPE (deliberately narrowed from the original P04 draft): this
+      requirement delivers the approximation INGREDIENT only. The reduced-range
+      COMPOSITION — chaining this bound with the P03 rounding bound via the
+      triangle inequality to a single kernel-checked
+      |computed - sin r| <= 1e-8 + 2^-24 (~6.9e-8) — is valid precisely
+      because the coefficients are identical, but assembling it as one
+      coqc-checked Rocq lemma (integrating the Gappa-emitted term with the
+      Interval term) is deferred to the P06 composition step, where the
+      reduced-range pieces are combined with the argument-reduction bound for
+      FULL-range accuracy. This artifact does not claim the composition is done.
     tags: [falcon, relay-math, f32, coq-interval, flocq, machine-checked, qualification, v1.128]
     fields:
       req-type: non-functional
       priority: should
       verification-criteria: >
-        A Coq-Interval proof of |P(r) - sin r| <= eps over [-0.8, 0.8],
-        kernel-checked by coqc, with a NON-VACUOUS (teeth-tested) eps — coqc
-        rejects a bound tighter than achievable. A composed Rocq lemma
-        deriving |computed - sin r| <= eps + 2^-24 from P04 and P03. Both run
-        under the required rocq.yml gate (bazel test //proofs/rocq:all
-        //proofs/gappa:all, extended to the interval proof).
+        proofs/rocq/sin_approx.v proves |P(r) - sin r| <= 1e-8 over
+        [-0.8, 0.8] via the Coq-Interval `interval` tactic (i_bisect, i_taylor,
+        i_degree 15), kernel-checked by the withPackages coqc
+        (rocq_interval_proof); the tactic's own success is never trusted
+        (CC-002). The bound has teeth — it is NON-VACUOUS: `interval` proves
+        1e-8 but FAILS to prove 8e-9 even at i_degree 18 (and 5e-9 at
+        i_degree 22), so the 1e-8 pass is not achievable at an arbitrary
+        bound. Runs as `bazel test //proofs/rocq:sin_approx_test`, included in
+        the required rocq.yml gate (//proofs/rocq:all). The composed
+        reduced-range lemma is NOT part of this requirement's evidence (see
+        scope note; tracked under P06).
     links:
       - type: derives-from
         target: SYSREQ-FALCON-002

proofs/rocq/BUILD.bazel

@@ -9,7 +9,7 @@
 # these are PURE ABSTRACT proofs — they use only Stdlib.ZArith and
 # do not depend on any translation infrastructure.
 
-load("@rules_rocq_rust//rocq:defs.bzl", "rocq_library", "rocq_proof_test")
+load("@rules_rocq_rust//rocq:defs.bzl", "rocq_interval_proof", "rocq_library", "rocq_proof_test")
 
 # ── Limit Checker proofs ────────────────────────────────────────────────
 
@@ -80,3 +80,21 @@ rocq_proof_test(
     srcs = ["cfdp_proofs.v"],
     deps = [":cfdp_proofs"],
 )
+
+# ── f32 sin approximation-error bound (MATHF32-P04, Coq-Interval) ─────────
+# The minimax-remainder half of the sin error: |P(r) - sin r| <= 1e-8 over
+# the reduced range, complementing the Gappa rounding bound in
+# proofs/gappa/sin_poly_rounding.gappa. Uses the withPackages Interval env
+# (rules_rocq_rust#43); the kernel-check is the point, the tactic is not
+# trusted (CC-002).
+
+rocq_interval_proof(
+    name = "sin_approx",
+    srcs = ["sin_approx.v"],
+)
+
+rocq_proof_test(
+    name = "sin_approx_test",
+    srcs = [],
+    deps = [":sin_approx"],
+)

proofs/rocq/sin_approx.v

@@ -0,0 +1,58 @@
+(* Machine-checked APPROXIMATION-error bound for relay-math's f32 sin kernel
+   (MATHF32-P04 — the Coq-Interval layer, rules_rocq_rust#41/#43).
+
+   CLAIM (approximation LAYER only): over the reduced range r in [-0.8, 0.8]
+   — the interval the Cody-Waite reduction clamps to; note sin_poly's doc
+   comment says |r| <= pi/4 (~0.785) but reduce() actually clamps to 0.8, so
+   we prove the wider CLAMP range, which contains [-pi/4, pi/4] — the exact
+   real value of the sin polynomial P(r) differs from the TRUE sine by at
+   most 1e-8:
+       |P(r) - sin r| <= 1e-8   for all r in [-0.8, 0.8].
+   This is the minimax remainder — the OTHER ingredient behind the exhaustive
+   1.19e-7 absolute-error bound (MATHF32-P02). The FIRST ingredient — that the
+   f32 Horner evaluation is faithful to this same polynomial (the rounding
+   remainder |Msin - Esin| <= 2^-24) — is proven separately by Gappa in
+   proofs/gappa/sin_poly_rounding.gappa (MATHF32-P03).
+
+   COMPOSITION (not asserted here): because both proofs use the IDENTICAL f32
+   coefficients (see below), Esin = P as real functions, so a triangle
+   inequality gives |Msin - sin r| <= 2^-24 + 1e-8 ~= 6.9e-8 over the reduced
+   range. Assembling that total (and carrying the reduction cancellation,
+   MATHF32-P06) is a further step; this file proves ONLY the approximation
+   remainder. Do not read it as closing the whole envelope error.
+
+   NON-VACUITY (teeth): the bound is tight and the tactic genuinely refutes a
+   tighter one. `interval` proves 1e-8 at i_degree 15; it FAILS to prove 8e-9
+   even at i_degree 18 (and 5e-9 fails at i_degree 22). A bound that passes at
+   any value would prove nothing — this one stops passing just below 1e-8.
+
+   Coefficients are the EXACT f32 dyadic values, copied verbatim from
+   proofs/gappa/sin_poly_rounding.gappa so the two layers compose:
+       S1 = -0x1.5555460p-3  = -357913696 / 2^31
+       S2 =  0x1.11073c0p-7  =  286290880 / 2^35
+       S3 = -0x1.9943f20p-13 = -429145888 / 2^41
+   Kernel source: crates/relay-math/src/lib.rs, sin_poly():
+       z = r*r;  r + r*z*(S1 + z*(S2 + z*S3))
+
+   `interval` emits a Flocq/Coq-Interval proof term; rocq_interval_proof
+   (rules_rocq_rust) kernel-checks it with the withPackages coqc — the tactic's
+   own success is never trusted (CC-002). *)
+
+Require Import Reals.
+Require Import Interval.Tactic.
+Local Open Scope R_scope.
+
+Definition S1 : R := -357913696 / 2147483648.
+Definition S2 : R :=  286290880 / 34359738368.
+Definition S3 : R := -429145888 / 2199023255552.
+
+Definition P (r : R) : R :=
+  let z := r * r in
+  r + r * z * (S1 + z * (S2 + z * S3)).
+
+Theorem sin_approx_bound :
+  forall r : R, -8/10 <= r <= 8/10 -> Rabs (P r - sin r) <= 1/100000000.
+Proof.
+  intros r Hr. unfold P, S1, S2, S3.
+  interval with (i_bisect r, i_taylor r, i_degree 15).
+Qed.