Let a connective settle what its truth table settles (#880)

[Rafael-SOWNet]

Closes #880 — which set this out as a fork and left it open for want of one measurement. This PR is
that measurement plus the branch it favours; say the word and I will close it instead.

The contradiction

Simplify gave the Kleene answer and evaluation absorbed everything into NaN, so the same expression
had two:

"True or (True and (x < 0))".Simplify()      ->  True
the same, at x := i, evaluated as written    ->  NaN     (was)
                                             ->  True    (is)

i < 0 has no truth value: the default codomain is Domain.Complex, and the complex numbers are not
ordered. What changes here is only what a connective does with such an operand.

expression	was	is
(i < 0) and False	NaN	False
(i < 0) or True	NaN	True
False implies (i < 0)	NaN	True
(i < 0) implies True	NaN	True
(i < 0) and True	NaN	NaN, unchanged
(i < 0) or False	NaN	NaN, unchanged
not (i < 0)	NaN	NaN, unchanged
(i < 0) xor (i < 0)	NaN	NaN, unchanged
(0/0) * 0, (0/0) + 1, (0/0) - (0/0)	NaN	NaN, unchanged

It is one line, and the tables were already right

Andf reads (_, Boolean(false)) as False and (Boolean(true), _) as its right operand — Kleene as
written. What overrode them is a single line in the shared ExpandOnTwoArguments:

if (left.IsNaN || right.IsNaN) return MathS.NaN;

running before the table is consulted. The four connectives now get first refusal on an undefined
operand through a settlesNaN flag, and hand back null where they cannot settle it — which is what
still reaches NaN. So #880's prediction holds exactly: under Kleene, no rule needs touching.

I checked all four tables row by row against Kleene's before enabling them, rather than assuming: and,
or, implies and xor each already give the right answer for an unknown operand, including leaving it
unknown where it genuinely decides the result (u and True, u xor u).

Opted in per node rather than changed in the helper for everything, because arithmetic must stay
strict. A rule for a zero factor exists, and NaN * 0 must not reach it. Measured with a computed NaN
rather than argued — the literal NaN token turns out to parse as a variable, which is its own defect
and is now #906.

The measurement #880 asked for

I have not measured how much of the suite pins strict propagation, so I am not proposing one over the
other here.

One assertion of 6385, and it is that issue's own guard clause. The row asserting x < 0 and x = 0
is NaN at x = i was written for #876 to keep the test from going vacuous if a comparison ever gained
a truth value. It has gained one indirectly: i = 0 is decidably False, and False and u is False.

Everything else is unchanged: suite 6389 passed / 0 failed, F# wrapper 130 passed, casbench 117/119 with
0 wrong, rootcheck 596/596, simpsweep 10463/10463, propcheck 1340 checks with 0 failures, crashcheck
1652 cases with 0 crashes, boundcheck unchanged at 2 disagreements.

One consequence, recorded rather than fixed

That row now moves the disagreement to the other side. The evaluator settles False for every x,
while Simplify answers False provided x in RR — and for this reduction the condition is over-strong:
it needs one conjunct false, not both operands real. So Simplify is now weaker than evaluation there
rather than stronger, which is the opposite of #876's original defect and not a regression in either.

It is pinned by a test that says so, because the rules #876 conditioned want going through one at a time
to see which of them still need the condition under Kleene. That is a separate change and I have not
made it here.

What this does not touch

Excluded middle, which #880 flags as surviving either fork: p or not p needs p to have a truth
value, and Kleene does not supply one, so NaN or not NaN is still NaN and #876's conditioning of
those is still the right shape. Its tests are unchanged and passing.

Cut from master at 8c56b59f.