The Apery numbers satisfy Apery's second-order recurrence

Identifier: F:apery-numbers-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 every integer n, the Apery numbers A(n) = sum over all integers k of C(n,k)^2 * C(n+k,k)^2 satisfy (n+1)^3 * A(n) - (2n+3)(17n^2 + 51n + 39) * A(n+1) + (n+2)^3 * A(n+2) = 0. Only the RECURRENCE is claimed. The Apery numbers have no hypergeometric closed form, so there is nothing further of that kind to establish; and the irrationality of zeta(3), which this recurrence was invented to prove, is emphatically NOT claimed here -- that argument needs the second solution of the same recurrence and a growth estimate, neither of which this route produces.

Formal statement

(define-hyperterm F (* (gamma (+ n 1)) (/ 1 (gamma (+ k 1))) (/ 1 (gamma (+ (- n k) 1)))))
(define-hyperterm G (* (gamma (+ n k 1)) (/ 1 (gamma (+ k 1))) (/ 1 (gamma (+ n 1)))))
(define-fn S (lambda (n) (sum ((k Int)) (* (^ F 2) (^ G 2)))))
(assert (forall ((n Int)) (= 0 (+ (* (^ (+ n 1) 3) (S n))
                                 (* -1 (+ (* 2 n) 3) (+ (* 17 (^ n 2)) (* 51 n) 39) (S (+ n 1)))
                                 (* (^ (+ n 2) 3) (S (+ n 2)))))))

Dependencies

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

0 direct dependencies 0 direct dependents

Evidence

wz-apery-order-two

Kind: witness-replay
Status: checked

Supports: an order-TWO creative-telescoping certificate for the deepest summand this route has reached, replayed by a checker that shares no code with the search that produced it

Checker command

cargo test -p axeyum-cas --test telescoping_identities apery_numbers_get_aperys_own_recurrence

Evidence notes

This summand DECLINED before the multivariate GCD moved out of i128, and the reason was measured rather than guessed: the derived degree bound is 2, which is exactly where the certificate lives, so the search design was never at fault. What failed was the primitive pseudo-remainder sequence reducing the degree-8 shift quotient -- `MvPoly::gcd_cost` reports that sequence passing through a 4187-bit coefficient, against the 127 bits an i128 numerator holds, to produce a GCD whose own coefficients fit in three. The search now finds the certificate in 90 ms. The test also replays the recurrence against the Apery numbers 1, 5, 73, 1445, 33001, 819005, 21460825 in i128 arithmetic, which is a check separate from the certificate. One detail of the check options is load-bearing and deliberate: the summation window starts at k = 0 rather than at a negative k, because at n = 0 the summand is not evaluable at a negative k (C(n+k,k) becomes C(-1,-1)) and the checker refuses a window edge it cannot evaluate. The certificate numerator carries a factor k^4, so the telescoped term still vanishes at that edge, which is what the boundary layer requires.

cas-certificate-artifact-apery-numbers-recurrence

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 mvpoly-bignum: axeyum_cas::telescoping::zeilberger (untrusted Gosper-Petkovsek search) + axeyum_cas::telescoping_check (independent checker), unblocked by moving MvPoly::gcd into an unbounded-integer ring",
  "source": "classical; the summand stated by this lane as a HyperTerm specification",
  "prior_art": [
    {
      "who": "R. Apery",
      "what": "the recurrence for sum_k C(n,k)^2*C(n+k,k)^2, and the irrationality of zeta(3) that follows from it",
      "year": 1979,
      "where": "Irrationalite de zeta(2) et zeta(3), Asterisque 61 (1979), 11-13",
      "attribution": "standard textbook attribution; this lane did not consult the primary source"
    },
    {
      "who": "A. van der Poorten",
      "what": "the expository reconstruction of Apery's proof that made the recurrence widely known",
      "year": 1979,
      "where": "A proof that Euler missed, Mathematical Intelligencer 1 (1979), 195-203",
      "attribution": "standard textbook attribution; this lane did not consult the primary source"
    },
    {
      "who": "Zeilberger",
      "what": "the creative-telescoping algorithm that mechanically produces this recurrence",
      "year": 1991,
      "where": "The method of creative telescoping, J. Symbolic Computation 11 (1991), 195-204; see also Petkovsek-Wilf-Zeilberger, A=B (1996), ch. 6",
      "attribution": "standard textbook attribution; this lane did not consult the primary source"
    }
  ]
}