In the book "A = B" by Petkovesk, Wilf, and Zeilberger, (downloadable here), the authors provide several algorithmic methods for finding closed forms or recurrences for sums involving e.g. binomial coefficients. Even more exciting, their methods provide seemingly short certificates for the truth of these computer-verified claims. In particular, the WZ method prints a single rational function as such a certificate.
In more detail, here is the broad outline of the WZ method, where I directly quote from page 25 of "A = B":
- Suppose that you wish to prove an identity of the form $\sum_k t(n, k) = rhs(n)$, and let’s assume, for now, that for each n it is true that the summand $t(n, k)$ vanishes for all $k$ outside of some finite interval.
- Divide through by the right hand side, so the identity that you wish to prove now reads as $\sum_k F (n, k) = 1$, where $F (n, k) = t(n, k)/rhs(n)$.
- Let $R(n, k)$ be the rational function that the WZ method provides as the proof of your identity (this is described in Chapter 7 of "A=B"). Define a new function $G(n, k) = R(n, k)F (n, k).$
- You will now observe that the equation $$F (n + 1, k) − F (n, k) = G(n, k + 1) − G(n, k)$$ is true. Sum that equation over all integers $k$, and note that the right side telescopes to 0. The result is that $$\sum_k F (n + 1, k) = \sum_k F (n, k),$$ hence we have shown that $\sum_k F (n, k)$ is independent of $n$, i.e., is constant.
- Verify that the constant is $1$ by checking that $F (0, k) = 1$.
What I want to know is:
Are there known bounds on the length of these certificates $R(n, k)$, in terms of the length of the description of the combinatorial sum in question? If so, what are they?