Metadata
bibkey: mathar2020a308815
authors: R. J. Mathar; OEIS Foundation Inc.
year: 2020
title: OEIS A308815 — D-finite recurrence for alternating Catalan numbers
doi: null
url: https://oeis.org/A308815
claim: Mathar conjectures the order-three polynomial-coefficient recurrence for the alternating Catalan numbers defined by the entry's PARI formula.
strata_touched:
- D5/S1/Recurrence/A308815DFiniteRecurrence
license: citation-only
triage: anchor
Verified locator
Source: https://oeis.org/A308815
The source has no page numbers. Its FORMULA section contains this sentence:
Conjecture: D-finite with recurrence: n*(2n+1)a(n) -32(9n-4)(n-1)a(n-1) +1024(3n^2-23n+29)a(n-2) +65536(n-2)(2*n-5)*a(n-3)=0. - R. J. Mathar, Jan 27 2020
Its PARI program defines the sequence by:
a(n) = 16^nsum(i=0, n, (-2)^ibinomial(n, i)C(2n-i));
Here C is the Catalan sequence. The NAME line instead prints:
a(n) = 16^nSum_{i=0..n} 2^ibinomial(n, i)Catalan(2n-i).
The minus sign in the PARI formula agrees with the data beginning
1,0,512,32768,3014656. The Lean sequence uses that formula with Mathlib’s
catalan, integer values and natural indices. The recurrence starts at n ≥ 3;
its polynomial coefficients are integers and its lagged indices are natural
subtractions.
Mathematical use
The coefficient of degree 2n in (1-2X)^n C(X) is the unscaled binomial
sum. A formal-series differential certificate annihilates that coefficient
and yields the recurrence after multiplication by 16^n.
The experiment entry is
docs/reports/oeis-a308815-dfinite-recurrence/check.py,
SHA256 d40f575913a33fcb60a373cfb2fb8bb80028ea340c3d255f780a485d87e6477b.
The reported command python3 check.py exits zero with bad= 0: the signed
formula matches all 17 displayed terms and the recurrence holds for
3 ≤ n ≤ 300. These finite readings are separate from the Lean proof for all
n ≥ 3.