An equation the solver cannot invert is left unsolved, not answered with no roots

[Rafael-SOWNet]

x! = 6 was answered { }, a claim that it has no roots, and it has 3. 2.5.0 does the same.

The solver isolates x by inverting the function around it. For some functions the inversion has no way to write the preimage, and it returned none, which the solver read as "no roots". Those functions are a factorial, a binomial coefficient, mod, gcd, lcm, min, max, phi, prime, the valuation, a sum, a product, a limit, a binder, and a set with x inside it. Several of these inversions carried comments calling the empty result "declining", but an empty result isn't a decline.

Now such an inversion throws CannotInvertException (internal). The analytical equation and set solvers catch it at the level where it was met, and answer that equation as the set of x for which it holds. The statement solver already does that for a statement it has no arm for, since "not the empty set, which claims there is no such x".

	2.5.0 and master	now
x! = 6	{ }	{ x : x! = 6 }
binomial(x, 2) = 3	{ } on master	{ x : binomial(x, 2) = 3 }
x mod 3 = 1	{ }	{ x : x mod 3 = 1 }
gcd(x, 4) = 2, max(x, 1) = 3, phi(x) = 4	{ }	the set of x for which it holds
prime(x) = 7	{ } on master (2.5.0 read prime(x) as prime * x)	{ x : prime(x) = 7 }
(x - 1) x! = 0	{ 1 }	{ 1 }
x! = 0, arcsin(x) = 5	{ }	{ }

A few properties of the change:

• Roots found beside an unsolved factor are kept. The catch is per level, so the answer is the union of the roots found and the unsolved remainder.
• An equation left whole is given back as written. It reads { x : x! = 6 }, not the rearranged { x : x! - 6 = 0 }.
• A value a function provably never takes still has no roots. The factorial is the gamma function one along, which has no zeros, so x! = 0 stays { }. That is also why (x - 1) x! = 0 is exactly { 1 }. The out-of-range inversions of arcsin and its siblings are unchanged, since those empty results are true.
• The Derivativef and Integralf inversions are left alone. Their empty results come from Solving an equation that contains the unknown's derivative returns a non-solution #964's reasoning about independence, which this change doesn't touch.

What it uncovered

InductionTest's forall n in ZZ+ : product((2 k - 1) / (2 k), k, 1, n) = (2 n)! / (4^n (n!)^2) depended on the old answer. Its step needs n!^2 = 0 to have no solution in ZZ+, and Solve answered { } because it couldn't invert the factorial. The conclusion was true and the reason wasn't. With the factorial's zero-free inversion, the step is proved for the right reason, and the row is True again.

Three tests pinned the empty set, and each is rewritten to what the answer means:

• SolveOneEquation's x! - 1 was pinned at no roots, and 0 and 1 are both roots.
• (x! provided x > 7) = 6 expected { }. That is true, but only because the solver claimed x! = 6 has no roots. The answer now keeps the condition, and 3 is excluded by it.
• ModulusTest.SolvingIsNotClaimed pinned { } on purpose, so that whoever changed it would notice. It now pins the unsolved set.

This is also what the error functions of #1501 need. Without it, erf(x) = 1/2 would be answered { }.

Measured

Measured on this branch after its rebase onto #1502's merge:

• The unit suite passes on net10.0: 12757 passed, 14 skipped, none failed, out of 12771, of which 8 are new.
• The allocation gate passes on all 19 gated benchmarks.

🤖 Generated with Claude Code

https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura

[Happypig375]

Using exceptions as control flow is bad. Shouldn't this return null when non-invertible instead?

[Rafael-SOWNet]

Agreed. It threw because the inversion recurses through lazy sequences, and an exception got out of them without every node having to check. I'll make Invert and InvertNode return null for "no written preimage": the solvers answer the set-builder on null, and each node that inverts a child passes a null on. With nullable annotations on and warnings as errors, the compiler flags every call site that doesn't handle it. The PR follows shortly.

[Rafael-SOWNet]

#1510.