`p or not p` depends on which side the `not` is written, and reduces to True where the proposition is undefined

[Rafael-SOWNet]

Found while re-measuring #536's recorded blocker (that issue is closed and fixed; this is a different thing sitting under it). Measured on master at 363edfa3, .NET 10, default settings.

1. or is commutative; this reduction is not

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

Same proposition, two answers, decided by which operand the not is written on. There is one excluded-middle rule and it matches the left form only — Patterns.Boolean.cs:30:

Orf(Notf(var any1), var any1a) when any1 == any1a && IsLogic(any1) => True,

There is no Orf(var any1, Notf(var any1a)) anywhere in the file. The line below it has the same handedness, turning not a or b into a implies b, so the left form gets rewritten and the right form is left alone.

A bare variable hides it — p or not p and not p or p both give True, presumably via the boolean minimiser, which is why this reads as working until a comparison is involved.

2. The reduction is unsound where the comparison has no value

The default codomain is Domain.Complex, and an order comparison against a non-real is NaN:

"(x < 0) and not (x < 0)"  at x := i, as written   ->  NaN
"(x < 0) and not (x < 0)"  simplified              ->  False
"(x < 0) and not (x < 0)"  simplified, then x := i ->  False

So Simplify turns NaN into False. It does not commute with Substitute, silently. The same holds for a bare variable:

(p or not p).Simplify()                        ->  True
  then Substitute(p, i < 0), evaluated         ->  True
(p or not p).Substitute(p, i < 0), evaluated   ->  NaN

Excluded middle needs the proposition to have a truth value, and over the complex plane an order comparison does not. The neighbouring rules already know this — lines 27, 35, 38 and 39 all carry .Provided(...DomainCondition). Line 30 is the one that does not.

3. and and or disagree about the same pair

Without any not at all:

(x < 0 and x >= 0).Simplify()   ->  False
(x < 0 or  x >= 0).Simplify()   ->  x < 0 or x >= 0

The unsatisfiable conjunction is decided and the valid disjunction is not — so the library takes the half of excluded middle that is unsound off the real line and skips the half that would be sound on it. This is also why piecewise(0 provided x < 0, 0 provided x >= 0) stops at piecewise(0 provided (x < 0 or x >= 0)) rather than 0: the cases are already merged, and only this last reduction is missing.

What would settle it

Under MathS.Settings.Codomain = Domain.Real all four reductions above are sound, and x < 0 or x >= 0 should be True. Measured, the setting changes none of them — the boolean and comparison rules never read it. That is the same gap #721 is about, reached from a different direction.

What I am not claiming

The measurements are direct. That the missing mirror pattern is the whole cause of §1 is inference from reading the rule table, not from instrumenting the pipeline; and I have not traced which rule decides §3's conjunction, only that no not is needed to reach it.