blog: "Closing the other half" — the sequel to One ulp of doubt - #138
Open
avrabe wants to merge 2 commits into
Open
blog: "Closing the other half" — the sequel to One ulp of doubt#138avrabe wants to merge 2 commits into
avrabe wants to merge 2 commits into
Conversation
The previous post ended by publishing what we had NOT proven: the approximation layer of the f32 sine kernel. This closes that debt, and the closing was more interesting than the result. Three beats, all grounded in what actually happened: - The tool didn't work. Coq-Interval was "in the build" but its dependency closure was never wired, so `Require Import Interval.Tactic` failed. Fixed, plus the lesson: the test must USE the tactic, not just fetch the package. - The compiler said no. A neighbouring team's per-stage lowering run found a 64-bit-to-float conversion blocking three stages, with a suggested source-level workaround. Diagnosis was exact; the workaround failed four different ways, verified by disassembling the output each time. We reported the negative result the same day rather than claim an unblock we hadn't achieved. - The cosine is 10x more accurate than the sine (1e-9 vs 1e-8) — because its kernel carries the exact `1 - 0.5z` terms and only fits the residual. Keeps the honest boundary the first post established: four bounds now proven, but the COMPOSITION of the two halves and the argument-reduction cancellation are still open, and the post says so plainly. Scheduled (draft + ready) for 2026-07-30. Site builds clean; the cross-link to /blog/one-ulp-of-doubt/ resolves (verified live, HTTP 200). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG
…e in-flight claim Publish immediately rather than schedule: date -> 2026-07-29, draft -> false, ready stays true (file renamed to match). Because it now goes live TODAY, one claim had to be made exactly true as of today: the cosine APPROXIMATION bound is proven and CI-green but its PR (relay#320) has not merged yet, so the four-bounds table would have overstated by one cell. Footnoted as "landing, not landed" rather than rounded up — which is the same discipline the post itself is about. The cosine ROUNDING bound is on main and needs no qualifier. zola build (no --drafts): 38 pages, 0 orphans, renders as published and appears on the blog index. 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.
Follow-up to One ulp of doubt, which ended by publishing what we had not proven — the approximation layer of the
f32sine kernel. That debt is now paid, and the paying was the story.What it covers
Require Import Interval.Tacticfailed. Fixed, with the transferable lesson: the test has to use the tactic, not just check the package downloaded.|P(r) − sin r| ≤ 1e-8, kernel-checked; coefficients copied verbatim from the Gappa proof (the reason the two halves compose at all); the bound fails at8e-9, so it isn't vacuous.f32.convert_i64_ublocking three stages and suggested a source-level narrowing. The diagnosis was exact — but the workaround failed four different ways, verified by disassembling the built component each time. We reported the negative result the same day instead of claiming an unblock we hadn't achieved.1e-9vs1e-8) — becausecos_polycarries the exact1 − 0.5·zterms and only fits the residual. A real result made visible by both numbers coming from the same machine-checked process.Honest boundary maintained
Four bounds now proven (sine/cosine × rounding/approximation), but the post is explicit that two proven halves are not a composition — the triangle-inequality lemma and the argument-reduction cancellation are still open. That distinction is the easiest thing to blur and the most flattering to blur, so it gets its own callout.
Checks
zola build --drafts: 40 pages, 0 orphans, clean./blog/one-ulp-of-doubt/verified live (HTTP 200) and resolves in the build.draft = true+ready = true+date = 2026-07-30→ auto-publishes on the date.🤖 Generated with Claude Code