A sum of a polynomial times a power of the index is answered in closed form, and a quantified piecewise is decided by cases on a parameter

[Rafael-SOWNet]

Two things from chapter 5 of Sullivan and Mackey's An Introduction to Proofs (#1409), re-measured against master today: §5.3.4 Try 6, sum((-1)^(k - 1) k^2, k, 1, n) = (-1)^(n - 1) n (n + 1)/2, whose sum had no closed form, and Ex 5.2.6, the geometric sum with q = 1 set aside, which the induction route pinned as "left as written" because the closed form has a case on a free parameter.

PolynomialGeometricSeries — a summand that is a polynomial in the index times a power with the index in the exponent, p(k) C b^(m k + s), read the way GeometricSeries reads its own with the polynomial beside it. For a ratio r ≠ 1 there is a polynomial q of the same degree with q(k + 1) r − q(k) = p(k), so q(k) r^k is a discrete antiderivative and the sum from a to b is q(b + 1) r^(b + 1) − q(a) r^a; the coefficients come highest first by one division by r − 1 each (Gosper specialised to a constant-denominator term ratio). A symbolic ratio carries the case r = 1 as the polynomial reader's answer over the same range; to +oo the series converges for |r| < 1. sum(k 2^k, k, 1, n) is (n − 1) 2^(n + 1) + 2, sum(k / 2^k, k, 1, +oo) is 2, sum(k x^k, k, 0, +oo) is x/(1 − x)^2 provided |x| < 1.

A quantified piecewise decided by cases on a parameter — the sum with a symbolic ratio comes as piecewise(… provided (q = 1 and n >= 0), … provided (n >= 0), 0 provided True), and the decider's piecewise route could take a case only where its whole condition held at every member. A case whose condition is a hypothesis about a parameter beside a part that holds throughout is now decided under the hypothesis (with q := 1 substituted where it is an equation) and under its negation, and the statement holds provided the hypothesis where it holds there alone: forall n in ZZ+ : sum(q^i, i, 0, n − 1) = (q^n − 1)/(q − 1) is True provided not q = 1 — the book's own remark on why q = 1 is excluded. WithoutRepeatedExclusions writes not q = 1 and not 1 − q = 0 and not q − 1 = 0 once, by the root each excludes.

Two pinned verdicts move with it, both in InductionTest: forall n in ZZ+ : sum(k x^k, k, 1, n) = x(1 − (n + 1)x^n + n x^(n + 1))/(1 − x)^2 is now True provided not x = 1 (was True provided not (1 − x)^2 = 0, from the induction route's denominator; the sum's own case is the condition now), and the geometric-sum row leaves LeftAsWritten. GeometricSeriesTest loses sum(k (1/2)^k, k, 0, +oo) from its "not this reader's" rows, since it is summed now. Syntax.md and BREAKING-CHANGES.md updated (2.5.0 column measured: all three sums as written there; the quantifier did not parse).

Tests: PolynomialGeometricSeriesTest — closed forms checked against the expanded sum at six bounds including one past the hundred-term expansion, an empty range, four convergent series, the symbolic ratio with its q = 1 case, and the two book identities decided from the closed form. Full suite 12543 passed, 0 failed; the kernel gate PASSED on all 19 gated benchmarks.

Part of #1409.

🤖 Generated with Claude Code

https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura