Repository navigation
Over the primes, a comparison settles past its root - #1590
Merged
Merged
Conversation
A comparison linear in p keeps one truth value past its root, so the primes below the last root are asked one by one; from there each comparison is the truth value it has, and what is left is decided by the modulus's prime factors and units as before. A comparison may stand anywhere in the statement, not only as a lower bound in the hypothesis: every prime is 2, or 1 or 3 modulo 4. Where a comparison with rational coefficients settles is found exactly. It was a decimal quotient, so it depended on the decimal precision: at 16 or 30 digits 2/3 rounds up, the root of 2/3 n - 2 came out below 3, and forall n in ZZ* : 2/3 n - 2 <= 0 was True, though it fails at 4. At the default 100 digits it was right. Part of #1409. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura
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.
forall p in PP : p = 1 (mod 4) or p = 3 (mod 4) or p = 2was left as written. Over the primes (#1579), a statement was decided only where it repeats modulo someMpast a lower bound set by a hypothesis, andp = 2does not repeat.A comparison linear in
pkeeps one truth value past its root. So the primes below the last root are now asked one by one, and from the last root on each comparison is the truth value it has there. What is left is decided by the prime factors and units of its modulus, as before. A comparison may stand anywhere in the statement, not only as a lower bound in a hypothesis:forall p in PP : p = 1 (mod 4) or p = 3 (mod 4) or p = 2isTrue, and withoutor p = 2it isFalse, at2.forall p in PP : p = 2 or p = 3 or 6 divides p^2 - 1isTrue.forall p in PP : p < 10 implies p = 2 or 2 divides p + 1isTrue, an upper bound.exists p in PP : p < 3 and p = 2 (mod 3)isTrue.Where a comparison settles is found exactly when its coefficients are rational. It was a decimal quotient, so a truth value depended on
MathS.Settings.DecimalPrecisionContext. At 16 or 30 digits,2/3rounds up, the root of2/3 n - 2came out below3, andforall n in ZZ* : 2/3 n - 2 <= 0wasTrue, though it fails at4. The same happened to5/9 n - 5at10. At the default 100 digits the answer was right.WhereAComparisonSettlesDoesNotDependOnThePrecisionfails on master at 16 and 30 digits, and passes here at all three. The route came in with #1580 and has not been released.Suite: 13,684 passed, 0 failed on net10.0, and every target framework builds. Gate: passed, with allocation as the baseline says on all 19 gated benchmarks.
BREAKING-CHANGES.md: the entry for the primes has a sentence and a row.Part of #1409.
🤖 Generated with Claude Code
https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura