The cross binomial row sum equals a central binomial coefficient

Identifier: F:cross-binomial-row-sum
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, cas.symbolic-gamma-arguments-avoid-poles

Recorded description

For symbolic m and every integer n >= 0, sum over all integers k of C(m,k)*C(n,k) = C(m+n,n). This is the Vandermonde form with both binomials sharing the summation index; m stays symbolic throughout, recurrence and base case alike.

Formal statement

(define-hyperterm F (* (gamma (+ m 1)) (/ 1 (gamma (+ k 1))) (/ 1 (gamma (+ (- m k) 1)))
                       (gamma (+ n 1)) (/ 1 (gamma (+ k 1))) (/ 1 (gamma (+ (- n k) 1)))))
(define-hyperterm T (* (gamma (+ (+ m n) 1)) (/ 1 (gamma (+ n 1))) (/ 1 (gamma (+ m 1)))))
(define-fn S (lambda (n) (sum ((k Int)) F)))
(assert (forall ((m Int) (n Int)) (=> (>= n 0) (= (S n) T))))

Dependencies

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

0 direct dependencies 0 direct dependents

Evidence

wz-cross-binomial-row-sum

Kind: witness-replay
Status: checked

Supports: the creative-telescoping certificate plus the symbolic base case, both replayed by a checker that shares no code with the search that produced them

Checker command

cargo test -p axeyum-cas --test telescoping_identities cross_binomial_sum_is_a_central_binomial

Evidence notes

Order-1 certificate in n with m symbolic. The base case at n = 0 collapses to the single point k = 0 by the parameter-free factors Gamma(k+1)^-2 (k >= 0) and Gamma(n-k+1)^-1 at n = 0 (k <= 0); the remaining Gamma powers cancel to the rational 1, matching C(m+0,0) = 1. Every other window point is checked to vanish.

cas-certificate-artifact-cross-binomial-row-sum

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-scale: axeyum_cas::telescoping::zeilberger (untrusted Gosper-Petkovsek search) + axeyum_cas::telescoping_check (independent checker)",
  "source": "classical binomial identity, stated by this lane as a HyperTerm specification",
  "prior_art": [
    {
      "who": "Vandermonde",
      "what": "the convolution identity in its equal-index form",
      "year": 1772,
      "where": "classical; see Graham-Knuth-Patashnik, Concrete Mathematics (1994), sec. 5.1, and Petkovsek-Wilf-Zeilberger, A=B (1996)",
      "attribution": "standard textbook attribution; this lane did not consult the primary source"
    }
  ]
}