Arndt compositions

DefinitionNumber of Arndt compositions with parts in a set#✓fully proved

For a set \(S\) of natural numbers and natural numbers \(n\) and \(k\), \(a_S(n, k)\) is the number of \(k\)-tuples \((c_1, \dots, c_k)\) of positive integers such that \(c_1 + \dots + c_k = n\), every \(c_i\) lies in \(S\), and \(c_{2i-1} > c_{2i}\) for every \(i\) with \(2i \le k\). These tuples are the Arndt compositions of \(n\) with \(k\) parts in \(S\).

def arndtCompositionCount (S : ℕ → Prop) [DecidablePred S] (n k : ℕ) : ℕ :=
  ((Finset.Nat.antidiagonalTuple k n).filter fun c =>
    (∀ i, 0 < c i ∧ S (c i)) ∧
      ∀ i j : Fin k, (i : ℕ) % 2 = 0 → (j : ℕ) = i + 1 → c j < c i).card

Sources

• Mohammed L. Nadji, Moussa Ahmia, Daniel F. Checa, and José L. Ramírez, Arndt Compositions with Restricted Parts, Palindromes, and Colored Variants, Journal of Integer Sequences 28 (2025), Article 25.3.6, Section 1 (definition of Arndt compositions, after D. F. Checa and J. L. Ramírez, arXiv:2311.15388, Section 1).

Used by 16

Used byAlternating sum and recurrence for Arndt compositions · Positive sum for Arndt compositions · Arndt compositions with a given number of parts as a sum of products · Holonomic recurrence for Arndt compositions · Asymptotics of Arndt compositions with a fixed number of parts · Arndt compositions of 6 with four parts · Arndt compositions of 6 with three parts · Arndt compositions of 6 with two parts · Expected number of parts of an Arndt composition · Arndt compositions are counted by Fibonacci numbers · Generating function of Arndt compositions with parts in a set · The Arndt generating function as a bivariate count series · Coefficients of the generating function of Arndt compositions · Arndt compositions and reduced anti-palindromic compositions are equinumerous · Arndt compositions with parts at most 4 and Narayana's cows sequence · Arndt compositions with parts at most 3 and the Padovan numbers

TheoremArndt compositions of 6 with two parts#✓fully proved

There are exactly \(2\) Arndt compositions of \(6\) with two parts.

They are \((5, 1)\) and \((4, 2)\).

theorem arndtCompositionCount_six_two : arndtCompositionCount (fun _ => True) 6 2 = 2

Sources

• D. F. Checa and J. L. Ramírez, Arndt compositions: a generating functions approach, arXiv:2311.15388, Section 1 (list of the Arndt compositions of 6).

Uses 1

Statement usesNumber of Arndt compositions with parts in a set

TheoremArndt compositions of 6 with three parts#✓fully proved

There are exactly \(4\) Arndt compositions of \(6\) with three parts.

They are \((4, 1, 1)\), \((3, 2, 1)\), \((3, 1, 2)\) and \((2, 1, 3)\).

theorem arndtCompositionCount_six_three : arndtCompositionCount (fun _ => True) 6 3 = 4

Sources

• D. F. Checa and J. L. Ramírez, Arndt compositions: a generating functions approach, arXiv:2311.15388, Section 1 (list of the Arndt compositions of 6).

Uses 1

Statement usesNumber of Arndt compositions with parts in a set

TheoremArndt compositions of 6 with four parts#✓fully proved

There is exactly one Arndt composition of \(6\) with four parts.

It is \((2, 1, 2, 1)\).

theorem arndtCompositionCount_six_four : arndtCompositionCount (fun _ => True) 6 4 = 1

Sources

• D. F. Checa and J. L. Ramírez, Arndt compositions: a generating functions approach, arXiv:2311.15388, Section 1 (list of the Arndt compositions of 6).

Uses 1

Statement usesNumber of Arndt compositions with parts in a set

DefinitionGenerating function of Arndt compositions with parts in a set#✓fully proved

An Arndt composition is a finite sequence \((\sigma_1, \dots, \sigma_k)\) of positive integers such that \(\sigma_{2i-1} > \sigma_{2i}\) for every \(i\) with \(2i \le k\). For a set \(S\) of natural numbers, let \(a_S(n, k)\) be the number of Arndt compositions of \(n\) with \(k\) parts, all in \(S\). The bivariate generating function of these compositions, by weight (\(x\)) and number of parts (\(y\)), is the power series \(A_S(x, y) = \sum_{n \ge 0} \left(\sum_{k=0}^{n} a_S(n, k)\, y^k\right) x^n\) in \(\mathbb{Z}[y][[x]]\).

noncomputable def arndtGF (S : ℕ → Prop) [DecidablePred S] : PowerSeries (Polynomial ℤ) :=
  PowerSeries.mk fun n =>
    ∑ k ∈ Finset.range (n + 1), (arndtCompositionCount S n k : Polynomial ℤ) * Polynomial.X ^ k

Sources

• Mohammed L. Nadji, Moussa Ahmia, Daniel F. Checa, and José L. Ramírez, Arndt Compositions with Restricted Parts, Palindromes, and Colored Variants, Journal of Integer Sequences 28 (2025), Article 25.3.6, Section 2.

Uses 1 · Used by 7

Statement usesNumber of Arndt compositions with parts in a set

Used byThe Arndt generating function as a bivariate count series · Generating functions of Arndt compositions with even parts and with odd parts · Generating function of Arndt compositions with bounded smallest part · Generating function of Arndt compositions with bounded largest part · Pair decomposition of the Arndt generating function · Generating function of all Arndt compositions · Coefficients of the generating function of Arndt compositions

TheoremCoefficients of the generating function of Arndt compositions#✓fully proved

For a set \(S\) of natural numbers and every \(n \ge 0\), the coefficient of \(x^n\) in the generating function \(A_S(x, y)\) of Arndt compositions with parts in \(S\) is the polynomial \(\sum_{k=0}^{n} a_S(n, k)\, y^k\) in \(\mathbb{Z}[y]\), where \(a_S(n, k)\) is the number of Arndt compositions of \(n\) with \(k\) parts, all in \(S\).

theorem coeff_arndtGF (S : ℕ → Prop) [DecidablePred S] (n : ℕ) :
    PowerSeries.coeff n (arndtGF S) =
      ∑ k ∈ Finset.range (n + 1),
        (arndtCompositionCount S n k : Polynomial ℤ) * Polynomial.X ^ k

Sources

• Mohammed L. Nadji, Moussa Ahmia, Daniel F. Checa, and José L. Ramírez, Arndt Compositions with Restricted Parts, Palindromes, and Colored Variants, Journal of Integer Sequences 28 (2025), Article 25.3.6, Section 2.

Uses 2

Statement usesNumber of Arndt compositions with parts in a set · Generating function of Arndt compositions with parts in a set

TheoremPair decomposition of the Arndt generating function#●ready to prove

Let \(S\) be a set of positive integers and let \(A_S(x, y)\) be the generating function of Arndt compositions with parts in \(S\): the formal power series in \(x\) over \(\mathbb{Z}[y]\) whose coefficient of \(x^n y^k\) is the number of Arndt compositions of \(n\) with \(k\) parts, all in \(S\). Put \(P_S(x) = \sum_{i \in S} x^i\) and \(Q_S(x) = \sum_{i, j \in S,\ j < i} x^{i+j}\). Then

\[A_S(x, y) \, (1 - y^2 Q_S(x)) = 1 + y P_S(x).\]

Equivalently, \(A_S(x, y) = (1 + y P_S(x)) \sum_{m \ge 0} Q_S(x)^m y^{2m}\).

public theorem_wanted arndtGF_mul_one_sub_pairs (S : ℕ → Prop) [DecidablePred S]
    (hS : ¬ S 0) :
    arndtGF S *
        (1 - PowerSeries.C (Polynomial.X ^ 2) *
          PowerSeries.mk fun n =>
            ((((Finset.range n) ×ˢ (Finset.range n)).filter fun ij =>
              ij.2 < ij.1 ∧ S ij.1 ∧ S ij.2 ∧ ij.1 + ij.2 = n).card : Polynomial ℤ)) =
      1 + PowerSeries.C Polynomial.X *
        PowerSeries.mk fun i => if S i then (1 : Polynomial ℤ) else 0

Sources

• Mohammed L. Nadji, Moussa Ahmia, Daniel F. Checa, and José L. Ramírez, Arndt Compositions with Restricted Parts, Palindromes, and Colored Variants, Journal of Integer Sequences 28 (2025), Article 25.3.6, Theorem 1 (jis-2025-25.3.6-thm-1).

Uses 1

Statement usesGenerating function of Arndt compositions with parts in a set

TheoremGenerating function of all Arndt compositions#●ready to prove

Let \(A(x, y)\) be the formal power series in \(x\) over \(\mathbb{Z}[y]\) whose coefficient of \(x^n y^k\) is the number of Arndt compositions of \(n\) with \(k\) parts. Then

\[A(x, y) \left((1 - x)(1 - x^2) - y^2 x^3\right) = (1 - x + xy)(1 - x^2).\]

Equivalently, \(A(x, y) = (1 + xy/(1 - x)) \sum_{m \ge 0} y^{2m} x^{3m} / (x; x)_2^m\) with \((x; x)_2 = (1 - x)(1 - x^2)\).

public theorem_wanted arndtGF_univ_mul :
    arndtGF (fun _ => True) *
        ((1 - PowerSeries.X) * (1 - PowerSeries.X ^ 2) -
          PowerSeries.C (Polynomial.X ^ 2) * PowerSeries.X ^ 3) =
      (1 - PowerSeries.X + PowerSeries.C Polynomial.X * PowerSeries.X) *
        (1 - PowerSeries.X ^ 2)

Sources

• Mohammed L. Nadji, Moussa Ahmia, Daniel F. Checa, and José L. Ramírez, Arndt Compositions with Restricted Parts, Palindromes, and Colored Variants, Journal of Integer Sequences 28 (2025), Article 25.3.6, Theorem 9 (jis-2025-25.3.6-thm-9).

Uses 1

Statement usesGenerating function of Arndt compositions with parts in a set

TheoremArndt compositions with a given number of parts as a sum of products#●ready to prove

For all natural numbers \(n\) and \(\ell\), the number of Arndt compositions of \(n\) with \(2\ell\) parts is

\[\sum_{(a_1, \dots, a_\ell)} \prod_{i=1}^{\ell} \left\lfloor \frac{a_i - 1}{2} \right\rfloor,\]

the sum running over the \(\ell\)-tuples of natural numbers with \(a_1 + \dots + a_\ell = n\) and every \(a_i \ge 3\); and the number of Arndt compositions of \(n\) with \(2\ell + 1\) parts is the same sum of products \(\prod_{i=1}^{\ell} \lfloor (a_i - 1)/2 \rfloor\), now running over the \((\ell + 1)\)-tuples \((a_1, \dots, a_{\ell+1})\) of natural numbers with \(a_1 + \dots + a_{\ell+1} = n\), \(a_1, \dots, a_\ell \ge 3\) and \(a_{\ell+1} \ge 1\).

public theorem_wanted arndtCompositionCount_eq_sum_prod (n ℓ : ℕ) :
    arndtCompositionCount (fun _ => True) n (2 * ℓ) =
        (∑ a ∈ (Finset.Nat.antidiagonalTuple ℓ n).filter (fun a => ∀ i, 3 ≤ a i),
          ∏ i, (a i - 1) / 2) ∧
      arndtCompositionCount (fun _ => True) n (2 * ℓ + 1) =
        (∑ a ∈ (Finset.Nat.antidiagonalTuple (ℓ + 1) n).filter
            (fun a => (∀ i : Fin ℓ, 3 ≤ a i.castSucc) ∧ 1 ≤ a (Fin.last ℓ)),
          ∏ i : Fin ℓ, (a i.castSucc - 1) / 2)

Sources

• Mohammed L. Nadji, Moussa Ahmia, Daniel F. Checa, and José L. Ramírez, Arndt Compositions with Restricted Parts, Palindromes, and Colored Variants, Journal of Integer Sequences 28 (2025), Article 25.3.6, Theorem 10 (jis-2025-25.3.6-thm-10).

Uses 1

Statement usesNumber of Arndt compositions with parts in a set

TheoremArndt compositions with parts at most 3 and the Padovan numbers#●ready to prove

For every \(n \ge 0\), the number of Arndt compositions of \(n\) (compositions \((\sigma_1, \dots, \sigma_k)\) with \(\sigma_{2i-1} > \sigma_{2i}\) whenever \(2i \le k\)) with all parts in \(\{1, 2, 3\}\), counting the empty composition when \(n = 0\), equals the shifted Padovan number \(s_{n+2}\), where \(s_0 = 1\), \(s_1 = 0\), \(s_2 = 1\) and \(s_{m+3} = s_{m+1} + s_m\). Equivalently, it is the Padovan number \(P(n)\) given by \(P(0) = P(1) = P(2) = 1\) and \(P(n) = P(n-2) + P(n-3)\) for \(n \ge 3\).

public theorem_wanted sum_arndtCompositionCount_le_three (n : ℕ) :
    ∑ k ∈ Finset.range (n + 1), arndtCompositionCount (fun i => i ≤ 3) n k =
      shiftedPadovanSequence (n + 2)

Sources

• Mohammed L. Nadji, Moussa Ahmia, Daniel F. Checa, and José L. Ramírez, Arndt Compositions with Restricted Parts, Palindromes, and Colored Variants, Journal of Integer Sequences 28 (2025), Article 25.3.6, Theorem 2 (jis-2025-25.3.6-thm-2).

Uses 2

Statement usesNumber of Arndt compositions with parts in a set · Shifted Padovan sequence

TheoremArndt compositions with parts at most 4 and Narayana's cows sequence#●ready to prove

For every \(n \ge 0\), the number of Arndt compositions of \(n\) (compositions \((\sigma_1, \dots, \sigma_k)\) with \(\sigma_{2i-1} > \sigma_{2i}\) whenever \(2i \le k\)) with all parts in \(\{1, 2, 3, 4\}\), counting the empty composition when \(n = 0\), equals \(N_{n+1}\), where \((N_m)\) is Narayana's cows sequence: \(N_0 = 0\), \(N_1 = N_2 = 1\) and \(N_m = N_{m-1} + N_{m-3}\) for \(m \ge 3\).

public theorem_wanted sum_arndtCompositionCount_le_four (n : ℕ) :
    ∑ k ∈ Finset.range (n + 1), arndtCompositionCount (fun i => i ≤ 4) n k =
      narayanaCowsSequence (n + 1)

Sources

• Mohammed L. Nadji, Moussa Ahmia, Daniel F. Checa, and José L. Ramírez, Arndt Compositions with Restricted Parts, Palindromes, and Colored Variants, Journal of Integer Sequences 28 (2025), Article 25.3.6, Theorem 4 (jis-2025-25.3.6-thm-4).

Uses 2

Statement usesNumber of Arndt compositions with parts in a set · Narayana's cows sequence

TheoremGenerating function of Arndt compositions with bounded largest part#●ready to prove

For a natural number \(\ell\), let \(A(x, y; \ell)\) be the formal power series in \(x\) over \(\mathbb{Z}[y]\) whose coefficient of \(x^n y^k\) is the number of Arndt compositions of \(n\) with \(k\) parts, all at most \(\ell\), and let

\[D_\ell(x, y) = 1 - x^{2+2\ell} y^2 + x^{2+\ell} (1 + x) y^2 - x (1 + x + x^2 (y^2 - 1)).\]

Then

\[A(x, y; \ell) \, D_\ell(x, y) = (1 - x^2)\left(1 - x + x (1 - x^\ell) y\right).\]

The paper assumes \(\ell \ge 2\); the identity also holds for \(\ell = 0, 1\).

public theorem_wanted arndtGF_le_mul (ℓ : ℕ) :
    arndtGF (fun i => i ≤ ℓ) *
        (1 - PowerSeries.X ^ (2 + 2 * ℓ) * PowerSeries.C (Polynomial.X ^ 2) +
          PowerSeries.X ^ (2 + ℓ) * (1 + PowerSeries.X) * PowerSeries.C (Polynomial.X ^ 2) -
          PowerSeries.X * (1 + PowerSeries.X +
            PowerSeries.X ^ 2 * (-1 + PowerSeries.C (Polynomial.X ^ 2)))) =
      (1 - PowerSeries.X ^ 2) *
        (1 - PowerSeries.X + PowerSeries.X * (1 - PowerSeries.X ^ ℓ) * PowerSeries.C Polynomial.X)

Sources

• Mohammed L. Nadji, Moussa Ahmia, Daniel F. Checa, and José L. Ramírez, Arndt Compositions with Restricted Parts, Palindromes, and Colored Variants, Journal of Integer Sequences 28 (2025), Article 25.3.6, Corollary 5 (jis-2025-25.3.6-cor-5).

Uses 1

Statement usesGenerating function of Arndt compositions with parts in a set

TheoremGenerating function of Arndt compositions with bounded smallest part#●ready to prove

For a natural number \(\ell \ge 1\), let \(B(x, y; \ell)\) be the formal power series in \(x\) over \(\mathbb{Z}[y]\) whose coefficient of \(x^n y^k\) is the number of Arndt compositions of \(n\) with \(k\) parts, all at least \(\ell\). Then

\[B(x, y; \ell) \left(1 - x - x^2 + x^3 - x^{2\ell+1} y^2\right) = (1 - x^2)(1 - x + x^\ell y).\]

public theorem_wanted arndtGF_ge_mul (ℓ : ℕ) (hℓ : 1 ≤ ℓ) :
    arndtGF (fun i => ℓ ≤ i) *
        (1 - PowerSeries.X - PowerSeries.X ^ 2 + PowerSeries.X ^ 3 -
          PowerSeries.X ^ (2 * ℓ + 1) * PowerSeries.C (Polynomial.X ^ 2)) =
      (1 - PowerSeries.X ^ 2) *
        (1 - PowerSeries.X + PowerSeries.X ^ ℓ * PowerSeries.C Polynomial.X)

Sources

• Mohammed L. Nadji, Moussa Ahmia, Daniel F. Checa, and José L. Ramírez, Arndt Compositions with Restricted Parts, Palindromes, and Colored Variants, Journal of Integer Sequences 28 (2025), Article 25.3.6, Corollary 6 (jis-2025-25.3.6-cor-6).

Uses 1

Statement usesGenerating function of Arndt compositions with parts in a set

TheoremGenerating functions of Arndt compositions with even parts and with odd parts#●ready to prove

Let \(A_E(x, y)\) and \(A_O(x, y)\) be the formal power series in \(x\) over \(\mathbb{Z}[y]\) whose coefficient of \(x^n y^k\) is the number of Arndt compositions of \(n\) with \(k\) parts, all even, respectively all odd. Then

\[A_E(x, y) \left(1 - x^2 - x^4 + x^6 (1 - y^2)\right) = (1 - x^4)\left(1 - x^2 (1 - y)\right)\]

and

\[A_O(x, y) \left(1 - x^2 + x^6 - x^4 (1 + y^2)\right) = (1 - x^4)(1 - x^2 + x y).\]

public theorem_wanted arndtGF_even_odd_mul :
    arndtGF (fun i => i % 2 = 0) *
          (1 - PowerSeries.X ^ 2 - PowerSeries.X ^ 4 +
            PowerSeries.X ^ 6 * (1 - PowerSeries.C (Polynomial.X ^ 2))) =
        (1 - PowerSeries.X ^ 4) *
          (1 - PowerSeries.X ^ 2 * (1 - PowerSeries.C Polynomial.X)) ∧
      arndtGF (fun i => i % 2 = 1) *
          (1 - PowerSeries.X ^ 2 + PowerSeries.X ^ 6 -
            PowerSeries.X ^ 4 * (1 + PowerSeries.C (Polynomial.X ^ 2))) =
        (1 - PowerSeries.X ^ 4) *
          (1 - PowerSeries.X ^ 2 + PowerSeries.X * PowerSeries.C Polynomial.X)

Sources

• Mohammed L. Nadji, Moussa Ahmia, Daniel F. Checa, and José L. Ramírez, Arndt Compositions with Restricted Parts, Palindromes, and Colored Variants, Journal of Integer Sequences 28 (2025), Article 25.3.6, Corollary 7 (jis-2025-25.3.6-cor-7).

Uses 1

Statement usesGenerating function of Arndt compositions with parts in a set

DefinitionDown/up compositions#✓fully proved

A down/up (descending wiggly) composition of \(n\) with \(k\) parts is a sequence \((\sigma_1, \dots, \sigma_k)\) of positive integers with sum \(n\) such that \(\sigma_1 > \sigma_2 < \sigma_3 > \sigma_4 < \cdots\), that is, \(\sigma_i > \sigma_{i+1}\) for odd \(i\) and \(\sigma_i < \sigma_{i+1}\) for even \(i\). For \(n, k, j \ge 0\), \(w(n, k, j)\) is the number of down/up compositions of \(n\) with \(k\) parts whose last part \(\sigma_k\) equals \(j\), where the empty composition (\(k = 0\)) is taken to have last part \(0\).

def downUpCompositionCount (n k j : ℕ) : ℕ :=
  ((Finset.Nat.antidiagonalTuple k n).filter fun c =>
    (∀ i, 0 < c i) ∧
      (∀ i i' : Fin k, (i' : ℕ) = i + 1 →
        ((i : ℕ) % 2 = 0 → c i' < c i) ∧ ((i : ℕ) % 2 = 1 → c i < c i')) ∧
      (if h : 0 < k then c ⟨k - 1, by omega⟩ else 0) = j).card

Sources

• Mohammed L. Nadji, Moussa Ahmia, Daniel F. Checa, and José L. Ramírez, Arndt Compositions with Restricted Parts, Palindromes, and Colored Variants, Journal of Integer Sequences 28 (2025), Article 25.3.6, Section 3 (the set W, OEIS A025049).

Used by 4

Used byDown/up compositions of 5 with two parts · Down/up compositions of 6 with three parts · Generating function of down/up compositions with an even number of parts · Generating function of down/up compositions with an odd number of parts

TheoremDown/up compositions of 5 with two parts#✓fully proved

Among the down/up compositions of \(5\) with two parts (pairs \((\sigma_1, \sigma_2)\) of positive integers with \(\sigma_1 + \sigma_2 = 5\) and \(\sigma_1 > \sigma_2\)), exactly one has last part \(1\), exactly one has last part \(2\), and none has last part \(3\).

The compositions counted are \((4, 1)\) and \((3, 2)\).

theorem downUpCompositionCount_five_two : downUpCompositionCount 5 2 1 = 1 ∧
    downUpCompositionCount 5 2 2 = 1 ∧ downUpCompositionCount 5 2 3 = 0

Sources

• Mohammed L. Nadji, Moussa Ahmia, Daniel F. Checa, and José L. Ramírez, Arndt Compositions with Restricted Parts, Palindromes, and Colored Variants, Journal of Integer Sequences 28 (2025), Article 25.3.6, Section 3 (the set W).

Uses 1

Statement usesDown/up compositions

TheoremDown/up compositions of 6 with three parts#✓fully proved

Among the down/up compositions of \(6\) with three parts (triples \((\sigma_1, \sigma_2, \sigma_3)\) of positive integers with sum \(6\) and \(\sigma_1 > \sigma_2 < \sigma_3\)), exactly one has last part \(3\), exactly one has last part \(2\), and none has last part \(1\).

The compositions counted are \((2, 1, 3)\) and \((3, 1, 2)\).

theorem downUpCompositionCount_six_three : downUpCompositionCount 6 3 3 = 1 ∧
    downUpCompositionCount 6 3 2 = 1 ∧ downUpCompositionCount 6 3 1 = 0

Sources

• Mohammed L. Nadji, Moussa Ahmia, Daniel F. Checa, and José L. Ramírez, Arndt Compositions with Restricted Parts, Palindromes, and Colored Variants, Journal of Integer Sequences 28 (2025), Article 25.3.6, Section 3 (the set W).

Uses 1

Statement usesDown/up compositions

DefinitionGenerating function of down/up compositions with an even number of parts#✓fully proved

\(F(x, y, z)\) is the formal power series in \(\mathbb{Q}[[x, y, z]]\) whose coefficient of \(x^n y^k z^j\) is the number of down/up compositions of \(n\) with \(k\) parts and last part \(j\) when \(k\) is even, and \(0\) when \(k\) is odd. The empty composition, with last part \(0\), contributes the constant term \(1\).

noncomputable def downUpEvenGF : MvPowerSeries (Fin 3) ℚ := fun e =>
  if e 1 % 2 = 0 then (downUpCompositionCount (e 0) (e 1) (e 2) : ℚ) else 0

Sources

• Mohammed L. Nadji, Moussa Ahmia, Daniel F. Checa, and José L. Ramírez, Arndt Compositions with Restricted Parts, Palindromes, and Colored Variants, Journal of Integer Sequences 28 (2025), Article 25.3.6, Section 3.1 (definition of F).

Uses 1 · Used by 3

Statement usesDown/up compositions

Used byFormula for the generating function of even-length down/up compositions · Odd-length down/up compositions from even-length ones · Generating function of palindromic Arndt compositions

DefinitionGenerating function of down/up compositions with an odd number of parts#✓fully proved

\(G(x, y, z)\) is the formal power series in \(\mathbb{Q}[[x, y, z]]\) whose coefficient of \(x^n y^k z^j\) is the number of down/up compositions of \(n\) with \(k\) parts and last part \(j\) when \(k\) is odd, and \(0\) when \(k\) is even.

noncomputable def downUpOddGF : MvPowerSeries (Fin 3) ℚ := fun e =>
  if e 1 % 2 = 1 then (downUpCompositionCount (e 0) (e 1) (e 2) : ℚ) else 0

Sources

• Mohammed L. Nadji, Moussa Ahmia, Daniel F. Checa, and José L. Ramírez, Arndt Compositions with Restricted Parts, Palindromes, and Colored Variants, Journal of Integer Sequences 28 (2025), Article 25.3.6, Section 3.1 (definition of G).

Uses 1 · Used by 1

Statement usesDown/up compositions

Used byOdd-length down/up compositions from even-length ones

DefinitionThe auxiliary series \(\alpha\) for down/up compositions#✓fully proved

In \(\mathbb{Q}[[x, y, z]]\) write \((a; x)_m = \prod_{j=0}^{m-1} (1 - a x^j)\). For a power series \(w\) in \(\mathbb{Q}[[x, y, z]]\), the series \(\alpha(x, y, w)\) is the coefficientwise convergent sum \(\alpha(x, y, w) = \sum_{n \ge 0} \frac{(-1)^n x^{n^2+n} y^{2n} w^n}{(xw; x)_{2n}}\).

The paper uses it with \(w = z\) and with \(w = x\).

noncomputable def arndtPalAlpha (w : MvPowerSeries (Fin 3) ℚ) : MvPowerSeries (Fin 3) ℚ :=
  ∑' n : ℕ, (-1 : MvPowerSeries (Fin 3) ℚ) ^ n * MvPowerSeries.X 0 ^ (n ^ 2 + n) *
    MvPowerSeries.X 1 ^ (2 * n) * w ^ n *
      (∏ k ∈ Finset.range (2 * n), (1 - MvPowerSeries.X 0 ^ (k + 1) * w))⁻¹

Sources

• Mohammed L. Nadji, Moussa Ahmia, Daniel F. Checa, and José L. Ramírez, Arndt Compositions with Restricted Parts, Palindromes, and Colored Variants, Journal of Integer Sequences 28 (2025), Article 25.3.6, Theorem 12, equation (5).

Used by 1

Used byFormula for the generating function of even-length down/up compositions

DefinitionThe auxiliary series \(\beta\) for down/up compositions#✓fully proved

In \(\mathbb{Q}[[x, y, z]]\) write \((a; x)_m = \prod_{j=0}^{m-1} (1 - a x^j)\). For a power series \(w\) in \(\mathbb{Q}[[x, y, z]]\), the series \(\beta(x, y, w)\) is the coefficientwise convergent sum \(\beta(x, y, w) = \sum_{n \ge 1} \frac{(-1)^{n+1} x^{n^2+n} y^{2n} w^n}{(1 - x)(xw; x)_{2n-1}}\).

The paper uses it with \(w = z\) and with \(w = x\).

noncomputable def arndtPalBeta (w : MvPowerSeries (Fin 3) ℚ) : MvPowerSeries (Fin 3) ℚ :=
  ∑' n : ℕ, (-1 : MvPowerSeries (Fin 3) ℚ) ^ (n + 2) * MvPowerSeries.X 0 ^ ((n + 1) ^ 2 + (n + 1)) *
    MvPowerSeries.X 1 ^ (2 * (n + 1)) * w ^ (n + 1) *
      ((1 - MvPowerSeries.X 0) *
        ∏ k ∈ Finset.range (2 * n + 1), (1 - MvPowerSeries.X 0 ^ (k + 1) * w))⁻¹

Sources

• Mohammed L. Nadji, Moussa Ahmia, Daniel F. Checa, and José L. Ramírez, Arndt Compositions with Restricted Parts, Palindromes, and Colored Variants, Journal of Integer Sequences 28 (2025), Article 25.3.6, Theorem 12, equation (5).

Used by 1

Used byFormula for the generating function of even-length down/up compositions

TheoremFormula for the generating function of even-length down/up compositions#●ready to prove

Let \(F(x, y, z) \in \mathbb{Q}[[x, y, z]]\) be the generating function of down/up compositions with an even number of parts (including the empty composition, with last part \(0\)) by weight (\(x\)), number of parts (\(y\)) and last part (\(z\)). For a power series \(w\), write \((xw; x)_m = \prod_{i=1}^{m} (1 - x^i w)\) and let

\[\alpha(x, y, w) = \sum_{n \ge 0} \frac{(-1)^n x^{n^2+n} y^{2n} w^n}{(xw; x)_{2n}}\]

and

\[\beta(x, y, w) = \sum_{n \ge 1} \frac{(-1)^{n+1} x^{n^2+n} y^{2n} w^n}{(1 - x)(xw; x)_{2n-1}},\]

with the sums taken coefficientwise. Then

\[F(x, y, z) = \alpha(x, y, z) + \frac{\alpha(x, y, x)\, \beta(x, y, z)}{1 - \beta(x, y, x)}.\]

public theorem_wanted downUpEvenGF_eq :
    downUpEvenGF = arndtPalAlpha (MvPowerSeries.X 2) +
      arndtPalAlpha (MvPowerSeries.X 0) * (1 - arndtPalBeta (MvPowerSeries.X 0))⁻¹ *
        arndtPalBeta (MvPowerSeries.X 2)

Sources

• Mohammed L. Nadji, Moussa Ahmia, Daniel F. Checa, and José L. Ramírez, Arndt Compositions with Restricted Parts, Palindromes, and Colored Variants, Journal of Integer Sequences 28 (2025), Article 25.3.6, Theorem 12 (jis-2025-25.3.6-thm-12).

Uses 3

Statement usesThe auxiliary series \(\alpha\) for down/up compositions · The auxiliary series \(\beta\) for down/up compositions · Generating function of down/up compositions with an even number of parts

TheoremOdd-length down/up compositions from even-length ones#●ready to prove

Let \(F(x, y, z)\) and \(G(x, y, z)\) in \(\mathbb{Q}[[x, y, z]]\) be the generating functions of down/up compositions with an even, respectively odd, number of parts by weight (\(x\)), number of parts (\(y\)) and last part (\(z\)). Then

\[G(x, y, z) = \frac{xyz}{1 - xz}\, F(x, y, xz).\]

public theorem_wanted downUpOddGF_eq :
    downUpOddGF = MvPowerSeries.X 0 * MvPowerSeries.X 1 * MvPowerSeries.X 2 *
      (1 - MvPowerSeries.X 0 * MvPowerSeries.X 2)⁻¹ *
        MvPowerSeries.subst
          ![MvPowerSeries.X 0, MvPowerSeries.X 1, MvPowerSeries.X 0 * MvPowerSeries.X 2]
          downUpEvenGF

Sources

• Mohammed L. Nadji, Moussa Ahmia, Daniel F. Checa, and José L. Ramírez, Arndt Compositions with Restricted Parts, Palindromes, and Colored Variants, Journal of Integer Sequences 28 (2025), Article 25.3.6, Theorem 13 (jis-2025-25.3.6-thm-13).

Uses 2

Statement usesGenerating function of down/up compositions with an even number of parts · Generating function of down/up compositions with an odd number of parts

DefinitionPalindromic Arndt compositions#✓fully proved

An Arndt composition of \(n\) with \(k\) parts is a sequence \((\sigma_1, \dots, \sigma_k)\) of positive integers with sum \(n\) such that \(\sigma_{2i-1} > \sigma_{2i}\) whenever \(2i \le k\); it is palindromic when \(\sigma_i = \sigma_{k+1-i}\) for all \(i\). For \(n, k, m \ge 0\), \(p(n, k, m)\) is the number of palindromic Arndt compositions of \(n\) with \(k \ge 1\) parts whose middle summand \(\sigma_{\lfloor k/2 \rfloor + 1}\) equals \(m\); in particular \(p(n, 0, m) = 0\).

def palindromicArndtCount (n k m : ℕ) : ℕ :=
  ((Finset.Nat.antidiagonalTuple k n).filter fun c =>
    (∀ i, 0 < c i) ∧
      (∀ i j : Fin k, (i : ℕ) % 2 = 0 → (j : ℕ) = i + 1 → c j < c i) ∧
      (∀ i j : Fin k, (i : ℕ) + j + 1 = k → c i = c j) ∧
      (if h : 0 < k then c ⟨k / 2, by omega⟩ = m else False)).card

Sources

• Mohammed L. Nadji, Moussa Ahmia, Daniel F. Checa, and José L. Ramírez, Arndt Compositions with Restricted Parts, Palindromes, and Colored Variants, Journal of Integer Sequences 28 (2025), Article 25.3.6, Section 3 (the set PA).

Used by 2

Used byPalindromic Arndt compositions of 5 · Palindromic Arndt generating function

TheoremPalindromic Arndt compositions of 5#✓fully proved

There is exactly one palindromic Arndt composition of \(5\) with one part and middle summand \(5\), exactly one with three parts and middle summand \(1\), and none with three parts and middle summand \(2\).

The compositions counted are \((5)\) and \((2, 1, 2)\); the paper reads them off the coefficient of \(x^5\) in the series expansion of the generating function of palindromic Arndt compositions.

theorem palindromicArndtCount_five : palindromicArndtCount 5 1 5 = 1 ∧
    palindromicArndtCount 5 3 1 = 1 ∧ palindromicArndtCount 5 3 2 = 0

Sources

• Mohammed L. Nadji, Moussa Ahmia, Daniel F. Checa, and José L. Ramírez, Arndt Compositions with Restricted Parts, Palindromes, and Colored Variants, Journal of Integer Sequences 28 (2025), Article 25.3.6, Section 3.2 (series expansion of PA(x, y, 1)).

Uses 1

Statement usesPalindromic Arndt compositions

DefinitionPalindromic Arndt generating function#✓fully proved

A palindromic Arndt composition of \(n\) with \(k \ge 1\) parts is a tuple \((\sigma_1, \dots, \sigma_k)\) of positive integers with sum \(n\) such that \(\sigma_{2i-1} > \sigma_{2i}\) whenever \(2i \le k\), and \(\sigma_i = \sigma_{k+1-i}\) for all \(i\); its middle summand is \(\sigma_{\lfloor k/2 \rfloor + 1}\). The generating function \(PA(x, y, z)\) is the formal power series in \(x, y, z\) with rational coefficients whose coefficient of \(x^n y^k z^m\) is the number of palindromic Arndt compositions of \(n\) with \(k\) parts and middle summand \(m\).

noncomputable def palindromicArndtGF : MvPowerSeries (Fin 3) ℚ := fun e =>
  (palindromicArndtCount (e 0) (e 1) (e 2) : ℚ)

Sources

• Mohammed L. Nadji, Moussa Ahmia, Daniel F. Checa, and José L. Ramírez, Arndt Compositions with Restricted Parts, Palindromes, and Colored Variants, Journal of Integer Sequences 28 (2025), Article 25.3.6, Section 3.2 (definition of PA).

Uses 1 · Used by 1

Statement usesPalindromic Arndt compositions

Used byGenerating function of palindromic Arndt compositions

TheoremGenerating function of palindromic Arndt compositions#●ready to prove

Let \(PA(x, y, z)\) be the generating function of nonempty palindromic Arndt compositions by weight (\(x\)), number of parts (\(y\)) and middle summand (\(z\)), and let \(F(x, y, z)\) be the generating function of down/up compositions \(\sigma_1 > \sigma_2 < \sigma_3 > \cdots\) with an even number of parts by weight (\(x\)), number of parts (\(y\)) and last part (\(z\)). Then, as formal power series over \(\mathbb{Q}\),

\[ PA(x, y, z) = \frac{xyz}{1 - xz} F(x^2, y^2, xz) + \frac{x^3 y^3 z}{(1 - x^2)(1 - xz)} F(x^2, y^2, x^2) - \frac{x^3 y^3 z}{(1 - xz)(1 - x^3 z)} F(x^2, y^2, x^3 z). \]

MetaMathlibExt.palindromicArndtGF_eq · 15 lines

public theorem_wanted palindromicArndtGF_eq :
    palindromicArndtGF =
      MvPowerSeries.X 0 * MvPowerSeries.X 1 * MvPowerSeries.X 2 *
          (1 - MvPowerSeries.X 0 * MvPowerSeries.X 2)⁻¹ *
          MvPowerSeries.subst ![MvPowerSeries.X 0 ^ 2, MvPowerSeries.X 1 ^ 2,
            MvPowerSeries.X 0 * MvPowerSeries.X 2] downUpEvenGF +
        MvPowerSeries.X 0 ^ 3 * MvPowerSeries.X 1 ^ 3 * MvPowerSeries.X 2 *
          ((1 - MvPowerSeries.X 0 ^ 2) * (1 - MvPowerSeries.X 0 * MvPowerSeries.X 2))⁻¹ *
          MvPowerSeries.subst ![MvPowerSeries.X 0 ^ 2, MvPowerSeries.X 1 ^ 2,
            MvPowerSeries.X 0 ^ 2] downUpEvenGF -
        MvPowerSeries.X 0 ^ 3 * MvPowerSeries.X 1 ^ 3 * MvPowerSeries.X 2 *
          ((1 - MvPowerSeries.X 0 * MvPowerSeries.X 2) *
            (1 - MvPowerSeries.X 0 ^ 3 * MvPowerSeries.X 2))⁻¹ *
          MvPowerSeries.subst ![MvPowerSeries.X 0 ^ 2, MvPowerSeries.X 1 ^ 2,
            MvPowerSeries.X 0 ^ 3 * MvPowerSeries.X 2] downUpEvenGF

Sources

• Mohammed L. Nadji, Moussa Ahmia, Daniel F. Checa, and José L. Ramírez, Arndt Compositions with Restricted Parts, Palindromes, and Colored Variants, Journal of Integer Sequences 28 (2025), Article 25.3.6, Theorem 14 (jis-2025-25.3.6-thm-14).

Uses 2

Statement usesGenerating function of down/up compositions with an even number of parts · Palindromic Arndt generating function

DefinitionColored Arndt compositions#✓fully proved

An Arndt composition of \(n\) with \(k\) parts is a sequence \((\sigma_1, \dots, \sigma_k)\) of positive integers with sum \(n\) such that \(\sigma_{2i-1} > \sigma_{2i}\) for every \(i\) with \(2i \le k\). In a colored Arndt composition, each part of size \(m\) carries one of \(m\) colors. The number \(c(n, k)\) of colored Arndt compositions of \(n\) with \(k\) parts is therefore the sum of \(\sigma_1 \sigma_2 \cdots \sigma_k\) over all Arndt compositions \((\sigma_1, \dots, \sigma_k)\) of \(n\) with \(k\) parts.

def coloredArndtCount (n k : ℕ) : ℕ :=
  ∑ c ∈ (Finset.Nat.antidiagonalTuple k n).filter (fun c =>
      (∀ i, 0 < c i) ∧ ∀ i j : Fin k, (i : ℕ) % 2 = 0 → (j : ℕ) = i + 1 → c j < c i),
    ∏ i, c i

Sources

• Mohammed L. Nadji, Moussa Ahmia, Daniel F. Checa, and José L. Ramírez, Arndt Compositions with Restricted Parts, Palindromes, and Colored Variants, Journal of Integer Sequences 28 (2025), Article 25.3.6, Section 4 (definition of colored Arndt compositions).

Used by 5

Used byColored Arndt compositions of 4 · Asymptotics of colored Arndt compositions with \(k\) parts · Generating function of colored Arndt compositions · Generating function of colored Arndt compositions with \(k\) parts · Generating function for the total number of colored Arndt compositions

TheoremColored Arndt compositions of 4#✓fully proved

Write \(m_a\) for a part of size \(m\) with color \(a \in \{1, \dots, m\}\). The colored Arndt compositions of \(4\) are \((4_1)\), \((4_2)\), \((4_3)\), \((4_4)\), \((3_a, 1_1)\) for \(a \le 3\), and \((2_a, 1_1, 1_1)\) for \(a \le 2\). Hence the numbers of colored Arndt compositions of \(4\) with \(1\), \(2\) and \(3\) parts are \(c(4, 1) = 4\), \(c(4, 2) = 3\) and \(c(4, 3) = 2\).

theorem coloredArndtCount_four : coloredArndtCount 4 1 = 4 ∧ coloredArndtCount 4 2 = 3 ∧
    coloredArndtCount 4 3 = 2

Sources

• Mohammed L. Nadji, Moussa Ahmia, Daniel F. Checa, and José L. Ramírez, Arndt Compositions with Restricted Parts, Palindromes, and Colored Variants, Journal of Integer Sequences 28 (2025), Article 25.3.6, Section 4, list (6).

Uses 1

Statement usesColored Arndt compositions

DefinitionGenerating function of colored Arndt compositions#✓fully proved

The bivariate generating function of colored Arndt compositions, by weight (\(x\)) and number of parts (\(y\)), is the power series \(C(x, y) = \sum_{n \ge 0} \left(\sum_{k=0}^{n} c(n, k)\, y^k\right) x^n\) in \(\mathbb{Z}[y][[x]]\), where \(c(n, k)\) is the number of colored Arndt compositions of \(n\) with \(k\) parts.

noncomputable def coloredArndtGF : PowerSeries (Polynomial ℤ) :=
  PowerSeries.mk fun n =>
    ∑ k ∈ Finset.range (n + 1), (coloredArndtCount n k : Polynomial ℤ) * Polynomial.X ^ k

Sources

• Mohammed L. Nadji, Moussa Ahmia, Daniel F. Checa, and José L. Ramírez, Arndt Compositions with Restricted Parts, Palindromes, and Colored Variants, Journal of Integer Sequences 28 (2025), Article 25.3.6, Section 4 (definition of C(x, y)).

Uses 1 · Used by 1

Statement usesColored Arndt compositions

Used byClosed form of the generating function of colored Arndt compositions

TheoremClosed form of the generating function of colored Arndt compositions#●ready to prove

Let \(C(x, y) = \sum_{n, k} c(n, k)\, x^n y^k\) in \(\mathbb{Z}[y][[x]]\), where \(c(n, k)\) is the number of colored Arndt compositions of \(n\) with \(k\) parts. Then \(C(x, y) \cdot (1 - x - 3x^2 - x^3(2y^2 - 3) - x^4(y^2 - 3) - x^5(3 + y^2) - x^6 + x^7) = (1 - x)^2 (1 + x)^3 (1 + x^2 + x(y - 2))\).

Since the second factor on the left has constant term \(1\), this says that \(C(x, y) = \frac{(1 - x)^2 (1 + x)^3 (1 + x^2 + x(y - 2))}{1 - x - 3x^2 - x^3(2y^2 - 3) - x^4(y^2 - 3) - x^5(3 + y^2) - x^6 + x^7}\).

public theorem_wanted coloredArndtGF_mul :
    coloredArndtGF *
        (1 - PowerSeries.X - 3 * PowerSeries.X ^ 2 -
          PowerSeries.X ^ 3 * (2 * PowerSeries.C (Polynomial.X ^ 2) - 3) -
          PowerSeries.X ^ 4 * (PowerSeries.C (Polynomial.X ^ 2) - 3) -
          PowerSeries.X ^ 5 * (3 + PowerSeries.C (Polynomial.X ^ 2)) -
          PowerSeries.X ^ 6 + PowerSeries.X ^ 7) =
      (1 - PowerSeries.X) ^ 2 * (1 + PowerSeries.X) ^ 3 *
        (1 + PowerSeries.X ^ 2 + PowerSeries.X * (PowerSeries.C Polynomial.X - 2))

Sources

• Mohammed L. Nadji, Moussa Ahmia, Daniel F. Checa, and José L. Ramírez, Arndt Compositions with Restricted Parts, Palindromes, and Colored Variants, Journal of Integer Sequences 28 (2025), Article 25.3.6, Theorem 17 (jis-2025-25.3.6-thm-17).

Uses 1

Statement usesGenerating function of colored Arndt compositions

TheoremGenerating function for the total number of colored Arndt compositions#●ready to prove

For \(n \ge 0\) let \(c(n, k)\) be the number of colored Arndt compositions of \(n\) with \(k\) parts, and let \(c(n) = \sum_{k=0}^{n} c(n, k)\) be the total number of colored Arndt compositions of \(n\) (so \(c(0) = 1\), counting the empty composition). Then, in the ring \(\mathbb{Z}[[x]]\) of formal power series,

\[\Big(\sum_{n \ge 0} c(n) x^n\Big) (1 - x - 3x^2 + x^3 + 2x^4 - 4x^5 - x^6 + x^7) = (1 - x)^2 (1 + x)^3 (1 - x + x^2).\]

public theorem_wanted coloredArndt_total_mul :
    (PowerSeries.mk fun n => ∑ k ∈ Finset.range (n + 1), (coloredArndtCount n k : ℤ)) *
        (1 - PowerSeries.X - 3 * PowerSeries.X ^ 2 + PowerSeries.X ^ 3 + 2 * PowerSeries.X ^ 4 -
          4 * PowerSeries.X ^ 5 - PowerSeries.X ^ 6 + PowerSeries.X ^ 7) =
      (1 - PowerSeries.X) ^ 2 * (1 + PowerSeries.X) ^ 3 *
        (1 - PowerSeries.X + PowerSeries.X ^ 2)

Sources

• Mohammed L. Nadji, Moussa Ahmia, Daniel F. Checa, and José L. Ramírez, Arndt Compositions with Restricted Parts, Palindromes, and Colored Variants, Journal of Integer Sequences 28 (2025), Article 25.3.6, Corollary 18 (jis-2025-25.3.6-cor-18).

Uses 1

Statement usesColored Arndt compositions

TheoremGenerating function of colored Arndt compositions with \(k\) parts#●ready to prove

For every \(k \ge 0\), let \(C_k(x) = \sum_{n \ge 0} c(n, k)\, x^n\) in \(\mathbb{Z}[[x]]\), where \(c(n, k)\) is the number of colored Arndt compositions of \(n\) with \(k\) parts. Then \(C_k(x)\, (1 - x)^{2k} (1 + x)^{3\lfloor k/2 \rfloor} = x^{k + \lfloor k/2 \rfloor} (x^2 + x + 2)^{\lfloor k/2 \rfloor}\).

Equivalently, since \((1 - x)^{2k} (1 + x)^{3\lfloor k/2 \rfloor}\) has constant term \(1\), \(C_k(x) = \frac{x^{k + \lfloor k/2 \rfloor} (x^2 + x + 2)^{\lfloor k/2 \rfloor}} {(1 - x)^{2k} (1 + x)^{3\lfloor k/2 \rfloor}}\).

public theorem_wanted coloredArndt_parts_mul (k : ℕ) :
    (PowerSeries.mk fun n => (coloredArndtCount n k : ℤ)) *
        ((1 - PowerSeries.X) ^ (2 * k) * (1 + PowerSeries.X) ^ (3 * (k / 2))) =
      PowerSeries.X ^ (k + k / 2) * (PowerSeries.X ^ 2 + PowerSeries.X + 2) ^ (k / 2)

Sources

• Mohammed L. Nadji, Moussa Ahmia, Daniel F. Checa, and José L. Ramírez, Arndt Compositions with Restricted Parts, Palindromes, and Colored Variants, Journal of Integer Sequences 28 (2025), Article 25.3.6, Theorem 19 (jis-2025-25.3.6-thm-19).

Uses 1

Statement usesColored Arndt compositions

TheoremAsymptotics of colored Arndt compositions with \(k\) parts#●ready to prove

For every fixed \(k \ge 1\), the number \(c(n, k)\) of colored Arndt compositions of \(n\) with \(k\) parts satisfies \(c(n, k) \sim \frac{n^{2k-1}}{2^{\lfloor k/2 \rfloor} (2k - 1)!}\) as \(n \to \infty\).

public theorem_wanted coloredArndtCount_isEquivalent (k : ℕ) (hk : 0 < k) :
    Asymptotics.IsEquivalent Filter.atTop (fun n => (coloredArndtCount n k : ℝ))
      fun n => (n : ℝ) ^ (2 * k - 1) / (2 ^ (k / 2) * (Nat.factorial (2 * k - 1) : ℝ))

Sources

• Mohammed L. Nadji, Moussa Ahmia, Daniel F. Checa, and José L. Ramírez, Arndt Compositions with Restricted Parts, Palindromes, and Colored Variants, Journal of Integer Sequences 28 (2025), Article 25.3.6, Corollary 20 (jis-2025-25.3.6-cor-20).

Uses 1

Statement usesColored Arndt compositions

DefinitionBivariate generating function of a two-index count#✓fully proved

For a function \(a\) assigning a natural number \(a(n, m)\) to every pair of natural numbers \(n, m\), its bivariate generating function is the power series \(\sum_{n \ge 0} \bigl(\sum_{m = 0}^{n} a(n, m)\, y^m\bigr) x^n\) in \(\mathbb{Z}[y][[x]]\), where \(x\) marks the first index (the weight) and \(y\) the second. Only the terms with \(m \le n\) enter; for counts with \(a(n, m) = 0\) whenever \(m > n\) it equals \(\sum_{n, m} a(n, m)\, x^n y^m\).

noncomputable def bivariateCountGF (a : ℕ → ℕ → ℕ) : PowerSeries (Polynomial ℤ) :=
  PowerSeries.mk fun n =>
    ∑ m ∈ Finset.range (n + 1), (a n m : Polynomial ℤ) * Polynomial.X ^ m

Sources

• Daniel F. Checa and José L. Ramírez, Arndt Compositions: A Generating Functions Approach, INTEGERS 24 (2024), Article A35, Section 2 (the series A(x, y), Ap(x, y), Bp(x, y), B(x, y), A_k(x, y) and A^{(k)}(x, y)).

Used by 8

Used byThe Arndt generating function as a bivariate count series · Generating function of anti-palindromic compositions · Generating function of Arndt compositions by last part · Generating function of block Arndt compositions · Generating function of \(k\)-Arndt compositions for negative \(k\) · Generating function of \(k\)-Arndt compositions for \(k \ge 0\) · Generating function of reduced anti-palindromic compositions · Coefficients of a bivariate generating function

TheoremCoefficients of a bivariate generating function#✓fully proved

For every function \(a\) assigning a natural number \(a(n, m)\) to each pair of natural numbers and every \(n \ge 0\), the coefficient of \(x^n\) in the bivariate generating function of \(a\) is the polynomial \(\sum_{m = 0}^{n} a(n, m)\, y^m \in \mathbb{Z}[y]\).

theorem coeff_bivariateCountGF (a : ℕ → ℕ → ℕ) (n : ℕ) :
    PowerSeries.coeff n (bivariateCountGF a) =
      ∑ m ∈ Finset.range (n + 1), (a n m : Polynomial ℤ) * Polynomial.X ^ m

Sources

• Daniel F. Checa and José L. Ramírez, Arndt Compositions: A Generating Functions Approach, INTEGERS 24 (2024), Article A35, Section 2.

Uses 1

Statement usesBivariate generating function of a two-index count

TheoremThe Arndt generating function as a bivariate count series#✓fully proved

For a set \(S\) of natural numbers, let \(a_S(n, m)\) be the number of Arndt compositions of \(n\) with \(m\) parts, all parts in \(S\). Then the Arndt generating function \(A_S(x, y)\) equals the bivariate generating function \(\sum_{n \ge 0} \sum_{m=0}^{n} a_S(n, m) x^n y^m\) in \(\mathbb{Z}[y][[x]]\).

theorem arndtGF_eq_bivariateCountGF (S : ℕ → Prop) [DecidablePred S] :
    arndtGF S = bivariateCountGF (arndtCompositionCount S)

Sources

• Daniel F. Checa and José L. Ramírez, Arndt Compositions: A Generating Functions Approach, INTEGERS 24 (2024), Article A35, Section 2 (definition of A(x, y)).

Uses 3

Statement usesNumber of Arndt compositions with parts in a set · Generating function of Arndt compositions with parts in a set · Bivariate generating function of a two-index count

DefinitionAnti-palindromic compositions#✓fully proved

For natural numbers \(n\) and \(m\), the number of anti-palindromic compositions of \(n\) with \(m\) parts: sequences \((c_1, \dots, c_m)\) of positive integers with \(c_1 + \dots + c_m = n\) and \(c_i \ne c_{m+1-i}\) for every \(i\) with \(2i \ne m + 1\). That is, each part differs from the part in the mirror position, except the middle part when \(m\) is odd.

def antiPalindromicCompositionCount (n m : ℕ) : ℕ :=
  ((Finset.Nat.antidiagonalTuple m n).filter fun c =>
    (∀ i, 0 < c i) ∧ ∀ i j : Fin m, (i : ℕ) + j + 1 = m → i ≠ j → c i ≠ c j).card

Sources

• Daniel F. Checa and José L. Ramírez, Arndt Compositions: A Generating Functions Approach, INTEGERS 24 (2024), Article A35, Section 2.1 (definition of anti-palindromic compositions, after Andrews, Just, and Simay).

Used by 3

Used byAnti-palindromic compositions of 6 with four parts · Anti-palindromic compositions of 6 with three parts · Generating function of anti-palindromic compositions

DefinitionReduced anti-palindromic compositions#✓fully proved

For natural numbers \(n\) and \(m\), this is the number of compositions \((\sigma_1, \ldots, \sigma_m)\) of \(n\) into \(m\) positive parts such that \(\sigma_i > \sigma_{m+1-i}\) for every \(i\) with \(2i < m + 1\).

A composition \((\sigma_1, \ldots, \sigma_m)\) is anti-palindromic when \(\sigma_i \ne \sigma_{m+1-i}\) for every \(i\) with \(2i \ne m + 1\). Two anti-palindromic compositions are equivalent when one arises from the other by swapping the entries \(\sigma_i\) and \(\sigma_{m+1-i}\) of some of the pairs; each class contains exactly one composition of the form above, so this is also the number of classes, the reduced anti-palindromic compositions of \(n\) with \(m\) parts.

def reducedAntiPalindromicCompositionCount (n m : ℕ) : ℕ :=
  ((Finset.Nat.antidiagonalTuple m n).filter fun c =>
    (∀ i, 0 < c i) ∧ ∀ i j : Fin m, (i : ℕ) + j + 1 = m → i < j → c j < c i).card

Sources

• Daniel F. Checa and José L. Ramírez, Arndt Compositions: A Generating Functions Approach, INTEGERS 24 (2024), Article A35, Section 2.1 (reduced anti-palindromic compositions and the choice of representative after Theorem 7).

Used by 4

Used byAnti-palindromic compositions of 6 with four parts · Generating function of reduced anti-palindromic compositions · Reduced anti-palindromic compositions of 6 with three parts · Arndt compositions and reduced anti-palindromic compositions are equinumerous

TheoremAnti-palindromic compositions of 6 with three parts#✓fully proved

There are exactly eight anti-palindromic compositions of \(6\) with three parts.

theorem antiPalindromicCompositionCount_six_three : antiPalindromicCompositionCount 6 3 = 8

Sources

• Daniel F. Checa and José L. Ramírez, Arndt Compositions: A Generating Functions Approach, INTEGERS 24 (2024), Article A35, Section 2.1 (each class has 2^{⌊ℓ/2⌋} members).

Uses 1

Statement usesAnti-palindromic compositions

TheoremReduced anti-palindromic compositions of 6 with three parts#✓fully proved

There are exactly four reduced anti-palindromic compositions of \(6\) with three parts.

theorem reducedAntiPalindromicCompositionCount_six_three :
    reducedAntiPalindromicCompositionCount 6 3 = 4

Sources

• Daniel F. Checa and José L. Ramírez, Arndt Compositions: A Generating Functions Approach, INTEGERS 24 (2024), Article A35, Section 2.1 (each class has 2^{⌊ℓ/2⌋} members).

Uses 1

Statement usesReduced anti-palindromic compositions

TheoremAnti-palindromic compositions of 6 with four parts#✓fully proved

There are exactly four anti-palindromic compositions of \(6\) with four parts, and exactly one reduced anti-palindromic composition of \(6\) with four parts.

theorem antiPalindromicCompositionCount_six_four :
    antiPalindromicCompositionCount 6 4 = 4 ∧ reducedAntiPalindromicCompositionCount 6 4 = 1

Sources

• Daniel F. Checa and José L. Ramírez, Arndt Compositions: A Generating Functions Approach, INTEGERS 24 (2024), Article A35, Section 2.1 (each class has 2^{⌊ℓ/2⌋} members).

Uses 2

Statement usesAnti-palindromic compositions · Reduced anti-palindromic compositions

DefinitionArndt compositions by last part#✓fully proved

An Arndt composition of \(n\) is a composition \((\sigma_1, \ldots, \sigma_\ell)\) of \(n\) into positive parts such that \(\sigma_{2i-1} > \sigma_{2i}\) for every \(i\) with \(2i \le \ell\). For natural numbers \(n\) and \(j\), \(b(n, j)\) is the number of Arndt compositions of \(n\), with any number of parts, whose last part is \(j\). The empty composition of \(0\) counts as having last part \(0\), so \(b(0, 0) = 1\) and \(b(0, j) = 0\) for \(j \ge 1\).

def arndtLastPartCount (n j : ℕ) : ℕ :=
  if n = 0 then (if j = 0 then 1 else 0) else
    ∑ m ∈ Finset.range n,
      ((Finset.Nat.antidiagonalTuple (m + 1) n).filter fun c =>
        (∀ i, 0 < c i) ∧
          (∀ i i' : Fin (m + 1), (i : ℕ) % 2 = 0 → (i' : ℕ) = i + 1 → c i' < c i) ∧
            c (Fin.last m) = j).card

Sources

• Daniel F. Checa and José L. Ramírez, Arndt Compositions: A Generating Functions Approach, INTEGERS 24 (2024), Article A35, Section 3 (definition of b(n, m) and Table 2).

Used by 5

Used byArndt compositions with last part at most or at least \(k\) · Closed formula for Arndt compositions by last part · Asymptotics of Arndt compositions with a fixed last part · Arndt compositions of 6 by last part · Generating function of Arndt compositions by last part

TheoremArndt compositions of 6 by last part#✓fully proved

Let \(b(n, j)\) be the number of Arndt compositions of \(n\) with last part \(j\). Then \(b(6, 1) = 4\), \(b(6, 2) = 2\), \(b(6, 3) = 1\) and \(b(6, 6) = 1\).

theorem arndtLastPartCount_six :
    arndtLastPartCount 6 1 = 4 ∧ arndtLastPartCount 6 2 = 2 ∧ arndtLastPartCount 6 3 = 1 ∧
      arndtLastPartCount 6 6 = 1

Sources

• Daniel F. Checa and José L. Ramírez, Arndt Compositions: A Generating Functions Approach, INTEGERS 24 (2024), Article A35, Section 3, Table 2.

Uses 1

Statement usesArndt compositions by last part

DefinitionNumber of \(k\)-Arndt compositions#✓fully proved

For an integer \(k\) and \(n, m \ge 0\), \(a_k(n, m)\) is the number of \(k\)-Arndt compositions of \(n\) with \(m\) parts: sequences \((c_0, \ldots, c_{m-1})\) of positive integers with \(c_0 + \cdots + c_{m-1} = n\) such that \(c_{2i} > c_{2i+1} + k\) for every \(i \ge 0\) with \(2i + 1 < m\). For \(k = 0\) these are the Arndt compositions.

def kArndtCompositionCount (k : ℤ) (n m : ℕ) : ℕ :=
  ((Finset.Nat.antidiagonalTuple m n).filter fun c =>
    (∀ i, 0 < c i) ∧
      ∀ i j : Fin m, (i : ℕ) % 2 = 0 → (j : ℕ) = i + 1 → (c j : ℤ) + k < c i).card

Sources

• Daniel F. Checa and José L. Ramírez, Arndt Compositions: A Generating Functions Approach, INTEGERS 24 (2024), Article A35, Section 4 (definition of k-Arndt compositions, after Hopkins and Tangboonduangjit; Theorem 11 treats k ≥ 0 and k < 0).

Used by 6

Used byGenerating function of \(k\)-Arndt compositions for negative \(k\) · Generating function of \(k\)-Arndt compositions for \(k \ge 0\) · Sample values of the \(k\)-Arndt composition counts · Counting \(k\)-Arndt compositions for negative \(k\) · Counting \(k\)-Arndt compositions for nonnegative \(k\) · Generalized Arndt compositions

TheoremSample values of the \(k\)-Arndt composition counts#✓fully proved

Writing \(a_k(n, m)\) for the number of \(k\)-Arndt compositions of \(n\) with \(m\) parts, \(a_3(7, 2) = 1\), \(a_3(7, 3) = 1\) and \(a_{-3}(4, 2) = 3\).

theorem kArndtCompositionCount_examples :
    kArndtCompositionCount 3 7 2 = 1 ∧ kArndtCompositionCount 3 7 3 = 1 ∧
      kArndtCompositionCount (-3) 4 2 = 3

Sources

• Daniel F. Checa and José L. Ramírez, Arndt Compositions: A Generating Functions Approach, INTEGERS 24 (2024), Article A35, Section 4 (series expansions after Theorem 11).

Uses 1

Statement usesNumber of \(k\)-Arndt compositions

DefinitionNumber of \(k\)-block Arndt compositions#✓fully proved

For \(k \ge 1\) and \(n, m \ge 0\), \(a^{(k)}(n, m)\) is the number of \(k\)-block Arndt compositions of \(n\) with \(m\) parts: sequences \((c_0, \ldots, c_{m-1})\) of positive integers with \(c_0 + \cdots + c_{m-1} = n\) that strictly decrease inside each block of \(k\) consecutive positions \(ki, ki + 1, \ldots, ki + k - 1\) (the last block may be shorter), that is, \(c_i > c_{i+1}\) for every \(i\) with \(i + 1 < m\) and \(i \not\equiv k - 1 \pmod{k}\). For \(k = 2\) these are the Arndt compositions.

The definition is meant for \(k \ge 1\); its value at \(k = 0\) has no combinatorial meaning.

def blockArndtCompositionCount (k n m : ℕ) : ℕ :=
  ((Finset.Nat.antidiagonalTuple m n).filter fun c =>
    (∀ i, 0 < c i) ∧
      ∀ i j : Fin m, (i : ℕ) % k ≠ k - 1 → (j : ℕ) = i + 1 → c j < c i).card

Sources

• Daniel F. Checa and José L. Ramírez, Arndt Compositions: A Generating Functions Approach, INTEGERS 24 (2024), Article A35, Section 5 (definition of k-block Arndt compositions).

Used by 2

Used byGenerating function of block Arndt compositions · Four-part 3-block Arndt compositions of 10

TheoremFour-part 3-block Arndt compositions of 10#✓fully proved

There are exactly \(7\) three-block Arndt compositions of \(10\) with \(4\) parts, that is, \(a^{(3)}(10, 4) = 7\).

They are \((6,2,1,1)\), \((5,3,1,1)\), \((5,2,1,2)\), \((4,3,2,1)\), \((4,3,1,2)\), \((4,2,1,3)\) and \((3,2,1,4)\).

theorem blockArndtCompositionCount_three_ten_four : blockArndtCompositionCount 3 10 4 = 7

Sources

• Daniel F. Checa and José L. Ramírez, Arndt Compositions: A Generating Functions Approach, INTEGERS 24 (2024), Article A35, Section 5 (list of the compositions counted by a^{(3)}(10) = 18).

Uses 1

Statement usesNumber of \(k\)-block Arndt compositions

TheoremAlternating sum and recurrence for Arndt compositions#●ready to prove

Let \(a(n, m)\) be the number of Arndt compositions of \(n\) with \(m\) parts, and write \(K = n - m - \lfloor m/2 \rfloor\). For all \(n, m \ge 0\): if \(m + \lfloor m/2 \rfloor \le n\), then

\[a(n, m) = \sum_{\ell=0}^{K} \binom{m+\ell-1}{\ell} \binom{n-m-\ell-1}{K-\ell} (-1)^{K-\ell},\]

and otherwise \(a(n, m) = 0\). Moreover, for all \(n \ge 3\) and \(m \ge 2\), \(a(n, m) = a(n-1, m) + a(n-2, m) - a(n-3, m) + a(n-3, m-2)\). The binomial coefficients are the generalized ones, \(\binom{r}{k} = r(r-1)\cdots(r-k+1)/k!\) for an integer \(r\), so the upper index \(-1\) is allowed and \(\binom{-1}{k} = (-1)^k\).

public theorem_wanted arndtCompositionCount_eq_alternating_sum_and_recurrence :
    (∀ n m : ℕ, (arndtCompositionCount (fun _ => True) n m : ℤ) =
      if m + m / 2 ≤ n then
        ∑ ℓ ∈ Finset.range (n - m - m / 2 + 1),
          Ring.choose ((m : ℤ) + ℓ - 1) ℓ * Ring.choose ((n : ℤ) - m - ℓ - 1) (n - m - m / 2 - ℓ) *
            (-1) ^ (n - m - m / 2 - ℓ)
      else 0) ∧
    ∀ n m : ℕ, 3 ≤ n → 2 ≤ m →
      (arndtCompositionCount (fun _ => True) n m : ℤ) =
        arndtCompositionCount (fun _ => True) (n - 1) m +
          arndtCompositionCount (fun _ => True) (n - 2) m -
            arndtCompositionCount (fun _ => True) (n - 3) m +
              arndtCompositionCount (fun _ => True) (n - 3) (m - 2)

Sources

• Daniel F. Checa and José L. Ramírez, Arndt Compositions: A Generating Functions Approach, INTEGERS 24 (2024), Article A35, Theorem 2.

Uses 1

Statement usesNumber of Arndt compositions with parts in a set

TheoremPositive sum for Arndt compositions#●ready to prove

Let \(a(n, m)\) be the number of Arndt compositions of \(n\) with \(m\) parts, and write \(h = \lfloor m/2 \rfloor\). For all \(n \ge 0\) and \(m \ge 1\): if \(m + h \le n\), then

\[a(n, m) = \sum_{\ell=0}^{\lfloor (n-m-h)/2 \rfloor} \binom{h+\ell-1}{\ell} \binom{n-2h-2\ell-1}{\lfloor (m-1)/2 \rfloor},\]

and otherwise \(a(n, m) = 0\). Here \(\binom{-1}{0} = 1\) (this term occurs for \(m = 1\)).

The paper states it for all \(n, m \ge 0\); at \(n = m = 0\) it fails (\(a(0, 0) = 1\), while the only term has lower index \(\lfloor -1/2 \rfloor = -1\) and vanishes), so the case \(m = 0\) is omitted.

public theorem_wanted arndtCompositionCount_eq_positive_sum (n m : ℕ) (hm : 0 < m) :
    (arndtCompositionCount (fun _ => True) n m : ℤ) =
      if m + m / 2 ≤ n then
        ∑ ℓ ∈ Finset.range ((n - m - m / 2) / 2 + 1),
          Ring.choose (((m / 2 : ℕ) : ℤ) + ℓ - 1) ℓ *
            Ring.choose ((n : ℤ) - 2 * (m / 2 : ℕ) - 2 * ℓ - 1) ((m - 1) / 2)
      else 0

Sources

• Daniel F. Checa and José L. Ramírez, Arndt Compositions: A Generating Functions Approach, INTEGERS 24 (2024), Article A35, Theorem 3.

Uses 1

Statement usesNumber of Arndt compositions with parts in a set

TheoremHolonomic recurrence for Arndt compositions#●ready to prove

Let \(a(n, m)\) be the number of Arndt compositions of \(n\) with \(m\) parts. For all \(n, m \ge 0\),

\[(m - n - 2 + \lfloor m/2 \rfloor)\, a(n+2, m) + (m - \lfloor m/2 \rfloor)\, a(n+1, m) + n\, a(n, m) = 0.\]

public theorem_wanted arndtCompositionCount_holonomic_recurrence (n m : ℕ) :
    ((m : ℤ) - n - 2 + (m / 2 : ℕ)) * arndtCompositionCount (fun _ => True) (n + 2) m +
        ((m : ℤ) - (m / 2 : ℕ)) * arndtCompositionCount (fun _ => True) (n + 1) m +
          (n : ℤ) * arndtCompositionCount (fun _ => True) n m = 0

Sources

• Daniel F. Checa and José L. Ramírez, Arndt Compositions: A Generating Functions Approach, INTEGERS 24 (2024), Article A35, Theorem 4.

Uses 1

Statement usesNumber of Arndt compositions with parts in a set

TheoremAsymptotics of Arndt compositions with a fixed number of parts#●ready to prove

Let \(a(n, m)\) be the number of Arndt compositions of \(n\) with \(m\) parts. For every fixed integer \(m \ge 1\),

\[a(n, m) \sim \frac{n^{m-1}}{2^{\lfloor m/2 \rfloor} (m-1)!} \quad (n \to \infty).\]

public theorem_wanted arndtCompositionCount_isEquivalent (m : ℕ) (hm : 0 < m) :
    Asymptotics.IsEquivalent Filter.atTop
      (fun n : ℕ => (arndtCompositionCount (fun _ => True) n m : ℝ))
      (fun n : ℕ => (n : ℝ) ^ (m - 1) / (2 ^ (m / 2) * (Nat.factorial (m - 1) : ℝ)))

Sources

• Daniel F. Checa and José L. Ramírez, Arndt Compositions: A Generating Functions Approach, INTEGERS 24 (2024), Article A35, Corollary 1.

Uses 1

Statement usesNumber of Arndt compositions with parts in a set

TheoremArndt compositions are counted by Fibonacci numbers#●ready to prove

Let \(a(n, m)\) be the number of Arndt compositions of \(n\) with \(m\) parts, let \(a(n) = \sum_{m=0}^{n} a(n, m)\) be the number of all Arndt compositions of \(n\), and let \(F_n\) be the \(n\)-th Fibonacci number (\(F_0 = 0\), \(F_1 = 1\)). Then, in \(\mathbb{Z}[[x]]\),

\[\Big(\sum_{n \ge 0} a(n) x^n\Big)(1 - x - x^2) = 1 - x^2,\]

and \(a(n) = F_n\) for every \(n \ge 1\).

public theorem_wanted arndtComposition_total_eq_fib :
    (PowerSeries.mk fun n =>
        ((∑ m ∈ Finset.range (n + 1), arndtCompositionCount (fun _ => True) n m : ℕ) : ℤ)) *
        (1 - PowerSeries.X - PowerSeries.X ^ 2) = 1 - PowerSeries.X ^ 2 ∧
      ∀ n : ℕ, 1 ≤ n →
        ∑ m ∈ Finset.range (n + 1), arndtCompositionCount (fun _ => True) n m = Nat.fib n

Sources

• Daniel F. Checa and José L. Ramírez, Arndt Compositions: A Generating Functions Approach, INTEGERS 24 (2024), Article A35, Corollary 2.

Uses 1

Statement usesNumber of Arndt compositions with parts in a set

TheoremExpected number of parts of an Arndt composition#●ready to prove

Let \(a(n, m)\) be the number of Arndt compositions of \(n\) with \(m\) parts, and \(F_n\) the \(n\)-th Fibonacci number (\(F_0 = 0\), \(F_1 = 1\)). Then

\[\frac{1}{F_n} \sum_{m=0}^{n} m\, a(n, m) \sim \left(\frac{3}{\sqrt 5} - 1\right) n \quad (n \to \infty).\]

Since there are \(F_n\) Arndt compositions of \(n\) for \(n \ge 1\), the left side is the expected number of parts of a uniformly random Arndt composition of \(n\).

public theorem_wanted arndtComposition_expected_parts_isEquivalent :
    Asymptotics.IsEquivalent Filter.atTop
      (fun n : ℕ =>
        (∑ m ∈ Finset.range (n + 1), (m * arndtCompositionCount (fun _ => True) n m : ℝ)) /
          (Nat.fib n : ℝ))
      (fun n : ℕ => (3 / Real.sqrt 5 - 1) * n)

Sources

• Daniel F. Checa and José L. Ramírez, Arndt Compositions: A Generating Functions Approach, INTEGERS 24 (2024), Article A35, Theorem 5.

Uses 1

Statement usesNumber of Arndt compositions with parts in a set

TheoremGenerating function of anti-palindromic compositions#●ready to prove

Let \(ap(n, m)\) be the number of anti-palindromic compositions of \(n\) with \(m\) parts, and let \(Ap(x, y) = \sum_{n \ge 0} \sum_{m=0}^{n} ap(n, m)\, x^n y^m \in \mathbb{Z}[y][[x]]\). Then \(Ap(x, y)\,(1 - x - x^2 + x^3 - 2x^3y^2) = 1 - x - x^2 + x^3 + xy - x^3y\), that is, \(Ap(x, y) = (1 - x - x^2 + x^3 + xy - x^3y)/(1 - x - x^2 + x^3 - 2x^3y^2)\).

public theorem_wanted bivariateCountGF_antiPalindromic :
    bivariateCountGF antiPalindromicCompositionCount *
        (1 - PowerSeries.X - PowerSeries.X ^ 2 + PowerSeries.X ^ 3 -
          PowerSeries.C (2 * Polynomial.X ^ 2) * PowerSeries.X ^ 3) =
      1 - PowerSeries.X - PowerSeries.X ^ 2 + PowerSeries.X ^ 3 +
        PowerSeries.C Polynomial.X * PowerSeries.X -
          PowerSeries.C Polynomial.X * PowerSeries.X ^ 3

Sources

• Daniel F. Checa and José L. Ramírez, Arndt Compositions: A Generating Functions Approach, INTEGERS 24 (2024), Article A35, Theorem 6.

Uses 2

Statement usesAnti-palindromic compositions · Bivariate generating function of a two-index count

TheoremGenerating function of reduced anti-palindromic compositions#●ready to prove

Let \(b(n, m)\) be the number of reduced anti-palindromic compositions of \(n\) with \(m\) parts, and let \(B_p(x, y) = \sum_{n \ge 0} \sum_{m = 0}^{n} b(n, m)\, x^n y^m\) in \(\mathbb{Z}[y][[x]]\), where \(x\) marks the weight and \(y\) the number of parts. Then

\[B_p(x, y)\,(1 - x - x^2 + x^3 - x^3 y^2) = 1 - x - x^2 + x^3 + xy - x^3 y,\]

that is, \(B_p(x, y) = (1 - x - x^2 + x^3 + xy - x^3 y)/(1 - x - x^2 + x^3 - x^3 y^2)\).

public theorem_wanted bivariateCountGF_reducedAntiPalindromic :
    bivariateCountGF reducedAntiPalindromicCompositionCount *
        (1 - PowerSeries.X - PowerSeries.X ^ 2 + PowerSeries.X ^ 3 -
          PowerSeries.C (Polynomial.X ^ 2) * PowerSeries.X ^ 3) =
      1 - PowerSeries.X - PowerSeries.X ^ 2 + PowerSeries.X ^ 3 +
        PowerSeries.C Polynomial.X * PowerSeries.X -
          PowerSeries.C Polynomial.X * PowerSeries.X ^ 3

Sources

• Daniel F. Checa and José L. Ramírez, Arndt Compositions: A Generating Functions Approach, INTEGERS 24 (2024), Article A35, Corollary 3.

Uses 2

Statement usesBivariate generating function of a two-index count · Reduced anti-palindromic compositions

TheoremArndt compositions and reduced anti-palindromic compositions are equinumerous#●ready to prove

For all natural numbers \(n\) and \(m\), the number of reduced anti-palindromic compositions of \(n\) with \(m\) parts equals the number of Arndt compositions of \(n\) with \(m\) parts, all positive integers being allowed as parts.

public theorem_wanted reducedAntiPalindromicCompositionCount_eq_arndtCompositionCount (n m : ℕ) :
    reducedAntiPalindromicCompositionCount n m = arndtCompositionCount (fun _ => True) n m

Sources

• Daniel F. Checa and José L. Ramírez, Arndt Compositions: A Generating Functions Approach, INTEGERS 24 (2024), Article A35, Theorem 7.

Uses 2

Statement usesNumber of Arndt compositions with parts in a set · Reduced anti-palindromic compositions

TheoremGenerating function of Arndt compositions by last part#●ready to prove

Let \(b(n, m)\) be the number of Arndt compositions of \(n\) with last part \(m\), where the empty composition of \(0\) counts as having last part \(0\) (so \(b(0, 0) = 1\)), and let \(B(x, y) = \sum_{n \ge 0} \sum_{m=0}^{n} b(n, m)\, x^n y^m \in \mathbb{Z}[y][[x]]\). Then \(B(x, y)\,(1 - x - x^2)(1 - xy)(1 - x^2y) = 1 - x - x^2 - x^2y + 2x^3y + 2x^4y - x^5y - x^4y^2\).

public theorem_wanted bivariateCountGF_arndtLastPart :
    bivariateCountGF arndtLastPartCount *
        ((1 - PowerSeries.X - PowerSeries.X ^ 2) *
          (1 - PowerSeries.C Polynomial.X * PowerSeries.X) *
            (1 - PowerSeries.C Polynomial.X * PowerSeries.X ^ 2)) =
      1 - PowerSeries.X - PowerSeries.X ^ 2 - PowerSeries.C Polynomial.X * PowerSeries.X ^ 2 +
        PowerSeries.C (2 * Polynomial.X) * PowerSeries.X ^ 3 +
          PowerSeries.C (2 * Polynomial.X) * PowerSeries.X ^ 4 -
            PowerSeries.C Polynomial.X * PowerSeries.X ^ 5 -
              PowerSeries.C (Polynomial.X ^ 2) * PowerSeries.X ^ 4

Sources

• Daniel F. Checa and José L. Ramírez, Arndt Compositions: A Generating Functions Approach, INTEGERS 24 (2024), Article A35, Theorem 8.

Uses 2

Statement usesArndt compositions by last part · Bivariate generating function of a two-index count

TheoremClosed formula for Arndt compositions by last part#●ready to prove

Let \(F_r\) be the \(r\)-th Fibonacci number (\(F_0 = 0\), \(F_1 = 1\)) and \(b(n, m)\) the number of Arndt compositions of \(n\) with last part \(m\). Define \(t_1, t_2 : \mathbb{N} \to \mathbb{N}\) by \(t_1(0) = 1\), \(t_1(1) = 0\), \(t_1(r) = F_{r-2}\) and \(t_2(0) = 0\), \(t_2(1) = 1\), \(t_2(r) = F_{r-1}\) for \(r \ge 2\). Then for all integers \(n \ge 1\) and \(m \ge 1\): \(b(n, m) = 0\) if \(n < m\), \(b(n, m) = t_1(n - m)\) if \(m \le n < 2m\), and \(b(n, m) = t_1(n - m) + t_2(n - 2m)\) if \(n \ge 2m\).

The paper leaves the range of \(m\) implicit; at \(m = 0\) the printed formula fails (\(b(1, 0) = 0\), while the formula gives \(t_1(1) + t_2(1) = 1\)), so \(m \ge 1\) is assumed.

public theorem_wanted arndtLastPartCount_eq (n m : ℕ) (hn : 1 ≤ n) (hm : 1 ≤ m) :
    let t₁ : ℕ → ℕ := fun r => if r = 0 then 1 else if r = 1 then 0 else Nat.fib (r - 2)
    let t₂ : ℕ → ℕ := fun r => if r = 0 then 0 else if r = 1 then 1 else Nat.fib (r - 1)
    arndtLastPartCount n m =
      if n < m then 0 else if n < 2 * m then t₁ (n - m) else t₁ (n - m) + t₂ (n - 2 * m)

Sources

• Daniel F. Checa and José L. Ramírez, Arndt Compositions: A Generating Functions Approach, INTEGERS 24 (2024), Article A35, Theorem 9.

Uses 1

Statement usesArndt compositions by last part

TheoremAsymptotics of Arndt compositions with a fixed last part#●ready to prove

Let \(b(n, m)\) be the number of Arndt compositions of \(n\) with last part \(m\), and let \(\varphi\) be the golden ratio. For every fixed integer \(m \ge 1\), \(b(n, m) \sim \frac{\varphi^{n-m-2}}{\sqrt{5}} \left(1 + \frac{1}{\varphi^{m-1}}\right)\) as \(n \to \infty\).

public theorem_wanted arndtLastPartCount_isEquivalent (m : ℕ) (hm : 0 < m) :
    Asymptotics.IsEquivalent Filter.atTop (fun n : ℕ => (arndtLastPartCount n m : ℝ))
      (fun n : ℕ => Real.goldenRatio ^ ((n : ℤ) - m - 2) / Real.sqrt 5 *
        (1 + 1 / Real.goldenRatio ^ ((m : ℤ) - 1)))

Sources

• Daniel F. Checa and José L. Ramírez, Arndt Compositions: A Generating Functions Approach, INTEGERS 24 (2024), Article A35, Theorem 10.

Uses 1

Statement usesArndt compositions by last part

TheoremArndt compositions with last part at most or at least \(k\)#●ready to prove

Let \(F_n\) be the \(n\)-th Fibonacci number (\(F_0 = 0\), \(F_1 = 1\)) and \(b(n, j)\) the number of Arndt compositions of \(n\) with last part \(j\). For all integers \(k \ge 1\) and \(n \ge 2k + 2\), the number of Arndt compositions of \(n\) with last part at most \(k\) is \(\sum_{j=1}^{k} b(n, j) = F_n - F_{n-k-1} - F_{n-2k-2}\), and the number with last part at least \(k\) is \(\sum_{j=k}^{n} b(n, j) = F_{n-k} + F_{n-2k}\).

The paper prints the second count as \(F_{n-k} - F_{n-2k}\), which is false: for \(k = 1\) and \(n = 4\) all \(F_4 = 3\) Arndt compositions of \(4\) have last part at least \(1\), while \(F_3 - F_2 = 1\). The sign \(+\) is the one the paper's own consequence uses (\(F_{n-2} + F_{n-4}\) compositions with last part greater than \(1\)), and it is what subtracting the number with last part at most \(k - 1\) from \(F_n\) gives.

public theorem_wanted arndtLastPart_atMost_atLeast (k n : ℕ) (hk : 1 ≤ k) (hn : 2 * k + 2 ≤ n) :
    ((∑ j ∈ Finset.Icc 1 k, arndtLastPartCount n j : ℕ) : ℤ) =
        Nat.fib n - Nat.fib (n - k - 1) - Nat.fib (n - 2 * k - 2) ∧
      ∑ j ∈ Finset.Icc k n, arndtLastPartCount n j = Nat.fib (n - k) + Nat.fib (n - 2 * k)

Sources

• Daniel F. Checa and José L. Ramírez, Arndt Compositions: A Generating Functions Approach, INTEGERS 24 (2024), Article A35, Corollary 4.

Uses 1

Statement usesArndt compositions by last part

TheoremGenerating function of \(k\)-Arndt compositions for \(k \ge 0\)#●ready to prove

Let \(k \ge 0\) be an integer, let \(a_k(n, m)\) be the number of \(k\)-Arndt compositions of \(n\) with \(m\) parts, and let \(A_k(x, y) = \sum_{n \ge 0} \sum_{m=0}^{n} a_k(n, m)\, x^n y^m \in \mathbb{Z}[y][[x]]\). Then \(A_k(x, y)\,(1 - x - x^2 + x^3 - x^{3+k}y^2) = (1 - x^2)(1 - x(1 - y))\), that is, \(A_k(x, y) = (1 - x^2)(1 - x(1 - y))/(1 - x - x^2 + x^3 - x^{3+k}y^2)\).

public theorem_wanted bivariateCountGF_kArndt_nonneg (k : ℕ) :
    bivariateCountGF (kArndtCompositionCount k) *
        (1 - PowerSeries.X - PowerSeries.X ^ 2 + PowerSeries.X ^ 3 -
          PowerSeries.C (Polynomial.X ^ 2) * PowerSeries.X ^ (3 + k)) =
      (1 - PowerSeries.X ^ 2) * (1 - PowerSeries.X + PowerSeries.C Polynomial.X * PowerSeries.X)

Sources

• Daniel F. Checa and José L. Ramírez, Arndt Compositions: A Generating Functions Approach, INTEGERS 24 (2024), Article A35, Theorem 11, case k ≥ 0.

Uses 2

Statement usesBivariate generating function of a two-index count · Number of \(k\)-Arndt compositions

TheoremGenerating function of \(k\)-Arndt compositions for negative \(k\)#●ready to prove

Let \(k' \ge 1\) and \(k = -k'\), let \(a_k(n, m)\) be the number of \(k\)-Arndt compositions of \(n\) with \(m\) parts, and let \(A_k(x, y) = \sum_{n \ge 0} \sum_{m=0}^{n} a_k(n, m)\, x^n y^m \in \mathbb{Z}[y][[x]]\). Then \(A_k(x, y)\,(1 - x - x^2(1 + y^2) + x^3(1 - y^2) + y^2x^{2+k'}) = (1 - x^2)(1 - x(1 - y))\), that is, \(A_k(x, y) = (1 - x^2)(1 - x(1 - y))/(1 - x - x^2(1 + y^2) + x^3(1 - y^2) + y^2x^{2-k})\).

public theorem_wanted bivariateCountGF_kArndt_neg (k' : ℕ) (hk' : 0 < k') :
    bivariateCountGF (kArndtCompositionCount (-(k' : ℤ))) *
        (1 - PowerSeries.X - PowerSeries.C (1 + Polynomial.X ^ 2) * PowerSeries.X ^ 2 +
          PowerSeries.C (1 - Polynomial.X ^ 2) * PowerSeries.X ^ 3 +
            PowerSeries.C (Polynomial.X ^ 2) * PowerSeries.X ^ (2 + k')) =
      (1 - PowerSeries.X ^ 2) * (1 - PowerSeries.X + PowerSeries.C Polynomial.X * PowerSeries.X)

Sources

• Daniel F. Checa and José L. Ramírez, Arndt Compositions: A Generating Functions Approach, INTEGERS 24 (2024), Article A35, Theorem 11, case k < 0.

Uses 2

Statement usesBivariate generating function of a two-index count · Number of \(k\)-Arndt compositions

TheoremCounting \(k\)-Arndt compositions for nonnegative \(k\)#●ready to prove

Let \(k \ge 0\) be an integer and let \(a_k(n) = \sum_{m = 0}^{n} a_k(n, m)\) be the number of \(k\)-Arndt compositions of \(n\). Then, in \(\mathbb{Z}[[x]]\),

\[\Bigl(\sum_{n \ge 0} a_k(n)\, x^n\Bigr)(1 - x - x^2 + x^3 - x^{k+3}) = 1 - x^2,\]

that is, \(\sum_{n \ge 0} a_k(n)\, x^n = (1 - x^2)/(1 - x - x^2 + x^3 - x^{k+3})\).

public theorem_wanted kArndtComposition_total_gf_nonneg (k : ℕ) :
    (PowerSeries.mk fun n =>
        ((∑ m ∈ Finset.range (n + 1), kArndtCompositionCount k n m : ℕ) : ℤ)) *
        (1 - PowerSeries.X - PowerSeries.X ^ 2 + PowerSeries.X ^ 3 - PowerSeries.X ^ (k + 3)) =
      1 - PowerSeries.X ^ 2

Sources

• Daniel F. Checa and José L. Ramírez, Arndt Compositions: A Generating Functions Approach, INTEGERS 24 (2024), Article A35, Corollary 6, case k ≥ 0.

Uses 1

Statement usesNumber of \(k\)-Arndt compositions

TheoremCounting \(k\)-Arndt compositions for negative \(k\)#●ready to prove

Let \(k = -k'\) with \(k' \ge 1\) an integer, and let \(a_k(n) = \sum_{m = 0}^{n} a_k(n, m)\) be the number of \(k\)-Arndt compositions of \(n\). Then, in \(\mathbb{Z}[[x]]\),

\[\Bigl(\sum_{n \ge 0} a_k(n)\, x^n\Bigr)(1 - x - 2x^2 + x^{2-k}) = 1 - x^2,\]

that is, \(\sum_{n \ge 0} a_k(n)\, x^n = (1 - x^2)/(1 - x - 2x^2 + x^{2-k})\).

public theorem_wanted kArndtComposition_total_gf_neg (k' : ℕ) (hk' : 0 < k') :
    (PowerSeries.mk fun n =>
        ((∑ m ∈ Finset.range (n + 1), kArndtCompositionCount (-(k' : ℤ)) n m : ℕ) : ℤ)) *
        (1 - PowerSeries.X - 2 * PowerSeries.X ^ 2 + PowerSeries.X ^ (2 + k')) =
      1 - PowerSeries.X ^ 2

Sources

• Daniel F. Checa and José L. Ramírez, Arndt Compositions: A Generating Functions Approach, INTEGERS 24 (2024), Article A35, Corollary 6, case k < 0.

Uses 1

Statement usesNumber of \(k\)-Arndt compositions

TheoremGenerating function of block Arndt compositions#●ready to prove

Let \(k \ge 1\), let \(a^{(k)}(n, m)\) be the number of \(k\)-block Arndt compositions of \(n\) with \(m\) parts, and let \(A^{(k)}(x, y) = \sum_{n \ge 0} \sum_{m=0}^{n} a^{(k)}(n, m)\, x^n y^m \in \mathbb{Z}[y][[x]]\). Then \(A^{(k)}(x, y) \bigl(\prod_{\ell=1}^{k} (1 - x^\ell) - x^{\binom{k+1}{2}} y^k\bigr) = \sum_{j=0}^{k-1} x^{\binom{j+1}{2}} y^j \prod_{\ell=j+1}^{k} (1 - x^\ell)\). Equivalently, with \(J_j(x, y) = x^{\binom{j+1}{2}} y^j \prod_{\ell=1}^{j} (1 - x^\ell)^{-1}\), \(A^{(k)}(x, y) = \bigl(\sum_{j=0}^{k-1} J_j(x, y)\bigr) / (1 - J_k(x, y))\).

public theorem_wanted bivariateCountGF_blockArndt (k : ℕ) (hk : 1 ≤ k) :
    bivariateCountGF (blockArndtCompositionCount k) *
        ((∏ ℓ ∈ Finset.Icc 1 k, (1 - PowerSeries.X ^ ℓ)) -
          PowerSeries.C (Polynomial.X ^ k) * PowerSeries.X ^ Nat.choose (k + 1) 2) =
      ∑ j ∈ Finset.range k,
        PowerSeries.C (Polynomial.X ^ j) * PowerSeries.X ^ Nat.choose (j + 1) 2 *
          ∏ ℓ ∈ Finset.Ioc j k, (1 - PowerSeries.X ^ ℓ)

Sources

• Daniel F. Checa and José L. Ramírez, Arndt Compositions: A Generating Functions Approach, INTEGERS 24 (2024), Article A35, Theorem 12.

Uses 2

Statement usesBivariate generating function of a two-index count · Number of \(k\)-block Arndt compositions

DefinitionGeneralized Arndt compositions#✓fully proved

For an integer \(k\) and a natural number \(n\), \(a(n, k)\) is the number of compositions \((c_1, \dots, c_m)\) of \(n\), with any number \(m \ge 0\) of parts, such that \(c_{2i-1} > c_{2i} + k\) for every \(i\) with \(2i \le m\); a final unpaired part is unconstrained. The empty composition gives \(a(0, k) = 1\), and \(k = 0\) gives Arndt compositions.

def kArndtTotalCount (k : ℤ) (n : ℕ) : ℕ :=
  ∑ m ∈ Finset.range (n + 1), kArndtCompositionCount k n m

Sources

• Brian Hopkins and Aram Tangboonduangjit, Arndt and De Morgan Compositions, INTEGERS 26 (2026), Article A64, Definition 4.

Uses 1 · Used by 5

Statement usesNumber of \(k\)-Arndt compositions

Used byGeneralized Arndt counts for compositions of five · Generalized Arndt compositions with negative even shift · Generalized Arndt compositions with negative odd shift · Recurrences for generalized Arndt counts · Arndt compositions and compositions into odd parts are equinumerous

TheoremGeneralized Arndt counts for compositions of five#✓fully proved

The numbers \(a(5, k)\) of generalized Arndt compositions of \(5\) (compositions \((c_1, \dots, c_m)\) of \(5\) with \(c_{2i-1} > c_{2i} + k\) whenever \(2i \le m\)) are \(a(5, 0) = 5\), \(a(5, -1) = 10\), \(a(5, -2) = 14\) and \(a(5, 1) = 3\).

theorem kArndtTotalCount_five :
    kArndtTotalCount 0 5 = 5 ∧ kArndtTotalCount (-1) 5 = 10 ∧ kArndtTotalCount (-2) 5 = 14 ∧
      kArndtTotalCount 1 5 = 3

Sources

• Brian Hopkins and Aram Tangboonduangjit, Arndt and De Morgan Compositions, INTEGERS 26 (2026), Article A64, Table 9.

Uses 1

Statement usesGeneralized Arndt compositions

DefinitionCompositions into odd or small even parts#✓fully proved

For natural numbers \(k\) and \(n\), \(c^{2k}_o(n)\) is the number of compositions of \(n\), with any number of parts, in which every part is odd or at most \(2k\). For \(k = 0\) these are De Morgan's compositions of \(n\) into odd parts.

def oddOrSmallEvenCompositionCount (k n : ℕ) : ℕ :=
  ∑ m ∈ Finset.range (n + 1), ((Finset.Nat.antidiagonalTuple m n).filter fun c =>
    ∀ i, 0 < c i ∧ (Odd (c i) ∨ c i ≤ 2 * k)).card

Sources

• Brian Hopkins and Aram Tangboonduangjit, Arndt and De Morgan Compositions, INTEGERS 26 (2026), Article A64, Definitions 2 and 5.

Used by 4

Used byRecurrences for even-or-small-odd and odd-or-small-even compositions · Generalized Arndt compositions with negative even shift · Arndt compositions and compositions into odd parts are equinumerous · Compositions of five into odd or small even parts

TheoremCompositions of five into odd or small even parts#✓fully proved

Let \(c^{2k}_o(n)\) be the number of compositions of \(n\) in which every part is odd or at most \(2k\). Then \(c^0_o(5) = 5\) and \(c^2_o(5) = 14\).

theorem oddOrSmallEvenCompositionCount_five :
    oddOrSmallEvenCompositionCount 0 5 = 5 ∧ oddOrSmallEvenCompositionCount 1 5 = 14

Sources

• Brian Hopkins and Aram Tangboonduangjit, Arndt and De Morgan Compositions, INTEGERS 26 (2026), Article A64, Table 3 and the discussion after Theorem 5.

Uses 1

Statement usesCompositions into odd or small even parts

DefinitionCompositions into even or small odd parts#✓fully proved

For natural numbers \(k\) and \(n\), \(c^{2k+1}_e(n)\) is the number of compositions of \(n\) (sequences of positive integers of any length, including the empty one, that sum to \(n\)) in which every part is even or at most \(2k + 1\). In particular \(c^{2k+1}_e(0) = 1\).

def evenOrSmallOddCompositionCount (k n : ℕ) : ℕ :=
  ∑ m ∈ Finset.range (n + 1), ((Finset.Nat.antidiagonalTuple m n).filter fun c =>
    ∀ i, 0 < c i ∧ (Even (c i) ∨ c i ≤ 2 * k + 1)).card

Sources

• Brian Hopkins and Aram Tangboonduangjit, Arndt and De Morgan Compositions, INTEGERS 26 (2026), Article A64, Definition 5.

Used by 3

Used byCompositions of \(5\) into even or small odd parts · Recurrences for even-or-small-odd and odd-or-small-even compositions · Generalized Arndt compositions with negative odd shift

TheoremCompositions of \(5\) into even or small odd parts#✓fully proved

\(c^1_e(5) = 10\) and \(c^3_e(5) = 15\), where \(c^{2k+1}_e(n)\) is the number of compositions of \(n\) in which every part is even or at most \(2k + 1\).

theorem evenOrSmallOddCompositionCount_five :
    evenOrSmallOddCompositionCount 0 5 = 10 ∧ evenOrSmallOddCompositionCount 1 5 = 15

Sources

• Brian Hopkins and Aram Tangboonduangjit, Arndt and De Morgan Compositions, INTEGERS 26 (2026), Article A64, Table 6 and the discussion after Theorem 6.

Uses 1

Statement usesCompositions into even or small odd parts

DefinitionThe map \(U\) on lists#✓fully proved

The map \(U\) sends a list \((c_1, c_2, \dots)\) of natural numbers to the concatenation of the images of its consecutive pairs \((c_1, c_2)\), \((c_3, c_4)\), and so on, where \(1^j\) denotes \(j\) parts equal to \(1\): a pair \((a, b)\) with \(b < a\) goes to \((1^{a - b - 1}, 2b + 1)\); a pair \((a, b)\) with \(b \ge a\) goes to \((1^{a + b - 2k}, 2k)\), where \(k = \lfloor (b - a)/2 \rfloor + 1\) is the integer \(k \ge 1\) with \(2k - 2 \le b - a < 2k\); and a final unpaired entry \(a\) goes to \(1^a\). The empty list goes to itself. The exponent \(a + b - 2k\) is read as \(0\) when it is negative, which happens only when \(a = 0\).

def arndtU : List ℕ → List ℕ
  | [] => []
  | [a] => List.replicate a 1
  | a :: b :: rest =>
      (if b < a then List.replicate (a - b - 1) 1 ++ [2 * b + 1]
        else List.replicate (a + b - 2 * ((b - a) / 2 + 1)) 1 ++ [2 * ((b - a) / 2 + 1)]) ++
        arndtU rest

Sources

• Brian Hopkins and Aram Tangboonduangjit, Arndt and De Morgan Compositions, INTEGERS 26 (2026), Article A64, Theorem 2 and its proof.

Used by 3

Used byValues of the map \(U\) · Compositions fixed by \(U\) and their Padovan count · The pairwise map U permutes compositions

TheoremValues of the map \(U\)#✓fully proved

The map \(U\) sends \((2, 3)\) to \((1, 1, 1, 2)\), \((1, 4)\) to \((1, 4)\), \((3, 2)\) to \((5)\), \((1, 1, 1, 2)\) to \((2, 1, 2)\) and \((1, 3, 1)\) to \((4, 1)\).

theorem arndtU_examples :
    arndtU [2, 3] = [1, 1, 1, 2] ∧ arndtU [1, 4] = [1, 4] ∧ arndtU [3, 2] = [5] ∧
      arndtU [1, 1, 1, 2] = [2, 1, 2] ∧ arndtU [1, 3, 1] = [4, 1]

Sources

• Brian Hopkins and Aram Tangboonduangjit, Arndt and De Morgan Compositions, INTEGERS 26 (2026), Article A64, Table 3.

Uses 1

Statement usesThe map \(U\) on lists

DefinitionThe map \(V\) on lists#✓fully proved

The map \(V\) sends a list \((c_1, c_2, \dots)\) of natural numbers to the concatenation of the images of its consecutive pairs \((c_1, c_2)\), \((c_3, c_4)\), and so on, where \(1^j\) denotes \(j\) parts equal to \(1\): a pair \((a, b)\) with \(b \le a\) goes to \((1^{a - b}, 2b)\); a pair \((a, b)\) with \(b > a\) goes to \((1^{a + b - 2k - 1}, 2k + 1)\), where \(k = \lfloor (b - a + 1)/2 \rfloor\) is the integer \(k \ge 1\) with \(2k - 1 \le b - a < 2k + 1\); and a final unpaired entry \(a\) goes to \(1^a\). The empty list goes to itself. The exponent \(a + b - 2k - 1\) is read as \(0\) when it is negative, which happens only when \(a = 0\).

def arndtV : List ℕ → List ℕ
  | [] => []
  | [a] => List.replicate a 1
  | a :: b :: rest =>
      (if b ≤ a then List.replicate (a - b) 1 ++ [2 * b]
        else List.replicate (a + b - 2 * ((b - a + 1) / 2) - 1) 1 ++
          [2 * ((b - a + 1) / 2) + 1]) ++
        arndtV rest

Sources

• Brian Hopkins and Aram Tangboonduangjit, Arndt and De Morgan Compositions, INTEGERS 26 (2026), Article A64, Theorem 3 and its proof.

Used by 3

Used byValues of the map \(V\) · Compositions fixed by \(V\) and their Fibonacci count · The map \(V\) permutes compositions

TheoremValues of the map \(V\)#✓fully proved

The map \(V\) sends \((2, 3)\) to \((1, 1, 3)\), \((1, 4)\) to \((5)\), \((4, 1)\) to \((1, 1, 1, 2)\), \((1, 3, 1)\) to \((1, 3, 1)\) and \((2, 2, 1)\) to \((4, 1)\).

theorem arndtV_examples :
    arndtV [2, 3] = [1, 1, 3] ∧ arndtV [1, 4] = [5] ∧ arndtV [4, 1] = [1, 1, 1, 2] ∧
      arndtV [1, 3, 1] = [1, 3, 1] ∧ arndtV [2, 2, 1] = [4, 1]

Sources

• Brian Hopkins and Aram Tangboonduangjit, Arndt and De Morgan Compositions, INTEGERS 26 (2026), Article A64, Table 6.

Uses 1

Statement usesThe map \(V\) on lists

TheoremArndt compositions and compositions into odd parts are equinumerous#●ready to prove

For every natural number \(n\), the number \(a(n, 0)\) of Arndt compositions of \(n\) (compositions \((c_1, \dots, c_m)\) of \(n\) with \(c_{2i-1} > c_{2i}\) whenever \(2i \le m\)) equals the number \(c^0_o(n)\) of compositions of \(n\) into odd parts. This includes \(n = 0\), where both counts are \(1\).

public theorem_wanted kArndtTotalCount_zero_eq_odd_compositions (n : ℕ) :
    kArndtTotalCount 0 n = oddOrSmallEvenCompositionCount 0 n

Sources

• Brian Hopkins and Aram Tangboonduangjit, Arndt and De Morgan Compositions, INTEGERS 26 (2026), Article A64, Theorem 1.

Uses 2

Statement usesGeneralized Arndt compositions · Compositions into odd or small even parts

TheoremThe pairwise map U permutes compositions#●ready to prove

For every natural number \(n\) there is a permutation \(\sigma\) of the compositions of \(n\) such that, for every composition \(c\) of \(n\), the list of parts of \(\sigma(c)\) is \(U(c)\), the result of applying the pairwise map \(U\) to the list of parts of \(c\). In particular, \(U\) sends compositions of \(n\) to compositions of \(n\) and permutes them.

public theorem_wanted exists_perm_composition_blocks_eq_arndtU (n : ℕ) :
    ∃ σ : Equiv.Perm (Composition n), ∀ c, (σ c).blocks = arndtU c.blocks

Sources

• Brian Hopkins and Aram Tangboonduangjit, Arndt and De Morgan Compositions, INTEGERS 26 (2026), Article A64, Theorem 2.

Uses 1

Statement usesThe map \(U\) on lists

TheoremThe map \(V\) permutes compositions#●ready to prove

For every natural number \(n\), the map \(V\) sends compositions of \(n\) to compositions of \(n\), and it is a permutation of the set of compositions of \(n\).

public theorem_wanted exists_perm_composition_blocks_eq_arndtV (n : ℕ) :
    ∃ σ : Equiv.Perm (Composition n), ∀ c, (σ c).blocks = arndtV c.blocks

Sources

• Brian Hopkins and Aram Tangboonduangjit, Arndt and De Morgan Compositions, INTEGERS 26 (2026), Article A64, Theorem 3.

Uses 1

Statement usesThe map \(V\) on lists

TheoremCompositions fixed by \(U\) and their Padovan count#●ready to prove

A composition \((c_1, \dots, c_m)\) of \(n\) is fixed by the map \(U\) if and only if \(c_i = 1\) for every odd \(i\) and \(c_i\) is even for every even \(i\). Let \(c_U(n)\) be the number of compositions of \(n\) fixed by \(U\). Then \(c_U(n) = c_U(n - 2) + c_U(n - 3)\) for every \(n \ge 4\), \(c_U(1) = 1\), \(c_U(2) = 0\), \(c_U(3) = 1\), and \(c_U(n) = P_{n-1}\) for every \(n \ge 1\), where \(P\) is the shifted Padovan sequence, given by \(P_0 = 1\), \(P_1 = 0\), \(P_2 = 1\) and \(P_{j+3} = P_{j+1} + P_j\).

public theorem_wanted arndtU_fixed_iff_and_count :
    (∀ (n : ℕ) (c : Composition n), arndtU c.blocks = c.blocks ↔
      ∀ (i : ℕ) (h : i < c.blocks.length),
        if i % 2 = 0 then c.blocks[i] = 1 else Even c.blocks[i]) ∧
    (∀ n : ℕ, 4 ≤ n →
      (Finset.univ.filter fun c : Composition n => arndtU c.blocks = c.blocks).card =
        (Finset.univ.filter fun c : Composition (n - 2) => arndtU c.blocks = c.blocks).card +
          (Finset.univ.filter fun c : Composition (n - 3) => arndtU c.blocks = c.blocks).card) ∧
    (Finset.univ.filter fun c : Composition 1 => arndtU c.blocks = c.blocks).card = 1 ∧
    (Finset.univ.filter fun c : Composition 2 => arndtU c.blocks = c.blocks).card = 0 ∧
    (Finset.univ.filter fun c : Composition 3 => arndtU c.blocks = c.blocks).card = 1 ∧
    ∀ n : ℕ, 1 ≤ n →
      (Finset.univ.filter fun c : Composition n => arndtU c.blocks = c.blocks).card =
        shiftedPadovanSequence (n - 1)

Sources

• Brian Hopkins and Aram Tangboonduangjit, Arndt and De Morgan Compositions, INTEGERS 26 (2026), Article A64, Proposition 1.

Uses 2

Statement usesThe map \(U\) on lists · Shifted Padovan sequence

TheoremCompositions fixed by \(V\) and their Fibonacci count#●ready to prove

A composition \((c_1, \dots, c_m)\) of \(n\) is fixed by the map \(V\) if and only if \(c_i = 1\) for every odd \(i\) and \(c_i\) is odd and at least \(3\) for every even \(i\). Let \(c_V(n)\) be the number of compositions of \(n\) fixed by \(V\). Then \(c_V(n) = c_V(n - 2) + c_V(n - 4)\) for every \(n \ge 5\), \(c_V(1) = c_V(4) = 1\), \(c_V(2) = c_V(3) = 0\), and \(c_V(2j) = c_V(2j + 1) = F_{j-1}\) for every \(j \ge 1\), where \(F\) is the Fibonacci sequence with \(F_0 = 0\) and \(F_1 = 1\).

MetaMathlibExt.arndtV_fixed_iff_and_count · 17 lines

public theorem_wanted arndtV_fixed_iff_and_count :
    (∀ (n : ℕ) (c : Composition n), arndtV c.blocks = c.blocks ↔
      ∀ (i : ℕ) (h : i < c.blocks.length),
        if i % 2 = 0 then c.blocks[i] = 1 else Odd c.blocks[i] ∧ 3 ≤ c.blocks[i]) ∧
    (∀ n : ℕ, 5 ≤ n →
      (Finset.univ.filter fun c : Composition n => arndtV c.blocks = c.blocks).card =
        (Finset.univ.filter fun c : Composition (n - 2) => arndtV c.blocks = c.blocks).card +
          (Finset.univ.filter fun c : Composition (n - 4) => arndtV c.blocks = c.blocks).card) ∧
    (Finset.univ.filter fun c : Composition 1 => arndtV c.blocks = c.blocks).card = 1 ∧
    (Finset.univ.filter fun c : Composition 4 => arndtV c.blocks = c.blocks).card = 1 ∧
    (Finset.univ.filter fun c : Composition 2 => arndtV c.blocks = c.blocks).card = 0 ∧
    (Finset.univ.filter fun c : Composition 3 => arndtV c.blocks = c.blocks).card = 0 ∧
    ∀ j : ℕ, 1 ≤ j →
      (Finset.univ.filter fun c : Composition (2 * j) => arndtV c.blocks = c.blocks).card =
          Nat.fib (j - 1) ∧
        (Finset.univ.filter fun c : Composition (2 * j + 1) =>
          arndtV c.blocks = c.blocks).card = Nat.fib (j - 1)

Sources

• Brian Hopkins and Aram Tangboonduangjit, Arndt and De Morgan Compositions, INTEGERS 26 (2026), Article A64, Proposition 2.

Uses 1

Statement usesThe map \(V\) on lists

TheoremRecurrences for generalized Arndt counts#●ready to prove

Let \(a(n, k)\) be the number of generalized Arndt compositions of \(n\) with shift \(k\), set \(a(m, k) = 0\) for \(m < 0\), and note that \(a(0, k) = 1\) counts the empty composition. For every natural number \(j\) and every \(n \ge 3\),

\[a(n, -j) = a(n - 1, -j) + 2a(n - 2, -j) - a(n - 2 - j, -j),\]

and for every natural number \(k\) and every \(n \ge 3\),

\[a(n, k) = a(n - 1, k) + a(n - 2, k) - a(n - 3, k) + a(n - 3 - k, k).\]

The paper sets \(a(n - 2 - j, -j) = 0\) whenever \(n - 2 - j \le 0\); at \(n - 2 - j = 0\) that is false (\(j = 1\), \(n = 3\): \(a(3, -1) = 3\), while \(a(2, -1) + 2a(1, -1) - 0 = 4\)), and its own bijection uses the empty composition there. At \(n = 2\) the recurrences fail for every shift (for instance \(a(2, k) \ne a(1, k) + 2a(0, k)\)), so \(n \ge 3\) is assumed.

public theorem_wanted kArndtTotalCount_recurrence :
    (∀ j n : ℕ, 3 ≤ n →
      (kArndtTotalCount (-(j : ℤ)) n : ℤ) =
        kArndtTotalCount (-(j : ℤ)) (n - 1) + 2 * kArndtTotalCount (-(j : ℤ)) (n - 2) -
          if j + 2 ≤ n then (kArndtTotalCount (-(j : ℤ)) (n - 2 - j) : ℤ) else 0) ∧
    ∀ k n : ℕ, 3 ≤ n →
      (kArndtTotalCount k n : ℤ) =
        kArndtTotalCount k (n - 1) + kArndtTotalCount k (n - 2) - kArndtTotalCount k (n - 3) +
          if k + 3 ≤ n then (kArndtTotalCount k (n - 3 - k) : ℤ) else 0

Sources

• Brian Hopkins and Aram Tangboonduangjit, Arndt and De Morgan Compositions, INTEGERS 26 (2026), Article A64, Theorem 4.

Uses 1

Statement usesGeneralized Arndt compositions

TheoremGeneralized Arndt compositions with negative even shift#●ready to prove

For every natural number \(j \ge 1\) and every natural number \(n\), the number \(a(n, -2j)\) of compositions \((c_1, \dots, c_m)\) of \(n\) with \(c_{2i-1} > c_{2i} - 2j\) whenever \(2i \le m\) equals the number \(c^{2j}_o(n)\) of compositions of \(n\) in which every part is odd or at most \(2j\). This includes \(n = 0\).

public theorem_wanted kArndtTotalCount_neg_even (j n : ℕ) (hj : 1 ≤ j) :
    kArndtTotalCount (-(2 * j : ℤ)) n = oddOrSmallEvenCompositionCount j n

Sources

• Brian Hopkins and Aram Tangboonduangjit, Arndt and De Morgan Compositions, INTEGERS 26 (2026), Article A64, Theorem 5.

Uses 2

Statement usesGeneralized Arndt compositions · Compositions into odd or small even parts

TheoremGeneralized Arndt compositions with negative odd shift#●ready to prove

For all natural numbers \(j\) and \(n\), the number \(a(n, -2j - 1)\) of compositions \((c_1, \dots, c_m)\) of \(n\) with \(c_{2i-1} > c_{2i} - 2j - 1\) whenever \(2i \le m\) equals the number \(c^{2j+1}_e(n)\) of compositions of \(n\) in which every part is even or at most \(2j + 1\). This includes \(n = 0\).

public theorem_wanted kArndtTotalCount_neg_odd (j n : ℕ) :
    kArndtTotalCount (-(2 * j + 1 : ℤ)) n = evenOrSmallOddCompositionCount j n

Sources

• Brian Hopkins and Aram Tangboonduangjit, Arndt and De Morgan Compositions, INTEGERS 26 (2026), Article A64, Theorem 6.

Uses 2

Statement usesCompositions into even or small odd parts · Generalized Arndt compositions

TheoremRecurrences for even-or-small-odd and odd-or-small-even compositions#●ready to prove

For natural numbers \(k\) and \(n\), let \(c^{2k+1}_e(n)\) be the number of compositions of \(n\) in which every part is even or at most \(2k + 1\), and \(c^{2k}_o(n)\) the number in which every part is odd or at most \(2k\). If \(k \ge 1\) and \(n \ge 3\), then

\[c^{2k+1}_e(n) = c^{2k+1}_e(n - 1) + 2c^{2k+1}_e(n - 2) - c^{2k+1}_e(n - 3 - 2k)\]

and

\[c^{2k}_o(n) = c^{2k}_o(n - 1) + 2c^{2k}_o(n - 2) - c^{2k}_o(n - 2 - 2k),\]

where the last term is read as \(0\) when its argument is negative.

Both recurrences fail at \(n = 2\).

public theorem_wanted evenOrSmallOdd_oddOrSmallEven_recurrence (k n : ℕ) (hk : 1 ≤ k)
    (hn : 3 ≤ n) :
    ((evenOrSmallOddCompositionCount k n : ℤ) =
        evenOrSmallOddCompositionCount k (n - 1) + 2 * evenOrSmallOddCompositionCount k (n - 2) -
          if 2 * k + 3 ≤ n then (evenOrSmallOddCompositionCount k (n - 3 - 2 * k) : ℤ)
          else 0) ∧
      (oddOrSmallEvenCompositionCount k n : ℤ) =
        oddOrSmallEvenCompositionCount k (n - 1) + 2 * oddOrSmallEvenCompositionCount k (n - 2) -
          if 2 * k + 2 ≤ n then (oddOrSmallEvenCompositionCount k (n - 2 - 2 * k) : ℤ) else 0

Sources

• Brian Hopkins and Aram Tangboonduangjit, Arndt and De Morgan Compositions, INTEGERS 26 (2026), Article A64, Corollary 1.

Uses 2

Statement usesCompositions into even or small odd parts · Compositions into odd or small even parts

43 fully proved42 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.