Compositions with an odd number of parts

DefinitionThe index set \(S(m, n, q)\)#✓fully proved

For natural numbers \(m\), \(n\) and \(q\), the set \(S(m, n, q)\) consists of the natural numbers \(k\) such that \(2k \equiv n - q \pmod{m}\), where the difference \(n - q\) is taken in the integers, and \(2k < n\).

For natural numbers the bound \(2k < n\) is equivalent to \(k \le \lfloor (n - 1)/2 \rfloor\); in particular the set is empty when \(n = 0\).

public def compositionHalfIndexSet (m n q : ℕ) : Set ℕ :=
  {k | 2 * (k : ℤ) ≡ (n : ℤ) - (q : ℤ) [ZMOD (m : ℤ)] ∧ 2 * k < n}
Sources
  • Bowman, Compositions with an Odd Number of Parts, and Other Congruences, Journal of Integer Sequences 27 (2024), Article 24.3.6, Theorem 13 (jis-2024-24.3.6-thm-13).
Used by 3

TheoremMembership in \(S(m, n, q)\)#✓fully proved

For natural numbers \(m\), \(n\), \(q\) and \(k\), the number \(k\) lies in the index set \(S(m, n, q)\) if and only if \(2k \equiv n - q \pmod{m}\), with the difference taken in the integers, and \(2k < n\).

public theorem mem_compositionHalfIndexSet {m n q k : ℕ} :
    k ∈ compositionHalfIndexSet m n q ↔
      2 * (k : ℤ) ≡ (n : ℤ) - (q : ℤ) [ZMOD (m : ℤ)] ∧ 2 * k < n
Sources
  • Bowman, Compositions with an Odd Number of Parts, and Other Congruences, Journal of Integer Sequences 27 (2024), Article 24.3.6, Theorem 13 (jis-2024-24.3.6-thm-13).
Uses 1 · Used by 2

TheoremThe index set \(S(m, 0, q)\) is empty#✓fully proved

For all natural numbers \(m\) and \(q\), the index set \(S(m, 0, q)\) is empty.

public theorem compositionHalfIndexSet_zero (m q : ℕ) :
    compositionHalfIndexSet m 0 q = ∅
Sources
  • Bowman, Compositions with an Odd Number of Parts, and Other Congruences, Journal of Integer Sequences 27 (2024), Article 24.3.6, Theorem 13 (jis-2024-24.3.6-thm-13).
Uses 2

DefinitionThe index set \(T(m, n, q)\)#✓fully proved

For natural numbers \(m\), \(n\) and \(q\), the set \(T(m, n, q)\) consists of the natural numbers \(k\) such that \(k \equiv n - q \pmod{m}\), where the difference \(n - q\) is taken in the integers, and \(k < n\).

public def compositionIndexSet (m n q : ℕ) : Set ℕ :=
  {k | (k : ℤ) ≡ (n : ℤ) - (q : ℤ) [ZMOD (m : ℤ)] ∧ k < n}
Sources
  • Bowman, Compositions with an Odd Number of Parts, and Other Congruences, Journal of Integer Sequences 27 (2024), Article 24.3.6, Theorem 17 (jis-2024-24.3.6-thm-17).
Used by 3

TheoremMembership in \(T(m, n, q)\)#✓fully proved

For natural numbers \(m\), \(n\), \(q\) and \(k\), the number \(k\) lies in the index set \(T(m, n, q)\) if and only if \(k \equiv n - q \pmod{m}\), with the difference taken in the integers, and \(k < n\).

public theorem mem_compositionIndexSet {m n q k : ℕ} :
    k ∈ compositionIndexSet m n q ↔
      (k : ℤ) ≡ (n : ℤ) - (q : ℤ) [ZMOD (m : ℤ)] ∧ k < n
Sources
  • Bowman, Compositions with an Odd Number of Parts, and Other Congruences, Journal of Integer Sequences 27 (2024), Article 24.3.6, Theorem 17 (jis-2024-24.3.6-thm-17).
Uses 1 · Used by 2

TheoremThe index set \(T(m, 0, q)\) is empty#✓fully proved

For all natural numbers \(m\) and \(q\), the index set \(T(m, 0, q)\) is empty.

public theorem compositionIndexSet_zero (m q : ℕ) :
    compositionIndexSet m 0 q = ∅
Sources
  • Bowman, Compositions with an Odd Number of Parts, and Other Congruences, Journal of Integer Sequences 27 (2024), Article 24.3.6, Theorem 17 (jis-2024-24.3.6-thm-17).
Uses 2

TheoremDoubling identity for the composition index sets#✓fully proved

For natural numbers \(m\), \(n\) and \(q\), let \(S(m, n, q)\) be the set of natural numbers \(k\) with \(2k \equiv n - q \pmod{m}\) and \(2k < n\), and let \(T(m, n, q)\) be the set of natural numbers \(k\) with \(k \equiv n - q \pmod{m}\) and \(k < n\), where the difference \(n - q\) is taken in the integers. Then for all natural numbers \(m\), \(n\) and \(q\) the sets satisfy \(S(2m, 2n, 2q) = T(m, n, q)\).

public theorem compositionHalfIndexSet_double (m n q : ℕ) :
    compositionHalfIndexSet (2 * m) (2 * n) (2 * q)
      = compositionIndexSet m n q
Sources
  • Bowman, Compositions with an Odd Number of Parts, and Other Congruences, Journal of Integer Sequences 27 (2024), Article 24.3.6, Lemma 18 (jis-2024-24.3.6-lem-18).
Uses 4
7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.