Repository navigation
Simplify collapses (x^2)^(1/2) to x and sqrt(-x) to i*sqrt(x), both wrong for negative x #752
Description
Two rules in Simplify rewrite a power in a way that is only valid on part of the plane, and both change the value for real negative arguments. Measured on bcfefc26.
1. (x^n)^(1/m) collapses the exponents
"sqrt(x ^ 2)".Simplify() // x — it is abs(x)
"(x ^ 2) ^ (1/2)".Simplify() // x
"sqrt(x * x)".Simplify() // x
"(x ^ 2) ^ (1/2 - 2)".Simplify() // 1 / x ^ 3 — it is 1 / abs(x) ^ 3
"(x ^ 2) ^ (1/2 - 1)".Simplify() // 1 / x — it is 1 / abs(x)At x = -0.63, sqrt(x^2) is 0.63 and the answer given is -0.63.
The rule is ({} ^ {}) ^ {} = {} ^ ({} * {}) in Patterns.PowerRules, applied unconditionally. (a^b)^c = a^(b*c) holds for a > 0, and for an even b with a fractional c it is exactly the case where it does not.
2. (-x)^(1/2) becomes i * sqrt(x)
"sqrt(-x)".Simplify() // i * sqrt(x)
"sqrt(-1 * x)".Simplify() // i * sqrt(x)
"sqrt(x / -1)".Simplify() // i * sqrt(x)
"(-x) ^ (1/2 - 1)".Simplify() // (-i) * x ^ (-1/2)
"(-x) ^ (1/2 - 2)".Simplify() // i * x ^ (-3/2)At x = -0.63, sqrt(-x) is sqrt(0.63) = 0.7937… and i * sqrt(x) is i * (0.7937…i) = -0.7937….
sqrt(-z) = i*sqrt(z) holds off the negative real axis and fails on it, which is where a real negative x puts z.
Why they are one report
Both are the same trade: a rewrite that is true on the principal branch for positive arguments, applied without a condition. Whichever way this is settled — a domain condition on the rewrite, abs in the result, a codomain the rewrite can read, or a decision that AngouriMath simplifies as though every base were positive and says so — it should be settled once for both rather than patched separately.
It is worth noting what the library already does elsewhere, because the machinery exists: {}/{} simplifies to 1 provided not {} = 0, and log(a, a) to 1 provided a > 0. Attaching provided x >= 0 here is the same move. What it costs is that sqrt(x^2) stops being x for callers who were relying on it, and every such simplification starts printing a condition — the same trade recorded against the ln(a) + ln(b) = ln(a*b) rewrite, which is still formally unsound for the same reason and is tracked separately.
This is not new and not a regression. Both reproduce on 61af68a2 and before. Filing it because it had not been written down, not because something changed.
How it was found
By work/simpsweep, a harness that generates expressions to a bounded depth from a small alphabet, simplifies each, and compares the two forms numerically wherever both are defined and real. 10463 expressions, 31 disagreements: 30 of them are these two families, and the 31st is a plain sign error filed separately as #751.
The sweep uses negative sample points deliberately. A corpus evaluated only at positive points would find none of this, and work/propcheck — 151 hand-written expressions, all passing — is that corpus.
Activity
Key polynomial long division by the power and not by how it was writt…
Apply the two power rewrites only where they are true (#752) (#758)
Collapse a three-term sum that is a square with a radical (#176, #203) (
Guard the product of two powers against the branch cut (#801) (#803)
Point AGENTS.md at work that is still open, and at keeping the harness (
A rule-level guard over two bindings, which is the last piece before …
Make a rewrite rule's left-hand side data, and prove it against the s…
A reciprocal inside a logarithm is not moved out unconditionally (#1063)
Thirty-five arms become thirty: Power is data, the largest set and th…
Thirty-five arms become thirty: Power is data, the largest set and th…
Thirty-five arms become thirty: Power is data, the largest set and th…
The documented examples are compiled and run against what they claim
The documented examples are compiled and run against what they claim (#…