Domain.Any is a codomain and not the universal set (#996)

[Rafael-SOWNet]

Answers #996 — should there be a
universal set, and is Domain.Any it? — from the repository rather than from the question, and
corrects the three places that had already answered it the other way.

The conclusion

Domain.Any is a codomain. It is not a set, and there is no universal set to add.

Three things in the code say so, none of them the comment on the enum member:

• Every one of the twelve nodes that declares Any — Variable, Matrix, ConditionalSet,
  Lambda, the set operators, the providers — means this node imposes no restriction. That is a
  statement about a node, not a claim that a collection contains every value.
• The enum is an order, narrowest to widest, and that is how it is read: evaluation asks
  Codomain < Domain.Complex for "narrower than the complex plane", and DomainConditionIn
  narrows a node whose codomain is wider than the reading. Any is the top of that order, which
  makes it the identity for narrowing — not a set of everything.
• The five domains that name a set are exactly the five SpecialSet.Create answers. Any throws,
  and every internal caller answers it before asking.

And the thing a universal set would be for is already there: { x : True } parses, prints,
round-trips, compares up to its bound name, and decides membership for a number, a truth value and
a matrix alike. Set-difference, intersection, union and Filter all work on it. Nothing in the
repository asked for AA, so none is introduced.

solve x in (x - x = 0) is CC, unchanged — and CC still decides against true and against
[1, 2] (#995), which is what makes it an answer rather than a universal set in disguise.

What was wrong

1. solve(a implies b) put truth values in the solution set of a numeric question.

The arm took the complement inside expr.Codomain — the statement node's codomain, which is
Boolean for every Impliesf. A TODO beside it asked for a universal set to subtract from.

"(x = 1) implies (x = 2)".ToEntity().Solve("x")     { 2 } \/ BB          was
                                                    { x : not x = 1 }    is
"x > 1 implies x > 0".ToEntity().Solve("x")         BB \ (1; +oo) \/ (0; +oo)
                                                    { x : not x > 1 } \/ (0; +oo)
"A implies B".ToEntity().Solve("A")                 BB \ { True }
                                                    { A : not A }

Neither the codomain nor a universal set was needed. The values of x where a does not hold
is { x : not a }, which names no universe at all and is right whatever x ranges over. That is
#996's answer: what the solver wanted was the difference, and the difference is expressible
without the universe — which is the case against adding one.

It does not make the implication solver complete. Solve(b, x) is still empty where b does not
mention x, so A implies True is { A : not A } rather than BB — as it was before, where the
answer was BB \ { True }. What stops is answering with a set the question was never asked over.

2. An unbounded interval widened to Any threw out of solve.

"domain((-oo; +oo), Any) = RR".ToEntity().Solve("x")
    NotSufficientlySupportedException: There is no special set for domain Any     was
    {  }                                                                          is

(-oo; +oo) becomes the domain it is an interval of; widened to Any there is no such domain, so
it is now left as written. Its data twin in MatchedRules declined the same case only because
MatchedRule.Build swallows what a replacement throws — the right answer arrived at by an
exception — so the condition says it instead.

3. The implicit Domain → Entity conversion read as "a domain is a set".

Kept for compatibility, now documented as partial: it is the map from the five domains that name a
set, and it throws for Any rather than inventing one.

Documentation

The enum member said "the domain of all values (might be removed in the future)" — the reading
this issue exists to rule out, and an open question in a place that looks like an answer. It now
says what Any is, what it is not, that the unconstrained set is { x : True }, and that the
ambient MathS.Settings.Codomain is a third thing again: a parameter of the question, not a
property of an expression and not a solution set.

Syntax.md still said Any cannot be written, which #1048 made false. Corrected, along with the
domain(...) entry, and the Sets table now records that there is no universal set and no literal
for one.

The SymPy exporter maps a set-builder's Any to S.UniversalSet. That stays — it is what SymPy
prints a ConditionSet without a third argument over — with a comment that it is a choice about
the target language, since SymPy has a universal set and this library does not, and an exporter
to Lean or SMT picks differently.

Tests

32 new tests, in DomainAnyIsNotAUniversalSetTest and SyntaxDocumentedTest. They pin the
invariant rather than the implementation: { x : True } as the unconstrained set (membership,
round-trip, stability, bound-name independence), the five domains converting to sets and Any not,
no literal for AA or UU, Any as a codomain keyword and not a set literal, x - x = 0
answering the domain it was asked in and that domain excluding a truth value and a matrix, an
implication asserting no domain, and the widened interval. Three of them fail against the previous
behaviour; the rest would fail the day a universal set is added by accident.

Measured

• Unit suite 9159 passed, 0 failed, 14 skipped.
• casbench 116/119, 0 wrong, 0 error, 0 timeout.
• crashcheck 1834 cases, 0 crashed, 0 unexpected.
• rulecheck 30 sets, 17532 applications, 0 value changes, 0 never settle.
• confluence SetOperator 0 nodes with several arms, 0 disagreeing.
• Two entries in BREAKING-CHANGES.md, both measured on a build.

Deliberately not in this PR

• AnalyticalEquationSolver answers a tautology with a hardcoded MathS.Sets.C rather than the
  ambient MathS.Settings.Codomain, so solve x in (x - x = 0) is CC even under
  Codomain.Set(Domain.Real). Conservative and correct at the default; making the tautology answer
  follow the ambient reading is a solver change with its own blast radius.
• Solve has no Notf arm, so not (x = 1) answers { } — the empty set as a positive claim,
  which is the defect Giving up on a resource is spelled the same as a mathematical negative #1036 fixed for equations, unfixed for negation. Filed as Solve answers every negation with the empty set, because the statement solver has no arm for not #1127.

Neither is a domain-versus-set confusion, which is what this one is about.