Gather a quotient of powers whose exponents a rewrite has already moved (#740) - #748
Merged
Merged
Conversation
…ed (#740) `a^p / b^p` is gathered into `(a/b)^p`, and stopped being gathered as soon as one of the bases was itself a power: (a^2)^x / (b^2)^x gathers (a^2)^x / b^x did not (a^2 + 1)^x / (a^2)^x did not It is not the shape of the quotient but the order the rules run in. The rule that rewrites `(b^c)^p` as `b^(c*p)` applies to the *child*, on the way up, so by the time the pair of powers is looked at it has already happened. Where both bases are powers it moves both exponents together and the pair survives -- which is why the first line above works, and why it looked like the shape mattered. Where only one base is a power it moves one exponent and not the other, the exponents stop matching, and there is nothing left to pair on. So the pair is read back: `a^p / b^(c*p)` is `(a / b^c)^p`, and the same the other way up. Restricted to a whole `c`, so that `b^c` moves into the base and nothing gains a root it did not have -- a fractional `c` would have to divide the exponent instead, turning `(sqrt(x) + 1)^x / sqrt(x)^x` into `((sqrt(x) + 1)^2 / x)^(x/2)`, which buys a gathered form with a squared numerator. That is a judgement about output rather than the gap this fixes, so it is left as it stands and pinned as such. Why it is worth gathering: the limit machinery reads a `1^oo` off a single power and cannot see one in a quotient, so the same function was answered or not according only to how it had been written. lim x->+oo (x^2 + 1)^x / (x^2)^x unevaluated after 5.5 s -> 1 in 31 ms lim x->+oo (x^3 + 1)^x / (x^3)^x the same A quotient of numeric powers is untouched, because a numeric exponent is not written as a product and so matches nothing here: `x^4 / y^2` keeps its form. `2^(2x) / 3^x` becoming `(4/3)^x` is the one visible widening beyond the issue. Suite 4979 -> 4986 passed / 0 failed, F# 130/130, corpus 112/117 with 0 wrong and every verdict and answer byte-identical. rootcheck is 595/596 on this branch, its one incomplete case being #744, fixed in PR #745 rather than here. Co-Authored-By: Claude Opus 5 <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
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 #740.
What was wrong
a^p / b^pis gathered into(a/b)^p, and stopped being gathered as soon as one of the bases was itself a power:It is not the shape of the quotient but the order the rules run in. The rule that rewrites
(b^c)^pasb^(c*p)applies to the child, on the way up, so by the time the pair of powers is looked at it has already happened:What the fix does
Reads the pair back:
a^p / b^(c*p)is(a / b^c)^p, and the same the other way up.Restricted to a whole
c, sob^cmoves into the base and nothing gains a root it did not have. A fractionalcwould have to divide the exponent instead, turning(sqrt(x) + 1)^x / sqrt(x)^xinto((sqrt(x) + 1)^2 / x)^(x/2)— a gathered form bought with a squared numerator. That is a judgement about output rather than the gap this fixes, so the issue's second example is deliberately left as it stands, and pinned as such.(a^2 + 1)^x / (a^2)^x(1 + 1/a^2)^x(x^3 + 1)^x / (x^3)^x(1 + 1/x^3)^x(a^2)^x / b^x(a^2 / b)^xx^(2a) / y^a(x^2 / y)^a2^(2x) / 3^x(4/3)^xx^4 / y^2Why it is worth gathering
The limit machinery reads a
1^oooff a single power and cannot see one in a quotient, so the same function was answered or not according only to how it had been written:lim x->+oo (x^2 + 1)^x / (x^2)^xlim x->+oo (x^3 + 1)^x / (x^3)^xlim x->+oo ((x^2 + 1) / x^2)^xMeasured
work/rootcheck595/596; its one incomplete case is A power of a polynomial is solved by inverting into itself, so the roots come back containing x #744, fixed in Only invert an equation whose variable occurs once (#744) #745, not here.The tests pin the value as well as the shape — the rewrite is checked numerically at a point where every base is positive, which is where
a^p / b^(c*p) = (a/b^c)^pholds without a branch argument — and the limits #739 fixed are pinned alongside, since they go through this same gathering.🤖 Generated with Claude Code