The Chu-Vandermonde convolution satisfies a first-order recurrence in p

Identifier: F:chu-vandermonde-convolution-recurrence
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 symbolic m and n and every integer p, the convolution S(p) = sum over all integers k of C(m,k)*C(n,p-k) satisfies (p+1)*S(p+1) = (m+n-p)*S(p). This is the recurrence C(m+n,p) also satisfies; together with S(0) = 1 it yields Chu-Vandermonde, sum_k C(m,k)*C(n,p-k) = C(m+n,p). Only the RECURRENCE is claimed by this fact; the closed form is F:chu-vandermonde-convolution, which adds the symbolic base case.

Formal statement

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

Dependencies

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

0 direct dependencies 1 direct dependents

Evidence

wz-chu-vandermonde-recurrence

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 = m + n - p, a_1 = -(p + 1), R(p,k) = k*(k + n - p) / (p - k + 1). The certificate identity is symbolic in ALL of m, n, p, k -- four variables -- so the recurrence is established for symbolic m and n, not merely at sample values. The closed form is not claimed by this fact; turning the recurrence into C(m+n,p) needs the base case S(0) = 1 at symbolic m and n, which lane `telescoping-scale` later established -- see F:chu-vandermonde-convolution.

cas-certificate-artifact-chu-vandermonde-convolution

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": "Chu Shih-Chieh; Vandermonde",
      "what": "the convolution identity",
      "year": 1772,
      "where": "classical; see Petkovsek-Wilf-Zeilberger, A=B (1996), ch. 4-7",
      "attribution": "standard textbook attribution; this lane did not consult the primary source"
    }
  ]
}