Every cell \((i, v) \in Y(\lambda /\mu )\) satisfies \(v {\gt} \mu _i \geq 0\), hence \(v \geq 1\), so \(\operatorname {col}_{\geq 1} T\) has the same domain as \(T\).

The cells counted by \(\operatorname {cont}(\operatorname {col}_{\geq j+1} T)_i\) form a subset of those counted by \(\operatorname {cont}(\operatorname {col}_{\geq j} T)_i\).

When \(j\) exceeds all column lengths, the domain \(\{ (u,v) \in Y(\lambda /\mu ) \mid v \geq j\} \) is empty.

The sets \(\{ c \mid T'(c) = i\} \) and \(\{ c \mid T(c) = i\} \) are equal by the hypothesis (each cell belongs to one set if and only if it belongs to the other), so they have the same cardinality.

Both parts follow from the definition of alternants as signed sums over permutations.

(a) If \(\alpha _i = \alpha _j\) with \(i \neq j\), then the map \(\sigma \mapsto (i\; j) \circ \sigma \) is a sign-reversing involution on \(S_N\) that preserves \(x^{\alpha \circ \sigma }\) (since \(\alpha \) is invariant under swapping \(i\) and \(j\)). The terms cancel in pairs, giving \(a_{\alpha } = 0\).

(b) If \(\beta = \alpha \circ (i\; j)\), then reindexing the sum defining \(a_{\beta }\) via \(\tau \mapsto (i\; j) \circ \tau \) introduces a factor of \(\operatorname {sign}((i\; j)) = -1\), giving \(a_{\beta } = -a_{\alpha }\).

We have \(a\left( u-v\right) =au-av=0\) (since \(au=av\)). However, \(a\) is regular; in other words, every \(x\in L\) satisfying \(ax=0\) satisfies \(x=0\) (by the definition of “regular”). Applying this to \(x=u-v\), we obtain \(u-v=0\) (since \(a\left( u-v\right) =0\)). Thus, \(u=v\).

Each of the indeterminates \(x_{1},x_{2},\ldots ,x_{N}\) is regular (as an element of \(\mathcal{P}\)). Indeed, multiplying a polynomial \(f\) by an indeterminate \(x_{i}\) merely shifts the coefficients of \(f\) to different monomials; thus, if \(x_{i}f=0\), then \(f=0\). Next, the polynomial \(x_{i}-x_{j}\in \mathcal{P}\) is regular whenever \(1\leq i{\lt}j\leq N\). Indeed, this polynomial \(x_{i}-x_{j}\) is the image of the indeterminate \(x_{i}\) under a \(K\)-algebra automorphism of \(\mathcal{P}\) (the automorphism that sends \(x_{i}\) to \(x_{i}-x_{j}\) while leaving all other indeterminates unchanged), and therefore is regular because \(x_{i}\) is regular (and because any ring automorphism sends regular elements to regular elements). Any finite product of regular elements is again regular. Thus, the element \(\prod _{1\leq i{\lt}j\leq N}\left( x_{i}-x_{j}\right) \in \mathcal{P}\) is regular. Since \(a_{\rho } = \prod _{1\leq i{\lt}j\leq N}\left( x_{i}-x_{j}\right)\) (the Vandermonde determinant), the element \(a_{\rho }\in \mathcal{P}\) is regular.

Lean note: The Lean formalization takes a shortcut by assuming \(R\) is an integral domain, which makes the polynomial ring an integral domain; regularity then follows from the Vandermonde polynomial being nonzero.

Row-weak ordering is preserved because in each row, unmatched \((k{+}1)\)’s (which become \(k\)) lie to the left of unmatched \(k\)’s (which become \(k{+}1\)), by the structure of the parenthesis matching (Lemma 6.159). Column-strict ordering is preserved because the dangerous case (an unmatched \(k\) above an unmatched \(k{+}1\) in the same column) is ruled out by the partition property, which forces adjacent \(k, k{+}1\) pairs to be forced (Lemma 6.160).

The proof proceeds by case analysis on the status of \(c_1\) and \(c_2\) (forced, matched free, unmatched free, or having value other than \(k\) or \(k{+}1\)). The key insight is that unmatched \((k{+}1)\)’s are the leftmost free \((k{+}1)\)’s and unmatched \(k\)’s are the rightmost free \(k\)’s in each row.

The proof proceeds by case analysis on whether \(c_1\) and \(c_2\) are unmatched free \(k\), unmatched free \((k{+}1)\), or unchanged. The dangerous case is when \(c_1\) (above) is an unmatched free \(k\) (becoming \(k{+}1\)) and \(c_2\) (below) is an unmatched free \((k{+}1)\) (becoming \(k\)), which would violate strict ordering. But this cannot happen: if \(T(c_1) = k\) and \(T(c_2) = k{+}1\) in the same column, the partition property forces them to be in adjacent rows, making them a forced pair (not free), so they are unchanged by \(\beta _k\). All other case combinations preserve strict ordering.

The matching structure is symmetric under BK: an unmatched free \(k\) becomes an unmatched free \((k{+}1)\) in \(T'\) and vice versa; matched and forced cells are unchanged. Applying BK twice therefore returns every cell to its original value.

A forced \(k\) cell has a forced \((k{+}1)\) partner directly below in the same column. Since forced cells are never unmatched, both cells retain their values under \(\beta _k\), preserving the forced structure.

After swapping the value from \(k\) to \(k{+}1\), the cell is free (not forced) because there is no cell directly above with value \(k\). The counting argument shows that the cumulative counts shift appropriately to make the cell unmatched in its new role.

Matched cells retain their original values. The counting argument for the parenthesis matching is preserved because the symmetric swap of unmatched cells leaves the matching structure invariant.

For \(i \notin \{ k, k{+}1\} \), cells with value \(i\) are unchanged by BK. For the swap of \(k\) and \(k{+}1\) counts, decompose each set into forced cells, matched free cells, and unmatched free cells. The forced bijection gives equal forced counts; matched counts are equal by the matching definition; and unmatched cells swap their values, contributing to the other count.

This follows directly from the content swap: renaming by \((k\; k{+}1)\) exchanges the exponents of \(x_k\) and \(x_{k+1}\).

It suffices to show invariance under adjacent transpositions \((k\; k{+}1)\), since these generate \(S_N\). For each \(k\), the BK involution \(\beta _k\) gives a bijection on semistandard tableaux with \(x^{\operatorname {cont}(\beta _k(T))} = \operatorname {rename}_{(k\; k{+}1)}(x^{\operatorname {cont}(T)})\). Reindexing the sum defining \(s_{\lambda /\mu }\) by this bijection shows invariance.

Expand the alternant as \(a_\alpha = \sum _\sigma (-1)^\sigma x^{\alpha \circ \sigma }\) and multiply by \(s_{\lambda /\mu } = \sum _T x^{\operatorname {cont}(T)}\). Using the symmetry of \(s_{\lambda /\mu }\) and regrouping terms gives the result.

By definition, \(T\) is not \(\nu \)-Yamanouchi iff there exists \(j {\gt} 0\) such that \(\nu + \operatorname {cont}(\operatorname {col}_{\geq j} T)\) is not a partition.

If \(\alpha \) is not weakly decreasing, there exist \(i {\lt} j\) with \(\alpha _i {\lt} \alpha _j\). By well-founded induction on \(j - i\), we find consecutive indices with this property.

Cells in columns \(\geq j\) are not modified by \(\beta _k^{{\lt}j}\).

Row-weak and column-strict ordering are verified by case analysis, similar to the full BK involution but restricted to the prefix. The Stembridge context hypotheses ensure that boundary cells (at column \(j\)) interact correctly with the modified prefix.

The suffix content is preserved (columns \(\geq j\) are unchanged), so the violator column and misstep index remain the same. Applying \(\beta _k^{{\lt}j}\) twice returns every prefix cell to its original value by the matching symmetry.

Since \(\beta = \nu + \operatorname {cont}(\operatorname {col}_{\geq j+1} T)\) is a partition and \(\alpha = \nu + \operatorname {cont}(\operatorname {col}_{\geq j} T)\) has a misstep at \(k\), the difference \(\alpha _k - \beta _k\) must be zero. Otherwise the misstep at \(k\) in \(\alpha \) would contradict the partition property of \(\beta \) combined with the constraint \(\alpha _{k+1} {\gt} \alpha _k\).

Follows from the involutivity theorem, which establishes semistandardness of \(T'\) as a prerequisite.

The violator column \(j\) remains a violator for \(T'\) because \(\beta _k^{{\lt}j}\) leaves columns \(\geq j\) unchanged, so \(\nu + \operatorname {cont}(\operatorname {col}_{\geq j} T') = \nu + \operatorname {cont}(\operatorname {col}_{\geq j} T)\), which is not a partition.

If \(j{+}1 \leq \max _i \lambda _i + 1\), then \(j{+}1\) is in the range of potential violator columns but is not a violator (since \(j\) is the max), so \(\nu + \operatorname {cont}(\operatorname {col}_{\geq j+1} T)\) is a partition by definition. Otherwise, \(\operatorname {cont}(\operatorname {col}_{\geq j+1} T) = \mathbf{0}\), and the result is \(\nu \), which is a partition by hypothesis.

The key insight is that the parameters \((j, k)\) are the same for \(T\) and \(T'\): the max violator column \(j'\) for \(T'\) equals \(j\) (since \(\beta _k^{{\lt}j}\) leaves columns \(\geq j\) unchanged, and columns \({\gt} j\) are not violators for either tableau). The misstep set is unchanged because \(\operatorname {cont}(\operatorname {col}_{\geq j} T') = \operatorname {cont}(\operatorname {col}_{\geq j} T)\). Therefore \(\operatorname {stemb}_\nu (T') = \beta _k^{{\lt}j}(\beta _k^{{\lt}j}(T)) = T\).

The proof uses the decomposition of content into prefix and suffix parts. The suffix is unchanged (\(\operatorname {col}_{\geq j}\) is preserved). The prefix content swaps: the number of \(k\)’s in the prefix of \(T'\) equals the number of \((k{+}1)\)’s in the prefix of \(T\), and vice versa. Combined with the misstep condition \(\alpha _{k+1} = \alpha _k + 1\) and the rho shift \(\rho _k - \rho _{k+1} = 1\), the full expressions at positions \(k\) and \(k{+}1\) are exchanged.

Decompose \(\operatorname {cont}(T)_i = (\text{prefix } i \text{ count}) + \operatorname {cont}(\operatorname {col}_{\geq j} T)_i\). The suffix is unchanged, so it suffices to show: \((\text{prefix } k \text{ count in } T') = (\text{prefix } (k{+}1) \text{ count in } T)\). The prefix cells where \(T'(c) = k\) are exactly the prefix cells that were \(k\) in \(T\) and stayed as \(k\) (forced \(k\)’s and matched free \(k\)’s), plus the unmatched free \((k{+}1)\)’s (which became \(k\)). The prefix cells where \(T(c) = k{+}1\) decompose into cells that stay as \((k{+}1)\) (forced and matched) and unmatched \((k{+}1)\)’s (which become \(k\)). The unchanged cells contribute equally to both sides, and the unmatched \((k{+}1)\)’s appear on both sides as well, yielding the identity.

By Lemma 6.182, the exponent tuple is related by a transposition. By Lemma 6.152 (b), swapping two entries of the exponent negates the alternant.

If \(T' = T\), then \(\operatorname {cont}(T') = \operatorname {cont}(T)\), so the content transposition gives \(f = f \circ (k\; k')\) with \(k \neq k'\), where \(f = \nu + \operatorname {cont}(T) + \rho \). This forces \(f(k) = f(k')\), so \(f\) has repeated entries. By Lemma 6.152 (a), \(a_f = 0\).

The Stembridge involution partitions the non-Yamanouchi tableaux into orbits of size \(1\) or \(2\). For each pair \(\{ T, T^*\} \) with \(T^* \neq T\), the sign-reversing property gives \(a_{\nu + \operatorname {cont}(T) + \rho } + a_{\nu + \operatorname {cont}(T^*) + \rho } = 0\). At fixed points (where \(T^* = T\)), the alternant is zero by Lemma 6.185. Hence, all terms cancel and the sum is zero.

The semistandard tableaux partition into Yamanouchi and non-Yamanouchi subsets. The sum over a disjoint union equals the sum of the parts.

The proof proceeds in several steps.

Step 1. By Lemma 6.168 (which uses the symmetry of \(s_{\lambda /\mu }\) from Lemma 6.167):

Step 2. By Lemma 6.187, split the sum into Yamanouchi and non-Yamanouchi tableaux.

Step 3. By Lemma 6.186, the non-Yamanouchi sum is zero (using the Stembridge involution from Definition 6.177, its sign-reversing property from Lemma 6.184, and its fixed-point behavior from Lemma 6.185).

This lemma is an easy consequence of the fact that the entries of a semistandard tableau increase strictly down each column. More precisely, the cells \((1, j), (2, j), \ldots , (i, j)\) all belong to \(Y(\lambda )\) (since \(\lambda \) is weakly decreasing), and the entries \(T(1, j) {\lt} T(2, j) {\lt} \cdots {\lt} T(i, j)\) are strictly increasing. Since \(T(1, j) \geq 1\), we get \(T(i, j) \geq i\) by induction.

Row-weak: \(T_0(i, j_1) = i = T_0(i, j_2)\) for any \(j_1 {\lt} j_2\). Column-strict: if \(i_1 {\lt} i_2\), then \(T_0(i_1, j) = i_1 {\lt} i_2 = T_0(i_2, j)\).

The minimalistic tableau is semistandard (entries weakly increase along rows and strictly increase down columns). For the \(\mathbf{0}\)-Yamanouchi condition, the content of \(\operatorname {col}_{\geq j} T_0\) at row \(i\) equals \(\max \{ \lambda _i - (j-1), 0\} \), which is weakly decreasing since \(\lambda \) is.

The minimalistic tableau has all entries in row \(i\) equal to \(i\), so the number of \(i\)’s in \(T_0\) is \(\lambda _i\) (the number of cells in row \(i\)).

By strong induction on \(i\). Suppose \(T(i, \lambda _i) = m \neq i\). By Lemma 6.189, \(m \geq i\), and since \(m \neq i\), we have \(m {\gt} i\). From the \(\mathbf{0}\)-Yamanouchi condition, \(\operatorname {cont}(\operatorname {col}_{\geq \lambda _i} T)\) is a partition, so \(\operatorname {cont}(\operatorname {col}_{\geq \lambda _i} T)_i \geq \operatorname {cont}(\operatorname {col}_{\geq \lambda _i} T)_m \geq 1\). Hence row \(i\) has some entry \(i\) in columns \(\geq \lambda _i\). But \((i, \lambda _i)\) is the rightmost cell of row \(i\), so \(T(i, \lambda _i) \leq i\) by weak row increase from the cell where \(i\) appears. For rows \(i' {\lt} i\), the inductive hypothesis gives \(T(i', \lambda _{i'}) = i'\); the strict column increase then prevents any cell in the same column as \((i, \lambda _i)\) from having value \(i\) in an earlier row. This contradicts \(m {\gt} i\).

By Lemma 6.193, \(T(i, \lambda _i) = i\) for each row. By Lemma 6.189, \(T(i, j) \geq i\) for all \((i, j)\). By weak row increase, \(T(i, j) \leq T(i, \lambda _i) = i\) for all \(j \leq \lambda _i\). Combining: \(T(i, j) = i\) for all \((i, j)\), so \(T = T_0\).

Apply Lemma 6.188 with \(\mu = \mathbf{0}\) and \(\nu = \mathbf{0}\):

By Lemma 6.191, the minimalistic tableau \(T_0\) is \(\mathbf{0}\)-Yamanouchi, and by Lemma 6.194, it is the only such tableau. Therefore the sum has a single term. By Lemma 6.192, \(\operatorname {cont}(T_0) = \lambda \), so we obtain \(a_{\rho } \cdot s_{\lambda } = a_{\lambda + \rho }\).

Step 1. By Lemma 6.195 (applied to \(\nu \) instead of \(\lambda \)), \(a_{\nu +\rho } = a_{\rho } \cdot s_{\nu }\).

Step 2. By Lemma 6.188,

Step 3. For each \(\nu \)-Yamanouchi tableau \(T\), the tuple \(\nu + \operatorname {cont} T\) is an \(N\)-partition (by the \(j=1\) case of the Yamanouchi condition), so Lemma 6.195 yields \(a_{\nu + \operatorname {cont} T + \rho } = a_{\rho } \cdot s_{\nu + \operatorname {cont} T}\).

Step 4. Substituting Steps 1 and 3 into Step 2:

Step 5. Since \(a_{\rho }\) is regular (Lemma 6.155), we can cancel it (Lemma 6.154) to obtain