The Franel numbers satisfy a second-order recurrence

Identifier: F:franel-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 Franel numbers S(n) = sum over all integers k of C(n,k)^3 satisfy (n+2)^2 * S(n+2) = (7n^2 + 21n + 16) * S(n+1) + 8(n+1)^2 * S(n). Only the RECURRENCE is claimed: the Franel numbers have no hypergeometric closed form, so there is nothing further to establish here.

Formal statement

(define-hyperterm F (* (gamma (+ n 1)) (/ 1 (gamma (+ k 1))) (/ 1 (gamma (+ (- n k) 1)))))
(define-fn S (lambda (n) (sum ((k Int)) (^ F 3))))
(assert (forall ((n Int)) (= (* (^ (+ n 2) 2) (S (+ n 2)))
                             (+ (* (+ (* 7 (^ n 2)) (* 21 n) 16) (S (+ n 1)))
                                (* 8 (^ (+ n 1) 2) (S n))))))

Dependencies

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

0 direct dependencies 0 direct dependents

Evidence

wz-franel-order-two

Kind: witness-replay
Status: checked

Supports: an order-TWO 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 franel_numbers_get_an_order_two_recurrence

Evidence notes

The first order-2 (J >= 2) certificate on this route. The sweep-based search that established the earlier binomial facts DECLINED on this summand after 9.8 s of release-build search, because the certificate numerator has degree 3 in k with coefficients of degree 5 in n and the old ansatz swept total degree over all variables. Deriving the denominator and the k-degree from the Gosper-Petkovsek normal form reduces the whole search to three linear systems and finds it in 86 ms. The test also replays the recurrence against the Franel numbers 1, 2, 10, 56, 346, 2252, 15184 in i128 arithmetic, which is a separate check from the certificate.

cas-certificate-artifact-franel-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 telescoping-scale: axeyum_cas::telescoping::zeilberger (untrusted Gosper-Petkovsek search) + axeyum_cas::telescoping_check (independent checker)",
  "source": "classical; the summand stated by this lane as a HyperTerm specification",
  "prior_art": [
    {
      "who": "J. Franel",
      "what": "the recurrence for sum_k C(n,k)^3",
      "year": 1894,
      "where": "L'Intermediaire des Mathematiciens 1 (1894), 45-47; see also OEIS A000172 and Petkovsek-Wilf-Zeilberger, A=B (1996)",
      "attribution": "standard textbook attribution; this lane did not consult the primary source"
    }
  ]
}