Tuples of ℓ-regular partitions

DefinitionNumber of \(\ell\)-regular partitions#✓fully proved

For natural numbers \(\ell\) and \(n\), the number of \(\ell\)-regular partitions of \(n\) is the number of partitions of \(n\) none of whose parts is divisible by \(\ell\).

public def lRegularPartitionCount (ℓ n : ℕ) : ℕ :=
  ((Finset.univ : Finset (Nat.Partition n)).filter fun p => ∀ a ∈ p.parts, ¬ ℓ ∣ a).card

Sources

• Bishnu Paudel, James A. Sellers, and Haiyang Wang, Extending Recent Work of Nath, Saikia, and Sarma on k-Tuple ℓ-Regular Partitions, INTEGERS 26 (2026), Article A4, Introduction (definition of ℓ-regular partitions).

Used by 4

Used byNumber of \(k\)-tuples of \(\ell\)-regular partitions · One tuple of \(\ell\)-regular partitions of total zero · Recurrence for tuples of \(\ell\)-regular partitions · Zero has one \(\ell\)-regular partition

DefinitionNumber of \(k\)-tuples of \(\ell\)-regular partitions#✓fully proved

For natural numbers \(\ell\), \(k\) and \(n\), the number \(T_{\ell,k}(n)\) is defined by recursion on \(k\): \(T_{\ell,0}(n)\) is \(1\) if \(n = 0\) and \(0\) otherwise, and

\[T_{\ell,k+1}(n) = \sum_{i=0}^{n} r_\ell(i) \, T_{\ell,k}(n-i),\]

where \(r_\ell(i)\) is the number of \(\ell\)-regular partitions of \(i\).

Peeling off the first component in this way, \(T_{\ell,k}(n)\) counts the \(k\)-tuples \((\lambda_1, \dots, \lambda_k)\) of \(\ell\)-regular partitions of \(n_1, \dots, n_k\) with \(n_1 + \dots + n_k = n\).

public def kTupleRegularPartitionCount (ℓ : ℕ) : ℕ → ℕ → ℕ
  | 0, n => if n = 0 then 1 else 0
  | k + 1, n => ∑ i ∈ Finset.range (n + 1),
      lRegularPartitionCount ℓ i * kTupleRegularPartitionCount ℓ k (n - i)

Sources

• Bishnu Paudel, James A. Sellers, and Haiyang Wang, Extending Recent Work of Nath, Saikia, and Sarma on k-Tuple ℓ-Regular Partitions, INTEGERS 26 (2026), Article A4, Introduction (definition of T_{ℓ,k}).

Uses 1 · Used by 5

Statement usesNumber of \(\ell\)-regular partitions

Used byOne tuple of \(\ell\)-regular partitions of total zero · Recurrence for tuples of \(\ell\)-regular partitions · The empty tuple of \(\ell\)-regular partitions · Prime-power congruences for \(k\)-tuples of \(\ell\)-regular partitions · Triples of \(\ell\)-regular partitions

TheoremThe empty tuple of \(\ell\)-regular partitions#✓fully proved

For all natural numbers \(\ell\) and \(n\), writing \(T_{\ell,k}(n)\) for the number of \(k\)-tuples of \(\ell\)-regular partitions with total \(n\), we have \(T_{\ell,0}(n) = 1\) if \(n = 0\) and \(T_{\ell,0}(n) = 0\) otherwise.

public theorem kTupleRegularPartitionCount_zero (ℓ n : ℕ) :
    kTupleRegularPartitionCount ℓ 0 n = if n = 0 then 1 else 0

Sources

• Bishnu Paudel, James A. Sellers, and Haiyang Wang, Extending Recent Work of Nath, Saikia, and Sarma on k-Tuple ℓ-Regular Partitions, INTEGERS 26 (2026), Article A4, Introduction (definition of T_{ℓ,k}).

Uses 1

Statement usesNumber of \(k\)-tuples of \(\ell\)-regular partitions

TheoremRecurrence for tuples of \(\ell\)-regular partitions#✓fully proved

For all natural numbers \(\ell\), \(k\) and \(n\), writing \(r_\ell(i)\) for the number of \(\ell\)-regular partitions of \(i\) and \(T_{\ell,k}(n)\) for the number of \(k\)-tuples of \(\ell\)-regular partitions with total \(n\),

\[T_{\ell,k+1}(n) = \sum_{i=0}^{n} r_\ell(i) \, T_{\ell,k}(n-i).\]

public theorem kTupleRegularPartitionCount_succ (ℓ k n : ℕ) :
    kTupleRegularPartitionCount ℓ (k + 1) n = ∑ i ∈ Finset.range (n + 1),
      lRegularPartitionCount ℓ i * kTupleRegularPartitionCount ℓ k (n - i)

Sources

• Bishnu Paudel, James A. Sellers, and Haiyang Wang, Extending Recent Work of Nath, Saikia, and Sarma on k-Tuple ℓ-Regular Partitions, INTEGERS 26 (2026), Article A4, Introduction (definition of T_{ℓ,k}).

Uses 2

Statement usesNumber of \(k\)-tuples of \(\ell\)-regular partitions · Number of \(\ell\)-regular partitions

DefinitionTriples of \(\ell\)-regular partitions#✓fully proved

For natural numbers \(\ell\) and \(n\), \(T_\ell(n) = T_{\ell,3}(n)\) is the number of triples \((\lambda_1, \lambda_2, \lambda_3)\) of \(\ell\)-regular partitions (partitions with no part divisible by \(\ell\)) whose sizes add up to \(n\).

public def tripleRegularPartitionCount (ℓ n : ℕ) : ℕ :=
  kTupleRegularPartitionCount ℓ 3 n

Sources

• Bishnu Paudel, James A. Sellers, and Haiyang Wang, Extending Recent Work of Nath, Saikia, and Sarma on k-Tuple ℓ-Regular Partitions, INTEGERS 26 (2026), Article A4, Introduction (definition of T_ℓ).

Uses 1 · Used by 5

Statement usesNumber of \(k\)-tuples of \(\ell\)-regular partitions

Used byThe Nath–Saikia–Sarma conjecture · Congruences modulo 24 for triples of 2-regular partitions · Prime-power congruences modulo 24 for triples of 2-regular partitions · Parity of triples of 2-regular partitions · Congruences modulo 8 and 24 for triples of 2-regular partitions

TheoremZero has one \(\ell\)-regular partition#✓fully proved

For every natural number \(\ell\), the number of \(\ell\)-regular partitions of \(0\) is \(1\); the only one is the empty partition.

public theorem lRegularPartitionCount_zero (ℓ : ℕ) : lRegularPartitionCount ℓ 0 = 1

Sources

• Bishnu Paudel, James A. Sellers, and Haiyang Wang, Extending Recent Work of Nath, Saikia, and Sarma on k-Tuple ℓ-Regular Partitions, INTEGERS 26 (2026), Article A4, Introduction (definition of ℓ-regular partitions).

Uses 1 · Used by 1

Statement usesNumber of \(\ell\)-regular partitions

Used byOne tuple of \(\ell\)-regular partitions of total zero

TheoremOne tuple of \(\ell\)-regular partitions of total zero#✓fully proved

For all natural numbers \(\ell\) and \(k\), writing \(T_{\ell,k}(n)\) for the number of \(k\)-tuples of \(\ell\)-regular partitions with total \(n\), we have \(T_{\ell,k}(0) = 1\): the only such tuple of total \(0\) is the tuple of empty partitions.

public theorem kTupleRegularPartitionCount_at_zero (ℓ k : ℕ) :
    kTupleRegularPartitionCount ℓ k 0 = 1

Sources

• Bishnu Paudel, James A. Sellers, and Haiyang Wang, Extending Recent Work of Nath, Saikia, and Sarma on k-Tuple ℓ-Regular Partitions, INTEGERS 26 (2026), Article A4, Introduction (definition of T_{ℓ,k}).

Uses 3

Statement usesNumber of \(k\)-tuples of \(\ell\)-regular partitions

Proof usesNumber of \(\ell\)-regular partitions · Zero has one \(\ell\)-regular partition

DefinitionBounded bilateral series#✓fully proved

Given functions \(e, w : \mathbb{Z} \to \mathbb{Z}\), the bounded bilateral series of \(e\) and \(w\) is the power series over \(\mathbb{Z}\) whose coefficient of \(q^n\), for each natural number \(n\), is the sum of \(w(m)\) over the integers \(m\) with \(-n-1 \le m \le n+1\) and \(e(m) = n\).

It agrees with the bilateral series \(\sum_{m \in \mathbb{Z}} w(m) q^{e(m)}\) whenever \(e\) takes no negative values and, for every natural number \(n\), every integer \(m\) with \(e(m) = n\) satisfies \(|m| \le n + 1\), as holds for the quadratic exponents used in Lemmas 1, 3 and 5 of the source; it is not intended for other exponents.

public def boundedBilateralSeries (exponent weight : ℤ → ℤ) : PowerSeries ℤ :=
  PowerSeries.mk fun n =>
    ∑ m ∈ Finset.Icc (-(n : ℤ) - 1) ((n : ℤ) + 1),
      if exponent m = (n : ℤ) then weight m else 0

Sources

• Bishnu Paudel, James A. Sellers, and Haiyang Wang, Extending Recent Work of Nath, Saikia, and Sarma on k-Tuple ℓ-Regular Partitions, INTEGERS 26 (2026), Article A4, Encoding for Lemmas 1, 3, and 5.

Used by 3

Used byCoefficients of the bounded bilateral series · A fifth-power Euler product identity · Gauss's theta identity for the Euler products

TheoremCoefficients of the bounded bilateral series#✓fully proved

For all functions \(e, w : \mathbb{Z} \to \mathbb{Z}\) and every natural number \(n\), the coefficient of \(q^n\) in the bounded bilateral series of \(e\) and \(w\) equals the sum of \(w(m)\) over the integers \(m\) with \(-n-1 \le m \le n+1\) and \(e(m) = n\).

public theorem coeff_boundedBilateralSeries (exponent weight : ℤ → ℤ) (n : ℕ) :
    PowerSeries.coeff n (boundedBilateralSeries exponent weight) =
      ∑ m ∈ Finset.Icc (-(n : ℤ) - 1) ((n : ℤ) + 1),
        if exponent m = (n : ℤ) then weight m else 0

Sources

• Bishnu Paudel, James A. Sellers, and Haiyang Wang, Extending Recent Work of Nath, Saikia, and Sarma on k-Tuple ℓ-Regular Partitions, INTEGERS 26 (2026), Article A4, Encoding for Lemmas 1, 3, and 5.

Uses 1

Statement usesBounded bilateral series

DefinitionTruncated one-sided series#✓fully proved

For functions \(e : \mathbb{N} \to \mathbb{N}\) and \(w : \mathbb{N} \to \mathbb{Z}\), this is the integer power series whose coefficient of \(q^n\) is the sum of \(w(m)\) over the integers \(m\) with \(1 \le m \le n\) and \(e(m) = n\).

When \(e(m) \ge m\) for every \(m \ge 1\), as for the square exponents in Lemma 5 and Corollary 3, this series is \(\sum_{m \ge 1} w(m) q^{e(m)}\).

public def positiveUnilateralSeries (exponent : ℕ → ℕ) (weight : ℕ → ℤ) : PowerSeries ℤ :=
  PowerSeries.mk fun n =>
    ∑ m ∈ Finset.Icc 1 n, if exponent m = n then weight m else 0

Sources

• Bishnu Paudel, James A. Sellers, and Haiyang Wang, Extending Recent Work of Nath, Saikia, and Sarma on k-Tuple ℓ-Regular Partitions, INTEGERS 26 (2026), Article A4, Encoding for Lemma 5 and Corollary 3.

Used by 3

Used byCoefficients of the positive unilateral series · Gauss's theta identity for the Euler products · The theta identity for the second Euler product

TheoremCoefficients of the positive unilateral series#✓fully proved

For all functions \(e : \mathbb{N} \to \mathbb{N}\) and \(w : \mathbb{N} \to \mathbb{Z}\) and every natural number \(n\), the coefficient of \(q^n\) in the positive unilateral series of \(e\) and \(w\) equals the sum of \(w(m)\) over the natural numbers \(m\) with \(1 \le m \le n\) and \(e(m) = n\).

public theorem coeff_positiveUnilateralSeries (exponent : ℕ → ℕ) (weight : ℕ → ℤ) (n : ℕ) :
    PowerSeries.coeff n (positiveUnilateralSeries exponent weight) =
      ∑ m ∈ Finset.Icc 1 n, if exponent m = n then weight m else 0

Sources

• Bishnu Paudel, James A. Sellers, and Haiyang Wang, Extending Recent Work of Nath, Saikia, and Sarma on k-Tuple ℓ-Regular Partitions, INTEGERS 26 (2026), Article A4, Encoding for Lemma 5 and Corollary 3.

Uses 1

Statement usesTruncated one-sided series

TheoremCongruences modulo 24 for triples of 2-regular partitions#●ready to prove

Let \(T_2(n)\) be the number of triples of 2-regular partitions (partitions with no even part) whose sizes add up to \(n\). If \(t\) is a positive integer with \(\gcd(t, 6) = 1\) and \(N \in \{33, 57\}\), then for every natural number \(n\),

\[T_2\left(9n + \frac{N t^2 - 1}{8}\right) \equiv 0 \pmod{24}.\]

Here \(N t^2 - 1\) is divisible by \(8\), so the fraction is an integer.

public theorem_wanted tripleTwo_mod_twentyFour (t n N : ℕ) (ht : 0 < t)
    (hcoprime : Nat.gcd t 6 = 1) (hN : N = 33 ∨ N = 57) :
    Nat.ModEq 24 (tripleRegularPartitionCount 2 (9 * n + (N * t ^ 2 - 1) / 8)) 0

Sources

• Bishnu Paudel, James A. Sellers, and Haiyang Wang, Extending Recent Work of Nath, Saikia, and Sarma on k-Tuple ℓ-Regular Partitions, INTEGERS 26 (2026), Article A4, Theorem 1, equation T29n24.

Uses 1

Statement usesTriples of \(\ell\)-regular partitions

TheoremThe Nath–Saikia–Sarma conjecture#●ready to prove

Let \(T_2(n)\) be the number of triples of 2-regular partitions (partitions with no even part) whose sizes add up to \(n\). Let \(p \ge 5\) be a prime with Legendre symbol \(\left(\frac{-2}{p}\right) = -1\), and let \(t\) be a positive integer with \(\gcd(t, 6) = 1\) and \(p \mid t\). Then for every natural number \(n\) and every \(j\) with \(1 \le j \le p - 1\),

\[T_2\left(9t^2 n + \frac{9t^2 j}{p} + \frac{57t^2 - 1}{8}\right) \equiv 0 \pmod{6}.\]

Both fractions are integers under these hypotheses.

public theorem_wanted nathSaikiaSarma_conjecture (p t n j : ℕ) [Fact (Nat.Prime p)]
    (hp : 5 ≤ p) (hlegendre : legendreSym p (-2) = -1) (ht : 0 < t)
    (hcoprime : Nat.gcd t 6 = 1) (hpt : p ∣ t) (hj₁ : 1 ≤ j) (hjp : j ≤ p - 1) :
    Nat.ModEq 6
      (tripleRegularPartitionCount 2
        (9 * t ^ 2 * n + 9 * t ^ 2 * j / p + (57 * t ^ 2 - 1) / 8)) 0

Sources

• Bishnu Paudel, James A. Sellers, and Haiyang Wang, Extending Recent Work of Nath, Saikia, and Sarma on k-Tuple ℓ-Regular Partitions, INTEGERS 26 (2026), Article A4, Corollary 1 (Conjecture conj.nss).

Uses 1

Statement usesTriples of \(\ell\)-regular partitions

TheoremCongruences modulo 8 and 24 for triples of 2-regular partitions#●ready to prove

Let \(T_2(n)\) be the number of triples of \(2\)-regular partitions (partitions with no even part) whose sizes add up to \(n\). Let \(p\) be a prime with \(p \equiv 3\), \(5\) or \(7 \pmod 8\), and let \(n\) and \(\alpha\) be natural numbers with \(p \nmid n\). Then

\[T_2\left(p^{2\alpha+1} n + \frac{p^{2\alpha+2}-1}{8}\right) \equiv 0 \pmod 8,\]

and if moreover \(3 \nmid n\), this value is also \(\equiv 0 \pmod{24}\).

The division by \(8\) is exact because \(p\) is odd.

public theorem_wanted tripleTwo_primePower_mod_eight_and_twentyFour (p n α : ℕ)
    (hp : Nat.Prime p) (hres : p % 8 = 3 ∨ p % 8 = 5 ∨ p % 8 = 7) (hpn : ¬ p ∣ n) :
    let index := p ^ (2 * α + 1) * n + (p ^ (2 * α + 2) - 1) / 8
    Nat.ModEq 8 (tripleRegularPartitionCount 2 index) 0 ∧
      (¬ 3 ∣ n → Nat.ModEq 24 (tripleRegularPartitionCount 2 index) 0)

Sources

• Bishnu Paudel, James A. Sellers, and Haiyang Wang, Extending Recent Work of Nath, Saikia, and Sarma on k-Tuple ℓ-Regular Partitions, INTEGERS 26 (2026), Article A4, Theorem 2, equations thm.p357mod8 and mod24.

Uses 1

Statement usesTriples of \(\ell\)-regular partitions

TheoremPrime-power congruences modulo 24 for triples of 2-regular partitions#●ready to prove

Let \(T_2(n)\) be the number of triples of 2-regular partitions (partitions with no even part) whose sizes add up to \(n\). Let \(p \ne 3\) be a prime with \(p \equiv 3\), \(5\) or \(7 \pmod 8\). Then for all natural numbers \(n\) and \(\alpha\) with \(p \nmid n\),

\[T_2\left(9 p^{2\alpha+1} n + \frac{9 p^{2\alpha+2} - 1}{8}\right) \equiv 0 \pmod{24}.\]

Since \(p\) is odd, the fraction is an integer.

public theorem_wanted tripleTwo_nine_primePower_mod_twentyFour (p n α : ℕ)
    (hp : Nat.Prime p) (hres : p % 8 = 3 ∨ p % 8 = 5 ∨ p % 8 = 7)
    (hp3 : p ≠ 3) (hpn : ¬ p ∣ n) :
    Nat.ModEq 24
      (tripleRegularPartitionCount 2
        (9 * p ^ (2 * α + 1) * n + (9 * p ^ (2 * α + 2) - 1) / 8)) 0

Sources

• Bishnu Paudel, James A. Sellers, and Haiyang Wang, Extending Recent Work of Nath, Saikia, and Sarma on k-Tuple ℓ-Regular Partitions, INTEGERS 26 (2026), Article A4, Corollary 2, equation cor.9pmod24.

Uses 1

Statement usesTriples of \(\ell\)-regular partitions

TheoremA fifth-power Euler product identity#●ready to prove

Write \(f_k = \prod_{i \ge 1} (1 - q^{ki})\) for the Euler products, as integer power series in \(q\). Then

\[f_1^5 = f_2^2 \sum_{m \in \mathbb{Z}} (6m + 1)\, q^{m(3m+1)/2}.\]

This is the identity \(f_1^5 / f_2^2 = \sum_{m \in \mathbb{Z}} (6m + 1)\, q^{m(3m+1)/2}\) with the denominator cleared. The coefficient of \(q^n\) in the sum is computed over the integers \(m\) with \(|m| \le n + 1\), which include every solution of \(m(3m+1)/2 = n\).

public theorem_wanted qEulerProduct_fifth_power_identity :
    qEulerProduct 1 ^ 5 = qEulerProduct 2 ^ 2 * boundedBilateralSeries
      (fun m => m * (3 * m + 1) / 2) (fun m => 6 * m + 1)

Sources

• Bishnu Paudel, James A. Sellers, and Haiyang Wang, Extending Recent Work of Nath, Saikia, and Sarma on k-Tuple ℓ-Regular Partitions, INTEGERS 26 (2026), Article A4, Lemma 3, equation f15/f22.

Uses 2

Statement usesBounded bilateral series · The Euler products of partition theory

TheoremA signed Euler product identity#●ready to prove

Write \(f_k = \prod_{i \ge 1} (1 - q^{ki})\) for the Euler products, as integer power series in \(q\), and let \((-q;-q)_\infty = \prod_{i \ge 1} (1 - (-q)^i)\) be \(f_1\) with \(q\) replaced by \(-q\). Then

\[(-q;-q)_\infty \, f_1 f_4 = f_2^3.\]

This is the identity \((-q;-q)_\infty = f_2^3 / (f_1 f_4)\) with the denominator cleared.

public theorem_wanted rescale_neg_one_qEulerProduct_identity :
    PowerSeries.rescale (-1) (qEulerProduct 1) * qEulerProduct 1 * qEulerProduct 4 =
      qEulerProduct 2 ^ 3

Sources

• Bishnu Paudel, James A. Sellers, and Haiyang Wang, Extending Recent Work of Nath, Saikia, and Sarma on k-Tuple ℓ-Regular Partitions, INTEGERS 26 (2026), Article A4, Lemma 4, equation f1-q.

Uses 1

Statement usesThe Euler products of partition theory

TheoremGauss's theta identity for the Euler products#●ready to prove

Write \(f_k = \prod_{i \ge 1} (1 - q^{ki})\) for the Euler products, as integer power series in \(q\), and let \(\theta = \sum_{m \in \mathbb{Z}} (-1)^m q^{m^2}\). Then \(f_1^2 = f_2\, \theta\) and \(\theta = 1 + 2 \sum_{m \ge 1} (-1)^m q^{m^2}\).

The coefficient of \(q^n\) in each sum is computed over the indices \(m\) with \(|m| \le n + 1\) (respectively \(1 \le m \le n\)), which include every solution of \(m^2 = n\).

public theorem_wanted qEulerProduct_square_theta_identity :
    let theta := boundedBilateralSeries (fun m => m ^ 2) (fun m => (-1 : ℤ) ^ m.natAbs)
    qEulerProduct 1 ^ 2 = qEulerProduct 2 * theta ∧
      theta = 1 + 2 * positiveUnilateralSeries (fun m => m ^ 2) (fun m => (-1 : ℤ) ^ m)

Sources

• Bishnu Paudel, James A. Sellers, and Haiyang Wang, Extending Recent Work of Nath, Saikia, and Sarma on k-Tuple ℓ-Regular Partitions, INTEGERS 26 (2026), Article A4, Lemma 5, equation f12/f2.

Uses 3

Statement usesBounded bilateral series · Truncated one-sided series · The Euler products of partition theory

TheoremThe theta identity for the second Euler product#●ready to prove

Write \(f_k = \prod_{i \ge 1} (1 - q^{ki})\) for the Euler products, as integer power series in \(q\). Then

\[f_2^2 = f_4 \left(1 + 2 \sum_{n \ge 1} (-1)^n q^{2n^2}\right).\]

This is the identity for \(f_2^2 / f_4\) with the denominator cleared.

public theorem_wanted qEulerProduct_two_square_identity :
    qEulerProduct 2 ^ 2 = qEulerProduct 4 *
      (1 + 2 * positiveUnilateralSeries (fun n => 2 * n ^ 2) (fun n => (-1 : ℤ) ^ n))

Sources

• Bishnu Paudel, James A. Sellers, and Haiyang Wang, Extending Recent Work of Nath, Saikia, and Sarma on k-Tuple ℓ-Regular Partitions, INTEGERS 26 (2026), Article A4, Corollary 3, equation f22/f4.

Uses 2

Statement usesTruncated one-sided series · The Euler products of partition theory

TheoremIterated prime-power congruence for Euler products#●ready to prove

For a natural number \(l\) write \(f_l = \prod_{i \ge 1} (1 - q^{li})\), an integer power series in \(q\). Let \(p\) be a prime and let \(k, l, s, m\) be natural numbers with \(l \ge 1\), \(s \ge 1\), \(m \ge 1\) and \(s \le k\). Then for every natural number \(n\), the coefficients of \(q^n\) in \(f_l^{p^k m}\) and in \(f_{l p^s}^{p^{k-s} m}\) are congruent modulo \(p^{k-s+1}\).

public theorem_wanted qEulerProduct_iterated_primePower_congruence (p k l s m : ℕ)
    (hp : Nat.Prime p) (hl : 0 < l) (hs : 0 < s) (hm : 0 < m) (hsk : s ≤ k) (n : ℕ) :
    PowerSeries.coeff n (qEulerProduct l ^ (p ^ k * m)) ≡
      PowerSeries.coeff n (qEulerProduct (l * p ^ s) ^ (p ^ (k - s) * m))
        [ZMOD (p : ℤ) ^ (k - s + 1)]

Sources

• Bishnu Paudel, James A. Sellers, and Haiyang Wang, Extending Recent Work of Nath, Saikia, and Sarma on k-Tuple ℓ-Regular Partitions, INTEGERS 26 (2026), Article A4, Lemma 7, equation cor.modp^k.

Uses 1

Statement usesThe Euler products of partition theory

TheoremParity of triples of 2-regular partitions#●ready to prove

For a natural number \(n\), let \(T_2(n)\) be the number of triples of \(2\)-regular partitions (partitions with no even part) whose sizes add up to \(n\). Then \(T_2(n)\) is odd if and only if \(n\) is a triangular number, that is, \(n = m(m+1)/2\) for some natural number \(m\).

Allowing integer \(m\) gives no new values, since \(m\) and \(-m-1\) give the same triangular number.

public theorem_wanted tripleTwo_odd_iff_triangular (n : ℕ) :
    tripleRegularPartitionCount 2 n % 2 = 1 ↔ ∃ m : ℕ, n = m * (m + 1) / 2

Sources

• Bishnu Paudel, James A. Sellers, and Haiyang Wang, Extending Recent Work of Nath, Saikia, and Sarma on k-Tuple ℓ-Regular Partitions, INTEGERS 26 (2026), Article A4, Lemma 8, equation mod2.

Uses 1

Statement usesTriples of \(\ell\)-regular partitions

TheoremPrime-power congruences for \(k\)-tuples of \(\ell\)-regular partitions#●ready to prove

Write \(T_{\ell,k}(n)\) for the number of \(k\)-tuples of \(\ell\)-regular partitions with total \(n\). Let \(p\) be a prime, let \(m\), \(\ell\) and \(s\) be positive integers, let \(\alpha \ge s\) and \(r\) be natural numbers with \(1 \le r \le p^s - 1\). Then for every natural number \(n\),

\[T_{\ell,p^\alpha m}(p^s n + r) \equiv 0 \pmod{p^{\alpha - s + 1}}.\]

Since \(s\) is positive, the hypothesis \(\alpha \ge s\) also gives \(\alpha \ge 1\).

public theorem_wanted kTupleRegularPartition_primePower_congruent (p m ℓ α s r n : ℕ)
    (hp : Nat.Prime p) (hm : 0 < m) (hℓ : 0 < ℓ) (hs : 0 < s) (hsα : s ≤ α) (hr₁ : 1 ≤ r) (hrp : r ≤
        p ^ s - 1) :
    Nat.ModEq (p ^ (α - s + 1))
      (kTupleRegularPartitionCount ℓ (p ^ α * m) (p ^ s * n + r)) 0

Sources

• Bishnu Paudel, James A. Sellers, and Haiyang Wang, Extending Recent Work of Nath, Saikia, and Sarma on k-Tuple ℓ-Regular Partitions, INTEGERS 26 (2026), Article A4, Theorem 3, equation thm.gen1.1.

Uses 1

Statement usesNumber of \(k\)-tuples of \(\ell\)-regular partitions

DefinitionRegular tripartition counts#✓fully proved

For natural numbers \(\ell\) and \(n\), \(T_\ell(n)\) is the number of triples \((\lambda_1, \lambda_2, \lambda_3)\) of integer partitions with \(|\lambda_1| + |\lambda_2| + |\lambda_3| = n\) in which no part of any \(\lambda_i\) is divisible by \(\ell\); these triples are the \(\ell\)-regular tripartitions of \(n\).

public def regularTripartitionCount (l n : ℕ) : ℕ :=
  ∑ x ∈ Finset.antidiagonal n, ∑ y ∈ Finset.antidiagonal x.2,
    (Nat.Partition.restricted x.1 (¬ l ∣ ·)).card *
      (Nat.Partition.restricted y.1 (¬ l ∣ ·)).card *
      (Nat.Partition.restricted y.2 (¬ l ∣ ·)).card

Sources

• Mohammed L. Nadji and Moussa Ahmia, Congruences for l-Regular Tripartitions for l in {2,3}, INTEGERS 24 (2024), Article A86, Section 1, definition of T_ℓ(n) (with generating function f_ℓ³ / f_1³, Section 1, eq. (1)).

Used by 11

Used byThe number of \(\ell\)-regular tripartitions of \(1\) · Congruences modulo 3 and 9 for 3-regular tripartitions · A congruence modulo 3 for 3-regular tripartitions at primes \(p \equiv 3 \pmod 4\) · A congruence modulo 6 for 3-regular tripartitions · The 3-dissection of the generating function of 3-regular tripartitions · Congruences modulo 3 and 6 for 2-regular tripartitions · Mod 12 congruences for 2-regular tripartitions · Even 2-regular tripartition counts for odd primes · Even 2-regular tripartition counts for primes at least 5 · The 3-dissection of the 2-regular tripartition generating function · The regular tripartition count at zero

TheoremThe regular tripartition count at zero#✓fully proved

For every natural number \(\ell\), \(T_\ell(0) = 1\), where \(T_\ell(n)\) is the number of \(\ell\)-regular tripartitions of \(n\): the only tripartition of \(0\) is the triple of empty partitions.

public theorem regularTripartitionCount_zero (l : ℕ) : regularTripartitionCount l 0 = 1

Sources

• Mohammed L. Nadji and Moussa Ahmia, Congruences for l-Regular Tripartitions for l in {2,3}, INTEGERS 24 (2024), Article A86 (definition of T_ℓ(n)).

Uses 1

Statement usesRegular tripartition counts

TheoremThe number of \(\ell\)-regular tripartitions of \(1\)#✓fully proved

For every natural number \(\ell \ne 1\), the number \(T_\ell(1)\) of \(\ell\)-regular tripartitions of \(1\) is \(3\): the single part \(1\) lies in one of the three components.

public theorem regularTripartitionCount_one (l : ℕ) (hl : l ≠ 1) :
    regularTripartitionCount l 1 = 3

Sources

• Mohammed L. Nadji and Moussa Ahmia, Congruences for l-Regular Tripartitions for l in {2,3}, INTEGERS 24 (2024), Article A86 (definition of T_ℓ(n)).

Uses 1

Statement usesRegular tripartition counts

TheoremCongruences modulo 3 and 6 for 2-regular tripartitions#●ready to prove

Let \(T_2(m)\) be the number of \(2\)-regular tripartitions of \(m\). For every natural number \(n\), \(3 \mid T_2(3n + 1)\) and \(6 \mid T_2(3n + 2)\).

public theorem_wanted regularTripartitionCount_two_mod_three_six (n : ℕ) :
    3 ∣ regularTripartitionCount 2 (3 * n + 1) ∧ 6 ∣ regularTripartitionCount 2 (3 * n + 2)

Sources

• Mohammed L. Nadji and Moussa Ahmia, Congruences for l-Regular Tripartitions for l in {2,3}, INTEGERS 24 (2024), Article A86, Corollary 1.

Uses 1

Statement usesRegular tripartition counts

TheoremCongruences modulo 3 and 9 for 3-regular tripartitions#●ready to prove

Let \(T_3(m)\) be the number of \(3\)-regular tripartitions of \(m\). For every natural number \(n\), \(3 \mid T_3(3n + 1)\) and \(9 \mid T_3(3n + 2)\).

public theorem_wanted regularTripartitionCount_three_mod_three_nine (n : ℕ) :
    3 ∣ regularTripartitionCount 3 (3 * n + 1) ∧ 9 ∣ regularTripartitionCount 3 (3 * n + 2)

Sources

• Mohammed L. Nadji and Moussa Ahmia, Congruences for l-Regular Tripartitions for l in {2,3}, INTEGERS 24 (2024), Article A86, Corollary 2 (congruences (53), (54)).

Uses 1

Statement usesRegular tripartition counts

TheoremA congruence modulo 6 for 3-regular tripartitions#●ready to prove

Let \(T_3(m)\) be the number of \(3\)-regular tripartitions of \(m\). For every natural number \(n\), \(6 \mid T_3(6n + 4)\).

public theorem_wanted regularTripartitionCount_three_six_mul_add_four (n : ℕ) :
    6 ∣ regularTripartitionCount 3 (6 * n + 4)

Sources

• Mohammed L. Nadji and Moussa Ahmia, Congruences for l-Regular Tripartitions for l in {2,3}, INTEGERS 24 (2024), Article A86, Corollary 3 (congruence (64)).

Uses 1

Statement usesRegular tripartition counts

TheoremEven 2-regular tripartition counts for primes at least 5#●ready to prove

Let \(T_2(n)\) be the number of 2-regular tripartitions of \(n\). For every prime \(p \ge 5\), all natural numbers \(\alpha\) and \(n\), and every \(i\) with \(1 \le i \le p - 1\), the number \(T_2\bigl(3 p^{2\alpha+1} (p n + i) + (p^{2\alpha+2} - 1)/8\bigr)\) is even (the division is exact).

public theorem_wanted regularTripartitionCount_two_prime_ge_five_even
    (p α n i : ℕ) (hp : p.Prime) (hp5 : 5 ≤ p) (hi : 1 ≤ i) (hip : i < p) :
    2 ∣ regularTripartitionCount 2
      (3 * p ^ (2 * α + 1) * (p * n + i) + (p ^ (2 * α + 2) - 1) / 8)

Sources

• Mohammed L. Nadji and Moussa Ahmia, Congruences for l-Regular Tripartitions for l in {2,3}, INTEGERS 24 (2024), Article A86, Theorem 1 (congruence (13)).

Uses 1

Statement usesRegular tripartition counts

TheoremEven 2-regular tripartition counts for odd primes#●ready to prove

Let \(T_2(n)\) be the number of 2-regular tripartitions of \(n\). For every odd prime \(p\), all natural numbers \(\alpha\) and \(n\), and every \(i\) with \(1 \le i \le p - 1\), the number \(T_2\bigl(9 p^{2\alpha+1} (p n + i) + (9 p^{2\alpha+2} - 1)/8\bigr)\) is even (the division is exact).

public theorem_wanted regularTripartitionCount_two_odd_prime_even
    (p α n i : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (hi : 1 ≤ i) (hip : i < p) :
    2 ∣ regularTripartitionCount 2
      (9 * p ^ (2 * α + 1) * (p * n + i) + (9 * p ^ (2 * α + 2) - 1) / 8)

Sources

• Mohammed L. Nadji and Moussa Ahmia, Congruences for l-Regular Tripartitions for l in {2,3}, INTEGERS 24 (2024), Article A86, Theorem 2 (congruence (21)).

Uses 1

Statement usesRegular tripartition counts

TheoremA congruence modulo 3 for 3-regular tripartitions at primes \(p \equiv 3 \pmod 4\)#●ready to prove

Let \(T_3(m)\) be the number of \(3\)-regular tripartitions of \(m\), and let \(p\) be a prime with \(p \equiv 3 \pmod 4\). For all natural numbers \(\alpha\) and \(n\) and every integer \(i\) with \(1 \le i \le p - 1\),

\[ T_3\Bigl(3 p^{2\alpha+1} (p n + i) + \frac{p^{2\alpha+2} - 1}{4}\Bigr) \equiv 0 \pmod 3, \]

where the division by \(4\) is exact.

public theorem_wanted regularTripartitionCount_three_prime_three_mod_four
    (p α n i : ℕ) (hp : p.Prime) (hp4 : p % 4 = 3) (hi : 1 ≤ i) (hip : i < p) :
    3 ∣ regularTripartitionCount 3
      (3 * p ^ (2 * α + 1) * (p * n + i) + (p ^ (2 * α + 2) - 1) / 4)

Sources

• Mohammed L. Nadji and Moussa Ahmia, Congruences for l-Regular Tripartitions for l in {2,3}, INTEGERS 24 (2024), Article A86, Theorem 5 (congruence (55)).

Uses 1

Statement usesRegular tripartition counts

TheoremToh's 3-dissection of \(f_2^3 / f_1^3\)#●ready to prove

For \(k \ge 1\) let \(f_k = \prod_{m \ge 1} (1 - q^{km})\) be the Euler product, an integer power series in \(q\). Then

\[ f_2^3 f_3^8 f_9 f_{18} = f_1^3 \bigl(f_3^7 f_6 f_9 f_{18} + 3q f_6^4 f_9^6 + 6q^2 f_3 f_6^3 f_9^3 f_{18}^3 + 12q^3 f_3^2 f_6^2 f_{18}^6\bigr). \]

Since each \(f_k\) has constant term \(1\) and so is invertible, this is the identity \(f_2^3/f_1^3 = f_6/f_3 + 3q f_6^4 f_9^5/(f_3^8 f_{18}) + 6q^2 f_6^3 f_9^2 f_{18}^2/f_3^7 + 12q^3 f_6^2 f_{18}^5/(f_3^6 f_9)\) with both sides multiplied by \(f_1^3 f_3^8 f_9 f_{18}\).

public theorem_wanted f2_cube_div_f1_cube_three_dissection :
    𝔣 2 ^ 3 * 𝔣 3 ^ 8 * 𝔣 9 * 𝔣 18 =
      𝔣 1 ^ 3 * (𝔣 3 ^ 7 * 𝔣 6 * 𝔣 9 * 𝔣 18 + 3 * X * 𝔣 6 ^ 4 * 𝔣 9 ^ 6 +
        6 * X ^ 2 * 𝔣 3 * 𝔣 6 ^ 3 * 𝔣 9 ^ 3 * 𝔣 18 ^ 3 +
        12 * X ^ 3 * 𝔣 3 ^ 2 * 𝔣 6 ^ 2 * 𝔣 18 ^ 6)

Sources

• Mohammed L. Nadji and Moussa Ahmia, Congruences for l-Regular Tripartitions for l in {2,3}, INTEGERS 24 (2024), Article A86, Lemma 1, eq. (3).

Uses 1

Statement usesThe Euler products of partition theory

TheoremThe 3-dissection of \(1/f_1^3\)#●ready to prove

For \(k \ge 1\) let \(f_k = \prod_{m \ge 1} (1 - q^{km})\) be the Euler product, an integer power series in \(q\). Then

\[ f_3^{12} = f_1^3 f_9^3 \bigl(f_1^6 + 9q f_1^3 f_9^3 + 27q^2 f_9^6\bigr) \]

and

\[ f_3^{14} f_6^4 f_9^3 f_{18}^6 = f_1^3 \bigl(f_6^6 f_9^{18} + 3q f_3 f_6^5 f_9^{15} f_{18}^3 + 9q^2 f_3^2 f_6^4 f_9^{12} f_{18}^6 + 8q^3 f_3^3 f_6^3 f_9^9 f_{18}^9 + 12q^4 f_3^4 f_6^2 f_9^6 f_{18}^{12} + 16q^6 f_3^6 f_{18}^{18}\bigr). \]

Since each \(f_k\) has constant term \(1\) and so is invertible, these are the identities \(1/f_1^3 = (f_9^3/f_3^{12})(f_1^6 + 9q f_1^3 f_9^3 + 27q^2 f_9^6)\) and \(1/f_1^3 = f_6^2 f_9^{15}/(f_3^{14} f_{18}^6) + 3q f_6 f_9^{12}/(f_3^{13} f_{18}^3) + 9q^2 f_9^9/f_3^{12} + 8q^3 f_9^6 f_{18}^3/(f_3^{11} f_6) + 12q^4 f_9^3 f_{18}^6/(f_3^{10} f_6^2) + 16q^6 f_{18}^{12}/(f_3^8 f_6^4 f_9^3)\), multiplied by \(f_1^3 f_3^{12}\) and by \(f_1^3 f_3^{14} f_6^4 f_9^3 f_{18}^6\) respectively.

public theorem_wanted one_div_f1_cube_three_dissection :
    𝔣 3 ^ 12 = 𝔣 1 ^ 3 * 𝔣 9 ^ 3 *
        (𝔣 1 ^ 6 + 9 * X * 𝔣 1 ^ 3 * 𝔣 9 ^ 3 + 27 * X ^ 2 * 𝔣 9 ^ 6) ∧
      𝔣 3 ^ 14 * 𝔣 6 ^ 4 * 𝔣 9 ^ 3 * 𝔣 18 ^ 6 =
        𝔣 1 ^ 3 * (𝔣 6 ^ 6 * 𝔣 9 ^ 18 + 3 * X * 𝔣 3 * 𝔣 6 ^ 5 * 𝔣 9 ^ 15 * 𝔣 18 ^ 3 +
          9 * X ^ 2 * 𝔣 3 ^ 2 * 𝔣 6 ^ 4 * 𝔣 9 ^ 12 * 𝔣 18 ^ 6 +
          8 * X ^ 3 * 𝔣 3 ^ 3 * 𝔣 6 ^ 3 * 𝔣 9 ^ 9 * 𝔣 18 ^ 9 +
          12 * X ^ 4 * 𝔣 3 ^ 4 * 𝔣 6 ^ 2 * 𝔣 9 ^ 6 * 𝔣 18 ^ 12 +
          16 * X ^ 6 * 𝔣 3 ^ 6 * 𝔣 18 ^ 18)

Sources

• Mohammed L. Nadji and Moussa Ahmia, Congruences for l-Regular Tripartitions for l in {2,3}, INTEGERS 24 (2024), Article A86, Lemma 3, eq. (6).

Uses 1

Statement usesThe Euler products of partition theory

TheoremCui–Gu \(p\)-dissection of \(\psi(q)\)#●ready to prove

Let \(p\) be an odd prime and \(q\) a complex number with \(|q| < 1\), let \(f(a, b) = \sum_{n \in \mathbb{Z}} a^{n(n+1)/2} b^{n(n-1)/2}\) be Ramanujan's theta function, and let \(\psi(q) = f(q, q^3)\). Then

\[ \psi(q) = \sum_{k=0}^{(p-3)/2} q^{k(k+1)/2} f\bigl(q^{(p^2 + (2k+1)p)/2}, q^{(p^2 - (2k+1)p)/2}\bigr) + q^{(p^2-1)/8} \psi(q^{p^2}), \]

and \((m^2 + m)/2 \not\equiv (p^2 - 1)/8 \pmod p\) for every integer \(m\) with \(0 \le m \le (p - 3)/2\). All the divisions are exact.

public theorem_wanted ramanujanPsi_prime_dissection (p : ℕ) (hp : p.Prime) (hp2 : p ≠ 2)
    (q : ℂ) (hq : ‖q‖ < 1) :
    ramanujanThetaRaw q (q ^ 3) =
        ∑ k ∈ Finset.range ((p - 1) / 2), q ^ (k * (k + 1) / 2) *
            ramanujanThetaRaw (q ^ ((p ^ 2 + (2 * k + 1) * p) / 2))
              (q ^ ((p ^ 2 - (2 * k + 1) * p) / 2)) +
          q ^ ((p ^ 2 - 1) / 8) * ramanujanThetaRaw (q ^ (p ^ 2)) (q ^ (3 * p ^ 2)) ∧
      ∀ m ≤ (p - 3) / 2, ¬ (m ^ 2 + m) / 2 ≡ (p ^ 2 - 1) / 8 [MOD p]

Sources

• Mohammed L. Nadji and Moussa Ahmia, Congruences for l-Regular Tripartitions for l in {2,3}, INTEGERS 24 (2024), Article A86, Lemma 4, eq. (7), quoting S. Cui and N. Gu, Arithmetic Properties of ℓ-Regular Partitions, Adv. Appl. Math. 51 (2013), 507–523, Theorem 2.1.

Uses 1

Statement usesRaw Ramanujan theta sum

TheoremCui–Gu \(p\)-dissection of \(f_1\)#●ready to prove

Let \(p \ge 5\) be a prime, let \(s = (p - 1)/6\) if \(p \equiv 1 \pmod 6\) and \(s = (-p - 1)/6\) otherwise, and let \(q\) be a complex number with \(|q| < 1\). Write \(f_k = (q^k; q^k)_\infty = \prod_{m \ge 1} (1 - q^{km})\), let \(f(a, b) = \sum_{n \in \mathbb{Z}} a^{n(n+1)/2} b^{n(n-1)/2}\) be Ramanujan's theta function, and let \(K\) be the set of integers \(k\) with \((1 - p)/2 \le k \le (p - 1)/2\) and \(k \ne s\). Then

\[ f_1 = \sum_{k \in K} (-1)^k q^{k(3k+1)/2} f\bigl(-q^{(3p^2 + (6k+1)p)/2}, -q^{(3p^2 - (6k+1)p)/2}\bigr) + (-1)^s q^{(p^2-1)/24} f_{p^2}. \]

All the divisions are exact and all the exponents of \(q\) are nonnegative integers.

public theorem_wanted qPochhammer_prime_dissection (p : ℕ) (hp : p.Prime) (hp5 : 5 ≤ p)
    (s : ℤ) (hs : s = if p % 6 = 1 then ((p : ℤ) - 1) / 6 else (-(p : ℤ) - 1) / 6)
    (q : ℂ) (hq : ‖q‖ < 1) :
    QPochhammer.qPochhammerInfRaw q q =
      ∑ k ∈ (Finset.Icc ((1 - (p : ℤ)) / 2) (((p : ℤ) - 1) / 2)).erase s,
          (-1 : ℂ) ^ k * q ^ (k * (3 * k + 1) / 2).toNat *
            ramanujanThetaRaw (-q ^ ((3 * (p : ℤ) ^ 2 + (6 * k + 1) * p) / 2).toNat)
              (-q ^ ((3 * (p : ℤ) ^ 2 - (6 * k + 1) * p) / 2).toNat) +
        (-1 : ℂ) ^ s * q ^ ((p ^ 2 - 1) / 24) *
          QPochhammer.qPochhammerInfRaw (q ^ (p ^ 2)) (q ^ (p ^ 2))

Sources

• Mohammed L. Nadji and Moussa Ahmia, Congruences for l-Regular Tripartitions for l in {2,3}, INTEGERS 24 (2024), Article A86, Lemma 5, eq. (8), quoting S. Cui and N. Gu, Arithmetic Properties of ℓ-Regular Partitions, Adv. Appl. Math. 51 (2013), 507–523, Theorem 2.2. The same identity is Nayaka, Dharmendra and Mahesh Kumar, Divisibility Properties for Overcubic Partition Triples, INTEGERS 24 (2024), Article A80, Lemma 4, eq. (43).

Uses 2

Statement usesRaw infinite q-Pochhammer product · Raw Ramanujan theta sum

TheoremThe 3-dissection of the 2-regular tripartition generating function#●ready to prove

Let \(T_2(n)\) be the number of 2-regular tripartitions of \(n\) and \(f_k = \prod_{m \ge 1} (1 - q^{km})\). In the ring \(\mathbb{Z}[[q]]\) of integer power series, \(f_1^6 f_3 \sum_{n \ge 0} T_2(3n) q^n = f_1^5 f_2 f_3 + 12 q f_2^2 f_6^5\), \(f_1^8 f_6 \sum_{n \ge 0} T_2(3n + 1) q^n = 3 f_2^4 f_3^5\) and \(f_1^7 \sum_{n \ge 0} T_2(3n + 2) q^n = 6 f_2^3 f_3^2 f_6^2\).

Since each \(f_k\) with \(k \ge 1\) is invertible in \(\mathbb{Z}[[q]]\), these say \(\sum_{n \ge 0} T_2(3n) q^n = f_2 / f_1 + 12 q f_2^2 f_6^5 / (f_1^6 f_3)\), \(\sum_{n \ge 0} T_2(3n + 1) q^n = 3 f_2^4 f_3^5 / (f_1^8 f_6)\) and \(\sum_{n \ge 0} T_2(3n + 2) q^n = 6 f_2^3 f_3^2 f_6^2 / f_1^7\).

public theorem_wanted regularTripartitionCount_two_three_dissection :
    𝔣 1 ^ 6 * 𝔣 3 * PowerSeries.mk (fun n => (regularTripartitionCount 2 (3 * n) : ℤ)) =
        𝔣 1 ^ 5 * 𝔣 2 * 𝔣 3 + 12 * X * 𝔣 2 ^ 2 * 𝔣 6 ^ 5 ∧
      𝔣 1 ^ 8 * 𝔣 6 * PowerSeries.mk (fun n => (regularTripartitionCount 2 (3 * n + 1) : ℤ)) =
        3 * 𝔣 2 ^ 4 * 𝔣 3 ^ 5 ∧
      𝔣 1 ^ 7 * PowerSeries.mk (fun n => (regularTripartitionCount 2 (3 * n + 2) : ℤ)) =
        6 * 𝔣 2 ^ 3 * 𝔣 3 ^ 2 * 𝔣 6 ^ 2

Sources

• Mohammed L. Nadji and Moussa Ahmia, Congruences for l-Regular Tripartitions for l in {2,3}, INTEGERS 24 (2024), Article A86, Lemma 7, eqs. (10)–(12).

Uses 2

Statement usesThe Euler products of partition theory · Regular tripartition counts

TheoremMod 12 congruences for 2-regular tripartitions#●ready to prove

Let \(T_2(n)\) be the number of 2-regular tripartitions of \(n\). For all natural numbers \(\alpha\) and \(n\), put \(A_\alpha = \sum_{i=0}^{2\alpha+1} 3^{2i}\) and \(B_\alpha = \sum_{i=0}^{2\alpha} 3^{2i}\). Then \(12\) divides each of \(T_2(3^{4\alpha+4} n + A_\alpha + 3^{4\alpha+3})\), \(T_2(3^{4\alpha+4} n + A_\alpha + 2 \cdot 3^{4\alpha+3})\), \(T_2(3^{4\alpha+2} n + B_\alpha + 3^{4\alpha+1})\) and \(T_2(3^{4\alpha+2} n + B_\alpha + 2 \cdot 3^{4\alpha+1})\).

public theorem_wanted regularTripartitionCount_two_mod_twelve (α n : ℕ) :
    12 ∣ regularTripartitionCount 2
        (3 ^ (4 * α + 4) * n + ∑ i ∈ Finset.range (2 * α + 2), 3 ^ (2 * i) +
          3 ^ (4 * α + 3)) ∧
      12 ∣ regularTripartitionCount 2
        (3 ^ (4 * α + 4) * n + ∑ i ∈ Finset.range (2 * α + 2), 3 ^ (2 * i) +
          2 * 3 ^ (4 * α + 3)) ∧
      12 ∣ regularTripartitionCount 2
        (3 ^ (4 * α + 2) * n + ∑ i ∈ Finset.range (2 * α + 1), 3 ^ (2 * i) +
          3 ^ (4 * α + 1)) ∧
      12 ∣ regularTripartitionCount 2
        (3 ^ (4 * α + 2) * n + ∑ i ∈ Finset.range (2 * α + 1), 3 ^ (2 * i) +
          2 * 3 ^ (4 * α + 1))

Sources

• Mohammed L. Nadji and Moussa Ahmia, Congruences for l-Regular Tripartitions for l in {2,3}, INTEGERS 24 (2024), Article A86, Theorem 3, eqs. (31)–(34).

Uses 1

Statement usesRegular tripartition counts

TheoremThe 3-dissection of the generating function of 3-regular tripartitions#●ready to prove

Let \(T_3(n)\) be the number of \(3\)-regular tripartitions of \(n\), and for \(k \ge 1\) let \(f_k = \prod_{m \ge 1} (1 - q^{km})\) be the Euler product. Then, as integer power series in \(q\),

\[ f_1^{11} f_2^4 f_3^3 f_6^6 \sum_{n \ge 0} T_3(3n) q^n = f_2^6 f_3^{18} + 8q f_1^3 f_2^3 f_3^9 f_6^9 + 16q^2 f_1^6 f_6^{18}, \]

\[ f_1^{10} f_2^2 f_6^3 \sum_{n \ge 0} T_3(3n + 1) q^n = 3 f_2^3 f_3^{12} + 12q f_1^3 f_3^3 f_6^9 \]

and

\[ f_1^9 \sum_{n \ge 0} T_3(3n + 2) q^n = 9 f_3^9. \]

Since each \(f_k\) has constant term \(1\) and so is invertible, these are the identities \(\sum T_3(3n) q^n = f_2^2 f_3^{15}/(f_1^{11} f_6^6) + 8q f_3^6 f_6^3/(f_1^8 f_2) + 16q^2 f_6^{12}/(f_1^5 f_2^4 f_3^3)\), \(\sum T_3(3n + 1) q^n = 3 f_2 f_3^{12}/(f_1^{10} f_6^3) + 12q f_3^3 f_6^6/(f_1^7 f_2^2)\) and \(\sum T_3(3n + 2) q^n = 9 f_3^9/f_1^9\) with the denominators cleared.

public theorem_wanted regularTripartitionCount_three_three_dissection :
    𝔣 1 ^ 11 * 𝔣 2 ^ 4 * 𝔣 3 ^ 3 * 𝔣 6 ^ 6 *
          PowerSeries.mk (fun n => (regularTripartitionCount 3 (3 * n) : ℤ)) =
        𝔣 2 ^ 6 * 𝔣 3 ^ 18 + 8 * X * 𝔣 1 ^ 3 * 𝔣 2 ^ 3 * 𝔣 3 ^ 9 * 𝔣 6 ^ 9 +
          16 * X ^ 2 * 𝔣 1 ^ 6 * 𝔣 6 ^ 18 ∧
      𝔣 1 ^ 10 * 𝔣 2 ^ 2 * 𝔣 6 ^ 3 *
          PowerSeries.mk (fun n => (regularTripartitionCount 3 (3 * n + 1) : ℤ)) =
        3 * 𝔣 2 ^ 3 * 𝔣 3 ^ 12 + 12 * X * 𝔣 1 ^ 3 * 𝔣 3 ^ 3 * 𝔣 6 ^ 9 ∧
      𝔣 1 ^ 9 * PowerSeries.mk (fun n => (regularTripartitionCount 3 (3 * n + 2) : ℤ)) =
        9 * 𝔣 3 ^ 9

Sources

• Mohammed L. Nadji and Moussa Ahmia, Congruences for l-Regular Tripartitions for l in {2,3}, INTEGERS 24 (2024), Article A86, Theorem 4, eqs. (49)–(51).

Uses 2

Statement usesThe Euler products of partition theory · Regular tripartition counts

14 fully proved24 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.