feat(interval): replay endpoint sine chronology - #9259
Merged
Conversation
kim-em
force-pushed
the
agent/interval-sin-ten-machin
branch
from
August 14, 2026 15:53
48efad6 to
865f951
Compare
kim-em
force-pushed
the
agent/interval-sin-ten-endpoint
branch
from
August 14, 2026 15:53
bd12c35 to
79ccd99
Compare
kim-em
force-pushed
the
agent/interval-sin-ten-machin
branch
from
August 14, 2026 16:20
865f951 to
d5759a5
Compare
kim-em
force-pushed
the
agent/interval-sin-ten-endpoint
branch
from
August 14, 2026 16:20
79ccd99 to
645d996
Compare
kim-em
force-pushed
the
agent/interval-sin-ten-machin
branch
from
August 14, 2026 16:42
d5759a5 to
48b7704
Compare
kim-em
force-pushed
the
agent/interval-sin-ten-endpoint
branch
from
August 14, 2026 16:42
645d996 to
13cb50c
Compare
Progress: progress/20260814T161000Z.md
kim-em
force-pushed
the
agent/interval-sin-ten-endpoint
branch
from
August 14, 2026 17:09
13cb50c to
fd7b65c
Compare
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
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.
Summary
sin 10canary with exact rational boundsProofFrontendto prove-1 ≤ Real.sin 10 ∧ Real.sin 10 < 03, and has an exact-fit resource envelopeValidation
lake build HexInterval.SinTenIntervalConformance HexIntervalMathlib.SinTenIntervalConformance(2230 jobs)lake build HexIntervalMathlib.SinTenConformance(2215 jobs)git diff --checkStacked on #9258.