plan(math): schedule the remaining machine-checked FP-kernel proof layers (v1.128–v1.130) - #302
Merged
Merged
Conversation
…yers The blog's honest "not yet proven" list, turned into tracked rivet requirements driven from the release plan rather than living only in prose: - MATHF32-P04 (v1.128): APPROXIMATION bound |P(r)-sin r| via Coq-Interval (now wired), COMPOSED with the P03 rounding bound → machine-checked reduced-range sine accuracy. Tractable — the tooling is ready. - MATHF32-P05 (v1.129): the same rounding+approximation method extended to cos_poly → reduced-range cosine accuracy. Small extension after P04. - MATHF32-P06 (v1.130): the HARD one — Cody-Waite argument-reduction cancellation (Gappa), composed with P04/P05 → FULL-range accuracy. Scoped as a large slice (weeks), sequenced last. All `proposed`; refine MATHF32-P03. Release fields are the plan (moved deliberately, not silently). Umbrella tracker mirrors to a GitHub issue. 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.
Turns the blog's honest "not yet proven" list into tracked rivet requirements driven from the release plan. Code-free — three
proposedsw-reqs refining MATHF32-P03.|P(r)−sin r| ≤ ε, composed with the P03 rounding bound → machine-checked reduced-range sine accuracycos_poly→ reduced-range cosineThe composition is the point: P03 already proves
\|computed − P(r)\| ≤ 2⁻²⁴; P04 adds\|P(r) − sin r\| ≤ ε; triangle-inequality gives a kernel-checked\|computed − sin r\|for the reduced range — turning "rounding proven" into "reduced-range kernel proven." P06 then extends it to the full input range.Release fields are the plan (moved deliberately, not silently). Umbrella tracker: the linked issue.
🤖 Generated with Claude Code
https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG