The sum of squared binomial coefficients is the central binomial coefficient

Identifier: F:squared-binomial-row-sum-central
Proof route: cas-certificate
External status: proved
Axiom footprint: cas.exact-rational-polynomial-normal-form, cas.gamma-functional-equation, cas.hyperterm-specification-denotes-the-summand, cas.telescoped-term-natural-boundary

Recorded description

For every natural n, the sum over all integers k of C(n,k)^2 equals C(2n,n). The summand vanishes outside 0 <= k <= n.

Formal statement

(define-hyperterm F (* (^ (gamma (+ n 1)) 2) (/ 1 (^ (gamma (+ k 1)) 2)) (/ 1 (^ (gamma (+ (- n k) 1)) 2))))
(define-hyperterm T (* (gamma (+ (* 2 n) 1)) (/ 1 (gamma (+ n 1))) (/ 1 (gamma (+ n 1)))))
(assert (forall ((n Int)) (=> (>= n 0) (= (sum ((k Int)) F) T))))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

0 direct dependencies 0 direct dependents

Evidence

wz-squared-binomial-row-sum

Kind: witness-replay
Status: checked

Supports: the creative-telescoping certificate, replayed by a checker that shares no code with the search that produced it

Checker command

cargo test -p axeyum-cas --test telescoping_identities

Evidence notes

Certificate: order 1, recurrence coefficients a_0 = 4n + 2, a_1 = -(n + 1) (i.e. (n+1)*S(n+1) = (4n+2)*S(n)), R(n,k) = k^2*(3n + 3 - 2k) / (n - k + 1)^2. Closed form C(2n,n) verified to satisfy the same recurrence; base case S(0) = 1 = C(0,0) checked by exact summation; leading coefficient -(n+1) has its only integer zero at n = -1, below the base, so the recurrence runs forward from n = 0.

cas-certificate-artifact-squared-binomial-row-sum-central

Kind: witness-replay
Status: checked

Supports: the serialised certificate itself, re-checked from the committed file with no search run

Checker command

cargo test -p axeyum-cas --test telescoping_certificate_artifacts

Evidence notes

This row exists so the fact rests on an ARTIFACT rather than on re-running the producer. The sweep reads every committed certificate, parses it, and hands it to the independent checker; nothing in that path calls the search. Tamper controls in the same file: a certificate numerator edited by one, a recurrence coefficient edited by one, and a certificate re-pointed at a neighbouring file's summand are each rejected, and a truncated / foreign-format / decimal-bearing file is refused by the reader before the checker sees it.

Provenance

{
  "date": "2026-08-14",
  "established_by": "lane telescoping: axeyum_cas::telescoping::zeilberger (untrusted search) + axeyum_cas::telescoping_check (independent checker)",
  "source": "classical binomial identity, stated by this lane as a HyperTerm specification",
  "prior_art": [
    {
      "who": "Attributed to standard combinatorial identity (Vandermonde specialisation)",
      "what": "the squared-binomial row-sum identity",
      "year": 1991,
      "where": "classical; see Petkovsek-Wilf-Zeilberger, A=B (1996), ch. 4-7",
      "attribution": "standard textbook attribution; this lane did not consult the primary source"
    }
  ]
}