The binomial coefficient's identities as rules, and its sums in closed form

[Rafael-SOWNet]

Item 7 of the docket on #1409, the identities of §8.4 (Sullivan and Mackey).

Three rules in the factorial-gathering set, each in the direction that collects, so the book's identities are True as statements of symbols (Props 8.4.1–8.4.3, which the book proves by counting in two ways; here they are identities of the falling factorial for a whole lower index and of the gamma function elsewhere):

rule	rewrite	Simplify
Pascal	binomial(n - 1, k) + binomial(n - 1, k - 1) → binomial(n, k) (either order, the lower index one less found by simplifying the difference)	binomial(n + 1, k + 1) = binomial(n, k + 1) + binomial(n, k) → True
chairperson	n binomial(n - 1, k - 1) → k binomial(n, k)	k binomial(n, k) = n binomial(n - 1, k - 1) → True
symmetry	binomial(n, n - k) → binomial(n, k) where the complement is the smaller expression (binomial(n, 2) stays)	binomial(n, k) = binomial(n, n - k) → True

A binomial coefficient is three factorials, and the simplifier runs the factorial sets on an expression holding one (it gated them on Factorialf alone). The binomial-sum evaluator reads the coefficient written as the node, binomial(N, k) or binomial(N, N - k), beside the factorial spelling it read already: sum(binomial(n, k), k, 0, n) is 2^n, with 2^(n-k) it is 3^n (Try 3), with x^k y^(n-k) it is (x + y)^n (Thm 8.4.8), each provided n >= 0.

Wrong answer fixed on the way, in both spellings (Ex 8.4.9): the alternating sum is 0^n, which is 1 at n = 0 and 0 above it; written as the power it carried a condition that the piecewise read as "no value", so sum(n!/(k!(n − k)!) (−1)^k, k, 0, n) was piecewise(0 provided True) — 0 at n = 0 where it is 1. A base that simplifies to zero is said outright: piecewise(1 provided n = 0, 0 provided True).

Counts: 335 rules, 306 names, 332 identities, 149 conditional, 126 at Unknown growth (the three are code replacements that fire on a condition the helper decides), 969 subsumption claims. BinomialIdentityTest, 20 rows. BREAKING-CHANGES.md rows measured on a v2.5.0 build. Full suite 12246 passed, 0 failed; benchmark gate PASSED (SimplifyHard and SimplifyEasy the same bytes as the baseline).

One thing left open, by design: k binomial(n, k) − n binomial(n − 1, k − 1) as a difference simplifies to 0 in one order of the two terms and not the other (a tie-break in the candidate ranking); the identity as an equality decides either way, which is what the book states.

Part of #1409.

🤖 Generated with Claude Code

https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura