Order an inequality's endpoints by a comparison that can be made (#757)

[Rafael-SOWNet]

Closes #757.

What was wrong

The quadratic formula returns (-b - sqrt(D))/(2a) before (-b + sqrt(D))/(2a), which is ascending only while a is positive, and SortRealsAndNonReals orders the roots it can compare and leaves the rest as they came. Solving expr <= 0 negates the expression, so it arrives with a negative leading coefficient and the pair the wrong way round:

(x - a)(x + a) <= 0    ->    { a, -a } \/ (sqrt(a^2); -sqrt(a^2))

an interval running from |a| down to -|a| — empty for either sign, with the entire solution set lost between the endpoints.

The fix, and why it is one interval and not three branches

The issue proposed a Piecewise case split on the sign of a. It does not need one: the ordering has a closed form. min(p, q) is (p + q - |p - q|)/2 and max(p, q) is (p + q + |p - q|)/2, so the answer is the single interval [-|a|; |a|] — the issue's own first line — right for either sign of a and for a = 0.

That is better than the case split on three counts: it is one interval rather than three branches each holding on part of the line; it keeps the result a Set, which a Piecewise is not (it is an Entity, so Solve cannot return one); and it collapses to exactly the old output when the roots are concrete, so (x - 2)(x + 2) <= 0 is still [-2; 2] and nothing a numeric coefficient produces changes shape.

Where both roots are real numbers the existing sort has already ordered them and they are handed back untouched.

A double root now collapses to the point it is

Not sought, but it falls out — the span between coincident endpoints is empty:

(x - a)^2 <= 0     was an interval built from an unevaluated discriminant,  is  { a }
(x - a)^2 <  0     "                                                        is  { }
x^2 - 2*a*x + a^2 < 0                                                       is  { }

One thing this does not fix, and a crash it did cause

Simplifying an endpoint can cancel a symbol against itself, which holds only away from zero and comes back as a Providedf. A condition where an endpoint belongs makes the interval an Entity rather than a Set — that threw InvalidCastException on a*x^2 - 1 <= 0 in the first version of this change. The unsimplified endpoint is the same number and assumes nothing, so it is kept there.

Those are exactly the expressions whose leading coefficient is symbolic, and this PR does not claim to answer them. Whether the solution lies inside the roots or outside them turns on the sign of that coefficient, and unlike the endpoint ordering that has no closed form — it genuinely needs the case split. It is a second defect, filed separately with the evidence below.

Measured

Correctness here cannot be read off the printed form (1/2 * abs(X) and abs(X) / 2 are one number and two trees), so each case is checked by membership: solve with the symbol, substitute a value of each sign, and compare what the resulting set holds at eleven points against the inequality itself.

128 specialisations — 8 shapes × 4 directions × a ∈ {3, -3, 1/2, -1/2}:

	master	this branch
correct	81	108
wrong	39	20
ElementInSetAmbiguousException	8	0

27 wrong → right, 0 right → wrong. Every one of the 20 that remain is the symbolic-leading-coefficient family above.

Suites and harnesses, from a clean build:

• unit tests 5254 passed, 0 failed (5225 on master; 29 added here, and the whole new group fails without the change)
• F# wrapper tests 130 passed
• casbench 112/117 solved, 0 wrong, 0 error, 0 timeout — unchanged
• propcheck 0 failures, rootcheck 596/596, simpsweep 0 disagreements of 10463

AGENTS.md

Also carries the rule this issue turned out to be the worked example for: "not answering is a legitimate answer" is a floor and not a target, difficulty is not an argument for choosing between two approaches, and a closed form is worth looking for before a case analysis is built. It sits under the existing section it qualifies, since that is the rule that is easiest to misread as a licence to refuse.

[Rafael-SOWNet]

Follow-up commit: SolveInequality.AutoTestSkip was skipped as "Piecewise required" and held six cases. Two of them are answered by this change — (x + a)(x + b) <= 0 and < 0 — because what they wanted was the smaller of two symbolic roots as the left endpoint, and that has a closed form. No case split was needed for them after all. They move to AutoTest and pass.

The other four put a symbol on the right-hand side, which moves the roots rather than permuting them: whether the quadratic has real roots at all turns on the sign of a + 1/4, and where it has none the answer is the whole line or nothing — no interval between endpoints in any order. Those stay skipped, with the reason corrected from "Piecewise required" to name the actual blocker, and a pointer to #762 for the sibling case.

Unit tests 5254 → 5256.