Repository navigation
Re-read the second remarkable limit after simplification (#738) - #739
Merged
Merged
Conversation
`lim x->+oo (x - 5)^x / x^x` came back 1 where it is `e^(-5)`, and so did every quotient of two powers whose base ratio tends to 1. The rule that reads a `1^oo` runs once, at the top of `ComputeLimit`, against the expression as it was written. A quotient of powers is not a `1^oo` at that point -- it is a quotient -- so the rule had nothing to match on. The descent then reaches `SimplifyAndComputeLimitToInfinity`, whose first act is to simplify, and `(x - 5)^x / x^x` becomes `((x - 5)/x)^x`: a `1^oo` which nothing now re-reads, because the rule that reads one has already run. Straight on into the solvers, where `1^(+oo)` evaluates to 1. Neither the simplification nor the rule is wrong. What was wrong is that a form *created* by simplification was judged by rules that ran before it existed. So the same rule is asked again where the expression is in the form the solvers read it in, which is also where every destination has already been normalised to `+oo`. Guarded by a depth counter like the other rules here, since each level of it asks for limits of its own. This closes both of the routes the issue separates, because both of them run through that one point after the simplification has happened: the `SolveBySubstitution` route, where `(1 + 1/x)^x` substitutes to an exact `1^(+oo)`, and the `Powf` descent route, where `((x - 5)/x)^x` builds `1^x` and that simplifies to 1. It also turns out not to need PR #736 underneath it, which the earlier tracing had expected: the rewrite answers these outright rather than dropping them through to Gruntz. Measured, at x -> +oo: (x - 5)^x / x^x 1 -> 1/e^5 (309 ms) (x + 1)^x / x^x 1 -> e (16 ms) (x + 3)^x / x^x 1 -> e^3 (21 ms) x^x / (x + 1)^x 1 -> 1/e (57 ms) x^x / (x - 5)^x 1 -> e^5 (50 ms) (2x + 1)^x / (2x)^x 1 -> sqrt(e) (59 ms) (x - 1)^x / x^x unevaluated in 5.2 s -> 1/e in 163 ms and the neighbouring quotients, where the base ratio does not tend to 1, are untouched: `(2x)^x / x^x` and `(x^2)^x / x^x` are still `+oo`, `x^x / (2x)^x` still 0. What this does not reach: `(x^2 + 1)^x / (x^2)^x`, which `Simplify` leaves written as a quotient, so no `1^oo` is created for anything to re-read. That one is left unevaluated rather than answered wrongly, and its cause is in the simplification rather than in the limits -- the same quotient written `((x^2 + 1) / x^2)^x` is answered 1 without any of this. Filed separately. The other half of #738 -- that `1^(+oo)` evaluates to 1 at all -- reaches everything that evaluates a power rather than only limits, and wants its own measurement rather than being bundled in here. Left open. Full suite 4909 passed / 0 failed (4889 + 20 new), F# 130/130, corpus 112/117 with 0 wrong, 0 error, 0 timeout, and the suite still runs in 3 m 30 s. Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
The cases already here all approach +oo, which is the one destination that arrives at SimplifyAndComputeLimitToInfinity unsubstituted. The others get there by a substitution first, and that is a different road to the same rule, so it is worth pinning that they arrive at all. x -> -oo was wrong in the same way and is fixed by the same change: lim x->-oo (x - 5)^x / x^x answered 1 on master and now answers e^(-5), which is right -- (1 - 5/x)^x for x -> -oo is 1/(1 + 5/t)^t at t -> +oo. Measured against stock master at 318ac9f. The finite destinations were never wrong, because (1 + x)^(1/x) is already a 1^oo as written and the rule catches it at the top of ComputeLimit without anything needing to be re-read. They are pinned because the re-read runs on that path too and must not disturb it, and measuring confirmed it does not. Full suite 4913 passed / 0 failed, 3 m 22 s. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Member
Author
Update: destinations reached by substitutionThe cases originally here all approach
The finite destinations were never wrong — Full suite now 4913 passed / 0 failed, 3 m 22 s. |
This was referenced Aug 5, 2026
Rafael-SOWNet
added a commit
that referenced
this pull request
Aug 7, 2026
`sqrt(x) * sqrt(y)` was simplified to `sqrt(x * y)`, and at x = y = -1 the first
is i * i = -1 while the second is sqrt(1) = 1. A wrong answer, reached from an
expression anyone might write.
`{1}^n * {2}^n = ({1} * {2})^n` was applied unconditionally in two places -- once
in PowerRules and once, separately, in FactorizeRules. Both now carry the same
condition the ({}^{})^{} rule directly above the first already had, and were
missing for the same reason: #752 fixed that rule and did not look at its
neighbours. True for a whole n whatever the signs, since a^3 b^3 is (ab)(ab)(ab),
and for positive real bases whatever the exponent. Outside those two the sides
can differ by a full turn of the argument.
sqrt(x) * sqrt(y) sqrt(x * y) -> unchanged
x ^ (3/2) * y ^ (3/2) gathered -> unchanged
sqrt(2) * sqrt(3) sqrt(6) unchanged -- both bases positive
x ^ 2 * y ^ 2 (x * y) ^ 2 unchanged -- whole exponent
How it was found: not by a harness. The perfect-square collapse for #176 asked
`Simplify` whether a cross term was twice the product of two roots, and got back
an answer that leaned on this rewrite -- so the collapse fired on
`x + 2*sqrt(x*y) + y`, which is 0 at x = y = -1 where its "square" is -4. That
fix gates its symbolic match on a numeric check, so the wrong collapse never
shipped; this is the cause underneath it. `simpsweep` cannot reach it, because
it generates single-variable expressions and this needs two, both negative.
**The quotient form is deliberately left, and is #802.** It has the same hole --
sqrt(2)/sqrt(-3) is -0.8165i where (2/-3)^(1/2) is +0.8165i -- but guarding it
costs answers rather than shapes: it is what lets the limit machinery read a
1^oo out of a quotient, and with it guarded `(x^2 + 1)^x / (x^2)^x` has no limit
at all, which is the whole of #739 and #740. Measured: twelve tests fail, two of
them limits. Which to prefer is a maintainer's call, so it is filed with the
options rather than taken here, and pinned by a test that asserts the
disagreement so the day it is fixed that test fails and says where to look.
Unit 5544 pass 0 fail; F# 130/130; casbench 113/117 0 wrong; rootcheck 596/596;
simpsweep 10463/10463; propcheck 0 failures.
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
Rafael-SOWNet
added a commit
that referenced
this pull request
Aug 8, 2026
…ier (#802) (#805) `a^n / b^n` was gathered into `(a/b)^n` unconditionally, and that is false across the branch cuts: sqrt(2)/sqrt(-3) is -0.8165i where (2/-3)^(1/2) is +0.8165i. It is the quotient twin of #801 and was left out of that fix, because guarding it cost *answers*: `(x^2 + 1)^x / (x^2)^x` stopped having a limit at all, which is the whole of #739 and #740. That framing was wrong, and this is the correction. The gathering was never the point -- #740 wanted it so the limit machinery could read a 1^oo out of a quotient, and its own test comment says so. The right place for the rewrite is therefore the limit reader, not the simplifier, because that is the only place where it can be justified: a limit needs the identity to hold in a neighbourhood of the destination, so requiring both bases to be eventually positive there is enough, and there is a destination to check that against. In the simplifier there is no destination and nothing to check, which is why it was unconditional. So ApplySecondRemarkable now recognises `a^n / b^n` itself, and the simplifier's rule takes the same guard its whole family carries. Every limit survives: (x^2 + 1)^x / (x^2)^x 1 unchanged (x^3 + 1)^x / (x^3)^x 1 unchanged (x - 5)^x / x^x e^(-5) unchanged (sqrt(x) + 1)^x / sqrt(x)^x unchanged sqrt(x) / sqrt(y) sqrt(x/y) -> unchanged, and correct at x=2, y=-3 Eleven tests in PowerQuotientGatheringTest moved from asserting the *mechanism* -- a single power in Simplify's output -- to asserting the *outcome* it existed for, which is that the limit is answered. That distinction is the whole content of this change, and the tests that pinned the mechanism were pinning something unsound. The four with symbolic bases no longer gather at all and now assert that simplifying does not change their value, since nothing can say a symbolic quotient stays on the principal branch. The test recording #802 as open is flipped to assert it stays fixed, which is what it was written to do. Unit 5543 pass 0 fail; F# 130/130; casbench 113/117 0 wrong; rootcheck 596/596; simpsweep 10463/10463; propcheck 0 failures. Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
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.
Closes the first half of #738.
lim x->+oo (x - 5)^x / x^xcame back1where it ise^(-5), and so did every quotient of two powers whose base ratio tends to 1.Cause
The rule that reads a
1^oo— the second remarkable limit — runs once, at the top ofComputeLimit, against the expression as it was written. A quotient of powers is not a1^ooat that point, so the rule has nothing to match on. The descent then reachesSimplifyAndComputeLimitToInfinity, whose first act is to simplify, and(x - 5)^x / x^xbecomes((x - 5)/x)^x— a1^oothat nothing will now re-read, because the rule that reads one has already run. Straight on into the solvers, where1^(+oo)evaluates to1.Written as the single power the same limits were always right (
((x - 5)/x)^xgives1/e^5), which is what locates the cause in the ordering rather than in the rule.Fix
Neither the simplification nor the rule is wrong; what was wrong is that a form created by simplification was judged by rules that ran before it existed. The same rule is asked again at the point where the expression is in the form the solvers read it in — which is also where every destination has already been normalised to
+oo. Guarded by a depth counter like the other rules in that file, since each level asks for limits of its own. 52 lines added to the library, nothing removed.This closes both of the routes #738 separates, because both run through that one point after the simplification: the
SolveBySubstitutionroute, where(1 + 1/x)^xsubstitutes to an exact1^(+oo), and thePowfdescent route, where((x - 5)/x)^xbuilds1^xand that simplifies to1. It also turns out not to need #736 underneath it, which earlier tracing had expected — the rewrite answers these outright rather than dropping them through to Gruntz.Measured
lim x->+oo(x - 5)^x / x^x11/e^5(309 ms)(x + 1)^x / x^x1e(16 ms)(x + 3)^x / x^x1e^3(21 ms)x^x / (x + 1)^x11/e(57 ms)x^x / (x - 5)^x1e^5(50 ms)(2x + 1)^x / (2x)^x1sqrt(e)(59 ms)(x - 1)^x / x^x1/e, 163 msThe neighbouring quotients, where the base ratio does not tend to 1, are untouched:
(2x)^x / x^xand(x^2)^x / x^xare still+oo,x^x / (2x)^xstill0.What this does not do
(x^2 + 1)^x / (x^2)^xis not reached.Simplifyleaves it written as a quotient, so no1^oois ever created for anything to re-read. It is left unevaluated rather than answered wrongly, and its cause sits in the simplification rather than in the limits — the same quotient written((x^2 + 1) / x^2)^xis answered1without any of this. Recorded in the test's own docs and filed as Simplify does not gather a^p / b^p into (a/b)^p when a base is itself a power #740.1^(+oo)evaluates to1at all — reaches everything that evaluates a power rather than only limits, so it wants its own measurement rather than being bundled in here. 1^oo evaluates to 1, so lim x->+oo (x-5)^x / x^x gives 1 where it is e^(-5) #738 stays open for it.Validation
Full suite 4909 passed / 0 failed (4889 on master + 20 new cases), F# 130/130, corpus 112/117 with 0 wrong, 0 error, 0 timeout — identical to master's baseline. The suite still runs in 3 m 30 s, so the extra re-read costs nothing measurable.
🤖 Generated with Claude Code