Diagonal sequences of integer partitions

DefinitionDiagonal sequence of a partition#✓fully proved

Let \(\alpha\) be a partition with parts \(\alpha_1 \ge \alpha_2 \ge \dots \ge \alpha_t\), and set \(\alpha_i = 0\) for \(i > t\). Its diagonal sequence \(\delta(\alpha) = (d_k)_{k \ge 0}\) has \(d_0 = 0\) and, for \(k \ge 1\), \(d_k\) equal to the number of indices \(i\) with \(1 \le i \le k\) and \(\alpha_i + i - 1 \ge k\), that is, the number of cells of the Young diagram on its \(k\)-th diagonal from upper right to lower left. Equivalently, \(d_k\) is the number of \(i\) with \(1 \le i \le k\) such that at least \(i\) parts of \(\alpha\) are at least \(k + 1 - i\); the definition uses this form, with the parts given as a finite multiset of natural numbers.

def diagonalSequence (s : Multiset ℕ) (k : ℕ) : ℕ :=
  ((Finset.Icc 1 k).filter fun i => i ≤ s.countP (k + 1 - i ≤ ·)).card

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Section 1, Definition of the diagonal sequence (1.1).

Used by 19

Used byNumber of partitions with a given diagonal sequence · Partitions in a diagonal class with as many parts as the initial staircase · Partitions in a diagonal class with more parts than the initial staircase · Diagonal classes whose multiplicities are at least two · Diagonal class of a partition · Diagonal classes of size at most three · Partitions with a prescribed diagonal sequence · The diagonal class lies between the maximal and minimal partitions in majorization · The maximal partition has the prescribed diagonal normal form · Equal diagonal sequences of the maximal and minimal partitions · Diagonal sequence of \((7, 7, 4, 1, 1, 1)\) · Increments of the diagonal sequence · Repeated parts and large gaps in a diagonal class · Existence and uniqueness of the diagonal normal form · A partition lies in the class of its diagonal sequence · Every partition lies in its diagonal class · Counting diagonal sequences · Sums of squared parts and the diagonal sequence · The largest part of a partition with given diagonal sequence

TheoremDiagonal sequence of \((7, 7, 4, 1, 1, 1)\)#✓fully proved

The diagonal sequence of the partition \((7, 7, 4, 1, 1, 1)\) takes the values \(0, 1, 2, 3, 4, 4, 4, 2, 1, 0\) at the indices \(0, 1, \dots, 9\). This is the paper's running example.

theorem diagonalSequence_seven_seven_four_one_one_one :
    (List.range 10).map (diagonalSequence {7, 7, 4, 1, 1, 1}) = [0, 1, 2, 3, 4, 4, 4, 2, 1, 0]

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Section 1 (example after the definition); characteristic check of diagonalSequence.

Uses 1

Statement usesDiagonal sequence of a partition

DefinitionSequence of a finite list#✓fully proved

A finite list \((d_1, \dots, d_\ell)\) of natural numbers determines the sequence of natural numbers whose value at index \(k\) is \(d_k\) for \(1 \le k \le \ell\), and \(0\) for \(k = 0\) and for \(k > \ell\). This is the indexing of diagonal sequences, which take the value \(0\) at index \(0\).

def diagonalOfList (l : List ℕ) (k : ℕ) : ℕ :=
  (0 :: l).getD k 0

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Section 1 (trailing zeroes of δ(α) are omitted).

Used by 11

Used byCapping the multiplicities of a diagonal sequence at two · Truncating the staircase of a diagonal sequence · Diagonal classes whose multiplicities are at least two · Diagonal classes of size at most three · The diagonal class lies between the maximal and minimal partitions in majorization · The maximal partition has the prescribed diagonal normal form · The list sequence of \((1, 2, 1)\) · Equal diagonal sequences of the maximal and minimal partitions · Repeated parts and large gaps in a diagonal class · Existence and uniqueness of the diagonal normal form · The largest part of a partition with given diagonal sequence

TheoremThe list sequence of \((1, 2, 1)\)#✓fully proved

The sequence given by the list \((1, 2, 1)\) takes the values \(0, 1, 2, 1, 0, 0\) at the indices \(0, 1, 2, 3, 4, 5\).

theorem diagonalOfList_one_two_one :
    (List.range 6).map (diagonalOfList [1, 2, 1]) = [0, 1, 2, 1, 0, 0]

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Section 1; characteristic check of diagonalOfList.

Uses 1

Statement usesSequence of a finite list

DefinitionNormal form of a diagonal sequence#✓fully proved

For a natural number \(q\) and a sequence \(s = (s_k)\) of natural numbers, the normal form is the list \((1, 2, \dots, q - 1, q, q^{(s_q)}, (q-1)^{(s_{q-1})}, \dots, 1^{(s_1)})\), where \(v^{(m)}\) denotes \(m\) copies of \(v\): the numbers \(1, \dots, q\) followed by \(s_v\) copies of \(v\) for \(v = q, q - 1, \dots, 1\).

def diagonalNormalForm (q : ℕ) (s : ℕ → ℕ) : List ℕ :=
  List.range' 1 q ++ (List.range q).reverse.flatMap fun j => List.replicate (s (j + 1)) (j + 1)

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Corollary 1, display (2.1).

Used by 10

Used byCapping the multiplicities of a diagonal sequence at two · Truncating the staircase of a diagonal sequence · Diagonal classes whose multiplicities are at least two · The diagonal class lies between the maximal and minimal partitions in majorization · The maximal partition has the prescribed diagonal normal form · Diagonal normal form for \(q = 4\) and \(s = (1, 1, 0, 2)\) · Equal diagonal sequences of the maximal and minimal partitions · Repeated parts and large gaps in a diagonal class · Existence and uniqueness of the diagonal normal form · The largest part of a partition with given diagonal sequence

TheoremDiagonal normal form for \(q = 4\) and \(s = (1, 1, 0, 2)\)#✓fully proved

For \(q = 4\) and \(s_1 = 1\), \(s_2 = 1\), \(s_3 = 0\), \(s_4 = 2\), the diagonal normal form \((1, 2, 3, 4, 4^{(s_4)}, 3^{(s_3)}, 2^{(s_2)}, 1^{(s_1)})\), where \(v^{(m)}\) denotes \(m\) copies of \(v\), is \((1, 2, 3, 4, 4, 4, 2, 1)\).

theorem diagonalNormalForm_four_example :
    diagonalNormalForm 4 (fun k => [0, 1, 1, 0, 2].getD k 0) = [1, 2, 3, 4, 4, 4, 2, 1]

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Section 2 (example after Corollary 4); characteristic check of diagonalNormalForm.

Uses 1

Statement usesNormal form of a diagonal sequence

DefinitionMaximal partition of a diagonal normal form#✓fully proved

For a natural number \(q\) and a sequence \(s = (s_k)\) of natural numbers, \(\bar\alpha = (\bar\alpha_1, \dots, \bar\alpha_q)\) is the list of the \(q\) numbers \(\bar\alpha_i = q - i + 1 + \sum_{k=i}^{q} s_k\), \(1 \le i \le q\), in this order.

def diagonalMaxPartition (q : ℕ) (s : ℕ → ℕ) : List ℕ :=
  (List.range q).map fun j => q - j + ∑ k ∈ Finset.Icc (j + 1) q, s k

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Proposition 1.

Used by 6

Used byConjugate of a partition with prescribed gaps between its parts · Maximal partition for \(q = 4\) and \(s = (1, 1, 0, 2)\) · The diagonal class lies between the maximal and minimal partitions in majorization · The maximal partition has the prescribed diagonal normal form · Equal diagonal sequences of the maximal and minimal partitions · Repeated parts and large gaps in a diagonal class

TheoremMaximal partition for \(q = 4\) and \(s = (1, 1, 0, 2)\)#✓fully proved

For \(q = 4\) and \(s_1 = 1\), \(s_2 = 1\), \(s_3 = 0\), \(s_4 = 2\), the maximal partition \(\bar\alpha\), with parts \(\bar\alpha_i = q - i + 1 + \sum_{k=i}^{q} s_k\) for \(1 \le i \le q\), is \((8, 6, 4, 3)\).

theorem diagonalMaxPartition_four_example :
    diagonalMaxPartition 4 (fun k => [0, 1, 1, 0, 2].getD k 0) = [8, 6, 4, 3]

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Section 2 (example after Corollary 4); characteristic check of diagonalMaxPartition.

Uses 1

Statement usesMaximal partition of a diagonal normal form

DefinitionMinimal partition of a diagonal normal form#✓fully proved

For a natural number \(q\) and a sequence \(s = (s_k)\) of natural numbers, \(\underline\alpha\) is the list \((q^{(s_q + 1)}, (q-1)^{(s_{q-1} + 1)}, \dots, 1^{(s_1 + 1)})\), where \(v^{(m)}\) denotes \(m\) copies of \(v\): first \(s_q + 1\) copies of \(q\), then \(s_{q-1} + 1\) copies of \(q - 1\), and so on down to \(s_1 + 1\) copies of \(1\).

def diagonalMinPartition (q : ℕ) (s : ℕ → ℕ) : List ℕ :=
  (List.range q).reverse.flatMap fun j => List.replicate (s (j + 1) + 1) (j + 1)

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Proposition 2.

Used by 5

Used byConjugate of a partition with prescribed gaps between its parts · The diagonal class lies between the maximal and minimal partitions in majorization · Minimal partition for \(q = 4\) and \(s = (1, 1, 0, 2)\) · Equal diagonal sequences of the maximal and minimal partitions · Repeated parts and large gaps in a diagonal class

TheoremMinimal partition for \(q = 4\) and \(s = (1, 1, 0, 2)\)#✓fully proved

For \(q = 4\) and \(s_1 = 1\), \(s_2 = 1\), \(s_3 = 0\), \(s_4 = 2\), the minimal partition \(\underline\alpha = (4^{(s_4 + 1)}, 3^{(s_3 + 1)}, 2^{(s_2 + 1)}, 1^{(s_1 + 1)})\), where \(v^{(m)}\) denotes \(m\) copies of \(v\), is \((4, 4, 4, 3, 2, 2, 1, 1)\).

theorem diagonalMinPartition_four_example :
    diagonalMinPartition 4 (fun k => [0, 1, 1, 0, 2].getD k 0) = [4, 4, 4, 3, 2, 2, 1, 1]

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Section 2 (example after Corollary 4); characteristic check of diagonalMinPartition.

Uses 1

Statement usesMinimal partition of a diagonal normal form

DefinitionConjugate of a multiset of parts#✓fully proved

For a finite multiset \(\alpha\) of natural numbers with largest element \(m\) (and \(m = 0\) if \(\alpha\) is empty), the conjugate \(\alpha^*\) is the multiset of the \(m\) numbers \(c_0, c_1, \dots, c_{m-1}\), where \(c_j\) is the number of elements of \(\alpha\) greater than \(j\), counted with multiplicity. When \(\alpha\) is the multiset of parts of a partition, these are the parts of the conjugate partition.

def conjugateParts (s : Multiset ℕ) : Multiset ℕ :=
  (Multiset.range s.sup).map fun j => s.countP (j < ·)

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Section 1 (conjugate partition α*).

Used by 4

Used byConjugate of a partition with prescribed gaps between its parts · The conjugate of \((3, 1)\) is \((2, 1, 1)\) · Conjugation reverses majorization · Sums of squared parts and the diagonal sequence

TheoremThe conjugate of \((3, 1)\) is \((2, 1, 1)\)#✓fully proved

The conjugate of the partition with parts \(\{3, 1\}\) is the partition with parts \(\{2, 1, 1\}\).

theorem conjugateParts_three_one : conjugateParts {3, 1} = {2, 1, 1}

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Section 1; characteristic check of conjugateParts.

Uses 1

Statement usesConjugate of a multiset of parts

DefinitionDiagonal class of a partition#✓fully proved

For a partition \(p\) of \(n\), its diagonal class \(\delta^{-1}(\delta(p))\) is the finite set of all partitions \(\beta\) of \(n\) whose diagonal sequence \(\delta(\beta)\) equals the diagonal sequence \(\delta(p)\) of \(p\).

noncomputable def diagonalClass {n : ℕ} (p : Nat.Partition n) : Finset (Nat.Partition n) :=
  open Classical in Finset.univ.filter fun β => diagonalSequence β.parts = diagonalSequence p.parts

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Section 1 (definition of [d]).

Uses 1 · Used by 7

Statement usesDiagonal sequence of a partition

Used byNumber of partitions with a given diagonal sequence · Partitions in a diagonal class with as many parts as the initial staircase · Partitions in a diagonal class with more parts than the initial staircase · Diagonal classes whose multiplicities are at least two · Diagonal classes of size at most three · Every positive integer is the size of a diagonal class · Every partition lies in its diagonal class

TheoremEvery partition lies in its diagonal class#✓fully proved

For every partition \(p\) of \(n\), \(p\) belongs to the diagonal class of \(p\), the set of partitions of \(n\) whose diagonal sequence equals that of \(p\).

theorem mem_diagonalClass_self {n : ℕ} (p : Nat.Partition n) : p ∈ diagonalClass p

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Section 1 (definition of [d]); characteristic check of diagonalClass.

Uses 2

Statement usesDiagonal class of a partition

Proof usesDiagonal sequence of a partition

DefinitionPartitions with a prescribed diagonal sequence#✓fully proved

For a natural number \(n\) and a sequence \(d = (d_k)_{k \ge 0}\) of natural numbers, \([d]\) is the finite set of partitions \(\beta\) of \(n\) whose diagonal sequence \(\delta(\beta)\) equals \(d\).

noncomputable def diagonalClassOf (n : ℕ) (d : ℕ → ℕ) : Finset (Nat.Partition n) :=
  open Classical in Finset.univ.filter fun β => diagonalSequence β.parts = d

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Section 1 (definition of [d] for d ∈ Δ(n)).

Uses 1 · Used by 3

Statement usesDiagonal sequence of a partition

Used byCapping the multiplicities of a diagonal sequence at two · Truncating the staircase of a diagonal sequence · A partition lies in the class of its diagonal sequence

TheoremA partition lies in the class of its diagonal sequence#✓fully proved

Every partition \(\beta\) of \(n\) belongs to the set of partitions of \(n\) whose diagonal sequence equals that of \(\beta\).

theorem mem_diagonalClassOf_diagonalSequence {n : ℕ} (β : Nat.Partition n) :
    β ∈ diagonalClassOf n (diagonalSequence β.parts)

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Section 1 (definition of [d]); characteristic check of diagonalClassOf.

Uses 2

Statement usesPartitions with a prescribed diagonal sequence · Diagonal sequence of a partition

DefinitionMajorization of part lists#✓fully proved

For finite lists \(a = (a_1, \dots, a_s)\) and \(b = (b_1, \dots, b_t)\) of natural numbers, \(a\) majorizes \(b\), written \(a \succ b\), when \(b_1 + \dots + b_k \le a_1 + \dots + a_k\) for every natural number \(k \le \min\{s, t\}\).

No ordering of the lists is required; the source applies majorization to the parts of partitions listed in decreasing order.

def PartitionMajorizes (a b : List ℕ) : Prop :=
  ∀ k ≤ min a.length b.length, (b.take k).sum ≤ (a.take k).sum

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Section 3 (definition of majorization).

Used by 3

Used byThe diagonal class lies between the maximal and minimal partitions in majorization · Conjugation reverses majorization · Majorization of \((2, 2)\) by \((3, 1)\)

TheoremMajorization of \((2, 2)\) by \((3, 1)\)#✓fully proved

The partition \((3, 1)\) majorizes the partition \((2, 2)\): \(3 \ge 2\) and \(3 + 1 \ge 2 + 2\).

theorem partitionMajorizes_three_one_two_two : PartitionMajorizes [3, 1] [2, 2]

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Section 3; characteristic check of PartitionMajorizes.

Uses 1

Statement usesMajorization of part lists

DefinitionNumber of \(k\)-vn-arrangements#✓fully proved

Let \(k\) be a natural number and \(M\) a finite multiset of integers. A \(k\)-vn-arrangement of \(M\) is a finite sequence \((v_1, \dots, v_b)\) of integers whose multiset of entries is \(M\) and with \(v_{i+1} - v_i \le k\) for all \(1 \le i < b\). This is the number of distinct such sequences; sequences are compared entry by entry, so exchanging two equal entries gives the same arrangement. For \(k = 1\) these are the vn-arrangements.

noncomputable def vnArrangementCount (k : ℕ) (M : Multiset ℤ) : ℕ :=
  Set.ncard {l : List ℤ | (l : Multiset ℤ) = M ∧ l.IsChain fun a b => b - a ≤ (k : ℤ)}

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Section 4 (definitions of vn-arrangement and k-vn-arrangement).

Used by 4

Used byVn-arrangements of consecutive integers · Counting \(k\)-vn-arrangements of a multiset · Counting vn-arrangements of a multiset · A singleton multiset has one \(k\)-vn-arrangement

TheoremA singleton multiset has one \(k\)-vn-arrangement#✓fully proved

For every natural number \(k\) and every integer \(a\), the one-element multiset \(\{a\}\) has exactly one \(k\)-vn-arrangement.

theorem vnArrangementCount_singleton (k : ℕ) (a : ℤ) : vnArrangementCount k {a} = 1

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Section 4; characteristic check of vnArrangementCount.

Uses 1

Statement usesNumber of \(k\)-vn-arrangements

TheoremIncrements of the diagonal sequence#●ready to prove

Let \(\alpha\) be a partition of \(n\) with diagonal sequence \((d_k)_{k \ge 0}\), where \(d_0 = 0\), and let \(k \ge 0\). Then \(d_{k+1} \le d_k + 1\), with equality if and only if \(d_j = j\) for every \(j\) with \(1 \le j \le k + 1\). Moreover, if \(d_{k+1} \le d_k\), then \(d_{k+2} \le d_{k+1}\).

public theorem_wanted diagonalSequence_succ_le_and_antitone {n : ℕ} (p : Nat.Partition n)
    (k : ℕ) :
    (diagonalSequence p.parts (k + 1) ≤ diagonalSequence p.parts k + 1 ∧
      (diagonalSequence p.parts (k + 1) = diagonalSequence p.parts k + 1 ↔
        ∀ j ∈ Finset.Icc 1 (k + 1), diagonalSequence p.parts j = j)) ∧
    (diagonalSequence p.parts (k + 1) ≤ diagonalSequence p.parts k →
      diagonalSequence p.parts (k + 2) ≤ diagonalSequence p.parts (k + 1))

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Lemma 1.

Uses 1

Statement usesDiagonal sequence of a partition

TheoremExistence and uniqueness of the diagonal normal form#●ready to prove

Write \(v^{(m)}\) for \(m\) copies of \(v\). For every partition \(\alpha\) of \(n \ge 1\) there are an integer \(q > 0\) and natural numbers \(s_1, \dots, s_q\) such that the diagonal sequence of \(\alpha\), indexed from \(0\), is \((0, 1, 2, \dots, q, q^{(s_q)}, (q-1)^{(s_{q-1})}, \dots, 1^{(s_1)}, 0, 0, \dots)\) and \(q(q+1)/2 + \sum_{k=1}^{q} k s_k = n\). Moreover \(q\) and \(s_1, \dots, s_q\) are unique: if \(q' > 0\) and \(s'_1, \dots, s'_{q'}\) give the same diagonal sequence, then \(q' = q\) and \(s'_k = s_k\) for \(1 \le k \le q\).

public theorem_wanted exists_unique_diagonalNormalForm {n : ℕ} (hn : 0 < n)
    (p : Nat.Partition n) :
    ∃ q, 0 < q ∧ ∃ s : ℕ → ℕ,
      diagonalSequence p.parts = diagonalOfList (diagonalNormalForm q s) ∧
      q * (q + 1) / 2 + ∑ k ∈ Finset.Icc 1 q, k * s k = n ∧
      ∀ q' (s' : ℕ → ℕ), 0 < q' →
        diagonalSequence p.parts = diagonalOfList (diagonalNormalForm q' s') →
        q' = q ∧ ∀ k ∈ Finset.Icc 1 q, s' k = s k

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Corollary 1.

Uses 3

Statement usesNormal form of a diagonal sequence · Sequence of a finite list · Diagonal sequence of a partition

TheoremThe maximal partition has the prescribed diagonal normal form#●ready to prove

Let \(q > 0\) and let \(s_1, \dots, s_q\) be natural numbers with \(q(q+1)/2 + \sum_{k=1}^{q} k s_k = n\), and let \(\bar\alpha = (\bar\alpha_1, \dots, \bar\alpha_q)\) with \(\bar\alpha_i = q - i + 1 + \sum_{k=i}^{q} s_k\). Then the entries of \(\bar\alpha\) are positive, sum to \(n\) and are strictly decreasing; the diagonal sequence of \(\bar\alpha\) is \((1, 2, \dots, q, q^{(s_q)}, (q-1)^{(s_{q-1})}, \dots, 1^{(s_1)})\) followed by zeros, where \(v^{(m)}\) denotes \(m\) copies of \(v\); \(s_i = \bar\alpha_i - \bar\alpha_{i+1} - 1\) for \(1 \le i < q\); and \(s_q = \bar\alpha_q - 1\).

public theorem_wanted diagonalMaxPartition_spec (n q : ℕ) (hq : 0 < q) (s : ℕ → ℕ)
    (hn : q * (q + 1) / 2 + ∑ k ∈ Finset.Icc 1 q, k * s k = n) :
    ((diagonalMaxPartition q s).sum = n ∧ ∀ x ∈ diagonalMaxPartition q s, 0 < x) ∧
    (diagonalMaxPartition q s).SortedGT ∧
    diagonalSequence ↑(diagonalMaxPartition q s) = diagonalOfList (diagonalNormalForm q s) ∧
    (∀ i ∈ Finset.Ico 1 q, s i =
      (diagonalMaxPartition q s).getD (i - 1) 0 - (diagonalMaxPartition q s).getD i 0 - 1) ∧
    s q = (diagonalMaxPartition q s).getD (q - 1) 0 - 1

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Proposition 1.

Uses 4

Statement usesMaximal partition of a diagonal normal form · Normal form of a diagonal sequence · Sequence of a finite list · Diagonal sequence of a partition

TheoremCounting diagonal sequences#●ready to prove

For every natural number \(n\), including \(n = 0\), the number of distinct diagonal sequences of partitions of \(n\) equals the number of partitions of \(n\) into distinct parts, and the number of partitions of \(n\) into distinct parts equals the number of partitions of \(n\) into odd parts.

public theorem_wanted ncard_diagonalSequences_eq_card_distincts (n : ℕ) :
    (Set.range fun p : Nat.Partition n => diagonalSequence p.parts).ncard =
        (Nat.Partition.distincts n).card ∧
      (Nat.Partition.distincts n).card = (Nat.Partition.odds n).card

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Corollary 2.

Uses 1

Statement usesDiagonal sequence of a partition

TheoremConjugate of a partition with prescribed gaps between its parts#●ready to prove

Let \(q \ge 0\) and let \(s_1, \dots, s_q\) be natural numbers. The conjugate of the partition \(\bar\alpha\) with parts \(\bar\alpha_i = q - i + 1 + \sum_{k=i}^{q} s_k\) for \(1 \le i \le q\) is the partition \(\underline{\alpha} = (q^{(s_q + 1)}, (q-1)^{(s_{q-1} + 1)}, \dots, 1^{(s_1 + 1)})\), where \(v^{(r)}\) means \(r\) copies of \(v\); the parts are compared as multisets.

public theorem_wanted conjugateParts_diagonalMaxPartition (q : ℕ) (s : ℕ → ℕ) :
    conjugateParts ↑(diagonalMaxPartition q s) = ↑(diagonalMinPartition q s)

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Proposition 2.

Uses 3

Statement usesConjugate of a multiset of parts · Maximal partition of a diagonal normal form · Minimal partition of a diagonal normal form

TheoremEqual diagonal sequences of the maximal and minimal partitions#●ready to prove

Let \(q \ge 0\) and \(s_1, \dots, s_q \ge 0\) be natural numbers, write \(v^{(m)}\) for \(m\) copies of \(v\), and let \(\bar\alpha\) and \(\underline\alpha\) be the partitions with parts \(\bar\alpha_i = q - i + 1 + s_i + s_{i+1} + \dots + s_q\) for \(1 \le i \le q\) and \(\underline\alpha = (q^{(s_q + 1)}, (q-1)^{(s_{q-1} + 1)}, \dots, 1^{(s_1 + 1)})\). Then \(\bar\alpha\) and \(\underline\alpha\) have the same diagonal sequence; this diagonal sequence, indexed from \(0\), is \((0, 1, 2, \dots, q, q^{(s_q)}, \dots, 1^{(s_1)}, 0, 0, \dots)\); and the multiset of its nonzero entries \(1, 2, \dots, q, q^{(s_q)}, \dots, 1^{(s_1)}\) equals the multiset of parts of \(\underline\alpha\).

public theorem_wanted diagonalSequence_max_eq_min_and_multiset (q : ℕ) (s : ℕ → ℕ) :
    diagonalSequence ↑(diagonalMaxPartition q s) =
        diagonalSequence ↑(diagonalMinPartition q s) ∧
      diagonalSequence ↑(diagonalMinPartition q s) = diagonalOfList (diagonalNormalForm q s) ∧
      (↑(diagonalNormalForm q s) : Multiset ℕ) = ↑(diagonalMinPartition q s)

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Corollary 3.

Uses 5

Statement usesMaximal partition of a diagonal normal form · Minimal partition of a diagonal normal form · Normal form of a diagonal sequence · Sequence of a finite list · Diagonal sequence of a partition

TheoremRepeated parts and large gaps in a diagonal class#●ready to prove

Let \(q \ge 0\) and \(s_1, \dots, s_q \ge 0\) be natural numbers, write \(v^{(m)}\) for \(m\) copies of \(v\), and let \(\bar\alpha\) and \(\underline\alpha\) be the partitions with parts \(\bar\alpha_i = q - i + 1 + s_i + s_{i+1} + \dots + s_q\) for \(1 \le i \le q\) and \(\underline\alpha = (q^{(s_q + 1)}, (q-1)^{(s_{q-1} + 1)}, \dots, 1^{(s_1 + 1)})\). Let \(\alpha\) be a partition of \(n\) with parts \(\alpha_1 \ge \dots \ge \alpha_t\), set \(\alpha_{t+1} = 0\), and suppose that the diagonal sequence of \(\alpha\), indexed from \(0\), is \((0, 1, 2, \dots, q, q^{(s_q)}, \dots, 1^{(s_1)}, 0, 0, \dots)\). If \(\alpha \ne \bar\alpha\), then \(\alpha_i = \alpha_{i+1}\) for some \(i\) with \(1 \le i < t\). If \(\alpha \ne \underline\alpha\), then \(\alpha_i - \alpha_{i+1} \ge 2\) for some \(i\) with \(1 \le i \le t\).

public theorem_wanted exists_eq_succ_of_ne_diagonalMaxPartition {n : ℕ} (p : Nat.Partition n)
    (q : ℕ) (s : ℕ → ℕ)
    (hd : diagonalSequence p.parts = diagonalOfList (diagonalNormalForm q s)) :
    (p.parts.sort (· ≥ ·) ≠ diagonalMaxPartition q s →
      ∃ i, i + 1 < p.parts.card ∧
        (p.parts.sort (· ≥ ·)).getD i 0 = (p.parts.sort (· ≥ ·)).getD (i + 1) 0) ∧
    (p.parts.sort (· ≥ ·) ≠ diagonalMinPartition q s →
      ∃ i, i < p.parts.card ∧
        (p.parts.sort (· ≥ ·)).getD (i + 1) 0 + 1 < (p.parts.sort (· ≥ ·)).getD i 0)

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Corollary 4.

Uses 5

Statement usesMaximal partition of a diagonal normal form · Minimal partition of a diagonal normal form · Normal form of a diagonal sequence · Sequence of a finite list · Diagonal sequence of a partition

TheoremThe largest part of a partition with given diagonal sequence#●ready to prove

Let \(\alpha\) be a partition of \(n\), let \(q\) and \(s_1, s_2, \dots\) be natural numbers, and suppose the diagonal sequence of \(\alpha\) is \((1, 2, \dots, q, q^{(s_q)}, (q-1)^{(s_{q-1})}, \dots, 1^{(s_1)})\) followed by zeros, where \(v^{(m)}\) denotes \(m\) copies of \(v\). Then the largest part of \(\alpha\) (taken to be \(0\) if \(\alpha\) has no parts) lies in the set \(A_1 = \{q + \sum_{i=j}^{q} s_i : 1 \le j \le q + 1\}\), that is, \(A_1 = \{q, q + s_q, q + s_q + s_{q-1}, \dots, q + s_q + \dots + s_1\}\).

public theorem_wanted sup_parts_mem_diagonalFirstPartSet {n : ℕ} (p : Nat.Partition n) (q : ℕ)
    (s : ℕ → ℕ) (hd : diagonalSequence p.parts = diagonalOfList (diagonalNormalForm q s)) :
    p.parts.sup ∈ (Finset.Icc 1 (q + 1)).image fun j => q + ∑ i ∈ Finset.Icc j q, s i

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Proposition 3.

Uses 3

Statement usesNormal form of a diagonal sequence · Sequence of a finite list · Diagonal sequence of a partition

TheoremSums of squared parts and the diagonal sequence#●ready to prove

Let \(\alpha\) be a partition of \(n\) with diagonal sequence \((d_k)_{k \ge 1}\) and conjugate partition \(\alpha^*\), and write \(s(\gamma)\) for the sum of the squares of the parts of a partition \(\gamma\). Then \(s(\alpha) + s(\alpha^*) = 2 \sum_{k=1}^{2n} k \, d_k\). Consequently every partition \(\beta\) of \(n\) with the same diagonal sequence as \(\alpha\) satisfies \(s(\beta) + s(\beta^*) = s(\alpha) + s(\alpha^*)\).

The paper sums only up to the last diagonal \(t + \alpha_1 - 1\), where \(t\) is the number of parts and \(\alpha_1\) the largest part; summing to \(2n\) adds only zero terms.

public theorem_wanted sum_sq_add_sum_sq_conjugate_eq {n : ℕ} (p : Nat.Partition n) :
    (p.parts.map (· ^ 2)).sum + ((conjugateParts p.parts).map (· ^ 2)).sum =
        2 * ∑ k ∈ Finset.Icc 1 (2 * n), k * diagonalSequence p.parts k ∧
      ∀ β : Nat.Partition n, diagonalSequence β.parts = diagonalSequence p.parts →
        (β.parts.map (· ^ 2)).sum + ((conjugateParts β.parts).map (· ^ 2)).sum =
          (p.parts.map (· ^ 2)).sum + ((conjugateParts p.parts).map (· ^ 2)).sum

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Proposition 4.

Uses 2

Statement usesConjugate of a multiset of parts · Diagonal sequence of a partition

TheoremConjugation reverses majorization#●ready to prove

For partitions \(\alpha\) and \(\beta\) of \(n\), with parts listed in decreasing order, \(\alpha\) majorizes \(\beta\) if and only if the conjugate partition \(\beta^*\) majorizes the conjugate partition \(\alpha^*\), again with parts listed in decreasing order.

This is Theorem 7.B.5 of Marshall, Olkin and Arnold, as quoted in the source.

public theorem_wanted partitionMajorizes_iff_conjugate {n : ℕ} (α β : Nat.Partition n) :
    PartitionMajorizes (α.parts.sort (· ≥ ·)) (β.parts.sort (· ≥ ·)) ↔
      PartitionMajorizes ((conjugateParts β.parts).sort (· ≥ ·))
        ((conjugateParts α.parts).sort (· ≥ ·))

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, proof of Proposition 5 (citing [4], Theorem 7.B.5).

Uses 2

Statement usesMajorization of part lists · Conjugate of a multiset of parts

TheoremThe diagonal class lies between the maximal and minimal partitions in majorization#●ready to prove

Let \(p\) be a partition of \(n\), let \(q\) be a natural number and \(s = (s_k)\) a sequence of natural numbers, and suppose that the diagonal sequence of \(p\) is \((1, 2, \dots, q, q^{(s_q)}, (q-1)^{(s_{q-1})}, \dots, 1^{(s_1)})\) followed by zeros, where \(v^{(m)}\) denotes \(m\) copies of \(v\). Let \(\alpha\) be the parts of \(p\) in decreasing order, let \(\bar\alpha = (\bar\alpha_1, \dots, \bar\alpha_q)\) with \(\bar\alpha_i = q - i + 1 + \sum_{k=i}^{q} s_k\), and let \(\underline\alpha = (q^{(s_q + 1)}, (q-1)^{(s_{q-1} + 1)}, \dots, 1^{(s_1 + 1)})\). Then \(\bar\alpha \succ \alpha\) and \(\alpha \succ \underline\alpha\), where for lists \(a\) and \(b\), \(a \succ b\) means \(b_1 + \dots + b_k \le a_1 + \dots + a_k\) for every \(k\) up to the length of the shorter list.

public theorem_wanted diagonalMaxPartition_majorizes_majorizes_min {n : ℕ}
    (p : Nat.Partition n) (q : ℕ) (s : ℕ → ℕ)
    (hd : diagonalSequence p.parts = diagonalOfList (diagonalNormalForm q s)) :
    PartitionMajorizes (diagonalMaxPartition q s) (p.parts.sort (· ≥ ·)) ∧
      PartitionMajorizes (p.parts.sort (· ≥ ·)) (diagonalMinPartition q s)

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Proposition 5.

Uses 6

Statement usesMajorization of part lists · Maximal partition of a diagonal normal form · Minimal partition of a diagonal normal form · Normal form of a diagonal sequence · Sequence of a finite list · Diagonal sequence of a partition

TheoremCounting vn-arrangements of a multiset#●ready to prove

Let \(t\) be a natural number, let \(b_0, b_1, \dots\) be natural numbers, and let \(M\) be the multiset of integers containing \(b_i\) copies of \(i\) for each \(0 \le i \le t\), so that \(M\) has \(m = b_0 + \dots + b_t\) elements. Then the number of vn-arrangements of \(M\), that is, orderings \((v_1, \dots, v_m)\) of \(M\) with \(v_{j+1} - v_j \le 1\) for all \(j\), is \(\prod_{i=0}^{t-1} \binom{b_i + b_{i+1}}{b_i}\).

public theorem_wanted vnArrangementCount_one_eq_prod (t : ℕ) (b : ℕ → ℕ) :
    vnArrangementCount 1 (∑ i ∈ Finset.range (t + 1), Multiset.replicate (b i) (i : ℤ)) =
      ∏ i ∈ Finset.range t, (b i + b (i + 1)).choose (b i)

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Proposition 6.

Uses 1

Statement usesNumber of \(k\)-vn-arrangements

TheoremVn-arrangements of consecutive integers#●ready to prove

For every integer \(a\) and every natural number \(t \ge 1\), the set \(\{a, a + 1, \dots, a + t - 1\}\) of \(t\) consecutive integers has exactly \(2^{t-1}\) vn-arrangements, that is, orderings \((v_1, \dots, v_t)\) of its elements with \(v_{i+1} - v_i \le 1\) for all \(i\).

public theorem_wanted vnArrangementCount_consecutive (a : ℤ) (t : ℕ) (ht : 1 ≤ t) :
    vnArrangementCount 1 (Finset.Ico a (a + t)).val = 2 ^ (t - 1)

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Corollary 5.

Uses 1

Statement usesNumber of \(k\)-vn-arrangements

TheoremCounting \(k\)-vn-arrangements of a multiset#●ready to prove

Let \(k \le t\) be natural numbers, let \(b_0, b_1, \dots\) be natural numbers, and let \(M\) be the multiset of integers containing \(b_i\) copies of \(i\) for each \(0 \le i \le t\), so that \(M\) has \(m = b_0 + \dots + b_t\) elements. Then the number of \(k\)-vn-arrangements of \(M\), that is, orderings \((v_1, \dots, v_m)\) of \(M\) with \(v_{j+1} - v_j \le k\) for all \(j\), is

\[ \binom{b_0 + \dots + b_k}{b_0, \dots, b_k} \prod_{i=1}^{t-k} \binom{b_i + \dots + b_{i+k}}{b_{i+k}} \]

public theorem_wanted vnArrangementCount_eq_multinomial_mul_prod (t k : ℕ) (hk : k ≤ t)
    (b : ℕ → ℕ) :
    vnArrangementCount k (∑ i ∈ Finset.range (t + 1), Multiset.replicate (b i) (i : ℤ)) =
      Nat.multinomial (Finset.range (k + 1)) b *
        ∏ i ∈ Finset.Icc 1 (t - k), (∑ j ∈ Finset.Icc i (i + k), b j).choose (b (i + k))

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Proposition 7.

Uses 1

Statement usesNumber of \(k\)-vn-arrangements

TheoremPartitions in a diagonal class with as many parts as the initial staircase#●ready to prove

Let \(\alpha\) be a partition of \(n\) with diagonal sequence \(\delta(\alpha) = (d_j)_{j \ge 1}\), set \(d_0 = 0\), and let \(q, L \ge 0\) be integers with \(d_j = j\) for all \(1 \le j \le q\), \(d_{q+1} \ne q + 1\), \(d_L \ne 0\) and \(d_{L+1} = 0\). Put \(b_i = \max(d_i - d_{i+1}, 0)\). Then the number of partitions of \(n\) with exactly \(q\) parts whose diagonal sequence equals \(\delta(\alpha)\) is

\[\prod_{i=q}^{L-1} \binom{b_i + b_{i+1}}{b_i}.\]

public theorem_wanted card_diagonalClass_filter_card_parts_eq_q {n : ℕ} (p : Nat.Partition n)
    (q L : ℕ) (hq : ∀ j ∈ Finset.Icc 1 q, diagonalSequence p.parts j = j)
    (hq' : diagonalSequence p.parts (q + 1) ≠ q + 1) (hL : diagonalSequence p.parts L ≠ 0)
    (hL' : diagonalSequence p.parts (L + 1) = 0) :
    ((diagonalClass p).filter fun β => β.parts.card = q).card =
      ∏ i ∈ Finset.Ico q L,
        ((diagonalSequence p.parts i - diagonalSequence p.parts (i + 1)) +
            (diagonalSequence p.parts (i + 1) - diagonalSequence p.parts (i + 2))).choose
          (diagonalSequence p.parts i - diagonalSequence p.parts (i + 1))

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Proposition 8.

Uses 2

Statement usesDiagonal class of a partition · Diagonal sequence of a partition

TheoremPartitions in a diagonal class with more parts than the initial staircase#●ready to prove

Let \(\alpha\) be a partition of \(n\) with diagonal sequence \(\delta(\alpha) = (d_j)_{j \ge 1}\), set \(d_0 = 0\), and let \(q, L \ge 0\) be integers with \(d_j = j\) for all \(1 \le j \le q\), \(d_{q+1} \ne q + 1\), \(d_L \ne 0\) and \(d_{L+1} = 0\). Put \(b_i = \max(d_i - d_{i+1}, 0)\). Then for every \(k > q\) the number of partitions of \(n\) with exactly \(k\) parts whose diagonal sequence equals \(\delta(\alpha)\) is

\[\binom{b_{k-1} + b_k}{b_{k-1} + 1} \prod_{i=q}^{k-2} \binom{b_i + b_{i+1} + 1}{b_i + 1} \prod_{i=k}^{L-1} \binom{b_i + b_{i+1}}{b_i}.\]

For \(k > L\) both sides are \(0\).

MetaMathlibExt.card_diagonalClass_filter_card_parts_eq_of_lt · 17 lines

public theorem_wanted card_diagonalClass_filter_card_parts_eq_of_lt {n : ℕ}
    (p : Nat.Partition n) (q L k : ℕ)
    (hq : ∀ j ∈ Finset.Icc 1 q, diagonalSequence p.parts j = j)
    (hq' : diagonalSequence p.parts (q + 1) ≠ q + 1) (hL : diagonalSequence p.parts L ≠ 0)
    (hL' : diagonalSequence p.parts (L + 1) = 0) (hk : q < k) :
    ((diagonalClass p).filter fun β => β.parts.card = k).card =
      ((diagonalSequence p.parts (k - 1) - diagonalSequence p.parts k) +
            (diagonalSequence p.parts k - diagonalSequence p.parts (k + 1))).choose
          (diagonalSequence p.parts (k - 1) - diagonalSequence p.parts k + 1) *
        (∏ i ∈ Finset.Ico q (k - 1),
          ((diagonalSequence p.parts i - diagonalSequence p.parts (i + 1)) +
              (diagonalSequence p.parts (i + 1) - diagonalSequence p.parts (i + 2)) + 1).choose
            (diagonalSequence p.parts i - diagonalSequence p.parts (i + 1) + 1)) *
        ∏ i ∈ Finset.Ico k L,
          ((diagonalSequence p.parts i - diagonalSequence p.parts (i + 1)) +
              (diagonalSequence p.parts (i + 1) - diagonalSequence p.parts (i + 2))).choose
            (diagonalSequence p.parts i - diagonalSequence p.parts (i + 1))

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Proposition 9.

Uses 2

Statement usesDiagonal class of a partition · Diagonal sequence of a partition

TheoremNumber of partitions with a given diagonal sequence#●ready to prove

Let \(\alpha\) be a partition of \(n\) with diagonal sequence \(\delta(\alpha) = (d_j)_{j \ge 1}\), set \(d_0 = 0\), and let \(q, L \ge 0\) be integers with \(d_j = j\) for all \(1 \le j \le q\), \(d_{q+1} \ne q + 1\), \(d_L \ne 0\) and \(d_{L+1} = 0\). Put \(b_i = \max(d_i - d_{i+1}, 0)\). Then the number of partitions of \(n\) whose diagonal sequence equals \(\delta(\alpha)\) is

\[\prod_{i=q}^{L-1} \binom{b_i + b_{i+1} + 1}{b_i + 1}.\]

public theorem_wanted card_diagonalClass_eq_prod_choose {n : ℕ} (p : Nat.Partition n) (q L : ℕ)
    (hq : ∀ j ∈ Finset.Icc 1 q, diagonalSequence p.parts j = j)
    (hq' : diagonalSequence p.parts (q + 1) ≠ q + 1) (hL : diagonalSequence p.parts L ≠ 0)
    (hL' : diagonalSequence p.parts (L + 1) = 0) :
    (diagonalClass p).card =
      ∏ i ∈ Finset.Ico q L,
        ((diagonalSequence p.parts i - diagonalSequence p.parts (i + 1)) +
            (diagonalSequence p.parts (i + 1) - diagonalSequence p.parts (i + 2)) + 1).choose
          (diagonalSequence p.parts i - diagonalSequence p.parts (i + 1) + 1)

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Theorem 1.

Uses 2

Statement usesDiagonal class of a partition · Diagonal sequence of a partition

TheoremDiagonal classes whose multiplicities are at least two#●ready to prove

Let \(q \ge 1\), let \(s = (s_1, s_2, \dots)\) be a sequence of natural numbers, and let \(\alpha\) be a partition of \(n\) whose diagonal sequence \(\delta(\alpha) = (d_i)_{i \ge 1}\) is \((1, 2, \dots, q, q^{(s_q)}, (q-1)^{(s_{q-1})}, \dots, 1^{(s_1)})\) followed by zeros, where \(v^{(r)}\) means \(r\) copies of \(v\). Put \(L = q + s_1 + \dots + s_q\). If \(s_i \ge 2\) for all \(1 \le i < q\), then exactly one partition of \(n\) with diagonal sequence \(\delta(\alpha)\) has exactly \(q\) parts; if moreover \(s_q \ge 1\), then the number of partitions of \(n\) with diagonal sequence \(\delta(\alpha)\) is \(\prod_{i=q}^{L} (\max(d_i - d_{i+1}, 0) + 1)\).

public theorem_wanted card_diagonalClass_of_two_le_s {n : ℕ} (p : Nat.Partition n) (q : ℕ)
    (hq : 1 ≤ q) (s : ℕ → ℕ)
    (hd : diagonalSequence p.parts = diagonalOfList (diagonalNormalForm q s))
    (hs : ∀ i ∈ Finset.Ico 1 q, 2 ≤ s i) :
    ((diagonalClass p).filter fun β => β.parts.card = q).card = 1 ∧
      (1 ≤ s q → (diagonalClass p).card =
        ∏ i ∈ Finset.Icc q (q + ∑ j ∈ Finset.Icc 1 q, s j),
          (diagonalSequence p.parts i - diagonalSequence p.parts (i + 1) + 1))

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Corollary 6 (1), (2).

Uses 4

Statement usesDiagonal class of a partition · Normal form of a diagonal sequence · Sequence of a finite list · Diagonal sequence of a partition

TheoremEvery positive integer is the size of a diagonal class#●ready to prove

For every positive integer \(m\) there are a natural number \(n\) and a partition \(\alpha\) of \(n\) whose class, the set of partitions of \(n\) with the same diagonal sequence as \(\alpha\), has exactly \(m\) elements.

public theorem_wanted exists_card_diagonalClass_eq (m : ℕ) (hm : 0 < m) :
    ∃ (n : ℕ) (p : Nat.Partition n), (diagonalClass p).card = m

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Corollary 6 (3).

Uses 1

Statement usesDiagonal class of a partition

TheoremTruncating the staircase of a diagonal sequence#●ready to prove

For \(m \ge 0\) and a sequence \(s = (s_1, s_2, \dots)\) of natural numbers, let \(d(m, s)\) be the sequence \((1, 2, \dots, m, m^{(s_m)}, (m-1)^{(s_{m-1})}, \dots, 1^{(s_1)})\) followed by zeros, where \(v^{(r)}\) means \(r\) copies of \(v\), and let \(n(m, s) = m(m+1)/2 + \sum_{j=1}^{m} j s_j\). Let \(1 \le k < q\) with \(s_k \ge 2\) and \(s_j = 0\) for all \(k < j \le q\). Then the number of partitions of \(n(q, s)\) with diagonal sequence \(d(q, s)\) equals the number of partitions of \(n(k, s)\) with diagonal sequence \(d(k, s)\).

public theorem_wanted card_diagonalClassOf_truncate (q k : ℕ) (s : ℕ → ℕ) (hk : 1 ≤ k)
    (hkq : k < q) (hsk : 2 ≤ s k) (hs : ∀ j ∈ Finset.Ioc k q, s j = 0) :
    (diagonalClassOf (q * (q + 1) / 2 + ∑ j ∈ Finset.Icc 1 q, j * s j)
        (diagonalOfList (diagonalNormalForm q s))).card =
      (diagonalClassOf (k * (k + 1) / 2 + ∑ j ∈ Finset.Icc 1 k, j * s j)
        (diagonalOfList (diagonalNormalForm k s))).card

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Corollary 6 (4).

Uses 3

Statement usesPartitions with a prescribed diagonal sequence · Normal form of a diagonal sequence · Sequence of a finite list

TheoremCapping the multiplicities of a diagonal sequence at two#●ready to prove

For \(m \ge 0\) and a sequence \(s = (s_1, s_2, \dots)\) of natural numbers, let \(d(m, s)\) be the sequence \((1, 2, \dots, m, m^{(s_m)}, (m-1)^{(s_{m-1})}, \dots, 1^{(s_1)})\) followed by zeros, where \(v^{(r)}\) means \(r\) copies of \(v\), and let \(n(m, s) = m(m+1)/2 + \sum_{j=1}^{m} j s_j\). Let \(q \ge 1\) and \(\sigma_j = \min(s_j, 2)\) for all \(j\). Then the number of partitions of \(n(q, s)\) with diagonal sequence \(d(q, s)\) equals the number of partitions of \(n(q, \sigma)\) with diagonal sequence \(d(q, \sigma)\).

public theorem_wanted card_diagonalClassOf_min_two (q : ℕ) (hq : 1 ≤ q) (s : ℕ → ℕ) :
    (diagonalClassOf (q * (q + 1) / 2 + ∑ j ∈ Finset.Icc 1 q, j * s j)
        (diagonalOfList (diagonalNormalForm q s))).card =
      (diagonalClassOf (q * (q + 1) / 2 + ∑ j ∈ Finset.Icc 1 q, j * min (s j) 2)
        (diagonalOfList (diagonalNormalForm q fun j => min (s j) 2))).card

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Corollary 6 (5).

Uses 3

Statement usesPartitions with a prescribed diagonal sequence · Normal form of a diagonal sequence · Sequence of a finite list

TheoremDiagonal classes of size at most three#●ready to prove

Let \(\alpha\) be a partition of \(n \ge 1\), let \(d = \delta(\alpha)\) be its diagonal sequence, written without its trailing zeros, and let \([\alpha]\) be the set of partitions of \(n\) with diagonal sequence \(d\), each written by its parts in decreasing order. Here \(v^{(r)}\) means \(r\) copies of \(v\), and a run \(a, a - 1, \dots, b\) with \(a < b\) is empty. (1) If \(|[\alpha]| = 1\), then there is \(q \ge 1\) with \(n = \binom{q+1}{2}\), \(d = (1, 2, \dots, q)\) and \([\alpha] = \{(q, q - 1, \dots, 1)\}\). (2) If \(|[\alpha]| = 2\), then either there are \(q \ge 1\) and \(k \ge 2\) with \(n = \binom{q+1}{2} + k\), \(d = (1, 2, \dots, q, 1^{(k)})\) and \([\alpha] = \{(q + k, q - 1, \dots, 1), (q, q - 1, \dots, 1, 1^{(k)})\}\), or \(n = 2\), \(d = (1, 1)\) and \([\alpha] = \{(2), (1, 1)\}\). (3) If \(|[\alpha]| = 3\), then either there are \(q \ge 2\) and \(k \ge 2\) with \(n = \binom{q+1}{2} + 2k\), \(d = (1, 2, \dots, q, 2^{(k)})\) and \([\alpha] = \{(q + k, q - 1 + k, q - 2, \dots, 1), (q, q - 1, \dots, 3, 2^{(k+1)}, 1), (q + k, q - 1, \dots, 2, 1^{(k+1)})\}\), or \(d = (1, 2, 1)\) and \([\alpha] = \{(3, 1), (2, 2), (2, 1, 1)\}\), or \(d = (1, 2, 2)\) and \([\alpha] = \{(3, 2), (3, 1, 1), (2, 2, 1)\}\).

Part (4) of the corollary, on classes of size \(4\), is false as printed and is not included.

MetaMathlibExt.diagonalClass_classification_card_le_three · 27 lines

public theorem_wanted diagonalClass_classification_card_le_three {n : ℕ} (hn : 0 < n)
    (p : Nat.Partition n) :
    ((diagonalClass p).card = 1 →
      ∃ q, 1 ≤ q ∧ n = (q + 1).choose 2 ∧
        diagonalSequence p.parts = diagonalOfList (List.range' 1 q) ∧
        (diagonalClass p).image (·.parts) = {(((List.range' 1 q).reverse : List ℕ) : Multiset ℕ)}) ∧
    ((diagonalClass p).card = 2 →
      (∃ q k, 1 ≤ q ∧ 2 ≤ k ∧ n = (q + 1).choose 2 + k ∧
        diagonalSequence p.parts = diagonalOfList (List.range' 1 q ++ List.replicate k 1) ∧
        (diagonalClass p).image (·.parts) =
          {(((q + k) :: (List.range' 1 (q - 1)).reverse : List ℕ) : Multiset ℕ),
            (((List.range' 1 q).reverse ++ List.replicate k 1 : List ℕ) : Multiset ℕ)}) ∨
      (n = 2 ∧ diagonalSequence p.parts = diagonalOfList [1, 1] ∧
        (diagonalClass p).image (·.parts) = {{2}, {1, 1}})) ∧
    ((diagonalClass p).card = 3 →
      (∃ q k, 2 ≤ q ∧ 2 ≤ k ∧ n = (q + 1).choose 2 + 2 * k ∧
        diagonalSequence p.parts = diagonalOfList (List.range' 1 q ++ List.replicate k 2) ∧
        (diagonalClass p).image (·.parts) =
          {(([q + k, q - 1 + k] ++ (List.range' 1 (q - 2)).reverse : List ℕ) : Multiset ℕ),
            (((List.range' 3 (q - 2)).reverse ++ List.replicate (k + 1) 2 ++ [1] : List ℕ) :
              Multiset ℕ),
            (((q + k) :: ((List.range' 2 (q - 2)).reverse ++ List.replicate (k + 1) 1) :
              List ℕ) : Multiset ℕ)}) ∨
      (diagonalSequence p.parts = diagonalOfList [1, 2, 1] ∧
        (diagonalClass p).image (·.parts) = {{3, 1}, {2, 2}, {2, 1, 1}}) ∨
      (diagonalSequence p.parts = diagonalOfList [1, 2, 2] ∧
        (diagonalClass p).image (·.parts) = {{3, 2}, {3, 1, 1}, {2, 2, 1}}))

Sources

• Michael Neubauer and Harmony Vargas, Diagonal Sequences of Integer Partitions, INTEGERS 25 (2025), Article A60, Corollary 7 (1)–(3).

Uses 3

Statement usesDiagonal class of a partition · Sequence of a finite list · Diagonal sequence of a partition

20 fully proved22 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.