Only invert an equation whose variable occurs once (#744)

[Rafael-SOWNet]

Closes #744.

What was wrong

Inverting an expression isolates the variable by walking down to it and undoing each node on the way, which works only if there is one place to walk to — Invert's own documentation requires "exactly ONE occurance of x". Solving f(x) = 0 did not check it, so an equation whose variable occurs more than once came back rearranged rather than solved:

equation	was	is
(x^2 + x + 1)^2 = 0	{ sqrt(-1 - x), -sqrt(-1 - x) }	{ (-1 - sqrt(-3))/2, (-1 + sqrt(-3))/2 }
(x^2 + x)^2 = 0	{ sqrt(-x), -sqrt(-x) }	{ 0, -1 }
(x^3 + x + 1)^2 = 0	{ (-1 - x)^(1/3), … }	the three roots of the cubic
sqrt(x^2 + x + 1) = 0	{ sqrt(-1 - x), -sqrt(-1 - x) }	the two roots of the quadratic
sin(x^2 + x) = 0	{ ±sqrt(2·pi·n_1 - x), ±sqrt(pi + 2·pi·n_1 - x) }	{ (-1 ± sqrt(1 + 8·pi·n_1))/2, (-1 ± sqrt(1 + 4·pi + 8·pi·n_1))/2 }
ln(x^2 + x) = 0	{ sqrt(1 - x), -sqrt(1 - x) }	{ (-1 - sqrt(5))/2, (-1 + sqrt(5))/2 }
abs(x^2 + x) = 0	{ ±sqrt(-x) provided r_1 in RR }	{ 0, -1 }

x = sqrt(-1 - x) is x^2 + x + 1 = 0 moved to x^2 = -1 - x with the square inverted and the x on the right left where it stood. It is a true statement and not an answer.

Such a "root" satisfies nothing and cannot be evaluated at all, which is why nothing caught it: substituting it back leaves an expression rather than a residual, and root verification drops an answer only on positive evidence against it.

The issue records only the power shape and only whole exponents. The sqrt / ^(3/2) cases and the whole sin / ln / abs family are the same defect and are fixed with it.

What the fix does

1. case Function now requires the variable to occur once. Where it occurs more than once, the replacement machinery further down is what answers — it solves sin(t) = 0 and then t = x^2 + x for each root. That machinery was always there; a right-hand side of zero is the only reason it was being skipped, since a non-zero side leaves a subtraction that reaches it. This is why cos(x^2 + x + 1) = 1 has never been wrong while sin(x^2 + x) = 0 always was.

2. A power is routed directly to its base, because a power is zero exactly where its base is. This is not needed for correctness — the replacement machinery gets there too — but it makes f(x)^n = 0 answer identically to f(x) = 0 rather than merely equivalently. Without it (x^2 + x + 1)^2 = 0 reaches the same two numbers written -1/2 + -sqrt(-3/4), which is the output-quality complaint of #272 one step along, and takes about four times as long (238 ms vs 63 ms). Restricted to an exponent that is a positive number and free of x: a negative one is never zero, and one that moves with x is a different equation.

3. A root that mentions the variable it solves for is rejected in IsSpurious. Nothing reaches this once (1) and (2) are in — measured over eighteen function-shaped equations with the check disabled, none produced such a root — so it is a net rather than the fix, and the comment says so. It is kept because Invert requires the variable to occur once and only one of its five callers checks that.

How it was found

By work/rootcheck, a completeness harness that multiplies polynomials up from factors whose roots are known before anything is solved, then asks not "is every answer right" but "is every root there". Substituting answers back can only confirm the roots you were given.

Its one failing case was (x^2 + x + 1) * (x^2 + x + 1) — a product only until InnerSimplified writes it as a square.

Measured

• rootcheck: 596 cases, 1 incomplete / 2 missing roots → 0 and 0; 0 unsound either way.
• Corpus (work/casbench): 112/117 solved, 0 wrong, 0 error, 0 timeout — unchanged, and every verdict and answer byte-identical to before (only the ms column moves).
• Suite: 4979 → 4992 passed / 0 failed, F# 130/130.

Regression tests are in a new RepeatedVariableSolveTest, including the property the harness checks — no root mentions the variable it solves for — and the cases that must not change, where the variable occurs once and inversion is still the route.

🤖 Generated with Claude Code