Repository navigation
n in ZZ and 2^n > n^2 is solved to a set, and a power's residues repeat with the base's order - #1449
Merged
Merged
Conversation
…ails proved by induction
An inequality with an exponential or a factorial over the whole numbers, conjoined with the
membership, is searched over a window from the least member; the members are the points where it
holds, and the whole numbers from the start of the final run -- and over ZZ down from the end of the
first -- where the quantifier proves the statement there by induction. A tail it does not prove
leaves the inequality solver's refusal in place: a window is evidence about the window. Sullivan
and Mackey's Ex 5.3.2 is { 0, 1 } \/ ZZ /\ [5; +oo). The inequality induction reads the sign of
the whole expression off its shape before looking for a step, which is what proves a downward tail.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura
…e residues decide it forall n in ZZ+ : 3 divides 7^n - 4^n is one residue and forall n in ZZ* : not (7 divides 2^n + 1) three: a divisibility or a congruence in a polynomial of n and of powers a^e(n), a prime to the modulus and e a whole polynomial, has period lcm(m, ord_m(a), ...) in n over the non-negative whole numbers. A base sharing a factor with the modulus repeats only eventually, and over ZZ a power is fractional at a negative exponent; both are left as written. Sullivan and Mackey's §5.2.4 Try 3 and Ex 5.3.7. Co-Authored-By: Claude Opus 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.
Two more of Sullivan and Mackey's chapter-5 decisions, on top of #1446's induction.
Threshold sets.
"n in ZZ and 2^n > n^2".ToEntity().Solve("n")is{ 0, 1 } \/ ZZ /\ [5; +oo)(Ex 5.3.2): an inequality with an exponential or a factorial over the whole numbers, conjoined with the membership, is searched over a window from the least member, the members listed, and the tails proved by the quantifier's induction — upwards from the start of the final run and, overZZ, downwards from the end of the first. A tail the induction does not prove leaves the inequality solver's refusal in place: a window is evidence about the window (n in ZZ and 2^n >= n^2 - 3 n + 3is true from1and stays refused, since its step is not a multiple of the hypothesis plus something of known sign). The inequality induction reads the sign of the whole expression off its shape before looking for a step, which is what proves a downward tail (3^(-t - 1) + t^3 > 0onZZ*, term by term).n in ZZ and 2^n > n^2NotSufficientlySupportedException{ 0, 1 } \/ ZZ /\ [5; +oo)n in ZZ and n^3 < 3^(n - 1)(§5.3.4 Try 4)ZZ /\ (-oo; 0] \/ ZZ /\ [6; +oo)n in ZZ+ and 3^n > n^4,4^n > n^4(Prob 5.7.2){ 1 } \/ ZZ+ /\ [8; +oo),{ 1 } \/ ZZ+ /\ [5; +oo)n in ZZ+ and n! > 2^n,> 3^n,> 5^n(Prob 5.7.8–9)ZZ+ /\ [4; +oo),[7; +oo),[12; +oo)n in ZZ* and 2^n >= n + 1ZZ*Residues of a power.
forall n in ZZ+ : 3 divides 7^n - 4^nisTrueby one residue andforall n in ZZ* : not (7 divides 2^n + 1)by three (§5.2.4 Try 3, Ex 5.3.7): a divisibility or a congruence in a polynomial ofnand of powersa^e(n)withaprime to the modulus has periodlcm(m, ord_m(a), …)innover the non-negative whole numbers, so the residue route decides it. A base sharing a factor with the modulus repeats only eventually, and overZZa power is fractional at a negative exponent; both stay as written.Found on the way and filed as #1448:
2^(10^9)and2^(3^20)hang exact evaluation, which is what a witness search hits on Prob 5.7.13's3^(n + 1) divides 2^(3^n) + 1.ThresholdSetTest(15 rows, compared by membership at 41 points), nine rows inResidueClassTest;Syntax.mdandBREAKING-CHANGES.md. Full suite 12368 passed; the allocation gate passes on all 19 gated benchmarks on both commits.Part of #1409.
🤖 Generated with Claude Code
https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura