Walk Count by Type (Theorem 8.3)

This file formalizes Theorem 8.3 from Stanley's Algebraic Combinatorics: the walk count formula α(w,λ) = f^λ · ∏_{i ∈ S_w}(b_i - a_i) for Hasse walks of a given type w in Young's lattice.

Main definitions

• WalkTypeCount.walkTypeCount — α(w,λ): number of walks of type w from ∅ to λ
• WalkTypeCount.IsValidStepWord — predicate: w is a valid λ-word
• WalkTypeCount.downPositions — S_w: the set of positions i where w has a down-step
• WalkTypeCount.numDRight — a_i: number of D's to the right of position i in w
• WalkTypeCount.numURight — b_i: number of U's to the right of position i in w
• WalkTypeCount.downStepProduct — ∏_{i ∈ S_w}(b_i - a_i)
• WalkTypeCount.applyStepWord — operator application of a step word to a Finsupp element
• WalkTypeCount.downFactor — recursive accumulator of D-step factors starting at level m
• WalkTypeCount.finalLevel — final running level after processing word w from level m

Main result

• WalkTypeCount.walkTypeCount_eq_numSYT_mul_prod — Theorem 8.3: For a valid λ-word w, α(w,λ) = f^λ · ∏_{i ∈ S_w}(b_i - a_i)

References

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

def WalkTypeCount.runningLevel (w : List HasseWalks.HStep) (k : ℕ) : ℤ

The running level after the first k steps: number of U's minus number of D's in positions 0, …, k-1.

def WalkTypeCount.IsValidStepWord (w : List HasseWalks.HStep) (n : ℕ) : Prop

A walk type w : List HStep is a valid λ-word (Lemma 8.1) if the net displacement equals |λ| and every prefix has non-negative running level.

noncomputable def WalkTypeCount.walkTypeCount (w : List HasseWalks.HStep) (lam : YoungDiagram) : ℕ

α(w,λ): The number of Hasse walks of type w starting at ∅ and ending at λ.

def WalkTypeCount.downPositions (w : List HasseWalks.HStep) : Finset (Fin w.length)

S_w: the set of positions where the walk type w has a down-step.

def WalkTypeCount.numDRight (w : List HasseWalks.HStep) (i : Fin w.length) : ℕ

a_i: The number of D-steps strictly to the right of position i in w.

def WalkTypeCount.numURight (w : List HasseWalks.HStep) (i : Fin w.length) : ℕ

b_i: The number of U-steps strictly to the right of position i in w.

def WalkTypeCount.downStepProduct (w : List HasseWalks.HStep) : ℤ

The product ∏_{i ∈ S_w}(b_i - a_i) that appears in Theorem 8.3.

def WalkTypeCount.applyStepWord : List HasseWalks.HStep → (YoungDiagram →₀ ℤ) → YoungDiagram →₀ ℤ

Apply a step word (list of HStep) to an element of YoungDiagram →₀ ℤ. Each step is applied left-to-right: step 0 first.

def WalkTypeCount.netDisp (w : List HasseWalks.HStep) : ℤ

The net displacement of a step word: number of U's minus number of D's.

Linearity of applyStepWord

theorem WalkTypeCount.applyStepWord_add (w : List HasseWalks.HStep) (f g : YoungDiagram →₀ ℤ) : applyStepWord w (f + g) = applyStepWord w f + applyStepWord w g

theorem WalkTypeCount.applyStepWord_smul (w : List HasseWalks.HStep) (c : ℤ) (f : YoungDiagram →₀ ℤ) : applyStepWord w (c • f) = c • applyStepWord w f

theorem WalkTypeCount.applyStepWord_zero (w : List HasseWalks.HStep) : applyStepWord w 0 = 0

Auxiliary accumulator

def WalkTypeCount.downFactor : List HasseWalks.HStep → ℕ → ℤ

The product of running-level factors at D-steps when processing word w starting at running level m. This mirrors the recursive structure of applyStepWord.

def WalkTypeCount.finalLevel : List HasseWalks.HStep → ℕ → ℕ

The final running level after processing word w starting at level m.

theorem WalkTypeCount.applyStepWord_smul_iterU_emptyBasis (w : List HasseWalks.HStep) (c : ℤ) (m : ℕ) : applyStepWord w (c • (WalkCountFormula.iterU m) WalkCountFormula.emptyBasis) = (c * downFactor w m) • (WalkCountFormula.iterU (finalLevel w m)) WalkCountFormula.emptyBasis

theorem WalkTypeCount.applyStepWord_emptyBasis_eq (w : List HasseWalks.HStep) : applyStepWord w WalkCountFormula.emptyBasis = downFactor w 0 • (WalkCountFormula.iterU (finalLevel w 0)) WalkCountFormula.emptyBasis

Running level lemmas

@[simp]

theorem WalkTypeCount.runningLevel_zero (w : List HasseWalks.HStep) : runningLevel w 0 = 0

theorem WalkTypeCount.runningLevel_cons_U_succ (rest : List HasseWalks.HStep) (k : ℕ) : runningLevel (HasseWalks.HStep.U :: rest) (k + 1) = 1 + runningLevel rest k

theorem WalkTypeCount.runningLevel_cons_D_succ (rest : List HasseWalks.HStep) (k : ℕ) : runningLevel (HasseWalks.HStep.D :: rest) (k + 1) = runningLevel rest k - 1

finalLevel and runningLevel

theorem WalkTypeCount.finalLevel_eq_of_valid (w : List HasseWalks.HStep) (m : ℕ) (hvalid : ∀ k ≤ w.length, 0 ≤ ↑m + runningLevel w k) : ↑(finalLevel w m) = ↑m + runningLevel w w.length

downFactor equals downStepProduct

theorem WalkTypeCount.numURight_sub_numDRight_eq_runningLevel (w : List HasseWalks.HStep) (i : Fin w.length) : ↑(numURight w i) - ↑(numDRight w i) = runningLevel w ↑i

theorem WalkTypeCount.downStepProduct_eq_prod_runningLevel (w : List HasseWalks.HStep) : downStepProduct w = ∏ i ∈ downPositions w, runningLevel w ↑i

theorem WalkTypeCount.downFactor_eq_downStepProduct_offset (w : List HasseWalks.HStep) (m : ℕ) (hvalid : ∀ k ≤ w.length, 0 ≤ ↑m + runningLevel w k) : downFactor w m = ∏ i ∈ downPositions w, (↑m + runningLevel w ↑i)

theorem WalkTypeCount.downFactor_zero_eq_downStepProduct (w : List HasseWalks.HStep) (hvalid : ∀ k ≤ w.length, 0 ≤ runningLevel w k) : downFactor w 0 = downStepProduct w

Bridge axioms for Theorem 8.3

The combinatorial bridge (linking walkTypeCount to operator coefficients) is stated as an unproved axiom. The book treats this as an observation (not a separate theorem).

axiom HasseWalks.hasseWalk_finite (steps : List HStep) (start target : YoungDiagram) : Finite (HasseWalk steps start target)

instance instFiniteHasseWalk (steps : List HasseWalks.HStep) (start target : YoungDiagram) : Finite (HasseWalks.HasseWalk steps start target)

theorem WalkTypeCount.natCard_hasseWalk_cons_U_eq_sum (rest : List HasseWalks.HStep) (start lam : YoungDiagram) : ↑(Nat.card (HasseWalks.HasseWalk (HasseWalks.HStep.U :: rest) start lam)) = ∑ μ ∈ start.coversUp, ↑(Nat.card (HasseWalks.HasseWalk rest μ lam))

theorem WalkTypeCount.natCard_hasseWalk_cons_D_eq_sum (rest : List HasseWalks.HStep) (start lam : YoungDiagram) : ↑(Nat.card (HasseWalks.HasseWalk (HasseWalks.HStep.D :: rest) start lam)) = ∑ μ ∈ start.coversDown, ↑(Nat.card (HasseWalks.HasseWalk rest μ lam))

theorem WalkTypeCount.applyStepWord_finset_sum_single (w : List HasseWalks.HStep) (S : Finset YoungDiagram) : applyStepWord w (∑ σ ∈ S, Finsupp.single σ 1) = ∑ σ ∈ S, applyStepWord w (Finsupp.single σ 1)

applyStepWord w distributes over Finset.sum of basis elements.

theorem WalkTypeCount.walkTypeCount_general (w : List HasseWalks.HStep) (start lam : YoungDiagram) : ↑(Nat.card (HasseWalks.HasseWalk w start lam)) = (applyStepWord w (Finsupp.single start 1)) lam

Generalized bridge: for any start diagram, the walk count from start to lam equals the coefficient of lam in applyStepWord w (δ_start).

theorem WalkTypeCount.walkTypeCount_eq_applyStepWord_coeff (w : List HasseWalks.HStep) (lam : YoungDiagram) : ↑(walkTypeCount w lam) = (applyStepWord w WalkCountFormula.emptyBasis) lam

Main algebraic reduction (Theorem 8.3 core)

theorem WalkTypeCount.applyStepWord_emptyBasis_eq_downStepProduct_smul_iterU (w : List HasseWalks.HStep) (n : ℕ) (hw : IsValidStepWord w n) : applyStepWord w WalkCountFormula.emptyBasis = downStepProduct w • (WalkCountFormula.iterU n) WalkCountFormula.emptyBasis

The operator application of a valid step word w to emptyBasis equals downStepProduct w • iterU n emptyBasis. This is the heart of Theorem 8.3's proof.

theorem WalkTypeCount.iterU_emptyBasis_coeff_eq_numSYT (lam : YoungDiagram) : ((WalkCountFormula.iterU lam.card) WalkCountFormula.emptyBasis) lam = ↑(HasseWalkFormula.numSYT lam)

theorem WalkTypeCount.walkTypeCount_eq_numSYT_mul_prod (w : List HasseWalks.HStep) (lam : YoungDiagram) (hw : IsValidStepWord w lam.card) : ↑(walkTypeCount w lam) = ↑(HasseWalkFormula.numSYT lam) * downStepProduct w