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

`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, and no mirror of it anywhere in the file. So the same proposition had two
answers depending on which side it was written on.

A bare variable hid 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 see the hole, which
is why this survived. It reproduces on <, >, <=, = and in:

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

The `=` case 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; 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 not affected: it has no contradiction rule on either side, so it is symmetric. Where
`(x < 0) and not (x < 0)` reduces to False it is comparison reasoning about x < 0 and x >= 0
being unsatisfiable, not this rule, and it already worked both ways round.

This does not touch the soundness half of #876, which 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 fix wants the
rules to read MathS.Settings.Codomain, which nothing outside the limit machinery does yet.
DomainCondition is not the mechanism for it -- it records singularities, not where an order
comparison is defined.

Verified: 6227 C# tests and 130 F# tests pass, 0 fail. propcheck 1340 checks 0 failures,
simpsweep 62778 point comparisons 0 disagreements, rootcheck 596 cases 0 incomplete and
0 unsound, casbench 117/119 with 0 wrong, 0 error and 0 timeout, every verdict and answer
in coverage.md byte-identical. boolmin unchanged at 6/9.

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>

Author: Rafael-SOWNet

Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Boolean.cs

@@ -28,6 +28,9 @@ private static bool IsLogic(Entity a, Entity b, Entity c)
             Andf(Notf(var any1), Notf(var any2)) when IsLogic(any1, any2) => !(any1 | any2),
             Orf(Notf(var any1), Notf(var any2)) when IsLogic(any1, any2) => !(any1 & any2),
             Orf(Notf(var any1), var any1a) when any1 == any1a && IsLogic(any1) => True,
+            // The same law with the operands the other way round. `or` is commutative, so
+            // leaving this out made the answer depend on which side the negation was written.
+            Orf(var any1a, Notf(var any1)) when any1 == any1a && IsLogic(any1) => True,
             Orf(Notf(var any1), var any2) when IsLogic(any1, any2) => any1.Implies(any2),
             Andf(var any1, var any1a) when any1 == any1a && IsLogic(any1) => any1,
             Orf(var any1, var any1a) when any1 == any1a && IsLogic(any1) => any1,

Sources/Tests/UnitTests/Common/SimplificationRegressionTest.cs

@@ -434,5 +434,28 @@ public void ExpandKeepsTheValueOfAQuotientOfFactorials(string input, int at, dou
         [InlineData("(x + y + 1)! / (x + y)!")]
         public void ExpandCancelsAQuotientOfFactorialsRatherThanLeavingIt(string input)
             => Assert.DoesNotContain(input.ToEntity().Expand().Nodes, node => node is Entity.Factorialf);
+
+        // https://github.com/asc-community/AngouriMath/issues/876
+        // There was one excluded-middle rule and it matched the negation on the left operand
+        // only. `or` is commutative, so the same proposition had two answers depending on
+        // which side it was written: `not (x < 0) or (x < 0)` was True while
+        // `(x < 0) or not (x < 0)` was left as written. A bare variable hid it, because the
+        // boolean minimiser reduces those whichever way round they are — it takes a
+        // comparison, which the minimiser does not treat as an atom, to see it.
+        [Theory]
+        [InlineData("not (x < 0) or (x < 0)")]
+        [InlineData("(x < 0) or not (x < 0)")]
+        [InlineData("not (x > 0) or (x > 0)")]
+        [InlineData("(x > 0) or not (x > 0)")]
+        [InlineData("not (x <= 0) or (x <= 0)")]
+        [InlineData("(x <= 0) or not (x <= 0)")]
+        [InlineData("not (a = b) or (a = b)")]
+        [InlineData("(a = b) or not (a = b)")]
+        [InlineData("not (x in RR) or (x in RR)")]
+        [InlineData("(x in RR) or not (x in RR)")]
+        [InlineData("not p or p")]
+        [InlineData("p or not p")]
+        public void ExcludedMiddleHoldsWhicheverOperandCarriesTheNegation(string input)
+            => Assert.Equal(Entity.Boolean.True, input.ToEntity().Simplify());
     }
 }