Hold excluded middle whichever operand carries the negation (#876)

[Rafael-SOWNet]

Fixes §1 of #876. or is commutative and this reduction was not:

(not (x < 0) or (x < 0)).Simplify()   ->  True
((x < 0) or not (x < 0)).Simplify()   ->  x < 0 or x >= 0

There was one excluded-middle rule, Orf(Notf(a), a), matching the negation on the left operand only, with no mirror anywhere in the file. The same proposition therefore had two answers depending on which side it was written on.

Why it survived this long

A bare variable hides it — p or not p and not p or p both give True, because the boolean minimiser reduces expressions over boolean variables whichever way round they are. It takes an operand the minimiser does not treat as an atom — a comparison — to expose the hole:

input	was	now
(x < 0) or not (x < 0)	x < 0 or x >= 0	True
(x > 0) or not (x > 0)	x > 0 or x <= 0	True
(x <= 0) or not (x <= 0)	x <= 0 or x > 0	True
(a = b) or not (a = b)	a = b or not a = b	True
(x in RR) or not (x in RR)	x in RR or not x in RR	True

The = row is what rules out the obvious explanation. For <, the negation is rewritten to >= before the disjunction is looked at, which would destroy the pattern on its own — so that looked like the cause. For = there is no such rewrite, the shape Orf(a, Notf(a)) is intact, and it still did not reduce. The missing mirror is the whole cause.

and is unaffected: it has no contradiction rule on either side, so it is symmetric. Where (x < 0) and not (x < 0) gives False that is comparison reasoning about x < 0 and x >= 0 being unsatisfiable, and it already worked both ways round.

What this deliberately does not fix

The soundness half of #876 stays open. Excluded middle needs the proposition to have a truth value, and over the default complex codomain i < 0 is NaN — so the left-handed form was already answering True where the honest value is NaN. This change makes that reachable from one more spelling rather than introducing it.

The real fix wants these rules to read MathS.Settings.Codomain, which nothing outside the limit machinery does yet. Worth recording: DomainCondition is not the mechanism, despite the neighbouring rules using it — it records singularities (division by zero, log poles), not where an order comparison is defined.

Verification

• 6227 C# tests, 130 F# tests — 0 failures (12 of the C# tests are new, and 5 of them failed before the fix)
• propcheck 1340 checks, 0 failures
• simpsweep 62778 point comparisons over 10463 expressions, 0 disagreements
• rootcheck 596 cases, 0 incomplete, 0 unsound
• casbench 117/119, 0 wrong, 0 error, 0 timeout — every verdict and answer in coverage.md byte-identical, only timings moved
• boolmin unchanged at 6/9

🤖 Generated with Claude Code