Integrality and supercongruences of the factorial ratio $\frac{(6n)! n!}{(3n)! (2n)!^2}$

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

/-!
# Integrality and supercongruences of the factorial ratio $\frac{(6n)! n!}{(3n)! (2n)!^2}$

Integral factorial ratio sequence:
$$a(n) = \frac{(30n)! n!}{(15n)! (10n)! (6n)!}$$

*References:*
- [A211417](https://oeis.org/A211417)
- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al.
-/

namespace OeisA211417


/--
Integral factorial ratio sequence:
$$a(n) = \frac{(30n)! n!}{(15n)! (10n)! (6n)!}$$
-/
def a (n : ℕ) : ℕ :=
  (Nat.factorial (30 * n) * Nat.factorial n) /
  (Nat.factorial (15 * n) * Nat.factorial (10 * n) * Nat.factorial (6 * n))

open Nat Int Finset

def coprimeIndices (r : ℕ) : Finset ℕ :=
  (Finset.range (r + 1)).filter (fun i => 1 ≤ i ∧ Nat.gcd i 30 = 1)

/--
The product term in the denominator of the general conjecture:
$$\prod_{i = 1..r, i \text{ coprime to } 30} (30n - i)$$
We define this in ℤ to handle the $n=0$ case where $30n-i$ in the product might be negative.
-/
def divisorProduct (n r : ℕ) : ℤ :=
  (coprimeIndices r).prod (fun i : ℕ => 30 * (n : ℤ) - (i : ℤ))


@[category test, AMS 11]
lemma a_0 : a 0 = 1 := by rfl

@[category test, AMS 11]
lemma a_1 : a 1 = 77636318760 := by rfl

@[category test, AMS 11]
lemma a_2 : a 2 = 53837289804317953893960 := by rfl

@[category test, AMS 11]
lemma a_3 : a 3 = 43880754270176401422739454033276880 := by rfl

@[category test, AMS 11]
lemma a_4 : a 4 = 38113558705192522309151157825210540422513019720 := by rfl


/--
It appears that $a(n)/(30n - 1)$ is integral for all $n$ (checked up to $n = 1000$). - _Peter Bala_, Aug 28 2025

A formal proof has been found with the methods described in
[arxiv/2605.22763](https://arxiv.org/abs/2605.22763).
-/
@[category research solved, AMS 11, formal_proof using formal_conjectures at
"https://github.com/mo271/formal-conjectures/blob/a32396489dcb8f86c3549b93aa358ac6a10a3a1f/FormalConjectures/OEIS/211417.wip.lean#L243"]
theorem thirty_mul_sub_one_dvd_a (n : ℕ) : (30 * (n : ℤ) - 1) ∣ (a n : ℤ) := by
    sorry

/--
Conjecture: "7*a(n)/(2*n + 1) ... [is an] integer for all n (checked up to n = 1000)."
- _Peter Bala_, Aug 28 2025
-/
@[category research solved, AMS 11,
  formal_proof using lean4 at
    "https://github.com/KitaKen1/oeis-a211417/blob/cad1fb228b5b80573cab3eeb92c8be57fd73c506/lean/OeisA211417FC.lean#L866-L868"]
theorem seven_mul_a_dvd_two_mul_add_one (n : ℕ) :
    (2 * (n : ℤ) + 1) ∣ 7 * (a n : ℤ) := by
  sorry

/--
Conjecture: "a(n)/(3*n + 1) ... [is an] integer for all n (checked up to n = 1000)."
- _Peter Bala_, Aug 28 2025
-/
@[category research solved, AMS 11,
  formal_proof using lean4 at
    "https://github.com/KitaKen1/oeis-a211417/blob/cad1fb228b5b80573cab3eeb92c8be57fd73c506/lean/OeisA211417FC.lean#L1173-L1175"]
theorem a_dvd_three_mul_add_one (n : ℕ) :
    (3 * (n : ℤ) + 1) ∣ (a n : ℤ) := by
  sorry

/--
Conjecture: "a(n)/(5*n + 1) ... [is an] integer for all n (checked up to n = 1000)."
- _Peter Bala_, Aug 28 2025
-/
@[category research solved, AMS 11,
  formal_proof using lean4 at
    "https://github.com/KitaKen1/oeis-a211417/blob/cad1fb228b5b80573cab3eeb92c8be57fd73c506/lean/OeisA211417FC.lean#L1446-L1448"]
theorem a_dvd_five_mul_add_one (n : ℕ) :
    (5 * (n : ℤ) + 1) ∣ (a n : ℤ) := by
  sorry

/--
Conjecture: "42*a(n)/((2*n + 1)*(3*n + 1)*(5*n + 1)) [is an] integer for all n
(checked up to n = 1000)." - _Peter Bala_, Aug 28 2025
-/
@[category research solved, AMS 11,
  formal_proof using lean4 at
    "https://github.com/KitaKen1/oeis-a211417/blob/cad1fb228b5b80573cab3eeb92c8be57fd73c506/lean/OeisA211417FC.lean#L1514-L1524"]
theorem forty_two_mul_a_dvd_product (n : ℕ) :
    ((2 * (n : ℤ) + 1) * (3 * (n : ℤ) + 1) * (5 * (n : ℤ) + 1)) ∣
      42 * (a n : ℤ) := by
  sorry

/--
Conjecture: "More generally, for r >= 1, we conjecture that there exists a constant D(r) such that
D(r)*a(n)/Product_{i = 1..r, i coprime to 30} (30*n - i) is integral for all n."
- _Peter Bala_, Aug 28 2025

This generalizes `thirty_mul_sub_one_dvd_a` (the $r = 1$ case where $D(1) = 1$).

**Proof sketch** (kernel-checked development at the `formal_proof` permalink below, which
proves the non-vacuous form with the explicit positive witness $D = (r!)^{r^2}$):
Legendre-valuation analysis of the Landau step function
$\Delta(x) = \lfloor 30x \rfloor + \lfloor x \rfloor - \lfloor 15x \rfloor -
\lfloor 10x \rfloor - \lfloor 6x \rfloor$, whose values lie in $\{0, 1\}$. Three
ingredients: a unit-class rigidity lemma ($\Delta_c = 1$ for every unit class $c$ modulo
$30$), a witness-uniqueness bound for prime powers $p^k > r$ (at most one factor of the
divisor product is divisible by $p^k$), and a uniform low-layer budget for $p^k \le r$
absorbed by the witness constant.
-/
@[category research solved, AMS 11, formal_proof using formal_conjectures at
"https://github.com/chy4pro/formal-conjectures/blob/fbc6706451b0e80787580d91ee6c252c121e0165/FormalConjectures/OEIS/211417.lean#L651"]
theorem general_divisibility (r : ℕ) (hr : 1 ≤ r) :
    ∃ D : ℤ, 0 < D ∧ ∀ n : ℕ, (divisorProduct n r) ∣ (D * (a n : ℤ)) := by
  sorry

/--
Supercongruence: "a(p^k) == a(p^(k-1)) ( mod p^(3*k) ) for any prime p >= 5 and any positive
integer k." - _Peter Bala_, Jan 24 2020

More generally, "the congruences a(n*p^k) == a(n*p^(k-1)) ( mod p^(3*k) ) may hold for any
prime p >= 5 and any positive integers n and k."
-/
@[category research open, AMS 11]
theorem supercongruence (p k : ℕ) (hp : p.Prime) (hp5 : 5 ≤ p) (hk : 0 < k) :
    (p : ℤ) ^ (3 * k) ∣ ((a (p ^ k) : ℤ) - (a (p ^ (k - 1)) : ℤ)) := by
  sorry

end OeisA211417

• Formalization source ↗

On-site verification needs an executable Lean target. None is attached yet.

A source attachment or link is not a verified proof. The statement’s correspondence with the original question needs human review.