A condition on a bound name stays in its binder

[Rafael-SOWNet]

A node's domain condition was the conjunction of its children's, a binder's body included, so what a sum's body said about its index came out of the sum with the index free in it:

• The product rule leaves 0 * sum(...), and 0 * f keeps the condition f is defined under. So the derivative of 2 sum(ln(x - w), w in { w : w^3 + w + 1 = 0 }) was … provided not x - w = 0, with w free, and EvalNumerical could not decide it.
• sum(1/(k - x), k, 1, 3) and integral(1/(t - x), t, 0, 1) reported not k - x = 0 and not t - x = 0 the same way. Being expanded or evaluated first hid it there.

Such a conjunct is now read the way the binder reads it, as required at every value the name ranges over. It is not left free, and it is not left out: left out, 0 * sum(1/(k - x), k, 1, n) became a plain 0 at x = 1, where the sum has no value.

• Over the roots of a polynomial p with rational coefficients, "q(w) != 0 at every root" is Res_w(p, q) != 0, which mentions the other names alone. Above it is not x^3 + x + 1 = 0, where the logarithms are singular.
• A finite range of numbers is the conjunction over it.
• Anything else is forall over the range: the set of a sum over a set, of an extremum or of a quantifier; the whole numbers between a summation's or a product's bounds; the interval of a definite integral.
• A set builder's own condition on its name is part of whom it admits, and is left out of where the set is defined.
• A limit does not need its body defined throughout anything, so it is left as it was.

Measured

Input	Was (2.5.0)	Now
"sum(1/(k - x), k, 1, 3)".ToEntity().DomainCondition	not k - x = 0	not 1 - x = 0 and not 2 - x = 0 and not 3 - x = 0
"sum(1/(k - x), k, 1, n)".ToEntity().DomainCondition	not k - x = 0	forall k in { k : k in ZZ and 1 <= k and k <= n } : not k - x = 0
"integral(1/(t - x), t, 0, 1)".ToEntity().DomainCondition	not t - x = 0	forall t in [0; 1] : not t - x = 0
"sum(ln(x - w), w in { w : w^3 + w + 1 = 0 })".ToEntity().DomainCondition	(no such node)	not -1 + -x + (-x) ^ 3 = 0

• BinderConditionTest pins each reading. The derivative has no free w and evaluates. Over the roots of w^2 - 1, the condition is false at 1 and -1 and true elsewhere. The root polynomial itself as the condition is defined nowhere. 0 * sum(1/(k - x), k, 1, n) keeps its condition. 1..3 is the conjunction and 3..1 is empty. A set builder keeps nothing of its own.
• The unit tests pass: 14,177, none failed (net10.0). Nothing else leaned on the conditions that leaked.
• The performance gate passes on 4a11e4a2, whose code differs from this head's only in the resultant's zeroth power. Only a sum over a set reaches that, and no gated benchmark has one. Allocation matches the baseline on all 19 gated benchmarks.

Closes #1632.

🤖 Generated with Claude Code

[Rafael-SOWNet]

The resultant path is right, including where q's leading coefficient vanishes: Res(p, q) = lc(p)^m ∏ q(α) holds for any coefficients of q once p is fixed with a nonzero leading coefficient, and AtEveryRoot itself requires rational coefficients through SquareFreeParts, so a set builder typed with symbolic coefficients falls through to forall. The finite conjunction, 3..1 being empty and the set builder's reading are right too. Two things in the integral path:

1. Reversed limits look as though they lose the condition (inferred from the code, not yet probed). The range is MathS.Interval(from, to), and here an interval whose left end is above its right end reads as empty ((3; 1) /\ [0; 5] is { }). If [1; 0] does too, integral(1/(t - x), t, 1, 0) gets forall t in [1; 0] : …, which holds vacuously, and 0 * integral(1/(t - x), t, 1, 0) becomes a plain 0 at x = 1/2, which is the direction this PR exists to close. The segment between the limits in either order, MathS.Interval(from, to).Unite(MathS.Interval(to, from)), is right for symbolic limits as well.

2. Definedness on the closed interval is sufficient for a definite integral, not necessary. integral(ln(t), t, 0, 1) is -1, yet its condition is now forall t in [0; 1] : not t = 0, which is false. So the product rule's 0 * integral(…) should now be 0 provided false, and "2 * integral(x * ln(t), t, 0, 1)".Differentiate("x"), which is -2, should come out undefined. That is the same product-rule path as the RT derivative. Worth probing on the branch:

"2 * integral(x * ln(t), t, 0, 1)".Differentiate("x")      // -2
"0 * integral(ln(t), t, 0, 1)"                             // 0
"0 * integral(1/t, t, 0, 1)"                               // undefined: it diverges

The open interval does not fix it: it answers the second row and gives the third a value. No condition on the integrand's points decides whether an improper integral converges, so whichever reading is chosen, I'd state it in the doc comment and the BREAKING entry and pin one example of each direction, so the limitation is visible rather than silent.

Tests. Nothing in BinderConditionTest reaches Integralf, though the BREAKING table lists one. AZeroTimesASumKeepsTheSumsCondition asserts the shape (Providedf, no k); asserting the meaning would bind it: with n = 3, undefined at x = 1 and 0 at x = 1/2.

[Rafael-SOWNet]

Both points held, and are fixed in 8d8d3e8.

1. Reversed limits. forall t in [1; 0] : not t - 1/2 = 0 simplified to True, since [1; 0] is empty. Two numeric limits are put in order now. Symbolic ones are written as the values between the two, (a <= t and t <= b) or (b <= t and t <= a), rather than as the union you suggested: [a; b] \/ [b; a] simplifies to { b }, and [0; 1] \/ [1; 0] to { 1 }, on 2.5.0 as well. That is a wrong answer of its own: The union of an interval and its reversal is one point: [0; 1] \/ [1; 0] is { 1 } #1634.
2. An integrable singularity at a point of the range. I kept the closed segment. A pointwise condition can't tell a convergent improper integral from a divergent one, and the closed reading is the one that never gives a divergent integral a value. The cost, ln(t) over [0; 1] read as undefined, is in the doc comment and in BREAKING-CHANGES.md, with a test pinned each way ([0; 1] false, [1; 2] true). Where the integral is worked out, it isn't affected: the derivative of 2 integral(x ln(t), t, 0, 1) is -2.

Also added, as you asked: the integral in both orders at 1/2 and at 2, symbolic limits, and 0 * sum(1/(k - x), k, 1, n) checked by value, with none at x = 1 and 0 at x = 1/2. The suite passes, 14,208, none failed.

[Rafael-SOWNet]

Both points are addressed in 8d8d3e8. Numeric limits are put in order, and symbolic ones become the values between them in either order. The closed-segment reading is stated as sufficient, not necessary, and ln(t) is pinned over [0; 1] and [1; 2]. The 0 * sum case is now asserted by value. Looks right to me. The union this exposed, [0; 1] \/ [1; 0] giving { 1 }, is #1634, and I'm taking it.

[Rafael-SOWNet]

The native builds failed on the previous head: IL3050 in GenericTensor's expression compiler. The Sylvester determinant for a q of degree above one was a MathS.Matrix of entities, and that is reached from DomainCondition, which every node has. Fixed in the new head. Past a linear, the resultant is now taken only for rational coefficients, where it is a number and only its being zero matters, by Bareiss's elimination in whole numbers. A symbolic q of higher degree is left to forall. Locally, the native publish of AngouriMath.CPP.Exporting for linux-x64 compiles, and the suite passes: 14,208, none failed.