Hasse Walk Length Formula (Theorem 8.6)

This file formalizes Theorem 8.6 from Stanley's Algebraic Combinatorics: the formula for the number of Hasse walks of length ℓ from ∅ to a partition λ ⊢ n in Young's lattice.

Main results

• HasseWalkFormula.bijCoeff_n_0_eq: Specialization of Lemma 8.5 at j = 0: b_{n,0}(ℓ) = C(ℓ,n) · (ℓ-n-1)!! when n ≤ ℓ and ℓ - n is even.
• HasseWalkFormula.hasseWalkCount_formula (Theorem 8.6): β(ℓ, λ) = C(ℓ,n) · (ℓ-n-1)!! · f^λ.

References

• Stanley, Algebraic Combinatorics, Section 8 (Theorem 8.6)

Definitions

noncomputable def HasseWalkFormula.numSYT (lam : YoungDiagram) : ℕ

The number of standard Young tableaux of shape λ, denoted f^λ in the book. This equals the number of saturated chains from ∅ to λ in Young's lattice.

noncomputable def HasseWalkFormula.hasseWalkCount (ell : ℕ) (lam : YoungDiagram) : ℕ

The number of Hasse walks of length ℓ from ∅ to λ in Young's lattice, denoted β(ℓ, λ) in the book. Each consecutive pair in the walk is related by a covering relation (either up or down).

theorem HasseWalkFormula.hasseWalk_card_parity {ell : ℕ} (walk : Fin (ell + 1) → YoungDiagram) (hstart : walk ⟨0, ⋯⟩ = ⊥) (hstep : ∀ (i : Fin ell), walk ⟨↑i, ⋯⟩ ⋖ walk ⟨↑i + 1, ⋯⟩ ∨ walk ⟨↑i + 1, ⋯⟩ ⋖ walk ⟨↑i, ⋯⟩) (k : ℕ) (hk : k ≤ ell) : (walk ⟨k, ⋯⟩).card % 2 = k % 2

Helper: in a Hasse walk from ⊥, the cardinality at position k has parity k. Each step changes cardinality by ±1 (via card_covBy_succ), so starting from card 0, the parity of walk(k).card equals the parity of k.

theorem HasseWalkFormula.hasseWalkCount_parity (ell : ℕ) (lam : YoungDiagram) (h : ell % 2 ≠ lam.card % 2) : hasseWalkCount ell lam = 0

(F1) β(ℓ, λ) = 0 unless ℓ ≡ |λ| (mod 2). Each Hasse walk step changes the diagram's cardinality by ±1, so after ℓ steps from ∅ (card 0) the endpoint must have the same parity as ℓ.

noncomputable def HasseWalkFormula.upWalkCount (n : ℕ) (lam : YoungDiagram) : ℕ

The number of Hasse walks of length n from ∅ to λ that use only up-steps (i.e., each step is a cover relation going up in Young's lattice). Unlike numSYT, this is parameterized by an explicit walk length n and target λ, so it counts up-walks of any specified length. When n = |λ| the count coincides with numSYT λ.

theorem HasseWalkFormula.upWalk_card_eq {n : ℕ} (walk : Fin (n + 1) → YoungDiagram) (hstart : walk ⟨0, ⋯⟩ = ⊥) (hstep : ∀ (j : Fin n), walk ⟨↑j, ⋯⟩ ⋖ walk ⟨↑j + 1, ⋯⟩) (k : ℕ) (hk : k ≤ n) : (walk ⟨k, ⋯⟩).card = k

In an up-walk from ⊥, the diagram at position k has cardinality k.

theorem HasseWalkFormula.upWalkCount_eq_zero_of_ne (i : ℕ) (lam : YoungDiagram) (h : i ≠ lam.card) : upWalkCount i lam = 0

An up-walk of length i from ⊥ reaches a diagram of card i. If i ≠ λ.card, there are no such walks, so upWalkCount i λ = 0.

theorem HasseWalkFormula.upWalkCount_eq_numSYT (lam : YoungDiagram) : ↑(upWalkCount lam.card lam) = ↑(numSYT lam)

upWalkCount lam.card lam and numSYT lam count the same set: saturated chains from ⊥ to lam in Young's lattice. The definitions are identical when the walk length parameter n equals lam.card.

def HasseWalkFormula.HasseWalkType (n : ℕ) (lam : YoungDiagram) : Type

The walk type for hasseWalkCount n lam.

theorem HasseWalkFormula.hasseWalkCount_eq_card' (n : ℕ) (lam : YoungDiagram) : hasseWalkCount n lam = Nat.card (HasseWalkType n lam)

theorem HasseWalkFormula.hasseWalk_card_le {m : ℕ} (walk : Fin (m + 1) → YoungDiagram) (hstart : walk ⟨0, ⋯⟩ = ⊥) (hstep : ∀ (i : Fin m), walk ⟨↑i, ⋯⟩ ⋖ walk ⟨↑i + 1, ⋯⟩ ∨ walk ⟨↑i + 1, ⋯⟩ ⋖ walk ⟨↑i, ⋯⟩) (k : ℕ) (hk : k ≤ m) : (walk ⟨k, ⋯⟩).card ≤ k

In a Hasse walk from ⊥, the diagram at position k has card ≤ k.

theorem HasseWalkFormula.yd_cell_bounded (yd : YoungDiagram) (i j : ℕ) (h : (i, j) ∈ yd.cells) : i < yd.card ∧ j < yd.card

Cells of a YoungDiagram are bounded by its card.

theorem HasseWalkFormula.yd_cells_sub_grid {yd : YoungDiagram} {n : ℕ} (hn : yd.card ≤ n) : yd.cells ⊆ Finset.range n ×ˢ Finset.range n

Cells of a bounded-card diagram lie in a bounded grid.

instance HasseWalkFormula.yd_bounded_finite (n : ℕ) : Finite { yd : YoungDiagram // yd.card ≤ n }

Young diagrams with bounded card form a finite type.

theorem HasseWalkFormula.hasseWalkType_cells_bounded {m : ℕ} (w : Fin (m + 1) → YoungDiagram) (h0 : w ⟨0, ⋯⟩ = ⊥) (hs : ∀ (i : Fin m), w ⟨↑i, ⋯⟩ ⋖ w ⟨↑i + 1, ⋯⟩ ∨ w ⟨↑i + 1, ⋯⟩ ⋖ w ⟨↑i, ⋯⟩) (k : Fin (m + 1)) : (w k).cells ⊆ Finset.range m ×ˢ Finset.range m

In a Hasse walk from ⊥ to lam of length m, every position has cells ⊆ grid of size m.

instance HasseWalkFormula.hasseWalkType_finite (m : ℕ) (lam : YoungDiagram) : Finite (HasseWalkType m lam)

The walk type HasseWalkType m lam is finite for every m and lam.

theorem HasseWalkFormula.hasseWalkCount_succ_eq_finset_sum_DU (n : ℕ) (lam : YoungDiagram) (ih : ∀ (μ : YoungDiagram), ↑(hasseWalkCount n μ) = (((WalkCountFormula.liftD + WalkCountFormula.liftU) ^ n) WalkCountFormula.emptyBasis) μ) : ↑(hasseWalkCount (n + 1) lam) = ((WalkCountFormula.liftD + WalkCountFormula.liftU) (((WalkCountFormula.liftD + WalkCountFormula.liftU) ^ n) WalkCountFormula.emptyBasis)) lam

theorem HasseWalkFormula.hasseWalkCount_eq_DplusU_pow_apply (ell : ℕ) (lam : YoungDiagram) : ↑(hasseWalkCount ell lam) = (((WalkCountFormula.liftD + WalkCountFormula.liftU) ^ ell) WalkCountFormula.emptyBasis) lam

(F2): β(ℓ, λ) is the coefficient of λ in (D+U)^ℓ(∅).

theorem YoungDiagram.covBy_of_mem_coversUp {μ ν : YoungDiagram} (h : ν ∈ μ.coversUp) : μ ⋖ ν

If ν ∈ μ.coversUp then μ ⋖ ν in Young's lattice. Each element of coversUp is obtained by adding one cell, which produces a covering.

theorem YoungDiagram.mem_coversUp_of_covBy {μ ν : YoungDiagram} (hcov : μ ⋖ ν) : ν ∈ μ.coversUp

If μ ⋖ ν in Young's lattice then ν ∈ μ.coversUp. A covering in the poset must correspond to adding a single cell.

theorem YoungDiagram.covBy_iff_mem_coversUp (μ ν : YoungDiagram) : μ ⋖ ν ↔ ν ∈ μ.coversUp

μ ⋖ ν ↔ ν ∈ μ.coversUp in Young's lattice.

theorem YoungDiagram.covBy_of_mem_coversDown {μ ν : YoungDiagram} (h : μ ∈ ν.coversDown) : μ ⋖ ν

If μ ∈ ν.coversDown then μ ⋖ ν in Young's lattice. Each element of coversDown is obtained by removing one cell, which produces a covering from below.

theorem YoungDiagram.mem_coversDown_of_covBy {μ ν : YoungDiagram} (hcov : μ ⋖ ν) : μ ∈ ν.coversDown

If μ ⋖ ν in Young's lattice then μ ∈ ν.coversDown. A covering from below corresponds to removing a single cell.

theorem YoungDiagram.covBy_iff_mem_coversDown (μ ν : YoungDiagram) : μ ⋖ ν ↔ μ ∈ ν.coversDown

μ ⋖ ν ↔ μ ∈ ν.coversDown in Young's lattice.

theorem WalkCountFormula.iterU_emptyBasis_support_card (i : ℕ) (lam : YoungDiagram) (hlam : lam.card ≠ i) : ((iterU i) emptyBasis) lam = 0

iterU i emptyBasis is supported on diagrams of cardinality i.

Walk decomposition by penultimate step

Walks of length n+2 from ⊥ to lam biject with pairs (μ, walk of length n+1 from ⊥ to μ) where μ ⋖ lam. The book treats this as immediate from the definition of up-walks.

def HasseWalkFormula.UpWalkType (n : ℕ) (lam : YoungDiagram) : Type

The walk type for upWalkCount n lam.

theorem HasseWalkFormula.upWalkCount_eq_card (n : ℕ) (lam : YoungDiagram) : upWalkCount n lam = Nat.card (UpWalkType n lam)

theorem HasseWalkFormula.upWalkType_cells_subset {m : ℕ} {mu : YoungDiagram} (w : Fin (m + 1) → YoungDiagram) (_h0 : w ⟨0, ⋯⟩ = ⊥) (hs : ∀ (i : Fin m), w ⟨↑i, ⋯⟩ ⋖ w ⟨↑i + 1, ⋯⟩) (he : w ⟨m, ⋯⟩ = mu) (k : Fin (m + 1)) : (w k).cells ⊆ mu.cells

In an up-walk from ⊥ to mu, every position has cells ⊆ mu.cells.

instance HasseWalkFormula.upWalkType_finite (m : ℕ) (mu : YoungDiagram) : Finite (UpWalkType m mu)

The walk type UpWalkType m mu is finite for every m and mu.

theorem HasseWalkFormula.upWalkCount_succ_eq_finset_sum (n : ℕ) (lam : YoungDiagram) (hlam : n + 1 = lam.card) (ih : ∀ (μ : YoungDiagram), n = μ.card → ↑(upWalkCount n μ) = ((WalkCountFormula.iterU n) WalkCountFormula.emptyBasis) μ) : ↑(upWalkCount (n + 1) lam) = ∑ μ ∈ ((WalkCountFormula.iterU n) WalkCountFormula.emptyBasis).support, if μ ⋖ lam then ↑(upWalkCount n μ) else 0

theorem HasseWalkFormula.upWalkCount_eq_iterU_apply (i : ℕ) (lam : YoungDiagram) : ↑(upWalkCount i lam) = ((WalkCountFormula.iterU i) WalkCountFormula.emptyBasis) lam

theorem HasseWalkFormula.DplusU_pow_emptyBasis_eq_sum_bijCoeff_iterU (ell : ℕ) (lam : YoungDiagram) : ↑((((WalkCountFormula.liftD + WalkCountFormula.liftU) ^ ell) WalkCountFormula.emptyBasis) lam) = ∑ i ∈ Finset.range (ell + 1), NormalOrderCoeff.bijCoeff i 0 ell * ↑(((WalkCountFormula.iterU i) WalkCountFormula.emptyBasis) lam)

theorem HasseWalkFormula.hasseWalkCount_eq_sum_bijCoeff_upWalkCount (ell : ℕ) (lam : YoungDiagram) : ↑(hasseWalkCount ell lam) = ∑ i ∈ Finset.range (ell + 1), NormalOrderCoeff.bijCoeff i 0 ell * ↑(upWalkCount i lam)

theorem HasseWalkFormula.hasseWalkCount_eq_bijCoeff_mul_upWalkCount (ell : ℕ) (lam : YoungDiagram) : ↑(hasseWalkCount ell lam) = NormalOrderCoeff.bijCoeff lam.card 0 ell * ↑(upWalkCount lam.card lam)

Normal ordering decomposition: β(ℓ,λ) = b_{n,0}(ℓ) · (up-walks of length n to λ). The book's proof applies equation (44) (normal ordering of (D+U)^ℓ) to ∅, uses fact (F2) (β(ℓ,λ) is the coefficient of λ in (D+U)^ℓ(∅)), and the identity D^j(∅) = 0 for j > 0.

theorem HasseWalkFormula.hasseWalkCount_eq_bijCoeff_mul_numSYT (ell : ℕ) (lam : YoungDiagram) : ↑(hasseWalkCount ell lam) = NormalOrderCoeff.bijCoeff lam.card 0 ell * ↑(numSYT lam)

theorem HasseWalkFormula.walk_card_upper_bound {n : ℕ} (walk : Fin (n + 1) → YoungDiagram) (hstep : ∀ (i : Fin n), walk ⟨↑i, ⋯⟩ ⋖ walk ⟨↑i + 1, ⋯⟩ ∨ walk ⟨↑i + 1, ⋯⟩ ⋖ walk ⟨↑i, ⋯⟩) (base : ℕ) (hbase : base < n) (j : ℕ) (hj : j ≤ n) (hge : base + 1 ≤ j) : (walk ⟨j, ⋯⟩).card ≤ (walk ⟨base + 1, ⋯⟩).card + (j - (base + 1))

In a walk from ⊥ where each step is a covering relation (up or down), the cardinality at any position is bounded above by the position index plus the cardinality at the starting position offset. This upper bound is used to derive a contradiction when a down-step occurs in a length-n walk to a diagram of cardinality n.

theorem HasseWalkFormula.hasseWalkCount_eq_upWalkCount_of_card (lam : YoungDiagram) : hasseWalkCount lam.card lam = upWalkCount lam.card lam

When ℓ = |λ|, every Hasse walk from ⊥ to λ of length |λ| is an up-walk: there is no room for any down-step. This is because each step changes cardinality by ±1, and starting at 0, with n steps to reach n, every step must be +1.

Formally, the set of Hasse walks (allowing both up and down steps) of length n from ⊥ to λ with |λ| = n is in bijection with the set of up-walks.

Specialization of Lemma 8.5 at j = 0

theorem HasseWalkFormula.bijCoeff_n_0_eq {n ell : ℕ} (hn : n ≤ ell) (heven : (ell - n) % 2 = 0) : NormalOrderCoeff.bijCoeff n 0 ell = ↑(ell.choose n) * ↑(ell - n - 1).doubleFactorial

Specialization of Lemma 8.5 at j = 0: when n ≤ ℓ and ℓ - n is even, b_{n,0}(ℓ) = C(ℓ, n) · (2m-1)!! where m = (ℓ - n) / 2. The product (2m-1)!! = 1·3·5·⋯·(ℓ-n-1) appears in Theorem 8.6.

theorem HasseWalkFormula.bijCoeff_n_0_self (n : ℕ) : NormalOrderCoeff.bijCoeff n 0 n = 1

When ℓ = n, b_{n,0}(n) = 1.

Theorem 8.6: The Hasse walk formula

theorem HasseWalkFormula.hasseWalkCount_formula {ell n : ℕ} (lam : YoungDiagram) (hn : lam.card = n) (hle : n ≤ ell) (heven : (ell - n) % 2 = 0) : ↑(hasseWalkCount ell lam) = ↑(ell.choose n) * ↑(ell - n - 1).doubleFactorial * ↑(numSYT lam)

Theorem 8.6. Let ℓ ≥ n and λ ⊢ n, with ℓ - n even. Then β(ℓ, λ) = C(ℓ, n) · (1 · 3 · 5 · ⋯ · (ℓ - n - 1)) · f^λ.

Proof (from the book): Apply (D+U)^ℓ to ∅. Since U^i D^j(∅) = 0 unless j = 0, we get (D+U)^ℓ(∅) = ∑_i b_{i,0}(ℓ) U^i(∅). Since U^n(∅) = ∑_{λ ⊢ n} f^λ · λ, by (F2) the coefficient of λ in (D+U)^ℓ(∅) is b_{n,0}(ℓ) · f^λ. By Lemma 8.5, b_{n,0}(ℓ) = C(ℓ, n) · (1 · 3 · 5 · ⋯ · (ℓ-n-1)), giving the result.

theorem HasseWalkFormula.hasseWalkCount_formula_nat {ell n : ℕ} (lam : YoungDiagram) (hn : lam.card = n) (hle : n ≤ ell) (heven : (ell - n) % 2 = 0) : hasseWalkCount ell lam = ell.choose n * (ell - n - 1).doubleFactorial * numSYT lam

Theorem 8.6 (ℕ version). Let ℓ ≥ n and λ ⊢ n, with ℓ - n even. Then β(ℓ, λ) = C(ℓ, n) · (1 · 3 · 5 · ⋯ · (ℓ - n - 1)) · f^λ as natural numbers.

theorem HasseWalkFormula.hasseWalkCount_eq_numSYT (lam : YoungDiagram) : ↑(hasseWalkCount lam.card lam) = ↑(numSYT lam)

When ℓ = n, β(n, λ) = f^λ.

theorem HasseWalkFormula.hasseWalkCount_zero_of_lt {ell : ℕ} (lam : YoungDiagram) (hlt : ell < lam.card) : ↑(hasseWalkCount ell lam) = 0

β(ℓ, λ) = 0 when ℓ < |λ|.

theorem HasseWalkFormula.hasseWalkCount_zero_of_odd_diff {ell : ℕ} (lam : YoungDiagram) (hodd : (ell - lam.card) % 2 = 1) : ↑(hasseWalkCount ell lam) = 0

β(ℓ, λ) = 0 when ℓ - |λ| is odd (algebraic version of F1).

Corollary 8.7: Closed walks counted by double factorial

theorem HasseWalkFormula.bot_card : ⊥.card = 0

The empty Young diagram has card 0.

theorem HasseWalkFormula.numSYT_bot : numSYT ⊥ = 1

The number of standard Young tableaux of the empty shape is 1. There is exactly one saturated chain from ∅ to ∅: the trivial chain of length 0.

theorem HasseWalkFormula.closedWalkCount_eq_doubleFactorial (m : ℕ) : ↑(hasseWalkCount (2 * m) ⊥) = ↑(2 * m - 1).doubleFactorial

Corollary 8.7. The total number of Hasse walks in Young's lattice of length 2m from ∅ to ∅ is given by β(2m, ∅) = 1 · 3 · 5 · ⋯ · (2m-1) = (2m-1)!!.

Proof (from the book): Simply substitute λ = ∅ (so n = 0) and ℓ = 2m in Theorem 8.6. Then C(2m, 0) = 1, f^∅ = 1 (numSYT_bot), and the double factorial product gives 1 · 3 · 5 · ⋯ · (2m-1).

Dependency chain: closedWalkCount_eq_doubleFactorial → hasseWalkCount_formula (Theorem 8.6) → bijCoeff_n_0_eq (Lemma 8.5 at j=0) → bijCoeff_of_valid (fully proved in NormalOrderCoeff).

theorem HasseWalkFormula.closedWalkCount_eq_doubleFactorial_nat (m : ℕ) : hasseWalkCount (2 * m) ⊥ = (2 * m - 1).doubleFactorial

Corollary 8.7 (ℕ version). The total number of Hasse walks in Young's lattice of length 2m from ∅ to ∅ equals (2m-1)!! as natural numbers: β(2m, ∅) = 1 · 3 · 5 · ⋯ · (2m-1).

theorem HasseWalkFormula.hasseWalkCount_zero (lam : YoungDiagram) : hasseWalkCount 0 lam = if lam = ⊥ then 1 else 0

β(0, λ) = if λ = ⊥ then 1 else 0. A walk of length 0 from ⊥ is just the constant sequence at ⊥, so it exists iff λ = ⊥, and there is exactly one such walk.