[Rafael-SOWNet]

The sum of the first n odd numbers came out as piecewise((2 * n + (n - 1) ^ 2 - 1) provided (n - 1 >= -1), 0 provided True). Sullivan and Mackey write it n^2, and the condition means n >= 0. Prob 5.7.16's sum(2 k + 1, k, n, 2 n - 1) came out as 2 * n + (2 * n - 1) ^ 2 - (n - 1) ^ 2 under 2 * n - 1 >= n - 1, where the book writes 3 n^2.

Two changes, both where the closed form is made:

• Multiplied out where that rates simpler (PolynomialSummation.Simplest). A polynomial sum's closed form, and a polynomial times a power's, is kept expanded where its SimplifiedRate is lower. So the odd-number sums are n ^ 2 and 3 * n ^ 2, while sum(k, k, 1, n) keeps (n + n ^ 2) / 2. Simplify is untouched. Making it expand under conditions got the same forms, but it made SimplifyEasy allocate 5.4% more, because that benchmark's x ^ 0 becomes 1 provided not x = 0, and expanding every conditional polynomial made each one a fresh candidate.
• The range condition is a bound on its name (PolynomialSummation.NonEmpty and AtLeast, shared by the seven closed-form routines). A range is not empty where to >= from - 1, which was written as the ends left it. Where the two ends are about one name, it is now a bound on that name: n - 1 >= -1 is n >= 0, and product(2^k, k, 0, n - 1)'s n - 1 >= 0 is n >= 1. With two names it is left as it was, n >= m - 1.

AClosedFormReadsAsTheBookWritesIt and TheRangeConditionIsABoundOnItsName pin both, with the printed form asserted, since the printed form is the point here.

Suite: 13,750 passed, 0 failed on net10.0, and every target framework builds. Gate: passed, with allocation as the baseline says on all 19 gated benchmarks (SimplifyEasy at 79,010 B).

BREAKING-CHANGES.md has the entry, after the one for products of powers of one base, whose product(2^k, k, 0, n - 1) row now reads n >= 1, and 2.5.0 is measured.

Part of #1409.

🤖 Generated with Claude Code

https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura