Numerator of $sum_{k = 1}^n \frac{1}{k^3} * \binom{n}{k}^2 * \binom{n+k}{k}^2 for $n \ge 1$ with $a(0) = 0$.

Reference: A357513

def OeisA357513.a (n : ℕ) : ℕ

A357513: $a(n) = \text{numerator of } \sum_{k = 1..n} \frac{1}{k^3} \binom{n}{k}^2 \binom{n+k}{k}^2 \text{ for } n \ge 1 \text{ with } a(0) = 0$.

Equations

• OeisA357513.a n = (∑ k ∈ Finset.Icc 1 n, ↑(n.choose k) ^ 2 * ↑((n + k).choose k) ^ 2 / ↑k ^ 3).num.natAbs

theorem OeisA357513.zero : a 0 = 0

theorem OeisA357513.one : a 1 = 4

theorem OeisA357513.two : a 2 = 81

theorem OeisA357513.three : a 3 = 14651

theorem OeisA357513.four : a 4 = 956875

theorem OeisA357513.five : a 5 = 1335793103

theorem OeisA357513.a357513_supercongruence (p : ℕ) (hp : Nat.Prime p) (h_ge3 : p ≥ 3) (h_neq7 : p ≠ 7) : ↑(a (p - 1)) ≡ 0 [ZMOD ↑p ^ 4]

We have $a(p-1) \equiv 0 \pmod{p^4}$ for all primes $p \ge 3$ except $p=7$.

proved by AlphaProof

noncomputable def OeisA357513.u (m n : ℕ) : ℕ

Let m be a nonnegative integer and set $u(n) = $$the numerator of $$\sum{k=1}^{n} \frac{1}{k^{2m+1}} \binom{n}{k}^2 \binom{n+k}{k}^2$$ (seems like a typo in the OEIS entry: the sum starts with $k=0$ there. In order to avoid a division by zero, we replace start the sum at $k=1$.)

Equations

• OeisA357513.u m n = (∑ k ∈ Finset.Icc 1 n, ↑(n.choose k) ^ 2 * ↑((n + k).choose k) ^ 2 / ↑k ^ (2 * m + 1)).num.natAbs

theorem OeisA357513.general_supercongruence (m : ℕ) : ∃ (exceptions : Finset ℕ), ∀ (p : ℕ), Nat.Prime p → p ∉ exceptions → ↑(u m (p - 1)) = 0

We conjecture that $u(p-1) == 0 (mod p^4)$ for all primes $p$, with a finite number of exceptions that depend on $m$.

theorem OeisA357513.general_supercongruence_one_of_a357513_supercongruence : (∀ (p : ℕ), Nat.Prime p → p ≥ 3 → p ≠ 7 → ↑(a (p - 1)) ≡ 0 [ZMOD ↑p ^ 4]) → ∃ (exceptions : Finset ℕ), ∀ (p : ℕ), Nat.Prime p → p ∉ exceptions → ↑(u 1 (p - 1)) = 0