Collapse a three-term sum that is a square with a radical (#176, #203)

[Rafael-SOWNet]

Closes #176. Addresses #203, which names #176/#177/#178 as its content — the other two are already closed.

1 + sqrt(2x) + x/2 was left as written, where it is (1 + sqrt(x/2))^2. A three-term sum u + 2*sqrt(u)*sqrt(v) + v collapses to (sqrt(u) + sqrt(v))^2.

The identity is unconditional; the test for it is not

sqrt(u)^2 is u for every complex u — it is the square of a principal root, not the root of a square. sqrt(u^2) = u is the false one, and holds only for a non-negative u (#752).

What cannot be trusted is deciding whether the cross term matches. That needs Simplify, and the simplifier equates sqrt(x)*sqrt(y) with sqrt(x*y), which is false across the branch cuts:

at x = y = -1:   x + 2*sqrt(x*y) + y   =  0
                 (sqrt(x) + sqrt(y))^2 = -4

Asked symbolically, this rule fired on that sum and produced a wrong answer. The first version of it did exactly that, and the test that caught it had been written before the rule.

So the symbolic match only proposes and a numeric check disposes. The sample points include negative values — where a branch-cut error shows and nowhere else — and each free variable is offset from the last so x and y cannot coincide into a case that happens to hold. The rule withdraws unless every sampled point agrees.

It is its own pass, not an arm of FactorizeRules

Replace walks bottom-up, so the common-factor rule reaches the inner 4 + 4*sqrt(x) of 4 + 4*sqrt(x) + x first and rewrites it to 4 * (1 + sqrt(x)) — by then the three terms are gone. Ordering the arms within the switch does not help, because the two rules are looking at different nodes.

Measured

1 + sqrt(2 * x) + x / 2	(1 + sqrt(x / 2)) ^ 2
1 + 2 * sqrt(x) + x	(1 + sqrt(x)) ^ 2
4 + 4 * sqrt(x) + x	(2 + sqrt(x)) ^ 2
1 + 3 * sqrt(x) + x	unchanged — not a square, and not rounded into one
x + 2 * sqrt(x * y) + y	unchanged — not a square over ℂ
x ^ 2 + 2 * x + 1	unchanged here; at x = -3 it is 4 and (sqrt(x^2) + 1)^2 is 16

Every positive case is checked by sampling the collapsed form against the original, not by comparing text — sqrt(x/2) and sqrt(2x)/2 are one number and two trees.

Harnesses

• unit 5536 pass, 0 fail; F# 130/130
• casbench 113/117, 0 wrong; rootcheck 596/596; simpsweep 10463/10463; propcheck 0 failures

🤖 Generated with Claude Code