Carry the condition an order comparison is decided under (#876), and read a set-builder's predicate inside its binder (#878)

[Rafael-SOWNet]

Closes #876 and #878. Based on #877 — that PR is the first commit's parent, so merge it first and this diff shrinks to its own two commits.

What was wrong

The complex numbers are not ordered, so i < 0 is NaN. Three rules decided a pair of order comparisons as though a comparison always had a truth value:

input	was	at x := i, as written	now
x < 0 and x >= 0	False	NaN	False provided x in RR
x > 0 and x <= 0	False	NaN	False provided x in RR
x < x	False	NaN	False provided x in RR
x >= x	True	NaN	True provided x in RR
not (x < 0) or (x < 0)	True	NaN	True provided x in RR
x < 0 or x >= 0	not reduced	NaN	True provided x in RR
x <= 0 or x >= 0	not reduced	NaN	True provided x in RR

Simplify did not commute with Substitute, and the default codomain is Domain.Complex. The reductions themselves are right — they are the answers over the reals — so this attaches the condition rather than withdrawing the answer. Entity.Provided drops a condition that is True, so nothing is attached where the condition already holds:

2 < 0 and 2 >= 0          ->  False          (operands are numbers)
abs(x) < abs(x)           ->  False          (Absf.Codomain is Real)
(a = b) or not (a = b)    ->  True           (equality is total over C)
x < 0 and x >= 0          ->  False          under Codomain = Domain.Real

That last line is the first time anything outside the limit machinery reads MathS.Settings.Codomain, which is what #876 asked for.

DomainCondition is not the mechanism, despite the neighbouring rules using it. It records singularities — division by zero, log poles — and says nothing about where an order comparison is defined. x < x needs both.

The missing half

OppositeSigns decided the unsatisfiable conjunction; there was no counterpart for the disjunction, so the library took the half of excluded middle that needs the operands to be real and skipped the half that needs exactly the same thing. ExhaustiveSigns is its mirror, and over the reals it settles #876 §3's stated consequence:

piecewise(0 provided x < 0, 0 provided x >= 0)   ->   0

Why #877's test rows moved

#877 pinned not (x < 0) or (x < 0) to True, which its own body records as the unsound answer left for later. The six order-comparison rows move to a test that sets Codomain = Domain.Real, where True is honest; the rows that hold unconditionally — equality, set membership, a boolean variable — stay pinned to True outright. The new §2 test asserts a commutation rather than a printed form, so it holds whatever shape the condition takes.

#878, which this had to fix to avoid shipping a crash

{ x : x > 0 or x <= 0 } reaches a pre-existing abort once §3's rule fires. Both defects are on master with no help from this branch:

{ x : 1/x = 0 }.Simplify()    ->  {  } provided not x = 0
{ x : 1 = 1 }.Simplify()      ->  AngouriBugException
{ x : x = x }.Simplify()      ->  AngouriBugException
{ x : x/x = 1 }.Simplify()    ->  AngouriBugException

The first is a scope error: ConditionalSet passed its predicate to the generic argument-expanding helper, which lifts a Providedf onto the whole expression — right for a function, wrong for a binder, so the bound variable ended up outside its own binder. Reading membership as the predicate holding removes the need to hoist anything: a predicate that is False where its condition holds and undefined where it does not admits nothing, and one that is True under a condition admits exactly what the condition admits, so the condition becomes the predicate.

The crash was a branch that had never worked — for a true predicate the code returned the node's Codomain, a set-builder's Codomain is Domain.Any, and SpecialSet.Create has no case for Any. Nothing names every value a symbol could take, so such a predicate is now left as written.

TryContains needed the same reading and is fixed with it. Answers gained rather than lost:

{ x : 1/x = 0 }              ->  {  }
{ x : x/x = 1 }              ->  { x : not x = 0 }
{ x : x > 0 or x <= 0 }      ->  RR
{ x : x > 0 } /\ { z : z < 0 }  ->  {  }

What this deliberately does not fix

and and or are strict in NaN, not Kleene: (i<0) and False is NaN and (i<0) or True is NaN. Under that semantics the annihilation and absorption rules are unsound too — True or (True and (x<0)) simplifies to True and is NaN at x := i — but by a different root cause, and conditioning them one at a time is not the fix. Filed as #880 rather than smuggled in here.

{ x : True } is left as written because Domain.Any has no set. Naming the universal set is its own question.

Verification

• 6253 C# tests, 130 F# tests — 0 failures. 32 test rows are new across 6 new methods, and 16 of them fail with the four source files reverted to master; a further 6 rows moved out of Hold excluded middle whichever operand carries the negation (#876) #877's theory into the real-codomain test
• casbench 117/119, 0 wrong, 0 error, 0 timeout — every verdict and answer in coverage.md byte-identical, only timings moved
• propcheck 1340 checks, 0 failures
• simpsweep 62778 point comparisons over 10463 expressions, 0 disagreements
• rootcheck 596 cases, 0 incomplete, 0 unsound
• boolmin unchanged at 6/9

🤖 Generated with Claude Code