Repository navigation
Apply the two power rewrites only where they are true (#752) - #758
Merged
Merged
Conversation
sqrt(x^2) came back as x, which at -0.63 is -0.63 where it is 0.63
(x^2)^(3/2) came back as x^3, which at -2 is -8 where it is 8
sqrt(-x) came back as i*sqrt(x), which at -0.63 is -0.7937, not 0.7937
Two rules, each applied without the condition it needs. `(a^b)^c = a^(b*c)` holds
for a positive `a`, and for any `a` when `c` is whole -- `(a^b)^3` is `a^b`
multiplied by itself three times however `a` is signed. `(a*x)^c = a^c * x^c`
holds for a positive `a`, and again for a whole `c`. Both are restricted to
exactly that.
Where they hold they are unchanged: `(x^(1/2))^2` is still `x`, `(-x)^2` is
still `x^2`, `(2^2)^(1/2)` is still `2`, `(x^2)^2` is still `x^4`.
`sqrt(x^2)` is `abs(x)` and the library does not write that for you. It leaves
the expression alone rather than answering something false; writing `abs`
requires knowing the expression is real, which the codomain added in #755 now
makes sayable and the simplifier does not yet read.
Two test expectations move, and they are different cases:
- `PowerQuotientGatheringTest` pinned `(sqrt(x) + 1)^x / sqrt(x)^x` as
deliberately *not* gathered, because gathering it would have squared the
numerator. **It gathers now, and better**: `sqrt(x)^x` no longer flattens to
`x^(x/2)`, so both exponents stay `x` and the ordinary pairing rule reaches
it. The gap that file is about was a rewrite running ahead of the pairing, and
one less rewrite is one less way to run ahead of it.
- `SolveInequality.Test` pinned `(x - a)(x + a) <= 0` as `[a; -a]`. **That got
worse and it is a fudge coming out**, not a regression to hide: `[a; -a]` is
right for `a < 0` and empty for `a > 0`, and it read that way only because
`sqrt(4a^2)` was simplifying to `2a`. It now answers
`{ a, -a } \/ (sqrt(a^2); -sqrt(a^2))`, whose interval is empty for either
sign. Neither is right for both, because the solver has no case split on the
sign of a symbolic coefficient. Filed as #757 and pinned as it now stands with
a comment pointing there, rather than deleted -- the expectation is still
evidence, of something other than correctness.
Found by `work/simpsweep`, which generates the expressions it checks rather than
listing them. **Its count of disagreements over 10463 expressions goes 30 to 0**,
and those 30 were the whole of what it had left.
Suite 5147 -> 5169 passed / 0 failed, F# 130/130, corpus 112/117 with every
verdict and answer byte-identical, rootcheck 596/596, propcheck 0 failures.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Rafael-SOWNet
added a commit
that referenced
this pull request
Aug 7, 2026
PR #758 (#779) pinned four integrands as a *separate* known gap, declined rather than hung, so that they would not be read as the defect that file is about. PR #786 (#781) fixed that gap, and the two were cut independently from master, so neither could carry the other's half of this. The assertion is inverted rather than deleted, because these four are the evidence that the two changes compose: distributing `sin(x)^4 * (5 - 6 sin(x)^2)` over its sum is what *produces* `sin(x)^4 * (-6) * sin(x)^2`, and merging the two powers is what makes that answerable. Neither PR could show that on its own, and a deleted test would have left it unshown. 5442 pass, 0 fail on merged master. 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 #752.
What was wrong
Wrong by a whole sign, not a rounding. Two rules, each applied without the condition it needs:
(a^b)^c = a^(b*c)holds for a positivea, and for anyawhencis whole —(a^b)^3isa^bmultiplied by itself three times howeverais signed.(a*x)^c = a^c * x^cholds for a positivea, and again for a wholec.Both are now restricted to exactly that, and unchanged where they hold:
(x^(1/2))^2is stillx,(-x)^2is stillx^2,(2^2)^(1/2)is still2,(x^2)^2is stillx^4,sqrt(4*x)and(3*x)^2are untouched.sqrt(x^2)isabs(x), and the library does not write that for you — it leaves the expression alone rather than answering something false. Writingabsrequires knowing the expression is real, which #719's codomain (merged in #755) now makes sayable and the simplifier does not yet read.Measured
work/simpsweepgoes from 30 disagreements to 0 over 10463 generated expressions. Those 30 were the whole of what it had left after #751.work/rootcheck596/596 clean,work/propcheck0 failures.Two test expectations move, and they are different cases
One got better.
PowerQuotientGatheringTestpinned(sqrt(x) + 1)^x / sqrt(x)^xas deliberately not gathered, because gathering it would have squared the numerator. It gathers now, and without that trade:sqrt(x)^xno longer flattens tox^(x/2), so both exponents stayxand the ordinary pairing rule reaches it. The gap that file is about was a rewrite running ahead of the pairing, and one fewer rewrite is one fewer way to run ahead of it.One got worse, and it is a fudge coming out rather than a regression to hide.
SolveInequality.Testpinned(x - a)(x + a) <= 0as[a; -a]. That is right fora < 0and empty fora > 0, and it read that way only becausesqrt(4a^2)was simplifying to2a. It now answers{ a, -a } \/ (sqrt(a^2); -sqrt(a^2)), whose interval is empty for either sign.Neither form is right for both signs, because the solver has no case split on the sign of a symbolic coefficient. Filed as #757, and the expectation is pinned as it now stands with a comment pointing there rather than deleted — it is still evidence, just of something other than correctness. Concrete coefficients are unaffected:
(x - 2)(x + 2) <= 0is still[-2; 2].That is the one judgement call in this PR and it is worth your eye: it trades an answer that was right half the time for one that is right neither, in exchange for removing 30 measured wrong answers from
Simplify, which is the more used API.AGENTS.mdputs correctness ahead of compatibility, which is how I read it, but the inequality output is a real loss and I would rather you saw it stated than buried.🤖 Generated with Claude Code