Overpartitions with even parts distinct

DefinitionGenerating function of \((j, k)\)-overpartition pairs with even parts distinct#✓fully proved

For natural numbers \(j\) and \(k\), let \(f_a = \prod_{m \ge 1} (1 - q^{am})\) be the Euler products. This generating function is the integer power series \(f_4^2 \bigl(\prod_{i \ge 0} (1 + q^{j+ki})\bigr)^2 \, g\), where \(g\) is the inverse of \(f_1^2\) (whose constant coefficient is \(1\)) and the infinite products are taken in the coefficientwise topology. In \(q\)-Pochhammer notation it is \((q^4; q^4)_\infty^2 (-q^j; q^k)_\infty^2 / (q; q)_\infty^2\). It is used for \(k \ge j \ge 1\).

public noncomputable def overpartitionPairEvenDistinctGF (j k : ℕ) : ℤ⟦X⟧ :=
  qEulerProduct 4 ^ 2 * (∏' i : ℕ, (1 + X ^ (j + k * i))) ^ 2 *
    PowerSeries.invOfUnit (qEulerProduct 1 ^ 2) 1

Sources

• Adam Paksok and Nipen Saikia, New Congruences for [j, k]-Overpartition Pairs with Even Parts Distinct, INTEGERS 26 (2026), Article A118, Section 1, Equation (2).

Uses 1 · Used by 3

Statement usesThe Euler products of partition theory

Used byThe number of \((j, k)\)-overpartition pairs with even parts distinct · Cleared form of the generating function of \((j, k)\)-overpartition pairs with even parts distinct · The count of overpartition pairs of \(0\) with even parts distinct

DefinitionThe number of \((j, k)\)-overpartition pairs with even parts distinct#✓fully proved

For natural numbers \(j\), \(k\) and \(n\), \(\mathrm{bped}_{j,k}(n)\) is the integer coefficient of \(q^n\) in the generating function of \([j, k]\)-overpartition pairs with even parts distinct.

Combinatorially, for \(1 \le j \le k\), \(\mathrm{bped}_{j,k}(n)\) is the number of \([j, k]\)-overpartition pairs of \(n\) with even parts distinct, in which the first occurrence of each distinct part congruent to \(j\) modulo \(k\) may be overlined.

public noncomputable def overpartitionPairEvenDistinct (j k n : ℕ) : ℤ :=
  coeff n (overpartitionPairEvenDistinctGF j k)

Sources

• Adam Paksok and Nipen Saikia, New Congruences for [j, k]-Overpartition Pairs with Even Parts Distinct, INTEGERS 26 (2026), Article A118, Section 1, Equation (2).

Uses 1 · Used by 7

Statement usesGenerating function of \((j, k)\)-overpartition pairs with even parts distinct

Used byPaksok–Saikia congruences for \((3, 3)\)- and \((3, 6)\)-overpartition pairs (Theorem 2) · Paksok–Saikia congruences for \((3, 3)\)- and \((3, 6)\)-overpartition pairs (Theorem 3) · Paksok–Saikia congruences for \((3, 3)\)- and \((3, 6)\)-overpartition pairs (Theorem 4) · Paksok–Saikia congruences for \((3, 3)\)- and \((3, 6)\)-overpartition pairs (Theorem 5) · Paksok–Saikia congruences for \((3, 6)\)-overpartition pairs (Theorem 6) · Paksok–Saikia congruences for \((3, 3)\)-overpartition pairs (Theorem 1) · The count of overpartition pairs of \(0\) with even parts distinct

TheoremCleared form of the generating function of \((j, k)\)-overpartition pairs with even parts distinct#✓fully proved

Cleared form of the generating function of \([j, k]\)-overpartition pairs with even parts distinct. For natural numbers \(j\) and \(k\), let \(f_a = \prod_{m \ge 1} (1 - q^{am})\) be the Euler products and let \(G_{j,k}\) be the generating function of \([j, k]\)-overpartition pairs with even parts distinct. Then, as integer power series in \(q\), \(G_{j,k} \, f_1^2 = f_4^2 \bigl(\prod_{i \ge 0} (1 + q^{j+ki})\bigr)^2\), where the infinite product is taken in the coefficientwise topology. In \(q\)-Pochhammer notation this reads \(G_{j,k} \cdot (q; q)_\infty^2 = (q^4; q^4)_\infty^2 (-q^j; q^k)_\infty^2\).

public theorem overpartitionPairEvenDistinctGF_mul_qEulerProduct_sq (j k : ℕ) :
    overpartitionPairEvenDistinctGF j k * qEulerProduct 1 ^ 2 =
      qEulerProduct 4 ^ 2 * (∏' i : ℕ, (1 + X ^ (j + k * i))) ^ 2

Sources

• Adam Paksok and Nipen Saikia, New Congruences for [j, k]-Overpartition Pairs with Even Parts Distinct, INTEGERS 26 (2026), Article A118, Section 1, Equation (2).

Uses 3

Statement usesGenerating function of \((j, k)\)-overpartition pairs with even parts distinct · The Euler products of partition theory

Proof usesConstant term of the Euler products

TheoremThe count of overpartition pairs of \(0\) with even parts distinct#✓fully proved

For natural numbers \(j \ge 1\) and \(k \ge 1\), the number \(\mathrm{bped}_{j,k}(0)\) of \([j, k]\)-overpartition pairs of \(0\) with even parts distinct equals \(1\) (the pair of empty overpartitions).

public theorem overpartitionPairEvenDistinct_zero (j k : ℕ) (hj : 1 ≤ j) (hk : 1 ≤ k) :
    overpartitionPairEvenDistinct j k 0 = 1

Sources

• Adam Paksok and Nipen Saikia, New Congruences for [j, k]-Overpartition Pairs with Even Parts Distinct, INTEGERS 26 (2026), Article A118, Section 1, Equation (2).

Uses 4

Statement usesThe number of \((j, k)\)-overpartition pairs with even parts distinct

Proof usesConstant term of the Euler products · Generating function of \((j, k)\)-overpartition pairs with even parts distinct · The Euler products of partition theory

TheoremPaksok–Saikia congruences for \((3, 3)\)-overpartition pairs (Theorem 1)#●ready to prove

Let \(\mathrm{bped}_{j,k}(n)\) be the number of \([j, k]\)-overpartition pairs of \(n\) with even parts distinct. Let \(p > 5\) be a prime with Legendre symbol \(\left(\frac{-6}{p}\right) = -1\), and let \(k, m, \alpha, \beta\) be natural numbers with \(p \nmid m\). Then \(\mathrm{bped}_{3,3}\bigl(4 \cdot 3^{4\alpha+3} \cdot 5^{2\beta} p^{2k+1} m + (7 \cdot 3^{4\alpha+2} \cdot 5^{2\beta} p^{2k+2} - 1)/2\bigr) \equiv 0 \pmod{16}\) and \(\mathrm{bped}_{3,3}\bigl(12 \cdot 5^{2\beta} p^{2k+1} m + (7 \cdot 5^{2\beta} p^{2k+2} - 1)/2\bigr) \equiv 0 \pmod{8}\).

The paper prints \(p^{2\alpha+2}\) in place of \(p^{2k+2}\) in both congruences (its (6) and (7)); its proof substitutes \(n = p^{2k+1} m + 7(p^{2k+2} - 1)/24\), which gives \(p^{2k+2}\), and the printed exponent fails: at \(p = 13\), \(k = 1\), \(\alpha = \beta = 0\), \(m = 2\) the printed argument of the second congruence is \(53319\), and \(\mathrm{bped}_{3,3}(53319) \equiv 4 \pmod{8}\).

public theorem_wanted overpartitionPairEvenDistinct_three_three_congr_neg_six
    (p : ℕ) [Fact p.Prime] (hp : 5 < p) (hleg : legendreSym p (-6) = -1)
    (k m α β : ℕ) (hm : ¬ p ∣ m) :
    (16 : ℤ) ∣ overpartitionPairEvenDistinct 3 3
        (4 * 3 ^ (4 * α + 3) * 5 ^ (2 * β) * p ^ (2 * k + 1) * m +
          (7 * 3 ^ (4 * α + 2) * 5 ^ (2 * β) * p ^ (2 * k + 2) - 1) / 2) ∧
      (8 : ℤ) ∣ overpartitionPairEvenDistinct 3 3
        (12 * 5 ^ (2 * β) * p ^ (2 * k + 1) * m + (7 * 5 ^ (2 * β) * p ^ (2 * k + 2) - 1) / 2)

Sources

• Adam Paksok and Nipen Saikia, New Congruences for [j, k]-Overpartition Pairs with Even Parts Distinct, INTEGERS 26 (2026), Article A118, Theorem 1.

Uses 1

Statement usesThe number of \((j, k)\)-overpartition pairs with even parts distinct

TheoremPaksok–Saikia congruences for \((3, 3)\)- and \((3, 6)\)-overpartition pairs (Theorem 2)#●ready to prove

Let \(\mathrm{bped}_{j,k}(n)\) be the number of \([j, k]\)-overpartition pairs of \(n\) with even parts distinct. Let \(p \ge 5\) be a prime with Legendre symbol \(\left(\frac{-2}{p}\right) = -1\), and let \(k, m, \alpha, \beta\) be natural numbers with \(p \nmid m\). Then \(\mathrm{bped}_{3,3}\bigl(4 \cdot 3^{4\alpha+3} \cdot 5^{2\beta} p^{2k+1} m + (11 \cdot 3^{4\alpha+2} \cdot 5^{2\beta} p^{2k+2} - 1)/2\bigr) \equiv 0 \pmod{16}\), \(\mathrm{bped}_{3,3}\bigl(12 \cdot 5^{2\beta} p^{2k+1} m + (11 \cdot 5^{2\beta} p^{2k+2} - 1)/2\bigr) \equiv 0 \pmod{4}\), \(\mathrm{bped}_{3,6}\bigl(3^{4\alpha+2} \cdot 5^{2\beta} p^{2k+1} (24m + 11p)\bigr) \equiv 0 \pmod{32}\) and \(\mathrm{bped}_{3,6}\bigl(3 \cdot 5^{2\beta} p^{2k+1} (24m + 11p)\bigr) \equiv 0 \pmod{32}\).

The paper prints \(p^{2\alpha+2}\) in place of \(p^{2k+2}\) in the first two congruences (its (10) and (11)); the substitution in its proof gives \(p^{2k+2}\), and the printed exponent fails: at \(p = 5\), \(k = 1\), \(\alpha = \beta = 0\), \(m = 1\) the printed arguments are \(14737\) and \(1637\), and \(\mathrm{bped}_{3,3}(14737) \equiv 8 \pmod{16}\), \(\mathrm{bped}_{3,3}(1637) \equiv 2 \pmod{4}\).

public theorem_wanted overpartitionPairEvenDistinct_congr_neg_two_eleven
    (p : ℕ) [Fact p.Prime] (hp : 5 ≤ p) (hleg : legendreSym p (-2) = -1)
    (k m α β : ℕ) (hm : ¬ p ∣ m) :
    (16 : ℤ) ∣ overpartitionPairEvenDistinct 3 3
        (4 * 3 ^ (4 * α + 3) * 5 ^ (2 * β) * p ^ (2 * k + 1) * m +
          (11 * 3 ^ (4 * α + 2) * 5 ^ (2 * β) * p ^ (2 * k + 2) - 1) / 2) ∧
      (4 : ℤ) ∣ overpartitionPairEvenDistinct 3 3
        (12 * 5 ^ (2 * β) * p ^ (2 * k + 1) * m + (11 * 5 ^ (2 * β) * p ^ (2 * k + 2) - 1) / 2) ∧
      (32 : ℤ) ∣ overpartitionPairEvenDistinct 3 6
        (3 ^ (4 * α + 2) * 5 ^ (2 * β) * p ^ (2 * k + 1) * (24 * m + 11 * p)) ∧
      (32 : ℤ) ∣ overpartitionPairEvenDistinct 3 6
        (3 * 5 ^ (2 * β) * p ^ (2 * k + 1) * (24 * m + 11 * p))

Sources

• Adam Paksok and Nipen Saikia, New Congruences for [j, k]-Overpartition Pairs with Even Parts Distinct, INTEGERS 26 (2026), Article A118, Theorem 2.

Uses 1

Statement usesThe number of \((j, k)\)-overpartition pairs with even parts distinct

TheoremPaksok–Saikia congruences for \((3, 3)\)- and \((3, 6)\)-overpartition pairs (Theorem 3)#●ready to prove

Let \(\mathrm{bped}_{j,k}(n)\) be the number of \([j, k]\)-overpartition pairs of \(n\) with even parts distinct. Let \(p \ge 5\) be a prime with Legendre symbol \(\left(\frac{-2}{p}\right) = -1\), and let \(k, m, \alpha, \beta\) be natural numbers with \(p \nmid m\). Then \(\mathrm{bped}_{3,3}\bigl(4 \cdot 3^{4\alpha+3} \cdot 5^{2\beta} p^{2k+1} m + (19 \cdot 3^{4\alpha+2} \cdot 5^{2\beta} p^{2k+2} - 1)/2\bigr) \equiv 0 \pmod{16}\), \(\mathrm{bped}_{3,3}\bigl(12 \cdot 5^{2\beta} p^{2k+1} m + (19 \cdot 5^{2\beta} p^{2k+2} - 1)/2\bigr) \equiv 0 \pmod{8}\), \(\mathrm{bped}_{3,6}\bigl(3^{4\alpha+2} \cdot 5^{2\beta} p^{2k+1} (24m + 19p)\bigr) \equiv 0 \pmod{32}\) and \(\mathrm{bped}_{3,6}\bigl(3 \cdot 5^{2\beta} p^{2k+1} (24m + 19p)\bigr) \equiv 0 \pmod{32}\).

The paper prints \(p^{2\alpha+2}\) in place of \(p^{2k+2}\) in the first two congruences (its (16) and (17)); the substitution in its proof gives \(p^{2k+2}\), and the printed exponent fails: at \(p = 5\), \(k = 1\), \(\alpha = \beta = 0\), \(m = 1\) the printed arguments are \(15637\) and \(1737\), and \(\mathrm{bped}_{3,3}(15637) \equiv 8 \pmod{16}\), \(\mathrm{bped}_{3,3}(1737) \equiv 4 \pmod{8}\).

public theorem_wanted overpartitionPairEvenDistinct_congr_neg_two_nineteen
    (p : ℕ) [Fact p.Prime] (hp : 5 ≤ p) (hleg : legendreSym p (-2) = -1)
    (k m α β : ℕ) (hm : ¬ p ∣ m) :
    (16 : ℤ) ∣ overpartitionPairEvenDistinct 3 3
        (4 * 3 ^ (4 * α + 3) * 5 ^ (2 * β) * p ^ (2 * k + 1) * m +
          (19 * 3 ^ (4 * α + 2) * 5 ^ (2 * β) * p ^ (2 * k + 2) - 1) / 2) ∧
      (8 : ℤ) ∣ overpartitionPairEvenDistinct 3 3
        (12 * 5 ^ (2 * β) * p ^ (2 * k + 1) * m + (19 * 5 ^ (2 * β) * p ^ (2 * k + 2) - 1) / 2) ∧
      (32 : ℤ) ∣ overpartitionPairEvenDistinct 3 6
        (3 ^ (4 * α + 2) * 5 ^ (2 * β) * p ^ (2 * k + 1) * (24 * m + 19 * p)) ∧
      (32 : ℤ) ∣ overpartitionPairEvenDistinct 3 6
        (3 * 5 ^ (2 * β) * p ^ (2 * k + 1) * (24 * m + 19 * p))

Sources

• Adam Paksok and Nipen Saikia, New Congruences for [j, k]-Overpartition Pairs with Even Parts Distinct, INTEGERS 26 (2026), Article A118, Theorem 3.

Uses 1

Statement usesThe number of \((j, k)\)-overpartition pairs with even parts distinct

TheoremPaksok–Saikia congruences for \((3, 3)\)- and \((3, 6)\)-overpartition pairs (Theorem 4)#●ready to prove

Let \(\mathrm{bped}_{j,k}(n)\) be the number of \([j, k]\)-overpartition pairs of \(n\) with even parts distinct. Let \(p \ge 5\) be a prime with Legendre symbol \(\left(\frac{-1}{p}\right) = -1\), and let \(k, m, \alpha, \gamma\) be natural numbers with \(p \nmid m\). Then \(\mathrm{bped}_{3,3}\bigl(4 \cdot 3^{4\alpha+2} \cdot 7^{2\gamma} p^{2k+1} m + (5 \cdot 3^{4\alpha+1} \cdot 7^{2\gamma} p^{2k+2} - 1)/2\bigr) \equiv 0 \pmod{8}\), \(\mathrm{bped}_{3,6}\bigl(3^{4\alpha+2} \cdot 7^{2\gamma} p^{2k+1} (24m + 5p)\bigr) \equiv 0 \pmod{16}\) and \(\mathrm{bped}_{3,6}\bigl(3 \cdot 7^{2\gamma} p^{2k+1} (24m + 5p)\bigr) \equiv 0 \pmod{16}\).

The paper allows \(p \ge 3\), but its proof needs \(p \nmid 24m + 5p\), which fails for \(p = 3\), and all three congruences fail there: at \(k = \alpha = \gamma = 0\), \(m = 1\) one has \(\mathrm{bped}_{3,3}(175) \equiv 4 \pmod{8}\), \(\mathrm{bped}_{3,6}(1053) \equiv 8 \pmod{16}\) and \(\mathrm{bped}_{3,6}(351) \equiv 8 \pmod{16}\); so \(p \ge 5\) is assumed. The paper also prints \(p^{2\alpha+2}\) in place of \(p^{2k+2}\) in the first congruence (its (22)); the substitution in its proof gives \(p^{2k+2}\), and the printed exponent fails: at \(p = 7\), \(k = 1\), \(\alpha = \gamma = 0\), \(m = 1\) the printed argument is \(12715\), and \(\mathrm{bped}_{3,3}(12715) \equiv 4 \pmod{8}\).

public theorem_wanted overpartitionPairEvenDistinct_congr_neg_one_five
    (p : ℕ) [Fact p.Prime] (hp : 5 ≤ p) (hleg : legendreSym p (-1) = -1)
    (k m α γ : ℕ) (hm : ¬ p ∣ m) :
    (8 : ℤ) ∣ overpartitionPairEvenDistinct 3 3
        (4 * 3 ^ (4 * α + 2) * 7 ^ (2 * γ) * p ^ (2 * k + 1) * m +
          (5 * 3 ^ (4 * α + 1) * 7 ^ (2 * γ) * p ^ (2 * k + 2) - 1) / 2) ∧
      (16 : ℤ) ∣ overpartitionPairEvenDistinct 3 6
        (3 ^ (4 * α + 2) * 7 ^ (2 * γ) * p ^ (2 * k + 1) * (24 * m + 5 * p)) ∧
      (16 : ℤ) ∣ overpartitionPairEvenDistinct 3 6
        (3 * 7 ^ (2 * γ) * p ^ (2 * k + 1) * (24 * m + 5 * p))

Sources

• Adam Paksok and Nipen Saikia, New Congruences for [j, k]-Overpartition Pairs with Even Parts Distinct, INTEGERS 26 (2026), Article A118, Theorem 4.

Uses 1

Statement usesThe number of \((j, k)\)-overpartition pairs with even parts distinct

TheoremPaksok–Saikia congruences for \((3, 3)\)- and \((3, 6)\)-overpartition pairs (Theorem 5)#●ready to prove

Let \(\mathrm{bped}_{j,k}(n)\) be the number of \([j, k]\)-overpartition pairs of \(n\) with even parts distinct. Let \(p \ge 5\) be a prime with Legendre symbol \(\left(\frac{-3}{p}\right) = -1\), and let \(k, m, \alpha, \beta\) be natural numbers with \(p \nmid m\). Then \(\mathrm{bped}_{3,3}\bigl(4 \cdot 3^{4\alpha+2} \cdot 5^{2\beta} p^{2k+1} m + (13 \cdot 3^{4\alpha+1} \cdot 5^{2\beta} p^{2k+2} - 1)/2\bigr) \equiv 0 \pmod{8}\), \(\mathrm{bped}_{3,6}\bigl(3^{4\alpha+2} \cdot 5^{2\beta} p^{2k+1} (24m + 13p)\bigr) \equiv 0 \pmod{16}\) and \(\mathrm{bped}_{3,6}\bigl(3 \cdot 5^{2\beta} p^{2k+1} (24m + 13p)\bigr) \equiv 0 \pmod{16}\).

The paper prints \(p^{2\alpha+2}\) in place of \(p^{2k+2}\) in the first congruence (its (27)); the substitution in its proof gives \(p^{2k+2}\), and the printed exponent fails: at \(p = 5\), \(k = 1\), \(\alpha = \beta = 0\), \(m = 3\) the printed argument is \(13987\), and \(\mathrm{bped}_{3,3}(13987) \equiv 4 \pmod{8}\).

public theorem_wanted overpartitionPairEvenDistinct_congr_neg_three_thirteen
    (p : ℕ) [Fact p.Prime] (hp : 5 ≤ p) (hleg : legendreSym p (-3) = -1)
    (k m α β : ℕ) (hm : ¬ p ∣ m) :
    (8 : ℤ) ∣ overpartitionPairEvenDistinct 3 3
        (4 * 3 ^ (4 * α + 2) * 5 ^ (2 * β) * p ^ (2 * k + 1) * m +
          (13 * 3 ^ (4 * α + 1) * 5 ^ (2 * β) * p ^ (2 * k + 2) - 1) / 2) ∧
      (16 : ℤ) ∣ overpartitionPairEvenDistinct 3 6
        (3 ^ (4 * α + 2) * 5 ^ (2 * β) * p ^ (2 * k + 1) * (24 * m + 13 * p)) ∧
      (16 : ℤ) ∣ overpartitionPairEvenDistinct 3 6
        (3 * 5 ^ (2 * β) * p ^ (2 * k + 1) * (24 * m + 13 * p))

Sources

• Adam Paksok and Nipen Saikia, New Congruences for [j, k]-Overpartition Pairs with Even Parts Distinct, INTEGERS 26 (2026), Article A118, Theorem 5.

Uses 1

Statement usesThe number of \((j, k)\)-overpartition pairs with even parts distinct

TheoremPaksok–Saikia congruences for \((3, 6)\)-overpartition pairs (Theorem 6)#●ready to prove

Let \(\mathrm{bped}_{j,k}(n)\) be the number of \([j, k]\)-overpartition pairs of \(n\) with even parts distinct. Let \(p \ge 5\) be a prime with Legendre symbol \(\left(\frac{-1}{p}\right) = -1\), and let \(k, m, \alpha\) be natural numbers with \(p \nmid m\). Then \(\mathrm{bped}_{3,6}\bigl(3^{4\alpha+2} p^{2k+1} (12m + 5p)\bigr) \equiv 0 \pmod{16}\) and \(\mathrm{bped}_{3,6}\bigl(3 p^{2k+1} (12m + 5p)\bigr) \equiv 0 \pmod{16}\).

The paper allows \(p \ge 3\), but its proof needs \(p \nmid 24m + 10p\), which fails for \(p = 3\), and both congruences fail there: at \(k = \alpha = 0\), \(m = 1\) one has \(\mathrm{bped}_{3,6}(729) \equiv 12 \pmod{16}\) and \(\mathrm{bped}_{3,6}(243) \equiv 12 \pmod{16}\); so \(p \ge 5\) is assumed. The paper's unused quantifier \(\beta\) is dropped.

public theorem_wanted overpartitionPairEvenDistinct_three_six_congr_neg_one_five
    (p : ℕ) [Fact p.Prime] (hp : 5 ≤ p) (hleg : legendreSym p (-1) = -1)
    (k m α : ℕ) (hm : ¬ p ∣ m) :
    (16 : ℤ) ∣ overpartitionPairEvenDistinct 3 6
        (3 ^ (4 * α + 2) * p ^ (2 * k + 1) * (12 * m + 5 * p)) ∧
      (16 : ℤ) ∣ overpartitionPairEvenDistinct 3 6 (3 * p ^ (2 * k + 1) * (12 * m + 5 * p))

Sources

• Adam Paksok and Nipen Saikia, New Congruences for [j, k]-Overpartition Pairs with Even Parts Distinct, INTEGERS 26 (2026), Article A118, Theorem 6.

Uses 1

Statement usesThe number of \((j, k)\)-overpartition pairs with even parts distinct

TheoremRamanujan's 5-dissection of Euler's product#●ready to prove

Let \(q\) be a complex number with \(|q| < 1\). For \(k \ge 1\) let \(f_k = (q^k; q^k)_\infty = \prod_{n \ge 0} (1 - q^k q^{kn})\), and for complex \(a\), \(b\) with \(|a|, |b| < 1\) let \(f(a, b) = \sum_{n \in \mathbb{Z}} a^{n(n+1)/2} b^{n(n-1)/2}\) be Ramanujan's general theta function; all these products and series converge, so the raw infinite product and the raw theta sum take these values. For \(|x| < 1\) put \(R(x) = f(-x, -x^4) / f(-x^2, -x^3)\). Then \(f_1 = f_{25} \left( R(q^5)^{-1} - q - q^2 R(q^5) \right)\).

public theorem_wanted qPochhammerInf_five_dissection (q : ℂ) (hq : ‖q‖ < 1) :
    let R : ℂ → ℂ := fun x => ramanujanThetaRaw (-x) (-x ^ 4) / ramanujanThetaRaw (-x ^ 2) (-x ^ 3)
    qPochhammerInfRaw q q =
      qPochhammerInfRaw (q ^ 25) (q ^ 25) * ((R (q ^ 5))⁻¹ - q - q ^ 2 * R (q ^ 5))

Sources

• Harishkumar T, Shruthi Menezes, and M. S. Mahadeva Naika, On [j, k]-Overpartitions with Even Parts Distinct, INTEGERS 25 (2025), Article A69, Lemma 5.

Uses 2

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

TheoremRamanujan's 7-dissection of Euler's product#●ready to prove

Let \(q\) be a complex number with \(|q| < 1\). For \(k \ge 1\) let \(f_k = (q^k; q^k)_\infty = \prod_{n \ge 0} (1 - q^k q^{kn})\), and for complex \(a\), \(b\) with \(|a|, |b| < 1\) let \(f(a, b) = \sum_{n \in \mathbb{Z}} a^{n(n+1)/2} b^{n(n-1)/2}\) be Ramanujan's general theta function; all these products and series converge, so the raw infinite product and the raw theta sum take these values. For \(|x| < 1\) put \(A(x) = f(-x^3, -x^4)\), \(B(x) = f(-x^2, -x^5)\) and \(C(x) = f(-x, -x^6)\). Then \(f_1 = f_{49} \left( B(q^7)/C(q^7) - q A(q^7)/B(q^7) - q^2 + q^5 C(q^7)/A(q^7) \right)\).

public theorem_wanted qPochhammerInf_seven_dissection (q : ℂ) (hq : ‖q‖ < 1) :
    let A : ℂ → ℂ := fun x => ramanujanThetaRaw (-x ^ 3) (-x ^ 4)
    let B : ℂ → ℂ := fun x => ramanujanThetaRaw (-x ^ 2) (-x ^ 5)
    let C : ℂ → ℂ := fun x => ramanujanThetaRaw (-x) (-x ^ 6)
    qPochhammerInfRaw q q =
      qPochhammerInfRaw (q ^ 49) (q ^ 49) *
        (B (q ^ 7) / C (q ^ 7) - q * A (q ^ 7) / B (q ^ 7) - q ^ 2 + q ^ 5 * C (q ^ 7) / A (q ^ 7))

Sources

• Harishkumar T, Shruthi Menezes, and M. S. Mahadeva Naika, On [j, k]-Overpartitions with Even Parts Distinct, INTEGERS 25 (2025), Article A69, Lemma 6.

Uses 2

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

DefinitionThe generating series for \(\mathrm{ped}_{9,9}\)#✓fully proved

For \(k \ge 1\) let \(f_k = \prod_{m \ge 1} (1 - q^{km})\), an integer power series in \(q\) with constant coefficient \(1\). This is the integer power series

\[\frac{f_4 f_{18}}{f_1 f_9},\]

where the inverse of \(f_1 f_9\) is taken in the ring of integer power series. For a natural number \(n\), its coefficient of \(q^n\) is denoted \(\mathrm{ped}_{9,9}(n)\).

By the source's equation (2), this is the generating function of the \([9, 9]\)-overpartitions with even parts distinct: partitions whose even parts are distinct, in which the first occurrence of each part divisible by \(9\) may be overlined.

noncomputable def pedNineNineSeries : ℤ⟦X⟧ :=
  𝔣 4 * 𝔣 18 * invOfUnit (𝔣 1 * 𝔣 9) 1

Sources

• Harishkumar T, Shruthi Menezes, and M. S. Mahadeva Naika, On [j, k]-Overpartitions with Even Parts Distinct, INTEGERS 25 (2025), Article A69, equations (2) and (22).

Uses 1 · Used by 2

Statement usesThe Euler products of partition theory

Used byThe partition function \(\mathrm{ped}_{9,9}\) · Generating function identity for \(\mathrm{ped}_{9,9}\)

DefinitionThe partition function \(\mathrm{ped}_{9,9}\)#✓fully proved

For \(k \ge 1\) let \(f_k = \prod_{m \ge 1} (1 - q^{km})\), an integer power series in \(q\) with constant coefficient \(1\). For a natural number \(n\), \(\mathrm{ped}_{9,9}(n)\) is the integer coefficient of \(q^n\) in the power series \(f_4 f_{18} / (f_1 f_9)\).

By the source's equation (2), \(\mathrm{ped}_{9,9}(n)\) is the number of \([9, 9]\)-overpartitions of \(n\) with even parts distinct.

noncomputable def pedNineNine (n : ℕ) : ℤ :=
  coeff n pedNineNineSeries

Sources

• Harishkumar T, Shruthi Menezes, and M. S. Mahadeva Naika, On [j, k]-Overpartitions with Even Parts Distinct, INTEGERS 25 (2025), Article A69, equations (2) and (22).

Uses 1 · Used by 5

Statement usesThe generating series for \(\mathrm{ped}_{9,9}\)

Used byCongruences modulo 16 for \(\mathrm{ped}_{9,9}\) · Congruences modulo 32 for \(\mathrm{ped}_{9,9}\) · Generating function identity for \(\mathrm{ped}_{9,9}\) · Further congruences modulo 16 for \(\mathrm{ped}_{9,9}\) · Values of \(\mathrm{ped}_{9,9}\) and \(\mathrm{ped}_{9,18}\) at \(0\)

DefinitionThe generating series for \(\mathrm{ped}_{9,18}\)#✓fully proved

For \(k \ge 1\) let \(f_k = \prod_{m \ge 1} (1 - q^{km})\), an integer power series in \(q\) with constant coefficient \(1\). This is the integer power series

\[\frac{f_4 f_{18}^2}{f_1 f_9 f_{36}},\]

where the inverse of \(f_1 f_9 f_{36}\) is taken in the ring of integer power series. For a natural number \(n\), its coefficient of \(q^n\) is denoted \(\mathrm{ped}_{9,18}(n)\).

By the source's equation (2), this is the generating function of the \([9, 18]\)-overpartitions with even parts distinct: partitions whose even parts are distinct, in which the first occurrence of each part congruent to \(9\) modulo \(18\) may be overlined.

noncomputable def pedNineEighteenSeries : ℤ⟦X⟧ :=
  𝔣 4 * 𝔣 18 ^ 2 * invOfUnit (𝔣 1 * 𝔣 9 * 𝔣 36) 1

Sources

• Harishkumar T, Shruthi Menezes, and M. S. Mahadeva Naika, On [j, k]-Overpartitions with Even Parts Distinct, INTEGERS 25 (2025), Article A69, equations (2) and (77).

Uses 1 · Used by 2

Statement usesThe Euler products of partition theory

Used byThe partition function \(\mathrm{ped}_{9,18}\) · Product identity for the (9, 18)-overpartition generating function

DefinitionThe partition function \(\mathrm{ped}_{9,18}\)#✓fully proved

For \(k \ge 1\) let \(f_k = \prod_{m \ge 1} (1 - q^{km})\), an integer power series in \(q\) with constant coefficient \(1\). For a natural number \(n\), \(\mathrm{ped}_{9,18}(n)\) is the integer coefficient of \(q^n\) in the power series \(f_4 f_{18}^2 / (f_1 f_9 f_{36})\).

By the source's equation (2), \(\mathrm{ped}_{9,18}(n)\) is the number of \([9, 18]\)-overpartitions of \(n\) with even parts distinct.

noncomputable def pedNineEighteen (n : ℕ) : ℤ :=
  coeff n pedNineEighteenSeries

Sources

• Harishkumar T, Shruthi Menezes, and M. S. Mahadeva Naika, On [j, k]-Overpartitions with Even Parts Distinct, INTEGERS 25 (2025), Article A69, equations (2) and (77).

Uses 1 · Used by 7

Statement usesThe generating series for \(\mathrm{ped}_{9,18}\)

Used byCongruences modulo 9 and 27 for (9, 18)-overpartitions with even parts distinct · Congruences modulo 16 and 8 for (9, 18)-overpartitions with even parts distinct · Congruences modulo 64 for (9, 18)-overpartitions with even parts distinct · Congruences modulo 32 for (9, 18)-overpartitions with even parts distinct · Congruences modulo 27 for (9, 18)-overpartitions from the cubic coefficient vectors · Product identity for the (9, 18)-overpartition generating function · Values of \(\mathrm{ped}_{9,9}\) and \(\mathrm{ped}_{9,18}\) at \(0\)

TheoremGenerating function identity for \(\mathrm{ped}_{9,9}\)#✓fully proved

For \(k \ge 1\) let \(f_k = \prod_{m \ge 1} (1 - q^{km})\), an integer power series in \(q\), and let \(\mathrm{ped}_{9,9}(n)\) be the coefficient of \(q^n\) in \(f_4 f_{18} / (f_1 f_9)\). Then, as integer power series in \(q\),

\[f_1 f_9 \sum_{n \ge 0} \mathrm{ped}_{9,9}(n) q^n = f_4 f_{18}.\]

theorem pedNineNine_generatingFunction :
    𝔣 1 * 𝔣 9 * PowerSeries.mk pedNineNine = 𝔣 4 * 𝔣 18

Sources

• Harishkumar T, Shruthi Menezes, and M. S. Mahadeva Naika, On [j, k]-Overpartitions with Even Parts Distinct, INTEGERS 25 (2025), Article A69, equation (22).

Uses 4 · Used by 1

Statement usesThe partition function \(\mathrm{ped}_{9,9}\) · The Euler products of partition theory

Proof usesConstant term of the Euler products · The generating series for \(\mathrm{ped}_{9,9}\)

Used byValues of \(\mathrm{ped}_{9,9}\) and \(\mathrm{ped}_{9,18}\) at \(0\)

TheoremProduct identity for the (9, 18)-overpartition generating function#✓fully proved

Let \(\mathrm{ped}_{9,18}(n)\) be the number of \([9, 18]\)-overpartitions of \(n\) with even parts distinct, and let \(f_k = \prod_{m \ge 1} (1 - q^{km})\). Then, as integer power series in \(q\), \(f_1 f_9 f_{36} \sum_{n \ge 0} \mathrm{ped}_{9,18}(n) q^n = f_4 f_{18}^2\).

theorem pedNineEighteen_generatingFunction :
    𝔣 1 * 𝔣 9 * 𝔣 36 * PowerSeries.mk pedNineEighteen = 𝔣 4 * 𝔣 18 ^ 2

Sources

• Harishkumar T, Shruthi Menezes, and M. S. Mahadeva Naika, On [j, k]-Overpartitions with Even Parts Distinct, INTEGERS 25 (2025), Article A69, equation (77).

Uses 4 · Used by 1

Statement usesThe partition function \(\mathrm{ped}_{9,18}\) · The Euler products of partition theory

Proof usesConstant term of the Euler products · The generating series for \(\mathrm{ped}_{9,18}\)

Used byValues of \(\mathrm{ped}_{9,9}\) and \(\mathrm{ped}_{9,18}\) at \(0\)

TheoremValues of \(\mathrm{ped}_{9,9}\) and \(\mathrm{ped}_{9,18}\) at \(0\)#✓fully proved

For \(k \ge 1\) let \(f_k = \prod_{m \ge 1} (1 - q^{km})\), an integer power series in \(q\), and let \(\mathrm{ped}_{9,9}(n)\) and \(\mathrm{ped}_{9,18}(n)\) be the coefficients of \(q^n\) in \(f_4 f_{18} / (f_1 f_9)\) and in \(f_4 f_{18}^2 / (f_1 f_9 f_{36})\). Then \(\mathrm{ped}_{9,9}(0) = \mathrm{ped}_{9,18}(0) = 1\).

Both values count the empty overpartition.

theorem pedNineNine_zero_and_pedNineEighteen_zero :
    pedNineNine 0 = 1 ∧ pedNineEighteen 0 = 1

Sources

• Harishkumar T, Shruthi Menezes, and M. S. Mahadeva Naika, On [j, k]-Overpartitions with Even Parts Distinct, INTEGERS 25 (2025), Article A69, equations (22) and (77).

Uses 6

Statement usesThe partition function \(\mathrm{ped}_{9,18}\) · The partition function \(\mathrm{ped}_{9,9}\)

Proof usesConstant term of the Euler products · Product identity for the (9, 18)-overpartition generating function · Generating function identity for \(\mathrm{ped}_{9,9}\) · The Euler products of partition theory

DefinitionChan's matrix#✓fully proved

Chan's matrix \((m_{i,j})_{i,j \ge 1}\) is the integer matrix with first column \(m_{1,1} = 3\), \(m_{2,1} = 2\), \(m_{3,1} = 1\) and \(m_{i,1} = 0\) for \(i \ge 4\), and with \(m_{i,j} = 9 m_{i-1,j-1} + 3 m_{i-2,j-1} + m_{i-3,j-1}\) for \(i \ge 1\) and \(j \ge 2\), where entries with row index \(\le 0\) are taken to be \(0\).

The formalization indexes the matrix by all natural numbers, with row \(0\) and column \(0\) equal to \(0\).

def chanCubicMatrix : ℕ → ℕ → ℤ
  | _, 0 => 0
  | i, 1 => if i = 1 then 3 else if i = 2 then 2 else if i = 3 then 1 else 0
  | i, j + 2 =>
      9 * chanCubicMatrix (i - 1) (j + 1) + 3 * chanCubicMatrix (i - 2) (j + 1) +
        chanCubicMatrix (i - 3) (j + 1)

Sources

• Harishkumar T, Shruthi Menezes, and M. S. Mahadeva Naika, On [j, k]-Overpartitions with Even Parts Distinct, INTEGERS 25 (2025), Article A69, Section 2 (from H. C. Chan, Int. J. Number Theory 6 (2010), (11)-(19)).

Used by 2

Used byFirst six rows of Chan's matrix · Coefficient vectors from Chan's matrix

TheoremFirst six rows of Chan's matrix#✓fully proved

The upper left \(6 \times 6\) block of Chan's matrix \((m_{i,j})_{i,j \ge 1}\) is lower triangular, and its rows up to the diagonal are \((3)\), \((2, 27)\), \((1, 27, 243)\), \((0, 18, 324, 2187)\), \((0, 5, 270, 3645, 19683)\) and \((0, 1, 126, 3645, 39366, 177147)\): for \(1 \le j \le i \le 6\), \(m_{i,j}\) is the \(j\)th entry of the \(i\)th listed row, and \(m_{i,j} = 0\) for \(1 \le i < j \le 6\).

theorem chanCubicMatrix_first_rows :
    (List.range 6).map (fun i => (List.range 6).map fun j => chanCubicMatrix (i + 1) (j + 1)) =
      [[3, 0, 0, 0, 0, 0], [2, 27, 0, 0, 0, 0], [1, 27, 243, 0, 0, 0],
        [0, 18, 324, 2187, 0, 0], [0, 5, 270, 3645, 19683, 0],
        [0, 1, 126, 3645, 39366, 177147]]

Sources

• Harishkumar T, Shruthi Menezes, and M. S. Mahadeva Naika, On [j, k]-Overpartitions with Even Parts Distinct, INTEGERS 25 (2025), Article A69, Section 2.

Uses 1

Statement usesChan's matrix

DefinitionCoefficient vectors from Chan's matrix#✓fully proved

Let \((m_{i,j})_{i,j \ge 1}\) be Chan's matrix, and for \(i, j \ge 1\) let \(a_{i,j} = m_{4i-3,i+j-1}\) and \(b_{i,j} = m_{4i-1,i+j-1}\) be the entries of the infinite matrices \(A\) and \(B\). The coefficient vectors \(X_\alpha = (x_{\alpha,1}, x_{\alpha,2}, \dots)\) of integers, for \(\alpha \ge 0\), are defined by \(X_0 = (1, 0, 0, \dots)\) and, for \(j \ge 1\), \(x_{\alpha+1,j} = \sum_{i=1}^{3^\alpha} x_{\alpha,i} a_{i,j}\) if \(\alpha\) is even and \(x_{\alpha+1,j} = \sum_{i=1}^{3^\alpha} x_{\alpha,i} b_{i,j}\) if \(\alpha\) is odd.

Since Chan's matrix is lower triangular, row \(i\) of \(A\) or \(B\) vanishes beyond column \(3i\), so by induction \(x_{\alpha,i} = 0\) for \(i > 3^\alpha\); hence \(X_{\alpha+1} = X_\alpha A\) for even \(\alpha\) and \(X_{\alpha+1} = X_\alpha B\) for odd \(\alpha\).

The formalization indexes the vectors from \(0\): its value at \((\alpha, i)\) is \(x_{\alpha,i+1}\).

def cubicCoeffVector : ℕ → ℕ → ℤ
  | 0, i => if i = 0 then 1 else 0
  | α + 1, j => ∑ i ∈ Finset.range (3 ^ α), cubicCoeffVector α i *
      (if Even α then chanCubicMatrix (4 * i + 1) (i + j + 1)
        else chanCubicMatrix (4 * i + 3) (i + j + 1))

Sources

• Harishkumar T, Shruthi Menezes, and M. S. Mahadeva Naika, On [j, k]-Overpartitions with Even Parts Distinct, INTEGERS 25 (2025), Article A69, Section 2, equations (3)-(4), and Theorem 8.

Uses 1 · Used by 2

Statement usesChan's matrix

Used byInitial values of the cubic coefficient vectors · Congruences modulo 27 for (9, 18)-overpartitions from the cubic coefficient vectors

TheoremInitial values of the cubic coefficient vectors#✓fully proved

The coefficient vectors \(X_\alpha = (x_{\alpha,1}, x_{\alpha,2}, \dots)\) built from Chan's matrix satisfy \((x_{1,1}, \dots, x_{1,5}) = (3, 0, 0, 0, 0)\) and \((x_{2,1}, \dots, x_{2,5}) = (3, 81, 729, 0, 0)\).

theorem cubicCoeffVector_one_two :
    (List.range 5).map (cubicCoeffVector 1) = [3, 0, 0, 0, 0] ∧
      (List.range 5).map (cubicCoeffVector 2) = [3, 81, 729, 0, 0]

Sources

• Harishkumar T, Shruthi Menezes, and M. S. Mahadeva Naika, On [j, k]-Overpartitions with Even Parts Distinct, INTEGERS 25 (2025), Article A69, Theorem 8.

Uses 1

Statement usesCoefficient vectors from Chan's matrix

TheoremThe 2-dissection of \(f_1^4\)#●ready to prove

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

\[f_1^4 f_2^2 f_4^2 f_8^4 = f_4^{12} - 4 q f_2^4 f_8^8.\]

Dividing by \(f_2^2 f_4^2 f_8^4\) gives \(f_1^4 = \frac{f_4^{10}}{f_2^2 f_8^4} - 4q \frac{f_2^2 f_8^4}{f_4^2}\).

public theorem_wanted qEulerProduct_fourth_two_dissection :
    𝔣 1 ^ 4 * 𝔣 2 ^ 2 * 𝔣 4 ^ 2 * 𝔣 8 ^ 4 = 𝔣 4 ^ 12 - 4 * X * 𝔣 2 ^ 4 * 𝔣 8 ^ 8

Sources

• Harishkumar T, Shruthi Menezes, and M. S. Mahadeva Naika, On [j, k]-Overpartitions with Even Parts Distinct, INTEGERS 25 (2025), Article A69, Lemma 1, (7).

Uses 1

Statement usesThe Euler products of partition theory

TheoremA 3-dissection of a quotient of Euler products#●ready to prove

In the ring of integer power series in \(q\), let \(f_k = \prod_{m \ge 1} (1 - q^{km})\) denote the Euler products. Then \(f_1^2 f_6 f_9 f_{18} = f_2 f_6 f_9^3 - 2q f_2 f_3 f_{18}^3\). Since every \(f_k\) with \(k \ge 1\) has constant term \(1\), this is the 3-dissection \(f_1^2 / f_2 = f_9^2 / f_{18} - 2q f_3 f_{18}^2 / (f_6 f_9)\) with denominators cleared.

public theorem_wanted qEulerProduct_sq_div_three_dissection :
    𝔣 1 ^ 2 * 𝔣 6 * 𝔣 9 * 𝔣 18 = 𝔣 2 * 𝔣 6 * 𝔣 9 ^ 3 - 2 * X * 𝔣 2 * 𝔣 3 * 𝔣 18 ^ 3

Sources

• Harishkumar T, Shruthi Menezes, and M. S. Mahadeva Naika, On [j, k]-Overpartitions with Even Parts Distinct, INTEGERS 25 (2025), Article A69, Lemma 3, (11).

Uses 1

Statement usesThe Euler products of partition theory

TheoremCongruences modulo 32 for \(\mathrm{ped}_{9,9}\)#●ready to prove

For \(k \ge 1\) let \(f_k = \prod_{m \ge 1} (1 - q^{km})\), an integer power series in \(q\), and let \(\mathrm{ped}_{9,9}(n)\) be the coefficient of \(q^n\) in \(f_4 f_{18} / (f_1 f_9)\). Then for all natural numbers \(\alpha\), \(\beta\) and \(n\) the following congruences modulo \(32\) hold, where every division is exact.

(18) The coefficient of \(q^n\) in \(f_2^2 \sum_{m \ge 0} \mathrm{ped}_{9,9}(3^{4\alpha+2} m + (3^{4\alpha+2} - 1)/2) q^m\) is congruent to the coefficient of \(q^n\) in \(4 f_1^3 f_3 f_4 f_6 + 16 q f_2^2 f_6^6\). This is the source's congruence \(\sum_{m \ge 0} \mathrm{ped}_{9,9}(3^{4\alpha+2} m + (3^{4\alpha+2} - 1)/2) q^m \equiv 4 f_1^3 f_3 f_4 f_6 / f_2^2 + 16 q f_6^6\) multiplied by \(f_2^2\).

(19) \(\mathrm{ped}_{9,9}(4 \cdot 3^{4\alpha+6} n + (19 \cdot 3^{4\alpha+5} - 1)/2) \equiv \mathrm{ped}_{9,9}(4 \cdot 3^{4\alpha+4} n + (19 \cdot 3^{4\alpha+3} - 1)/2)\).

(20) \(\mathrm{ped}_{9,9}(4 \cdot 3^{4\alpha+4} \cdot 5^{2\beta} n + (19 \cdot 3^{4\alpha+3} \cdot 5^{2\beta} - 1)/2)\) is congruent to the coefficient of \(q^n\) in \(16 f_1 f_6^3\).

(21) \(\mathrm{ped}_{9,9}(4 \cdot 3^{4\alpha+4} \cdot 5^{2\beta+1} (5n + i) + (23 \cdot 3^{4\alpha+3} \cdot 5^{2\beta+1} - 1)/2) \equiv 0\) for \(i \in \{0, 1, 2, 4\}\).

public theorem_wanted pedNineNine_congruences_mod_thirtyTwo (α β n : ℕ) :
    coeff n (𝔣 2 ^ 2 *
        PowerSeries.mk fun m => pedNineNine (3 ^ (4 * α + 2) * m + (3 ^ (4 * α + 2) - 1) / 2)) ≡
      coeff n (4 * 𝔣 1 ^ 3 * 𝔣 3 * 𝔣 4 * 𝔣 6 + 16 * X * 𝔣 2 ^ 2 * 𝔣 6 ^ 6) [ZMOD 32] ∧
    pedNineNine (4 * 3 ^ (4 * α + 6) * n + (19 * 3 ^ (4 * α + 5) - 1) / 2) ≡
      pedNineNine (4 * 3 ^ (4 * α + 4) * n + (19 * 3 ^ (4 * α + 3) - 1) / 2) [ZMOD 32] ∧
    pedNineNine (4 * 3 ^ (4 * α + 4) * 5 ^ (2 * β) * n + (19 * 3 ^ (4 * α + 3) * 5 ^ (2 * β) - 1) / 2)
      ≡ coeff n (16 * 𝔣 1 * 𝔣 6 ^ 3) [ZMOD 32] ∧
    ∀ i ∈ ({0, 1, 2, 4} : Finset ℕ),
      pedNineNine (4 * 3 ^ (4 * α + 4) * 5 ^ (2 * β + 1) * (5 * n + i) +
        (23 * 3 ^ (4 * α + 3) * 5 ^ (2 * β + 1) - 1) / 2) ≡ 0 [ZMOD 32]

Sources

• Harishkumar T, Shruthi Menezes, and M. S. Mahadeva Naika, On [j, k]-Overpartitions with Even Parts Distinct, INTEGERS 25 (2025), Article A69, Theorem 1.

Uses 2

Statement usesThe partition function \(\mathrm{ped}_{9,9}\) · The Euler products of partition theory

TheoremCongruences modulo 16 for \(\mathrm{ped}_{9,9}\)#●ready to prove

For \(k \ge 1\) let \(f_k = \prod_{m \ge 1} (1 - q^{km})\), an integer power series in \(q\), and let \(\mathrm{ped}_{9,9}(n)\) be the coefficient of \(q^n\) in \(f_4 f_{18} / (f_1 f_9)\). Then for all natural numbers \(\alpha\), \(\beta\), \(\gamma\) and \(n\) the following congruences modulo \(16\) hold, where every division is exact.

(49) \(\mathrm{ped}_{9,9}(4 \cdot 3^{4\alpha+6} n + (13 \cdot 3^{4\alpha+5} - 1)/2) \equiv 0\) and \(\mathrm{ped}_{9,9}(4 \cdot 3^{4\alpha+4} n + (13 \cdot 3^{4\alpha+3} - 1)/2) \equiv 0\).

(50) \(\mathrm{ped}_{9,9}(4 \cdot 3^{4\alpha+6} n + (7 \cdot 3^{4\alpha+5} - 1)/2) \equiv \mathrm{ped}_{9,9}(4 \cdot 3^{4\alpha+4} n + (7 \cdot 3^{4\alpha+3} - 1)/2)\).

(51) \(\mathrm{ped}_{9,9}(2 \cdot 3^{4\alpha+5} n + (11 \cdot 3^{4\alpha+4} - 1)/2) \equiv 0\) and \(\mathrm{ped}_{9,9}(2 \cdot 3^{4\alpha+3} n + (11 \cdot 3^{4\alpha+2} - 1)/2) \equiv 0\).

(52) \(\mathrm{ped}_{9,9}(2 \cdot 3^{4\alpha+6} n + (11 \cdot 3^{4\alpha+5} - 1)/2) \equiv 0\) and \(\mathrm{ped}_{9,9}(2 \cdot 3^{4\alpha+4} n + (11 \cdot 3^{4\alpha+3} - 1)/2) \equiv 0\).

(53) \(\mathrm{ped}_{9,9}(4 \cdot 3^{4\alpha+4} \cdot 5^{2\beta} n + (7 \cdot 3^{4\alpha+3} \cdot 5^{2\beta} - 1)/2)\) is congruent to the coefficient of \(q^n\) in \(8 f_1^7\).

(54) \(\mathrm{ped}_{9,9}(4 \cdot 3^{4\alpha+4} \cdot 5^{2\beta+1} (5n + i) + (11 \cdot 3^{4\alpha+3} \cdot 5^{2\beta+1} - 1)/2) \equiv 0\) for \(i \in \{0, 2, 3, 4\}\).

(55) \(\mathrm{ped}_{9,9}(4 \cdot 3^{4\alpha+3} \cdot 7^{2\gamma} n + (5 \cdot 3^{4\alpha+2} \cdot 7^{2\gamma} - 1)/2)\) is congruent to the coefficient of \(q^n\) in \(8 f_1^5\).

(56) \(\mathrm{ped}_{9,9}(4 \cdot 3^{4\alpha+3} \cdot 7^{2\gamma+1} (7n + j) + (11 \cdot 3^{4\alpha+2} \cdot 7^{2\gamma+1} - 1)/2) \equiv 0\) for \(j \in \{0, 2, 3, 4, 5, 6\}\).

MetaMathlibExt.pedNineNine_congruences_mod_sixteen · 19 lines

public theorem_wanted pedNineNine_congruences_mod_sixteen (α β γ n : ℕ) :
    pedNineNine (4 * 3 ^ (4 * α + 6) * n + (13 * 3 ^ (4 * α + 5) - 1) / 2) ≡ 0 [ZMOD 16] ∧
    pedNineNine (4 * 3 ^ (4 * α + 4) * n + (13 * 3 ^ (4 * α + 3) - 1) / 2) ≡ 0 [ZMOD 16] ∧
    pedNineNine (4 * 3 ^ (4 * α + 6) * n + (7 * 3 ^ (4 * α + 5) - 1) / 2) ≡
      pedNineNine (4 * 3 ^ (4 * α + 4) * n + (7 * 3 ^ (4 * α + 3) - 1) / 2) [ZMOD 16] ∧
    pedNineNine (2 * 3 ^ (4 * α + 5) * n + (11 * 3 ^ (4 * α + 4) - 1) / 2) ≡ 0 [ZMOD 16] ∧
    pedNineNine (2 * 3 ^ (4 * α + 3) * n + (11 * 3 ^ (4 * α + 2) - 1) / 2) ≡ 0 [ZMOD 16] ∧
    pedNineNine (2 * 3 ^ (4 * α + 6) * n + (11 * 3 ^ (4 * α + 5) - 1) / 2) ≡ 0 [ZMOD 16] ∧
    pedNineNine (2 * 3 ^ (4 * α + 4) * n + (11 * 3 ^ (4 * α + 3) - 1) / 2) ≡ 0 [ZMOD 16] ∧
    pedNineNine (4 * 3 ^ (4 * α + 4) * 5 ^ (2 * β) * n + (7 * 3 ^ (4 * α + 3) * 5 ^ (2 * β) - 1) / 2)
      ≡ coeff n (8 * 𝔣 1 ^ 7) [ZMOD 16] ∧
    (∀ i ∈ ({0, 2, 3, 4} : Finset ℕ),
      pedNineNine (4 * 3 ^ (4 * α + 4) * 5 ^ (2 * β + 1) * (5 * n + i) +
        (11 * 3 ^ (4 * α + 3) * 5 ^ (2 * β + 1) - 1) / 2) ≡ 0 [ZMOD 16]) ∧
    pedNineNine (4 * 3 ^ (4 * α + 3) * 7 ^ (2 * γ) * n + (5 * 3 ^ (4 * α + 2) * 7 ^ (2 * γ) - 1) / 2)
      ≡ coeff n (8 * 𝔣 1 ^ 5) [ZMOD 16] ∧
    ∀ j ∈ ({0, 2, 3, 4, 5, 6} : Finset ℕ),
      pedNineNine (4 * 3 ^ (4 * α + 3) * 7 ^ (2 * γ + 1) * (7 * n + j) +
        (11 * 3 ^ (4 * α + 2) * 7 ^ (2 * γ + 1) - 1) / 2) ≡ 0 [ZMOD 16]

Sources

• Harishkumar T, Shruthi Menezes, and M. S. Mahadeva Naika, On [j, k]-Overpartitions with Even Parts Distinct, INTEGERS 25 (2025), Article A69, Theorem 2.

Uses 2

Statement usesThe partition function \(\mathrm{ped}_{9,9}\) · The Euler products of partition theory

TheoremFurther congruences modulo 16 for \(\mathrm{ped}_{9,9}\)#●ready to prove

For \(k \ge 1\) let \(f_k = \prod_{m \ge 1} (1 - q^{km})\), an integer power series in \(q\), and let \(\mathrm{ped}_{9,9}(n)\) be the coefficient of \(q^n\) in \(f_4 f_{18} / (f_1 f_9)\). Then for all natural numbers \(\alpha\), \(\beta\), \(\gamma\) and \(n\) the following congruences modulo \(16\) hold, where every division is exact.

(58) \(\mathrm{ped}_{9,9}(4 \cdot 3^{4\alpha+3} n + (13 \cdot 3^{4\alpha+2} - 1)/2) \equiv 0\).

(59) \(\mathrm{ped}_{9,9}(4 \cdot 3^{4\alpha+3} n + (19 \cdot 3^{4\alpha+2} - 1)/2) \equiv 0\).

(60) \(\mathrm{ped}_{9,9}(4 \cdot 3^{4\alpha+3} \cdot 5^{2\beta} n + (7 \cdot 3^{4\alpha+2} \cdot 5^{2\beta} - 1)/2)\) is congruent to the coefficient of \(q^n\) in \(8 f_1^7\).

(61) \(\mathrm{ped}_{9,9}(4 \cdot 3^{4\alpha+3} \cdot 5^{2\beta+1} (5n + i) + (11 \cdot 3^{4\alpha+2} \cdot 5^{2\beta+1} - 1)/2) \equiv 0\) for \(i \in \{0, 2, 3, 4\}\).

(62) \(\mathrm{ped}_{9,9}(4 \cdot 3^{4\alpha+5} n + (13 \cdot 3^{4\alpha+4} - 1)/2) \equiv 0\).

(63) \(\mathrm{ped}_{9,9}(2 \cdot 3^{4\alpha+5} n + (7 \cdot 3^{4\alpha+4} - 1)/2) \equiv \mathrm{ped}_{9,9}(2 \cdot 3^{4\alpha+3} n + (7 \cdot 3^{4\alpha+2} - 1)/2)\).

(64) \(\mathrm{ped}_{9,9}(4 \cdot 3^{4\alpha+4} \cdot 7^{2\gamma} n + (5 \cdot 3^{4\alpha+3} \cdot 7^{2\gamma} - 1)/2)\) is congruent to the coefficient of \(q^n\) in \(8 f_1^5\).

(65) \(\mathrm{ped}_{9,9}(4 \cdot 3^{4\alpha+4} \cdot 7^{2\gamma+1} (7n + j) + (11 \cdot 3^{4\alpha+3} \cdot 7^{2\gamma+1} - 1)/2) \equiv 0\) for \(j \in \{0, 2, 3, 4, 5, 6\}\).

MetaMathlibExt.pedNineNine_more_congruences_mod_sixteen · 16 lines

public theorem_wanted pedNineNine_more_congruences_mod_sixteen (α β γ n : ℕ) :
    pedNineNine (4 * 3 ^ (4 * α + 3) * n + (13 * 3 ^ (4 * α + 2) - 1) / 2) ≡ 0 [ZMOD 16] ∧
    pedNineNine (4 * 3 ^ (4 * α + 3) * n + (19 * 3 ^ (4 * α + 2) - 1) / 2) ≡ 0 [ZMOD 16] ∧
    pedNineNine (4 * 3 ^ (4 * α + 3) * 5 ^ (2 * β) * n + (7 * 3 ^ (4 * α + 2) * 5 ^ (2 * β) - 1) / 2)
      ≡ coeff n (8 * 𝔣 1 ^ 7) [ZMOD 16] ∧
    (∀ i ∈ ({0, 2, 3, 4} : Finset ℕ),
      pedNineNine (4 * 3 ^ (4 * α + 3) * 5 ^ (2 * β + 1) * (5 * n + i) +
        (11 * 3 ^ (4 * α + 2) * 5 ^ (2 * β + 1) - 1) / 2) ≡ 0 [ZMOD 16]) ∧
    pedNineNine (4 * 3 ^ (4 * α + 5) * n + (13 * 3 ^ (4 * α + 4) - 1) / 2) ≡ 0 [ZMOD 16] ∧
    pedNineNine (2 * 3 ^ (4 * α + 5) * n + (7 * 3 ^ (4 * α + 4) - 1) / 2) ≡
      pedNineNine (2 * 3 ^ (4 * α + 3) * n + (7 * 3 ^ (4 * α + 2) - 1) / 2) [ZMOD 16] ∧
    pedNineNine (4 * 3 ^ (4 * α + 4) * 7 ^ (2 * γ) * n + (5 * 3 ^ (4 * α + 3) * 7 ^ (2 * γ) - 1) / 2)
      ≡ coeff n (8 * 𝔣 1 ^ 5) [ZMOD 16] ∧
    ∀ j ∈ ({0, 2, 3, 4, 5, 6} : Finset ℕ),
      pedNineNine (4 * 3 ^ (4 * α + 4) * 7 ^ (2 * γ + 1) * (7 * n + j) +
        (11 * 3 ^ (4 * α + 3) * 7 ^ (2 * γ + 1) - 1) / 2) ≡ 0 [ZMOD 16]

Sources

• Harishkumar T, Shruthi Menezes, and M. S. Mahadeva Naika, On [j, k]-Overpartitions with Even Parts Distinct, INTEGERS 25 (2025), Article A69, Theorem 3.

Uses 2

Statement usesThe partition function \(\mathrm{ped}_{9,9}\) · The Euler products of partition theory

TheoremCongruences modulo 64 for (9, 18)-overpartitions with even parts distinct#●ready to prove

Let \(\mathrm{ped}_{9,18}(n)\) be the number of \([9, 18]\)-overpartitions of \(n\) with even parts distinct, let \(f_k = \prod_{m \ge 1} (1 - q^{km})\), and read congruences between integer power series in \(q\) coefficientwise. For all \(\alpha \ge 0\) the following hold modulo \(64\), where the statements about single values hold for every \(n \ge 0\): (73) \(f_2^2 \sum_{n \ge 0} \mathrm{ped}_{9,18}\bigl(3^{4\alpha+2} n + (3^{4\alpha+3} + 1)/4\bigr) q^n \equiv 12 f_1^4 f_3^6\); (74) \(\mathrm{ped}_{9,18}\bigl(3^{4\alpha+5} n + (7 \cdot 3^{4\alpha+4} + 1)/4\bigr) \equiv \mathrm{ped}_{9,18}\bigl(3^{4\alpha+3} n + (7 \cdot 3^{4\alpha+2} + 1)/4\bigr)\); (75) \(\mathrm{ped}_{9,18}\bigl(3^{4\alpha+5} n + (11 \cdot 3^{4\alpha+4} + 1)/4\bigr) \equiv \mathrm{ped}_{9,18}\bigl(3^{4\alpha+3} n + (11 \cdot 3^{4\alpha+2} + 1)/4\bigr)\); (76) \(\mathrm{ped}_{9,18}\bigl(3^{4\alpha+6} n + (5 \cdot 3^{4\alpha+5} + 1)/4\bigr) \equiv \mathrm{ped}_{9,18}\bigl(3^{4\alpha+4} n + (5 \cdot 3^{4\alpha+3} + 1)/4\bigr)\). All divisions by \(4\) are exact.

The paper states (73) with \(12 f_1^4 f_3^6 / f_2^2\) on the right; here \(f_2^2\) is cleared.

public theorem_wanted pedNineEighteen_congruences_mod_sixtyFour (α n : ℕ) :
    coeff n (𝔣 2 ^ 2 *
        PowerSeries.mk fun m => pedNineEighteen (3 ^ (4 * α + 2) * m + (3 ^ (4 * α + 3) + 1) / 4)) ≡
      coeff n (12 * 𝔣 1 ^ 4 * 𝔣 3 ^ 6) [ZMOD 64] ∧
    pedNineEighteen (3 ^ (4 * α + 5) * n + (7 * 3 ^ (4 * α + 4) + 1) / 4) ≡
      pedNineEighteen (3 ^ (4 * α + 3) * n + (7 * 3 ^ (4 * α + 2) + 1) / 4) [ZMOD 64] ∧
    pedNineEighteen (3 ^ (4 * α + 5) * n + (11 * 3 ^ (4 * α + 4) + 1) / 4) ≡
      pedNineEighteen (3 ^ (4 * α + 3) * n + (11 * 3 ^ (4 * α + 2) + 1) / 4) [ZMOD 64] ∧
    pedNineEighteen (3 ^ (4 * α + 6) * n + (5 * 3 ^ (4 * α + 5) + 1) / 4) ≡
      pedNineEighteen (3 ^ (4 * α + 4) * n + (5 * 3 ^ (4 * α + 3) + 1) / 4) [ZMOD 64]

Sources

• Harishkumar T, Shruthi Menezes, and M. S. Mahadeva Naika, On [j, k]-Overpartitions with Even Parts Distinct, INTEGERS 25 (2025), Article A69, Theorem 4.

Uses 2

Statement usesThe partition function \(\mathrm{ped}_{9,18}\) · The Euler products of partition theory

TheoremCongruences modulo 32 for (9, 18)-overpartitions with even parts distinct#●ready to prove

Let \(\mathrm{ped}_{9,18}(n)\) be the number of \([9, 18]\)-overpartitions of \(n\) with even parts distinct, let \(f_k = \prod_{m \ge 1} (1 - q^{km})\), and read congruences between integer power series in \(q\) coefficientwise. For all \(\alpha, \beta \ge 0\) the following hold modulo \(32\), where the statements about single values hold for every \(n \ge 0\): (94) \(\mathrm{ped}_{9,18}\bigl(3^{4\alpha+6} n + (3^{4\alpha+5} + 1)/4\bigr) \equiv \mathrm{ped}_{9,18}\bigl(3^{4\alpha+4} n + (3^{4\alpha+3} + 1)/4\bigr)\); (95) \(\sum_{n \ge 0} \mathrm{ped}_{9,18}\bigl(2 \cdot 3^{4\alpha+3} 5^{2\beta} n + (7 \cdot 3^{4\alpha+2} 5^{2\beta} + 1)/4\bigr) q^n \equiv 16 f_1^7\); (96) \(\mathrm{ped}_{9,18}\bigl(2 \cdot 3^{4\alpha+3} 5^{2\beta+1} (5n + i) + (11 \cdot 3^{4\alpha+2} 5^{2\beta+1} + 1)/4\bigr) \equiv 0\) for \(i \in \{0, 2, 3, 4\}\); (97) \(\sum_{n \ge 0} \mathrm{ped}_{9,18}\bigl(2 \cdot 3^{4\alpha+3} 5^{2\beta} n + (19 \cdot 3^{4\alpha+2} 5^{2\beta} + 1)/4\bigr) q^n \equiv 16 f_1 f_6^3\); (98) \(\mathrm{ped}_{9,18}\bigl(2 \cdot 3^{4\alpha+3} 5^{2\beta+1} (5n + j) + (23 \cdot 3^{4\alpha+2} 5^{2\beta+1} + 1)/4\bigr) \equiv 0\) for \(j \in \{0, 1, 2, 4\}\); (99) \(\mathrm{ped}_{9,18}\bigl(2 \cdot 3^{4\alpha+3} n + (23 \cdot 3^{4\alpha+2} + 1)/4\bigr) \equiv 0\); (100) \(\sum_{n \ge 0} \mathrm{ped}_{9,18}\bigl(2 \cdot 3^{4\alpha+3} 5^{2\beta} n + (11 \cdot 3^{4\alpha+2} 5^{2\beta} + 1)/4\bigr) q^n \equiv 16 f_2 f_3^3\); (101) \(\mathrm{ped}_{9,18}\bigl(2 \cdot 3^{4\alpha+3} 5^{2\beta+1} (5n + k) + (7 \cdot 3^{4\alpha+2} 5^{2\beta+1} + 1)/4\bigr) \equiv 0\) for \(k \in \{0, 1, 3, 4\}\). All divisions by \(4\) are exact.

MetaMathlibExt.pedNineEighteen_congruences_mod_thirtyTwo · 22 lines

public theorem_wanted pedNineEighteen_congruences_mod_thirtyTwo (α β n : ℕ) :
    pedNineEighteen (3 ^ (4 * α + 6) * n + (3 ^ (4 * α + 5) + 1) / 4) ≡
      pedNineEighteen (3 ^ (4 * α + 4) * n + (3 ^ (4 * α + 3) + 1) / 4) [ZMOD 32] ∧
    pedNineEighteen
        (2 * 3 ^ (4 * α + 3) * 5 ^ (2 * β) * n + (7 * 3 ^ (4 * α + 2) * 5 ^ (2 * β) + 1) / 4)
      ≡ coeff n (16 * 𝔣 1 ^ 7) [ZMOD 32] ∧
    (∀ i ∈ ({0, 2, 3, 4} : Finset ℕ),
      pedNineEighteen (2 * 3 ^ (4 * α + 3) * 5 ^ (2 * β + 1) * (5 * n + i) +
        (11 * 3 ^ (4 * α + 2) * 5 ^ (2 * β + 1) + 1) / 4) ≡ 0 [ZMOD 32]) ∧
    pedNineEighteen
        (2 * 3 ^ (4 * α + 3) * 5 ^ (2 * β) * n + (19 * 3 ^ (4 * α + 2) * 5 ^ (2 * β) + 1) / 4)
      ≡ coeff n (16 * 𝔣 1 * 𝔣 6 ^ 3) [ZMOD 32] ∧
    (∀ j ∈ ({0, 1, 2, 4} : Finset ℕ),
      pedNineEighteen (2 * 3 ^ (4 * α + 3) * 5 ^ (2 * β + 1) * (5 * n + j) +
        (23 * 3 ^ (4 * α + 2) * 5 ^ (2 * β + 1) + 1) / 4) ≡ 0 [ZMOD 32]) ∧
    pedNineEighteen (2 * 3 ^ (4 * α + 3) * n + (23 * 3 ^ (4 * α + 2) + 1) / 4) ≡ 0 [ZMOD 32] ∧
    pedNineEighteen
        (2 * 3 ^ (4 * α + 3) * 5 ^ (2 * β) * n + (11 * 3 ^ (4 * α + 2) * 5 ^ (2 * β) + 1) / 4)
      ≡ coeff n (16 * 𝔣 2 * 𝔣 3 ^ 3) [ZMOD 32] ∧
    ∀ k ∈ ({0, 1, 3, 4} : Finset ℕ),
      pedNineEighteen (2 * 3 ^ (4 * α + 3) * 5 ^ (2 * β + 1) * (5 * n + k) +
        (7 * 3 ^ (4 * α + 2) * 5 ^ (2 * β + 1) + 1) / 4) ≡ 0 [ZMOD 32]

Sources

• Harishkumar T, Shruthi Menezes, and M. S. Mahadeva Naika, On [j, k]-Overpartitions with Even Parts Distinct, INTEGERS 25 (2025), Article A69, Theorem 5.

Uses 2

Statement usesThe partition function \(\mathrm{ped}_{9,18}\) · The Euler products of partition theory

TheoremCongruences modulo 16 and 8 for (9, 18)-overpartitions with even parts distinct#●ready to prove

Let \(\mathrm{ped}_{9,18}(n)\) be the number of \([9, 18]\)-overpartitions of \(n\) with even parts distinct, let \(f_k = \prod_{m \ge 1} (1 - q^{km})\), and read congruences between integer power series in \(q\) coefficientwise. For all \(\alpha, \beta, \gamma \ge 0\) the following hold, where the statements about single values hold for every \(n \ge 0\): (105) \(\sum_{n \ge 0} \mathrm{ped}_{9,18}\bigl(2 \cdot 3^{4\alpha+4} 5^{2\beta} n + (13 \cdot 3^{4\alpha+3} 5^{2\beta} + 1)/4\bigr) q^n \equiv 8 f_1^{13} \pmod{16}\); (106) \(\mathrm{ped}_{9,18}\bigl(2 \cdot 3^{4\alpha+4} 5^{2\beta+1} (5n + i) + (17 \cdot 3^{4\alpha+3} 5^{2\beta+1} + 1)/4\bigr) \equiv 0 \pmod{16}\) for \(i \in \{0, 1, 3, 4\}\); (107) \(\sum_{n \ge 0} \mathrm{ped}_{9,18}\bigl(2 \cdot 3^{4\alpha+4} 7^{2\gamma} n + (5 \cdot 3^{4\alpha+3} 7^{2\gamma} + 1)/4\bigr) q^n \equiv 8 f_1^5 \pmod{16}\); (108) \(\mathrm{ped}_{9,18}\bigl(2 \cdot 3^{4\alpha+4} 7^{2\gamma+1} (7n + j) + (11 \cdot 3^{4\alpha+3} 7^{2\gamma+1} + 1)/4\bigr) \equiv 0 \pmod{16}\) for \(j \in \{0, 2, 3, 4, 5, 6\}\); (109) \(\mathrm{ped}_{9,18}\bigl(2 \cdot 3^{4\alpha+4} n + (3^{4\alpha+3} + 1)/4\bigr)\) is congruent to \(4\) modulo \(8\) if \(n = m(3m-1)/2\) for some integer \(m\) (a generalized pentagonal number), and to \(0\) modulo \(8\) otherwise. All divisions by \(4\) are exact.

MetaMathlibExt.pedNineEighteen_congruences_mod_sixteen · 17 lines

public theorem_wanted pedNineEighteen_congruences_mod_sixteen (α β γ n : ℕ) :
    pedNineEighteen
        (2 * 3 ^ (4 * α + 4) * 5 ^ (2 * β) * n + (13 * 3 ^ (4 * α + 3) * 5 ^ (2 * β) + 1) / 4)
      ≡ coeff n (8 * 𝔣 1 ^ 13) [ZMOD 16] ∧
    (∀ i ∈ ({0, 1, 3, 4} : Finset ℕ),
      pedNineEighteen (2 * 3 ^ (4 * α + 4) * 5 ^ (2 * β + 1) * (5 * n + i) +
        (17 * 3 ^ (4 * α + 3) * 5 ^ (2 * β + 1) + 1) / 4) ≡ 0 [ZMOD 16]) ∧
    pedNineEighteen
        (2 * 3 ^ (4 * α + 4) * 7 ^ (2 * γ) * n + (5 * 3 ^ (4 * α + 3) * 7 ^ (2 * γ) + 1) / 4)
      ≡ coeff n (8 * 𝔣 1 ^ 5) [ZMOD 16] ∧
    (∀ j ∈ ({0, 2, 3, 4, 5, 6} : Finset ℕ),
      pedNineEighteen (2 * 3 ^ (4 * α + 4) * 7 ^ (2 * γ + 1) * (7 * n + j) +
        (11 * 3 ^ (4 * α + 3) * 7 ^ (2 * γ + 1) + 1) / 4) ≡ 0 [ZMOD 16]) ∧
    ((∃ m : ℤ, 2 * (n : ℤ) = m * (3 * m - 1)) →
      pedNineEighteen (2 * 3 ^ (4 * α + 4) * n + (3 ^ (4 * α + 3) + 1) / 4) ≡ 4 [ZMOD 8]) ∧
    ((¬ ∃ m : ℤ, 2 * (n : ℤ) = m * (3 * m - 1)) →
      pedNineEighteen (2 * 3 ^ (4 * α + 4) * n + (3 ^ (4 * α + 3) + 1) / 4) ≡ 0 [ZMOD 8])

Sources

• Harishkumar T, Shruthi Menezes, and M. S. Mahadeva Naika, On [j, k]-Overpartitions with Even Parts Distinct, INTEGERS 25 (2025), Article A69, Theorem 6.

Uses 2

Statement usesThe partition function \(\mathrm{ped}_{9,18}\) · The Euler products of partition theory

TheoremCongruences modulo 9 and 27 for (9, 18)-overpartitions with even parts distinct#●ready to prove

Let \(\mathrm{ped}_{9,18}(n)\) be the number of \([9, 18]\)-overpartitions of \(n\) with even parts distinct. For every \(n \ge 0\), \(\mathrm{ped}_{9,18}(27n + 16)\) and \(\mathrm{ped}_{9,18}(27n + 25)\) are divisible by \(9\), and \(\mathrm{ped}_{9,18}(243n + 142)\), \(\mathrm{ped}_{9,18}(243n + 223)\) and \(\mathrm{ped}_{9,18}(729n + 547)\) are divisible by \(27\).

public theorem_wanted pedNineEighteen_congruences_mod_nine_twentySeven (n : ℕ) :
    pedNineEighteen (27 * n + 16) ≡ 0 [ZMOD 9] ∧ pedNineEighteen (27 * n + 25) ≡ 0 [ZMOD 9] ∧
      pedNineEighteen (243 * n + 142) ≡ 0 [ZMOD 27] ∧
      pedNineEighteen (243 * n + 223) ≡ 0 [ZMOD 27] ∧
      pedNineEighteen (729 * n + 547) ≡ 0 [ZMOD 27]

Sources

• Harishkumar T, Shruthi Menezes, and M. S. Mahadeva Naika, On [j, k]-Overpartitions with Even Parts Distinct, INTEGERS 25 (2025), Article A69, Theorem 7.

Uses 1

Statement usesThe partition function \(\mathrm{ped}_{9,18}\)

TheoremCongruences modulo 27 for (9, 18)-overpartitions from the cubic coefficient vectors#●ready to prove

Let \(\mathrm{ped}_{9,18}(n)\) be the number of \([9, 18]\)-overpartitions of \(n\) with even parts distinct, let \(f_k = \prod_{m \ge 1} (1 - q^{km})\), let \(X_\alpha = (x_{\alpha,1}, x_{\alpha,2}, \dots)\) be the coefficient vectors built from Chan's matrix, and read congruences between integer power series in \(q\) coefficientwise. For all \(\alpha \ge 0\), modulo \(27\), (124) \(\sum_{n \ge 0} \mathrm{ped}_{9,18}\bigl(3^{2\alpha+5} n + (3^{2\alpha+5} + 1)/4\bigr) q^n \equiv 9 \sum_{i=1}^{3^{2\alpha}} x_{2\alpha,i} \, q^{i-1} \left(\frac{f_3 f_6}{f_1 f_2}\right)^{4i-3}\) and (125) \(\sum_{n \ge 0} \mathrm{ped}_{9,18}\bigl(3^{2\alpha+6} n + (3^{2\alpha+7} + 1)/4\bigr) q^n \equiv 9 \sum_{i=1}^{3^{2\alpha+1}} x_{2\alpha+1,i} \, q^{i-1} \left(\frac{f_3 f_6}{f_1 f_2}\right)^{4i-1}\). All divisions by \(4\) are exact, and \(f_1 f_2\) is invertible as a power series because its constant term is \(1\).

The quotient \(f_3 f_6 / (f_1 f_2)\) is the generating function of 3-regular cubic partitions.

public theorem_wanted pedNineEighteen_cubicCoeffVector_congruences (α n : ℕ) :
    pedNineEighteen (3 ^ (2 * α + 5) * n + (3 ^ (2 * α + 5) + 1) / 4) ≡
      coeff n (9 * ∑ i ∈ Finset.range (3 ^ (2 * α)), (cubicCoeffVector (2 * α) i : ℤ⟦X⟧) *
        X ^ i * (𝔣 3 * 𝔣 6) ^ (4 * i + 1) * invOfUnit ((𝔣 1 * 𝔣 2) ^ (4 * i + 1)) 1) [ZMOD 27] ∧
    pedNineEighteen (3 ^ (2 * α + 6) * n + (3 ^ (2 * α + 7) + 1) / 4) ≡
      coeff n (9 * ∑ i ∈ Finset.range (3 ^ (2 * α + 1)),
        (cubicCoeffVector (2 * α + 1) i : ℤ⟦X⟧) * X ^ i * (𝔣 3 * 𝔣 6) ^ (4 * i + 3) *
          invOfUnit ((𝔣 1 * 𝔣 2) ^ (4 * i + 3)) 1) [ZMOD 27]

Sources

• Harishkumar T, Shruthi Menezes, and M. S. Mahadeva Naika, On [j, k]-Overpartitions with Even Parts Distinct, INTEGERS 25 (2025), Article A69, Theorem 8.

Uses 3

Statement usesCoefficient vectors from Chan's matrix · The partition function \(\mathrm{ped}_{9,18}\) · The Euler products of partition theory

15 fully proved18 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.