The binomial sums of chapter 8 are answered in closed form

[Rafael-SOWNet]

Chapter 8 of Sullivan and Mackey's An Introduction to Proofs (#1409): the binomial sums beyond the binomial theorem, which BinomialSum already reads (sum(binomial(n, k) x^k y^(n − k), k, 0, n) is (x + y)^n; 3^n and 4^n for the 2^(n−k) and 3^k weights; 0 for the alternating sum). Re-measured against master, the rest of the chapter's identity rows were left as written; BinomialIdentities answers them:

• A polynomial in the index beside the coefficient (Prop 8.4.4, §8.4.5 Try 2): read in the falling factorial basis by the Stirling numbers of the second kind, because k^(j falling) binomial(n, k) is n^(j falling) binomial(n − j, k − j) — the chairperson identity j times — and what is left is the binomial theorem. sum(k binomial(n, k), k, 0, n) is n 2^(n − 1), sum(k^2 binomial(n, k)) is n 2^(n−1) + n(n − 1) 2^(n−2), and the same beside x^k y^(n − k). The coefficient as its three factorials is read too, with the top one folded into a number where the bound is concrete, as BinomialSum does.
• Vandermonde (Prob 8.9.16): sum(binomial(a, i) binomial(b, k − i), i, 0, k) is binomial(a + b, k), the range written to k, a or b (the terms outside are zero), and the square case sum(binomial(n, k)^2, k, 0, n) is binomial(2 n, n) (Prob 8.9.34).
• The summation identity (Thm 8.4.6): sum(binomial(i, k), i, 0, n) is binomial(n + 1, k + 1).
• The sums over the even or the odd indices (Ex 8.3.11): sum(binomial(n, 2l), l, 0, floor(n/2)) and sum(binomial(n, 2l + 1), l, 0, floor((n − 1)/2)) are each 2^(n − 1) for n ≥ 1, with the even sum 1 and the odd sum empty at n = 0 — the book leaves the even sum's closed form open.

Under forall the identities are decided from the closed forms: forall n in ZZ+ : sum(k binomial(n, k), k, 0, n) = n 2^(n − 1), forall n in ZZ* : sum(binomial(n, k)^2, k, 0, n) = binomial(2 n, n) and the summation identity are True.

BinomialSumTest loses sum(N!/(k!(N−k)!) k, k, 0, N) from its "not of the shape" rows, since it is closed now; Syntax.md and BREAKING-CHANGES.md updated (the 2.5.0 column measured on a build of v2.5.0: the factorial spelling as written, binomial did not parse).

Tests: BinomialIdentitiesTest — ten closed forms checked against the expanded sum at six bounds including one past the hundred-term expansion, Vandermonde with both parameters free at four triples and two spellings of the range, the parity sums at zero, and the three identities under forall. Full suite 12567 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