plan(math): schedule the remaining machine-checked FP-kernel proof layers (v1.128–v1.130)

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

@@ -0,0 +1,36 @@
+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
+    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.
+    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).
+    links:
+      - type: derives-from
+        target: SYSREQ-FALCON-002
+      - type: refines
+        target: SWREQ-FALCON-MATHF32-P03

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

@@ -0,0 +1,27 @@
+artifacts:
+  - id: SWREQ-FALCON-MATHF32-P05
+    type: sw-req
+    title: "MATHF32-P05 — machine-checked reduced-range bound for the COSINE kernel (rounding + approximation)"
+    status: proposed
+    release: falcon-v1.129.0
+    description: >
+      Extend the sine-kernel proof method (MATHF32-P03 rounding + MATHF32-P04
+      approximation, composed) to the f32 COSINE polynomial (cos_poly): a
+      Gappa rounding bound on the Horner evaluation plus a Coq-Interval bound
+      on |Q(r) - cos r|, composed to a kernel-checked reduced-range accuracy
+      bound for cosf. A small extension once the sine machinery exists — the
+      same two tools, the same composition, different coefficients and
+      reference function.
+    tags: [falcon, relay-math, f32, gappa, coq-interval, machine-checked, v1.129]
+    fields:
+      req-type: non-functional
+      priority: should
+      verification-criteria: >
+        Gappa rounding proof + Coq-Interval approximation proof for cos_poly,
+        both coqc-kernel-checked and teeth-tested, composed to a reduced-range
+        |computed - cos r| bound; enforced under the rocq.yml gate.
+    links:
+      - type: derives-from
+        target: SYSREQ-FALCON-002
+      - type: refines
+        target: SWREQ-FALCON-MATHF32-P04

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

@@ -0,0 +1,34 @@
+artifacts:
+  - id: SWREQ-FALCON-MATHF32-P06
+    type: sw-req
+    title: "MATHF32-P06 — machine-checked Cody-Waite argument-reduction bound → FULL-range sin/cos accuracy"
+    status: proposed
+    release: falcon-v1.130.0
+    description: >
+      The remaining and HARDEST ingredient: a machine-checked bound on the
+      Cody-Waite argument reduction r = ((x - n*PIO2_HI) - n*PIO2_MID) -
+      n*PIO2_LO — that the reduced r is accurate (the three-part-subtraction
+      cancellation error stays bounded) for all quadrant counts |n| in the
+      qualified envelope |x| <= 128. A Gappa proof (rounding + the exactness
+      of n*PIO2_HI for bounded n). Composing this with the reduced-range
+      kernel bounds (P04 sine, P05 cosine) yields a kernel-checked accuracy
+      bound over the FULL input range, not just the reduced range — the
+      complete crlibm/CORE-MATH-style argument. Explicitly scoped as a LARGE
+      slice (the reduction cancellation is the part those references spend
+      most of their pages on — weeks, not days) and deliberately sequenced
+      AFTER P04/P05 so the reduced-range proof lands first.
+    tags: [falcon, relay-math, f32, gappa, argument-reduction, machine-checked, qualification, v1.130]
+    fields:
+      req-type: non-functional
+      priority: could
+      verification-criteria: >
+        A Gappa proof of the reduction error bound over |x| <= 128 (all |n|),
+        coqc-kernel-checked and teeth-tested; a composed Rocq lemma giving a
+        full-range |computed - sin/cos x| bound from P06 + P04/P05; enforced
+        under the rocq.yml gate. The exhaustive empirical bound (MATHF32-P02)
+        remains the cross-check the full-range proof must be consistent with.
+    links:
+      - type: derives-from
+        target: SYSREQ-FALCON-002
+      - type: refines
+        target: SWREQ-FALCON-MATHF32-P04