Humps and peaks in Motzkin paths

TheoremHumps and peaks at a given height in Motzkin paths#✓fully proved

Let \(n \ge 2\) and \(k \ge 1\). A Motzkin path of length \(n\) is a sequence of \(n\) steps, each up (\(+1\)), flat (\(0\)) or down (\(-1\)), whose partial sums are all nonnegative and whose total is \(0\). A hump at height \(k\) of such a path is a pair of positions \(i < j\) such that step \(i\) is up, step \(j\) is down, every step strictly between them is flat, and the sum of the steps up to and including step \(i\) equals \(k\); a peak at height \(k\) is such a hump with \(j = i + 1\). Let \(H_{n,k}\) be the number of pairs consisting of a Motzkin path of length \(n\) and a hump at height \(k\) of it, and let \(P_{n,k}\) be the same count for peaks. Then, as rational numbers,

\[H_{n,k} = \sum_{j} \frac{4k}{n - j + 2k} \binom{n}{j} \binom{n - j - 1}{(n - j)/2 + k - 1}\]

and

\[P_{n,k} = \sum_{j} \frac{4k}{n - j + 2k} \binom{n - 1}{j} \binom{n - j - 1}{(n - j)/2 + k - 1},\]

where both sums run over the integers \(0 \le j \le n - 2k\) with \(j \equiv n \pmod 2\).

MetaMathlibExt.motzkin_hump_peak_height_distribution · 37 lines

public theorem motzkin_hump_peak_height_distribution
    (n k : ℕ) (hn : 2 ≤ n) (hk : 1 ≤ k) :
    let step : Fin 3 → ℤ := fun s => (s.val : ℤ) - 1
    let IsMotzkin : (Fin n → Fin 3) → Prop := fun p =>
      (∀ m : ℕ, m ≤ n →
        0 ≤ ∑ i : Fin n, if i.val < m then step (p i) else 0) ∧
      ∑ i : Fin n, step (p i) = 0
    let IsHump : (Fin n → Fin 3) → Fin n → Fin n → Prop := fun p i j =>
      i.val < j.val ∧
      step (p i) = 1 ∧
      step (p j) = -1 ∧
      (∀ r : Fin n, i.val < r.val → r.val < j.val → step (p r) = 0) ∧
      (∑ r : Fin n, if r.val ≤ i.val then step (p r) else 0) = (k : ℤ)
    let IsPeak : (Fin n → Fin 3) → Fin n → Fin n → Prop := fun p i j =>
      IsHump p i j ∧ j.val = i.val + 1
    let Hnk := @Fintype.card
      {q : (Fin n → Fin 3) × Fin n × Fin n //
        IsMotzkin q.1 ∧ IsHump q.1 q.2.1 q.2.2}
      (Fintype.ofFinite _)
    let Pnk := @Fintype.card
      {q : (Fin n → Fin 3) × Fin n × Fin n //
        IsMotzkin q.1 ∧ IsPeak q.1 q.2.1 q.2.2}
      (Fintype.ofFinite _)
    (Hnk : ℚ) =
        (∑ j ∈ Finset.range (n + 1),
          if j + 2 * k ≤ n ∧ j % 2 = n % 2 then
            (((4 * k : ℕ) : ℚ) / ((n - j + 2 * k : ℕ) : ℚ)) *
              (Nat.choose n j : ℚ) *
              (Nat.choose (n - j - 1) ((n - j) / 2 + k - 1) : ℚ)
          else 0) ∧
      (Pnk : ℚ) =
        (∑ j ∈ Finset.range (n + 1),
          if j + 2 * k ≤ n ∧ j % 2 = n % 2 then
            (((4 * k : ℕ) : ℚ) / ((n - j + 2 * k : ℕ) : ℚ)) *
              (Nat.choose (n - 1) j : ℚ) *
              (Nat.choose (n - j - 1) ((n - j) / 2 + k - 1) : ℚ)
          else 0)

Sources

• Xiaomei Chen, "Humps in Motzkin Paths and Standard Young Tableaux in a \((2,1)\)-Hook", Journal of Integer Sequences 28 (2025), Article 25.8.1, Theorem thm:22, lines 147-156, https://cs.uwaterloo.ca/journals/JIS/VOL28/Chen/chen36.tex.

DefinitionHeight change of a Motzkin step#✓fully proved

The three Motzkin steps are encoded as \(0 = D\) (down), \(1 = F\) (flat) and \(2 = U\) (up). The height change of the step encoded by \(s \in \{0, 1, 2\}\) is the integer \(s - 1\); thus \(D\) changes the height by \(-1\), \(F\) by \(0\) and \(U\) by \(+1\).

public def motzkinStep (s : Fin 3) : ℤ := (s.val : ℤ) - 1

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Section 1 (definitions).

Used by 8

Used byMotzkin hump · Characterization of Motzkin humps · Motzkin prefix · Bounded Motzkin prefix condition · Bounded form of the Motzkin prefix condition · Unfolding the Motzkin prefix condition · Number of humps of a given height in Motzkin paths · Humps of height one in Motzkin paths of length four

DefinitionMotzkin prefix#✓fully proved

Let \(p = p_0 p_1 \cdots p_{n-1}\) be a word of length \(n\) in the steps \(D\), \(F\), \(U\) (encoded as \(0\), \(1\), \(2\)), whose vertical displacements are \(-1\), \(0\) and \(+1\), and let \(h \in \mathbb{Z}\). The word \(p\) is a Motzkin prefix ending at height \(h\) when, for every natural number \(m \le n\), the sum of the displacements of \(p_0, \dots, p_{m-1}\) is nonnegative, and the sum of the displacements of all \(n\) steps is \(h\).

public def IsMotzkinPrefix (n : ℕ) (h : ℤ) (p : Fin n → Fin 3) : Prop :=
  (∀ m : ℕ, m ≤ n → 0 ≤ ∑ i : Fin n, if i.val < m then motzkinStep (p i) else 0) ∧
  ∑ i : Fin n, motzkinStep (p i) = h

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Section 1 (definitions).

Uses 1 · Used by 8

Statement usesHeight change of a Motzkin step

Used byBounded form of the Motzkin prefix condition · Unfolding the Motzkin prefix condition · Motzkin prefixes whose first non-up step is down · Number of humps of a given height in Motzkin paths · Humps of height one in Motzkin paths of length four · Motzkin paths with a marked hump, over all heights · Humps correspond to last-up prefixes of twice the height · Motzkin prefixes of even height whose last non-flat step is up

DefinitionMotzkin hump#✓fully proved

Let \(p = p_0 p_1 \cdots p_{n-1}\) be a word of length \(n\) in the steps \(D\), \(F\), \(U\) (encoded as \(0\), \(1\), \(2\)), whose vertical displacements are \(-1\), \(0\) and \(+1\). For \(k \in \mathbb{N}\) and positions \(i, j \in \{0, \dots, n-1\}\), the pair \((i, j)\) is a hump of height \(k\) in \(p\) when \(i < j\), \(p_i = U\), \(p_j = D\), every \(p_r\) with \(i < r < j\) is \(F\), and the height after step \(i\), that is, the sum of the displacements of \(p_0, \dots, p_i\), equals \(k\).

public def IsMotzkinHump (n k : ℕ) (p : Fin n → Fin 3) (i j : Fin n) : Prop :=
  i.val < j.val ∧ motzkinStep (p i) = 1 ∧ motzkinStep (p j) = -1 ∧
  (∀ r : Fin n, i.val < r.val → r.val < j.val → motzkinStep (p r) = 0) ∧
  (∑ r : Fin n, if r.val ≤ i.val then motzkinStep (p r) else 0) = (k : ℤ)

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Section 1 (definitions).

Uses 1 · Used by 7

Statement usesHeight change of a Motzkin step

Used byCharacterization of Motzkin humps · Motzkin peak · Peaks are humps with adjacent endpoints · Number of humps of a given height in Motzkin paths · Humps of height one in Motzkin paths of length four · Motzkin paths with a marked hump, over all heights · Humps correspond to last-up prefixes of twice the height

TheoremUnfolding the Motzkin prefix condition#✓fully proved

Let \(p = p_0 p_1 \cdots p_{n-1}\) be a word of length \(n\) in the steps \(D\), \(F\), \(U\), whose vertical displacements are \(-1\), \(0\) and \(+1\), and let \(h \in \mathbb{Z}\). Then \(p\) is a Motzkin prefix ending at height \(h\) if and only if, for every natural number \(m \le n\), the sum of the displacements of \(p_0, \dots, p_{m-1}\) is nonnegative, and the sum of the displacements of all \(n\) steps is \(h\).

public theorem isMotzkinPrefix_iff (n : ℕ) (h : ℤ) (p : Fin n → Fin 3) :
    IsMotzkinPrefix n h p ↔
      (∀ m : ℕ, m ≤ n →
        0 ≤ ∑ i : Fin n, if i.val < m then motzkinStep (p i) else 0) ∧
      ∑ i : Fin n, motzkinStep (p i) = h

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Section 1 (definitions).

Uses 2

Statement usesMotzkin prefix · Height change of a Motzkin step

DefinitionBounded Motzkin prefix condition#✓fully proved

Let \(p = p_0 p_1 \cdots p_{n-1}\) be a word of length \(n\) in the steps \(D\), \(F\), \(U\) (encoded as \(0\), \(1\), \(2\)), whose vertical displacements are \(-1\), \(0\) and \(+1\), and let \(h \in \mathbb{Z}\). The word \(p\) satisfies the bounded Motzkin prefix condition for \(h\) when, for every \(m \in \{0, 1, \dots, n\}\), the sum of the displacements of \(p_0, \dots, p_{m-1}\) is nonnegative, and the sum of the displacements of all \(n\) steps is \(h\).

public def IsMotzkinPrefixFinite (n : ℕ) (h : ℤ) (p : Fin n → Fin 3) : Prop :=
  (∀ m : Fin (n + 1),
    0 ≤ ∑ i : Fin n, if i.val < m.val then motzkinStep (p i) else 0) ∧
  ∑ i : Fin n, motzkinStep (p i) = h

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Section 1 (definitions).

Uses 1 · Used by 3

Statement usesHeight change of a Motzkin step

Used byBounded form of the Motzkin prefix condition · Number of humps of a given height in Motzkin paths · Humps of height one in Motzkin paths of length four

TheoremBounded form of the Motzkin prefix condition#✓fully proved

Let \(p\) be a word of length \(n\) in the steps \(D\), \(F\), \(U\) and let \(h \in \mathbb{Z}\). Then \(p\) satisfies the bounded Motzkin prefix condition for \(h\), in which the prefix length \(m\) ranges over \(\{0, 1, \dots, n\}\), if and only if \(p\) is a Motzkin prefix ending at height \(h\), in which \(m\) ranges over all natural numbers with \(m \le n\).

public theorem isMotzkinPrefixFinite_iff (n : ℕ) (h : ℤ) (p : Fin n → Fin 3) :
    IsMotzkinPrefixFinite n h p ↔ IsMotzkinPrefix n h p

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Section 1 (definitions).

Uses 3 · Used by 2

Statement usesMotzkin prefix · Bounded Motzkin prefix condition

Proof usesHeight change of a Motzkin step

Used byNumber of humps of a given height in Motzkin paths · Humps of height one in Motzkin paths of length four

TheoremCharacterization of Motzkin humps#✓fully proved

Write a path of length \(n\) as a sequence of steps \(p_0, \dots, p_{n-1}\), and let \(s(p_r) \in \{-1, 0, 1\}\) be the vertical displacement of the step \(p_r\) (down, flat or up). For a natural number \(k\) and positions \(i, j < n\), the pair \((i, j)\) is a hump of height \(k\) if and only if \(i < j\), \(s(p_i) = 1\), \(s(p_j) = -1\), \(s(p_r) = 0\) for every \(r\) with \(i < r < j\), and \(\sum_{r \le i} s(p_r) = k\).

public theorem isMotzkinHump_iff (n k : ℕ) (p : Fin n → Fin 3) (i j : Fin n) :
    IsMotzkinHump n k p i j ↔
      i.val < j.val ∧ motzkinStep (p i) = 1 ∧ motzkinStep (p j) = -1 ∧
      (∀ r : Fin n, i.val < r.val → r.val < j.val → motzkinStep (p r) = 0) ∧
      (∑ r : Fin n, if r.val ≤ i.val then motzkinStep (p r) else 0) = (k : ℤ)

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Section 1 (definitions).

Uses 2

Statement usesMotzkin hump · Height change of a Motzkin step

DefinitionMotzkin peak#✓fully proved

Let \(p\) be a word of length \(n\) in the steps \(D\), \(F\), \(U\), let \(k \in \mathbb{N}\), and let \(i, j \in \{0, \dots, n-1\}\). The pair \((i, j)\) is a peak of height \(k\) in \(p\) when it is a hump of height \(k\) in \(p\) and \(j = i + 1\), that is, when the down step \(p_j\) immediately follows the up step \(p_i\).

public def IsMotzkinPeak (n k : ℕ) (p : Fin n → Fin 3) (i j : Fin n) : Prop :=
  IsMotzkinHump n k p i j ∧ i.val + 1 = j.val

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Section 1 (definitions).

Uses 1 · Used by 2

Statement usesMotzkin hump

Used byPeaks are humps with adjacent endpoints · Humps correspond to last-up prefixes of twice the height

TheoremPeaks are humps with adjacent endpoints#✓fully proved

Let \(p\) be a word of length \(n\) in the steps \(D\), \(F\), \(U\), let \(k \in \mathbb{N}\), and let \(i, j \in \{0, \dots, n-1\}\). Then \((i, j)\) is a peak of height \(k\) in \(p\) if and only if \((i, j)\) is a hump of height \(k\) in \(p\) and \(j = i + 1\).

public theorem isMotzkinPeak_iff (n k : ℕ) (p : Fin n → Fin 3) (i j : Fin n) :
    IsMotzkinPeak n k p i j ↔ IsMotzkinHump n k p i j ∧ i.val + 1 = j.val

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Section 1 (definitions).

Uses 2

Statement usesMotzkin hump · Motzkin peak

DefinitionPaths whose last non-flat step is up#✓fully proved

A word \(p = p_0 p_1 \cdots p_{n-1}\) of length \(n\) in the steps \(U\) (up), \(F\) (flat) and \(D\) (down) has last non-flat step up when some position \(i\) has \(p_i = U\) and every later step \(p_j\) with \(j > i\) is \(F\). In particular, such a word contains an up step.

Among the Motzkin prefixes of length \(n\) ending at height \(h\) (words that never go below height \(0\) and end at height \(h\)), these words form the paper's set \(\mathcal{M}^{*U}_{n,h}\).

public def LastNonflatStepUp (n : ℕ) (p : Fin n → Fin 3) : Prop :=
  ∃ i, p i = 2 ∧ ∀ j, i < j → p j = 1

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Section 1 (definitions).

Used by 3

Used byCharacterization of words whose last non-flat step is up · Humps correspond to last-up prefixes of twice the height · Motzkin prefixes of even height whose last non-flat step is up

TheoremCharacterization of words whose last non-flat step is up#✓fully proved

Let \(p = p_0 p_1 \cdots p_{n-1}\) be a word of length \(n\) in the steps \(D\), \(F\), \(U\). Then the last non-flat step of \(p\) is \(U\) if and only if there is a position \(i\) with \(p_i = U\) such that \(p_j = F\) for every position \(j > i\).

public theorem lastNonflatStepUp_iff (n : ℕ) (p : Fin n → Fin 3) :
    LastNonflatStepUp n p ↔ ∃ i, p i = 2 ∧ ∀ j, i < j → p j = 1

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Section 1 (definitions).

Uses 1

Statement usesPaths whose last non-flat step is up

DefinitionPaths whose first non-up step is down#✓fully proved

Write a path of length \(n\) as a sequence of steps \(p_0, \dots, p_{n-1}\), each \(D\) (down), \(F\) (flat) or \(U\) (up), encoded as \(0\), \(1\), \(2\). The path has first non-up step down when there is a position \(i\) with \(p_i = D\) and \(p_j = U\) for every \(j < i\). In particular, a path all of whose steps are up steps, including the empty path, does not qualify.

For a Motzkin prefix ending at height \(h\), this is membership in the paper's set \(\mathcal{M}^{D*}_{n,h}\).

public def FirstNonupStepDown (n : ℕ) (p : Fin n → Fin 3) : Prop :=
  ∃ i, p i = 0 ∧ ∀ j, j < i → p j = 2

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Section 1 (definitions).

Used by 2

Used byCharacterization of paths whose first non-up step is down · Motzkin prefixes whose first non-up step is down

TheoremCharacterization of paths whose first non-up step is down#✓fully proved

Write a path of length \(n\) as a sequence of steps \(p_0, \dots, p_{n-1}\), each \(D\) (down), \(F\) (flat) or \(U\) (up), encoded as \(0\), \(1\), \(2\). The path has first non-up step \(D\) if and only if there is a position \(i\) with \(p_i = D\) and \(p_j = U\) for every \(j < i\).

public theorem firstNonupStepDown_iff (n : ℕ) (p : Fin n → Fin 3) :
    FirstNonupStepDown n p ↔ ∃ i, p i = 0 ∧ ∀ j, j < i → p j = 2

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Section 1 (definitions).

Uses 1

Statement usesPaths whose first non-up step is down

DefinitionPaths ending with an up step#✓fully proved

Write a path of length \(n\) as a sequence of steps \(p_0, \dots, p_{n-1}\), each \(D\) (down), \(F\) (flat) or \(U\) (up), encoded as \(0\), \(1\), \(2\). The path ends with an up step when it has a last position, that is, some \(i < n\) with \(i + 1 = n\), and \(p_i = U\).

public def EndsWithUp (n : ℕ) (p : Fin n → Fin 3) : Prop :=
  ∃ i, i.val + 1 = n ∧ p i = 2

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Lemma 3 (jis-2025-25.8.1-lem-3).

Used by 2

Used byCharacterization of paths ending with an up step · Humps correspond to last-up prefixes of twice the height

TheoremCharacterization of paths ending with an up step#✓fully proved

Write a path of length \(n\) as a sequence of steps \(p_0, \dots, p_{n-1}\), each \(D\) (down), \(F\) (flat) or \(U\) (up), encoded as \(0\), \(1\), \(2\). The path ends with an up step if and only if there is a position \(i < n\) with \(i + 1 = n\) and \(p_i = U\).

public theorem endsWithUp_iff (n : ℕ) (p : Fin n → Fin 3) :
    EndsWithUp n p ↔ ∃ i, i.val + 1 = n ∧ p i = 2

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Lemma 3 (jis-2025-25.8.1-lem-3).

Uses 1

Statement usesPaths ending with an up step

DefinitionNumber of humps of a given height in Motzkin paths#✓fully proved

A Motzkin path of length \(n\) is a word of \(n\) steps \(U = (1,1)\), \(F = (1,0)\) and \(D = (1,-1)\) that ends at height \(0\) and never goes below height \(0\). A hump of height \(k\) in such a path is a pair consisting of an up step and a later down step with only flat steps between them, where the up step ends at height \(k\). For natural numbers \(n\) and \(k\), \(H_{n,k}\) is the number of pairs \((P, h)\) with \(P\) a Motzkin path of length \(n\) and \(h\) a hump of height \(k\) in \(P\), that is, the number of Motzkin paths of length \(n\) with one distinguished hump of height \(k\).

public def motzkinHumpCount (n k : ℕ) : ℕ :=
  Fintype.card {q : (Fin n → Fin 3) × Fin n × Fin n //
    IsMotzkinPrefix n 0 q.1 ∧ IsMotzkinHump n k q.1 q.2.1 q.2.2}

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Section 1 (definitions).

Uses 5 · Used by 3

Statement usesMotzkin hump · Motzkin prefix · Bounded Motzkin prefix condition · Bounded form of the Motzkin prefix condition · Height change of a Motzkin step

Used byHumps of height one in Motzkin paths of length four · Generating function for humps of a fixed height · Hook tableau counts as differences of hump counts

DefinitionMotzkin generating function#✓fully proved

The Motzkin series is the formal power series \(M(x) = \sum_{n \ge 0} m_n x^n\) in \(\mathbb{Z}[[x]]\), where \(m_n\) is the \(n\)-th Motzkin number.

public def motzkinSeries : PowerSeries ℤ :=
  PowerSeries.mk (fun n => (motzkinNumber n : ℤ))

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Section 1 (definitions).

Uses 1 · Used by 3

Statement usesMotzkin numbers as a Catalan-weighted binomial sum

Used byGenerating function for the adjusted \((2,1)\)-hook tableau counts · Generating function for humps of a fixed height · Generating function for hook tableau counts

DefinitionStandard Young tableau#✓fully proved

A standard Young tableau of order \(n\) is encoded by a map \(T\) that assigns to each entry \(i \in \{0, \dots, n-1\}\) a cell \(T(i) = (r_i, c_i)\) with row and column indices in \(\{0, \dots, n-1\}\). The map \(T\) is a standard Young tableau when it is injective and, for every entry \(i\) and every cell \((r, c)\) with \(r \le r_i\) and \(c \le c_i\), there is an entry \(j \le i\) with \(T(j) = (r, c)\).

It follows that for every \(m \le n\) the cells of the entries \(0, \dots, m-1\) form a Young diagram, and that entries increase strictly along rows and down columns.

public def IsStandardYoungTableau (n : ℕ) (T : Fin n → Fin n × Fin n) : Prop :=
  Function.Injective T ∧
    ∀ i c, c.1 ≤ (T i).1 → c.2 ≤ (T i).2 → ∃ j, j ≤ i ∧ T j = c

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Section 1 (definitions).

Used by 5

Used byUnfolding the standard Young tableau condition · Standard Young tableaux in the \((2,1)\)-hook with given row difference · Hook tableaux of order 3 with row difference 1 · Hook tableaux of order 3 with row difference 0 · Hook tableaux of order 2 with row difference 1

TheoremUnfolding the standard Young tableau condition#✓fully proved

Let \(T\) assign to each entry \(i \in \{0, \dots, n-1\}\) a cell \(T(i) = (r_i, c_i)\) with row and column indices in \(\{0, \dots, n-1\}\). Then \(T\) is a standard Young tableau of order \(n\) if and only if \(T\) is injective and, for every entry \(i\) and every cell \((r, c)\) with \(r \le r_i\) and \(c \le c_i\), there is an entry \(j \le i\) with \(T(j) = (r, c)\).

public theorem isStandardYoungTableau_iff (n : ℕ) (T : Fin n → Fin n × Fin n) :
    IsStandardYoungTableau n T ↔
      Function.Injective T ∧
        ∀ i c, c.1 ≤ (T i).1 → c.2 ≤ (T i).2 → ∃ j, j ≤ i ∧ T j = c

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Section 1 (definitions).

Uses 1

Statement usesStandard Young tableau

DefinitionTableaux in the \((2,1)\)-hook#✓fully proved

Let \(T\) assign to each entry \(i < n\) a cell \((r_i, c_i)\) with zero-based row \(r_i < n\) and column \(c_i < n\). Then \(T\) lies in the \((2,1)\)-hook when no entry occupies a cell whose row is at least \(2\) and whose column is at least \(1\), that is, when no \(i\) has both \(r_i \ge 2\) and \(c_i \ge 1\).

public def IsInTwoOneHook (n : ℕ) (T : Fin n → Fin n × Fin n) : Prop :=
  ∀ i, ¬(2 ≤ (T i).1.val ∧ 1 ≤ (T i).2.val)

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Section 1 (definitions).

Used by 5

Used byCharacterization of tableaux in the \((2,1)\)-hook · Standard Young tableaux in the \((2,1)\)-hook with given row difference · Hook tableaux of order 3 with row difference 1 · Hook tableaux of order 3 with row difference 0 · Hook tableaux of order 2 with row difference 1

TheoremCharacterization of tableaux in the \((2,1)\)-hook#✓fully proved

Let \(T\) assign to each entry \(i < n\) a cell \((r_i, c_i)\) with zero-based row \(r_i < n\) and column \(c_i < n\). Then \(T\) lies in the \((2,1)\)-hook if and only if for no entry \(i\) do both \(r_i \ge 2\) and \(c_i \ge 1\) hold.

public theorem isInTwoOneHook_iff (n : ℕ) (T : Fin n → Fin n × Fin n) :
    IsInTwoOneHook n T ↔ ∀ i, ¬(2 ≤ (T i).1.val ∧ 1 ≤ (T i).2.val)

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Section 1 (definitions).

Uses 1

Statement usesTableaux in the \((2,1)\)-hook

DefinitionRow length of a tableau#✓fully proved

For a natural number \(n\), let \(T\) assign to each entry \(i \in \{0, \dots, n-1\}\) a cell \(T(i)\), given by a zero-based row index and a zero-based column index, both in \(\{0, \dots, n-1\}\). For a natural number \(r\), the length of row \(r\) is the number of entries \(i\) whose cell \(T(i)\) lies in row \(r\).

public def tableauRowLength (n : ℕ) (T : Fin n → Fin n × Fin n) (r : ℕ) : ℕ :=
  (Finset.univ.filter fun i => (T i).1.val = r).card

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Section 1 (definitions).

Used by 6

Used byFirst-two-row difference of a tableau · Characterization of the first-two-row difference · Standard Young tableaux in the \((2,1)\)-hook with given row difference · Hook tableaux of order 3 with row difference 1 · Hook tableaux of order 3 with row difference 0 · Hook tableaux of order 2 with row difference 1

DefinitionFirst-two-row difference of a tableau#✓fully proved

Let \(T\) assign to each entry \(i < n\) a cell \((r_i, c_i)\) with zero-based row \(r_i < n\) and column \(c_i < n\), and let \(\lambda_1\) and \(\lambda_2\) be the numbers of entries \(i\) with \(r_i = 0\) and with \(r_i = 1\) respectively. For a natural number \(k\), \(T\) has first-two-row difference \(k\) when \(\lambda_1 = \lambda_2 + k\), that is, when \(\lambda_1 - \lambda_2 = k\).

public def HasFirstTwoRowDifference (n k : ℕ) (T : Fin n → Fin n × Fin n) : Prop :=
  tableauRowLength n T 0 = tableauRowLength n T 1 + k

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Section 1 (definitions).

Uses 1 · Used by 5

Statement usesRow length of a tableau

Used byCharacterization of the first-two-row difference · Standard Young tableaux in the \((2,1)\)-hook with given row difference · Hook tableaux of order 3 with row difference 1 · Hook tableaux of order 3 with row difference 0 · Hook tableaux of order 2 with row difference 1

TheoremCharacterization of the first-two-row difference#✓fully proved

Let \(T\) assign to each entry \(i < n\) a cell \((r_i, c_i)\) with zero-based row \(r_i < n\) and column \(c_i < n\), and let \(\lambda_1\) and \(\lambda_2\) be the numbers of entries \(i\) with \(r_i = 0\) and with \(r_i = 1\) respectively. For a natural number \(k\), \(T\) has first-two-row difference \(k\) if and only if \(\lambda_1 = \lambda_2 + k\).

public theorem hasFirstTwoRowDifference_iff (n k : ℕ) (T : Fin n → Fin n × Fin n) :
    HasFirstTwoRowDifference n k T ↔
      tableauRowLength n T 0 = tableauRowLength n T 1 + k

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Section 1 (definitions).

Uses 2

Statement usesFirst-two-row difference of a tableau · Row length of a tableau

DefinitionStandard Young tableaux in the \((2,1)\)-hook with given row difference#✓fully proved

For natural numbers \(n\) and \(k\), \(\mathrm{SYT}_k(2,1;n)\) is the number of standard Young tableaux of order \(n\) whose shape \(\lambda\) lies in the \((2,1)\)-hook, that is \(\lambda_3 \le 1\), and whose first two row lengths satisfy \(\lambda_1 = \lambda_2 + k\) (a missing row has length \(0\)).

public def sytHookCount (n k : ℕ) : ℕ :=
  Fintype.card {T : Fin n → Fin n × Fin n //
    IsStandardYoungTableau n T ∧ IsInTwoOneHook n T ∧ HasFirstTwoRowDifference n k T}

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Section 1 (definitions).

Uses 4 · Used by 7

Statement usesFirst-two-row difference of a tableau · Tableaux in the \((2,1)\)-hook · Standard Young tableau · Row length of a tableau

Used byGenerating function for the adjusted \((2,1)\)-hook tableau counts · Hook tableau counts as differences of hump counts · Closed formula for hook tableau counts · Generating function for hook tableau counts · Hook tableaux of order 3 with row difference 1 · Hook tableaux of order 3 with row difference 0 · Hook tableaux of order 2 with row difference 1

DefinitionMotzkin paths with a marked hump, over all heights#✓fully proved

For a natural number \(n\), this is the set of triples \((k, P, h)\) where \(k\) is a natural number with \(1 \le k \le \lfloor n/2 \rfloor\), \(P\) is a Motzkin path of length \(n\) (a word of \(n\) steps \(U = (1,1)\), \(F = (1,0)\) and \(D = (1,-1)\) that ends at height \(0\) and never goes below height \(0\)), and \(h\) is a hump of height \(k\) in \(P\): an up step and a later down step with only flat steps between them, where the up step ends at height \(k\), recorded by the positions of its two steps.

This is the paper's disjoint union \(\bigcup_{1 \le k \le \lfloor n/2 \rfloor} \mathcal{H}_{n,k}\), keeping the height index \(k\) with each marked path.

public def MotzkinHumpFamily (n : ℕ) :=
  {q : ℕ × ((Fin n → Fin 3) × Fin n × Fin n) //
    1 ≤ q.1 ∧ q.1 ≤ n / 2 ∧ IsMotzkinPrefix n 0 q.2.1 ∧
      IsMotzkinHump n q.1 q.2.1 q.2.2.1 q.2.2.2}

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Lemma 3 (jis-2025-25.8.1-lem-3).

Uses 2 · Used by 1

Statement usesMotzkin hump · Motzkin prefix

Used byHumps correspond to last-up prefixes of twice the height

DefinitionMotzkin prefixes of even height whose last non-flat step is up#✓fully proved

Use the steps \(U = (1,1)\), \(F = (1,0)\) and \(D = (1,-1)\), and call a word in these steps a Motzkin prefix if none of its initial segments ends below height \(0\). For a natural number \(n\), this is the set of pairs \((k, p)\) where \(k\) is a natural number with \(1 \le k \le \lfloor n/2 \rfloor\) and \(p\) is a Motzkin prefix of length \(n\) ending at height \(2k\) that contains a \(U\) after which every step is \(F\).

This is the paper's disjoint union \(\bigcup_{1 \le k \le \lfloor n/2 \rfloor} \mathcal{M}^{*U}_{n,2k}\), keeping the index \(k\) with each path.

public def MotzkinLastUpEvenFamily (n : ℕ) :=
  {q : ℕ × (Fin n → Fin 3) //
    1 ≤ q.1 ∧ q.1 ≤ n / 2 ∧ IsMotzkinPrefix n (2 * q.1) q.2 ∧
      LastNonflatStepUp n q.2}

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Lemma 3 (jis-2025-25.8.1-lem-3).

Uses 2 · Used by 2

Statement usesMotzkin prefix · Paths whose last non-flat step is up

Used byA bijection between first-down and even-height last-up Motzkin prefixes · Humps correspond to last-up prefixes of twice the height

DefinitionMotzkin prefixes whose first non-up step is down#✓fully proved

Use the steps \(U = (1,1)\), \(F = (1,0)\) and \(D = (1,-1)\), and call a word in these steps a Motzkin prefix if none of its initial segments ends below height \(0\). For a natural number \(n\), this is the set of pairs \((k, p)\) where \(k\) is a natural number with \(k \le n - 2\) and \(p\) is a Motzkin prefix of length \(n\) ending at height \(k\) whose first step other than \(U\) exists and is \(D\).

This is the paper's disjoint union \(\bigcup_{0 \le k \le n-2} \mathcal{M}^{D*}_{n,k}\), keeping the index \(k\) with each path.

public def MotzkinFirstDownFamily (n : ℕ) :=
  {q : ℕ × (Fin n → Fin 3) //
    q.1 + 2 ≤ n ∧ IsMotzkinPrefix n q.1 q.2 ∧ FirstNonupStepDown n q.2}

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Lemma 6 (jis-2025-25.8.1-lem-6).

Uses 2 · Used by 1

Statement usesPaths whose first non-up step is down · Motzkin prefix

Used byA bijection between first-down and even-height last-up Motzkin prefixes

TheoremHook tableaux of order 3 with row difference 1#✓fully proved

The number \(\mathrm{SYT}_1(2,1;3)\) of standard Young tableaux of order \(3\) in the \((2,1)\)-hook whose first row is longer than its second row by exactly \(1\) equals \(2\).

public theorem sytHookCount_three_one : sytHookCount 3 1 = 2

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Initial-values table.

Uses 5

Statement usesStandard Young tableaux in the \((2,1)\)-hook with given row difference

Proof usesFirst-two-row difference of a tableau · Tableaux in the \((2,1)\)-hook · Standard Young tableau · Row length of a tableau

TheoremHook tableaux of order 3 with row difference 0#✓fully proved

The number \(\mathrm{SYT}_0(2,1;3)\) of standard Young tableaux of order \(3\) in the \((2,1)\)-hook whose first two rows have the same length equals \(1\).

public theorem sytHookCount_three_zero : sytHookCount 3 0 = 1

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Initial-values table.

Uses 5

Statement usesStandard Young tableaux in the \((2,1)\)-hook with given row difference

Proof usesFirst-two-row difference of a tableau · Tableaux in the \((2,1)\)-hook · Standard Young tableau · Row length of a tableau

TheoremHook tableaux of order 2 with row difference 1#✓fully proved

The number \(\mathrm{SYT}_1(2,1;2)\) of standard Young tableaux of order \(2\) in the \((2,1)\)-hook whose first row is longer than its second row by exactly \(1\) equals \(0\).

public theorem sytHookCount_two_one : sytHookCount 2 1 = 0

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Initial-values table.

Uses 5

Statement usesStandard Young tableaux in the \((2,1)\)-hook with given row difference

Proof usesFirst-two-row difference of a tableau · Tableaux in the \((2,1)\)-hook · Standard Young tableau · Row length of a tableau

TheoremHumps of height one in Motzkin paths of length four#✓fully proved

Let \(H_{n,k}\) be the number of pairs \((P, h)\) where \(P\) is a Motzkin path of length \(n\) and \(h\) is a hump of height \(k\) in \(P\), that is, an up step and a later down step with only flat steps between them, where the up step ends at height \(k\). Then \(H_{4,1} = 8\).

public theorem motzkinHumpCount_four_one : motzkinHumpCount 4 1 = 8

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Hump-count table.

Uses 6

Statement usesNumber of humps of a given height in Motzkin paths

Proof usesMotzkin hump · Motzkin prefix · Bounded Motzkin prefix condition · Bounded form of the Motzkin prefix condition · Height change of a Motzkin step

TheoremClosed formula for hook tableau counts#●ready to prove

For natural numbers \(n\) and \(k\) with \(k + 2 \le n\), let \(\mathrm{SYT}_k(2,1;n)\) be the number of standard Young tableaux of order \(n\) in the \((2,1)\)-hook whose first row is longer than its second row by exactly \(k\). Then, as an identity of rational numbers,

\[ \mathrm{SYT}_k(2,1;n) = (-1)^{n+k} + \sum_{i=0}^{\lfloor (n-k-1)/2 \rfloor} \sum_{\substack{0 \le j \le n-k-1-2i \\ j \equiv n+k-1 \pmod 2}} \frac{2k+2}{n+k+1-2i-j} \binom{n-2i-2}{j} \binom{n-2i-j-1}{\frac{n+k-j-1}{2} - i}. \]

When \(k = 0\) and \(2i = n - 1\), the upper argument \(n - 2i - 2\) would be \(-1\); it is read as \(0\), so the only term of that inner sum, \(j = 0\), has binomial factor \(\binom{0}{0} = 1\).

public theorem_wanted sytHookCount_closedForm (n k : ℕ) (hk : k + 2 ≤ n) :
    (sytHookCount n k : ℚ) =
      (-1 : ℚ) ^ (n + k) +
        ∑ i ∈ Finset.range ((n - k - 1) / 2 + 1),
          ∑ j ∈ Finset.range (n - k - 1 - 2 * i + 1),
            (if j % 2 = (n + k - 1) % 2 then (1 : ℚ) else 0) *
              ((2 * k + 2 : ℕ) : ℚ) / ((n + k + 1 - 2 * i - j : ℕ) : ℚ) *
              (Nat.choose (n - 2 * i - 2) j : ℚ) *
              (Nat.choose (n - 2 * i - j - 1) ((n + k - j - 1) / 2 - i) : ℚ)

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Theorem 2 (jis-2025-25.8.1-thm-2).

Uses 1

Statement usesStandard Young tableaux in the \((2,1)\)-hook with given row difference

TheoremHumps correspond to last-up prefixes of twice the height#●ready to prove

Use the steps \(U = (1,1)\), \(F = (1,0)\) and \(D = (1,-1)\). A Motzkin prefix of length \(n\) ending at height \(h\) is a word of \(n\) steps that never goes below height \(0\) and ends at height \(h\); a Motzkin path is a Motzkin prefix ending at height \(0\). A hump of height \(k\) in a path is a pair of an up step and a later down step with only flat steps between them, where the up step ends at height \(k\); the hump is a peak when the down step immediately follows the up step. For every natural number \(n\) there is a bijection from the set of triples \((k, P, h)\) with \(1 \le k \le \lfloor n/2 \rfloor\), \(P\) a Motzkin path of length \(n\) and \(h\) a hump of height \(k\) in \(P\), to the set of pairs \((k, p)\) with \(1 \le k \le \lfloor n/2 \rfloor\) and \(p\) a Motzkin prefix of length \(n\) ending at height \(2k\) that contains a \(U\) after which every step is \(F\). This bijection keeps the index \(k\), and the hump \(h\) is a peak exactly when the image path \(p\) ends with an up step.

public theorem_wanted motzkinHumpFamily_equiv_lastUpEvenFamily (n : ℕ) :
    ∃ e : MotzkinHumpFamily n ≃ MotzkinLastUpEvenFamily n,
      (∀ q, (e q).val.1 = q.val.1) ∧
        ∀ q, IsMotzkinPeak n q.val.1 q.val.2.1 q.val.2.2.1 q.val.2.2.2 ↔
          EndsWithUp n (e q).val.2

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Lemma 3 (jis-2025-25.8.1-lem-3).

Uses 7

Statement usesPaths ending with an up step · Motzkin hump · Motzkin peak · Motzkin prefix · Paths whose last non-flat step is up · Motzkin paths with a marked hump, over all heights · Motzkin prefixes of even height whose last non-flat step is up

TheoremGenerating function for humps of a fixed height#●ready to prove

Let \(H_{n,k}\) be the number of pairs \((P, h)\) where \(P\) is a Motzkin path of length \(n\) and \(h\) is a hump of height \(k\) in \(P\) (an up step and a later down step with only flat steps between them, the up step ending at height \(k\)), and let \(M(x) = \sum_{n \ge 0} m_n x^n\), where \(m_n\) is the \(n\)-th Motzkin number. For every integer \(k \ge 1\), in the ring \(\mathbb{Z}[[x]]\) of formal power series,

\[(1 - x) \sum_{n \ge 2k} H_{n,k} \, x^n = x^{2k} M(x)^{2k}.\]

The source also states this result in Riordan-array form.

public theorem_wanted motzkinHumpCount_generatingFunction (k : ℕ) (hk : 1 ≤ k) :
    (1 - (PowerSeries.X : PowerSeries ℤ)) *
        PowerSeries.mk (fun n => if 2 * k ≤ n then (motzkinHumpCount n k : ℤ) else 0) =
      PowerSeries.X ^ (2 * k) * motzkinSeries ^ (2 * k)

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Corollary 5 (jis-2025-25.8.1-cor-5).

Uses 2

Statement usesNumber of humps of a given height in Motzkin paths · Motzkin generating function

TheoremA bijection between first-down and even-height last-up Motzkin prefixes#●ready to prove

Use the steps \(U = (1,1)\), \(F = (1,0)\) and \(D = (1,-1)\), and call a word in these steps a Motzkin prefix if none of its initial segments ends below height \(0\). For every natural number \(n\) there is a bijection between the set of pairs \((k, p)\), where \(k\) is a natural number with \(k + 2 \le n\) and \(p\) is a Motzkin prefix of length \(n\) ending at height \(k\) whose first step other than \(U\) exists and is \(D\), and the set of pairs \((k, p)\), where \(k\) is a natural number with \(1 \le k \le \lfloor n/2 \rfloor\) and \(p\) is a Motzkin prefix of length \(n\) ending at height \(2k\) that contains a \(U\) after which every step is \(F\).

public theorem_wanted motzkinFirstDownFamily_equiv_lastUpEvenFamily (n : ℕ) :
    Nonempty (MotzkinFirstDownFamily n ≃ MotzkinLastUpEvenFamily n)

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Lemma 6 (jis-2025-25.8.1-lem-6).

Uses 2

Statement usesMotzkin prefixes whose first non-up step is down · Motzkin prefixes of even height whose last non-flat step is up

TheoremGenerating function for the adjusted \((2,1)\)-hook tableau counts#●ready to prove

Let \(k\) be a natural number, and let \(\mathrm{SYT}_k(2,1;n)\) be the number of standard Young tableaux with \(n\) cells in the \((2,1)\)-hook whose first two rows differ in length by \(k\). Set \(T_{n,k} = \mathrm{SYT}_k(2,1;n) + (-1)^{n+k+1}\) for \(n \ge k\) and \(T_{n,k} = 0\) for \(n < k\), and let \(M(x) = \sum_{n \ge 0} m_n x^n\) be the generating function of the Motzkin numbers \(m_n\). Then in the ring \(\mathbb{Z}[[x]]\) of formal power series

\[(1 + x) \sum_{n \ge 0} T_{n,k} x^n = (x M(x))^{k+1}.\]

Equivalently, \(\sum_{n \ge k} T_{n,k} x^n = x^{k+1} M(x)^{k+1} / (1 + x)\); the identity is stated without division.

public theorem_wanted adjustedSytHookCount_generatingFunction (k : ℕ) :
    (1 + (PowerSeries.X : PowerSeries ℤ)) *
        PowerSeries.mk (fun n =>
          if k ≤ n then (sytHookCount n k : ℤ) + (-1 : ℤ) ^ (n + k + 1) else 0) =
      (PowerSeries.X * motzkinSeries) ^ (k + 1)

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Lemma 7 (jis-2025-25.8.1-lem-7).

Uses 2

Statement usesMotzkin generating function · Standard Young tableaux in the \((2,1)\)-hook with given row difference

TheoremGenerating function for hook tableau counts#●ready to prove

For a natural number \(k\), let \(\mathrm{SYT}_k(2,1;n)\) be the number of standard Young tableaux of order \(n\) in the \((2,1)\)-hook whose first row is longer than its second row by exactly \(k\), and let \(M(x) = \sum_{n \ge 0} m_n x^n\) be the generating function of the Motzkin numbers \(m_n\). Then, in the ring of formal power series with integer coefficients,

\[ (1 + x) \sum_{n \ge k} \mathrm{SYT}_k(2,1;n)\, x^n = x^k \bigl(1 + x\, M(x)^{k+1}\bigr). \]

The factor \(1 + x\) is cleared, so the identity involves no division.

public theorem_wanted sytHookCount_generatingFunction (k : ℕ) :
    (1 + (PowerSeries.X : PowerSeries ℤ)) *
        PowerSeries.mk (fun n => if k ≤ n then (sytHookCount n k : ℤ) else 0) =
      PowerSeries.X ^ k * (1 + PowerSeries.X * motzkinSeries ^ (k + 1))

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Corollary 9 (jis-2025-25.8.1-cor-9).

Uses 2

Statement usesMotzkin generating function · Standard Young tableaux in the \((2,1)\)-hook with given row difference

TheoremHook tableau counts as differences of hump counts#●ready to prove

For natural numbers \(m\) and \(j\), let \(\mathrm{SYT}_j(2,1;m)\) be the number of standard Young tableaux of order \(m\) in the \((2,1)\)-hook whose first row is longer than its second row by exactly \(j\), and let \(H_{m,j}\) be the number of Motzkin paths of length \(m\) with one distinguished hump of height \(j\) (a hump is an up step followed by flat steps and then a down step; its height is the height reached by the up step). For natural numbers \(n\) and \(k\) with \(1 \le k \le \lfloor n/2 \rfloor\),

\[ \mathrm{SYT}_{2k-1}(2,1;n+1) + \mathrm{SYT}_{2k-1}(2,1;n) = H_{n+1,k} - H_{n,k}, \]

where the subtraction is taken in the integers.

public theorem_wanted sytHookCount_add_eq_humpCount_sub (n k : ℕ)
    (hk : 1 ≤ k) (hkn : k ≤ n / 2) :
    (sytHookCount (n + 1) (2 * k - 1) : ℤ) + (sytHookCount n (2 * k - 1) : ℤ) =
      (motzkinHumpCount (n + 1) k : ℤ) - (motzkinHumpCount n k : ℤ)

Sources

• Xiaomei Chen, Humps in Motzkin Paths and Standard Young Tableaux in a (2,1)-Hook, Journal of Integer Sequences 28 (2025), Article 25.8.1, Corollary 10 (jis-2025-25.8.1-cor-10).

Uses 2

Statement usesNumber of humps of a given height in Motzkin paths · Standard Young tableaux in the \((2,1)\)-hook with given row difference

33 fully proved7 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.