Guard the product of two powers against the branch cut (#801) - #803
Merged
Conversation
`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>
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.
Fixes #801. Splits out #802.
sqrt(x) * sqrt(y)was simplified tosqrt(x * y)— and atx = y = -1the first isi * i = -1while the second issqrt(1) = 1. A wrong answer, from an expression anyone might write.Two copies of the same unguarded rule
{1}^n * {2}^n = ({1} * {2})^nwas applied unconditionally in two places — once inPowerRules, and separately inFactorizeRules. Guarding only the first changed nothing, becauseSimplifyruns both.Both now carry the 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 wholenwhatever the signs, sincea^3 b^3is(ab)(ab)(ab), and for positive real bases whatever the exponent.sqrt(x) * sqrt(y)sqrt(x * y)x ^ (3/2) * y ^ (3/2)sqrt(2) * sqrt(3)sqrt(6)sqrt(6)— both bases positivex ^ 2 * y ^ 2(x * y) ^ 2(x * y) ^ 2— whole exponentHow it was found
Not by a harness. The perfect-square collapse for #176 asked
Simplifywhether a cross term was twice the product of two roots, and got an answer leaning on this rewrite — so the collapse fired onx + 2*sqrt(x*y) + y, which is0atx = y = -1where 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.simpsweepcannot reach this: it generates single-variable expressions, and this needs two variables taken negative at once.The quotient form is deliberately left — #802
It has the same hole (
sqrt(2)/sqrt(-3)is-0.8165iwhere(2/-3)^(1/2)is+0.8165i), but guarding it costs answers rather than shapes. It is what lets the limit machinery read a1^ooout of a quotient, and with it guarded:That is the whole of #739 and #740. I measured it — twelve tests fail, two of them limits — and it is a maintainer's call rather than mine, so #802 carries the counterexample, the measured cost and three options (leave it; add sign analysis so
x^2is known non-negative; or condition it onMathS.Settings.Codomain).It is pinned by
TheQuotientFormIsStillWrongAndThatIsRecorded, which asserts the disagreement — so on the day #802 is fixed, that test fails and points at it.Harnesses
casbench113/117, 0 wrong;rootcheck596/596;simpsweep10463/10463;propcheck0 failures🤖 Generated with Claude Code