Pipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The Hook Length Formula and Rsk Correspondence

1 · Prerequisites

2 · Summary

This page proves the hook length formula and builds the Robinson-Schensted correspondence on the combinatorial base of young-diagrams-tableaux-and-permutation-modules.

The first half is the Frame-Robinson-Thrall count. It fixes hooks, arms, legs and hook lengths with the English convention, proves the removal recursion for standard tableaux, computes how the hook product changes when a removable corner is deleted, and proves the branching identity that turns the recursion into the closed formula $f^{λ} = n! / \prod_{x \in [λ]} h (x)$ ; the dimension statement for Specht modules follows from Standard polytabloids form a basis of a complex Specht module.

The second half constructs RSK. Row insertion with its bumping route, reverse row deletion and the proof that they are inverse are followed by the recording tableau, the bijection between permutations and pairs of standard tableaux, the column insertion and commutation lemmas, the basic subsequences of the first row, and Schensted's longest increasing and decreasing subsequence theorem. The page closes with the RSK correspondence for two-line arrays, the symmetry under inversion, the sum-of-squares identity $\sum_{λ ⊢ n} (f^{λ})^{2} = n!$ and the count of involutions by standard tableaux. Concrete computations of the hook table and of RSK runs are collected on the accompanying examples page.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-6.1-sol)Open item page →

Hook, arm, leg, and hook length of a box

Definition

Let $λ ⊢ n$ with English Young diagram $[λ]$ (Partitions, English diagrams, and conjugation) and let $x = (i, j) \in [λ]$ . The hook of $x$ is the set $H (x) : = {(i, j^{'}) \in [λ] : j^{'} \geq j} \cup {(i^{'}, j) \in [λ] : i^{'} \geq i},$ the union of the boxes of $[λ]$ weakly to the right of $x$ in row $i$ and weakly below $x$ in column $j$ ; the box $x$ itself belongs to both parts and is counted once. The arm $arm (x)$ is the part in row $i$ strictly to the right of $x$ , so $arm (x) = {(i, j^{'}) : j < j^{'} \leq λ_{i}}$ ; the leg $leg (x)$ is the part in column $j$ strictly below $x$ , so $leg (x) = {(i^{'}, j) : i < i^{'} \leq λ_{j}^{'}}$ . The arm length is $a (x) : = λ_{i} - j$ , the leg length is $ℓ (x) : = λ_{j}^{'} - i$ , and the hook length is

$h (x) : = a (x) + ℓ (x) + 1 = λ_{i} - j + λ_{j}^{'} - i + 1,$

so that $H (x)$ has exactly $h (x)$ boxes. Here $λ_{j}^{'}$ is the number of rows of $[λ]$ of length at least $j$ , so the boxes of column $j$ below row $i$ are exactly the rows $i + 1, \dots, λ_{j}^{'}$ and the arm has $λ_{i} - j$ boxes; the arm, the leg and the anchor $x$ are pairwise disjoint and exhaust $H (x)$ , which gives the count.

A box is removable in the sense of Removable and addable nodes if and only if it is the last box of its row and of its column, i.e. if and only if $h (x) = 1$ : a row endpoint $(i, λ_{i})$ is removable exactly when no box lies immediately below it, that is when $λ_{i} > λ_{i + 1}$ , and then $a (x) = λ_{i} - λ_{i} = 0$ and $ℓ (x) = λ_{λ_{i}}^{'} - i = 0$ ; conversely $h (x) = 1$ forces $a (x) = ℓ (x) = 0$ , so $x$ ends both its row and its column. The empty partition has no boxes.

Finally $P (λ) : = \prod_{x \in [λ]} h (x)$ denotes the hook product of $λ$ , the empty product $P (\emptyset) = 1$ being part of the convention. This fixes the off-by-one convention used by the whole page: the anchor box contributes $1$ , the arm contributes $λ_{i} - j$ and the leg contributes $λ_{j}^{'} - i$ . No choice principle is used.

LemmaStatement: Literature-sourcedProof: Literature-sourcedjudge pass (gpt-6.1-sol)Open item page →

The removal recursion for standard tableaux

Statement

Let $n \geq 1$ and $λ ⊢ n$ . The map that sends a standard $λ$ -tableau $t$ to the pair $(x, t^{-})$ , where $x$ is the box occupied by $n$ and $t^{-}$ is the restriction of $t$ to $[λ] ∖ {x}$ , is a bijection from the set of standard $λ$ -tableaux onto the disjoint union, over the removable nodes $x \in Rem (λ)$ , of the sets of standard $(λ - x)$ -tableaux. Consequently

$f^{λ} = \sum_{x \in Rem (λ)} f^{λ - x} (λ ⊢ n, n \geq 1),$

and we adopt the convention $f^{\emptyset} = 1$ . For $n = 0$ the disjoint union is empty and the recursion is not asserted: the value $f^{\emptyset} = 1$ is the convention for the unique empty tableau.

Facts & Assumptions

Given: An integer $n \geq 1$ , a partition $λ ⊢ n$ , and the family of partitions $λ - x$ for $x \in Rem (λ)$ .

[L1]

A standard $λ$ -tableau is a bijection $t : [λ] \to {1, \dots, n}$ that strictly increases along rows and down columns; the shape is determined by $t$ (Tableaux and standard tableaux).

[L2]

The box occupied by the largest entry $n$ of a standard $λ$ -tableau is a removable node of $λ$ , and deleting it leaves a standard tableau of shape $λ - x$ (The largest standard entry lies in a removable box).

[L3]

A node $x$ is removable exactly when $[λ] ∖ {x}$ is the diagram of a partition $λ - x ⊢ n - 1$ ; the diagram $[λ - x]$ determines $λ - x$ (Removable and addable nodes).

Proof

technique · direct

1.1L2given

The map is well defined: by [L2] the box $x$ of $n$ is removable and $t^{-}$ is a standard tableau of shape $λ - x$ , and $(x, t^{-})$ lies in the $x$ -component of the displayed disjoint union.

1.2L1given

The map is injective: given its image $(x, t^{-})$ one recovers $t$ by $t (x) = n$ and $t = t^{-}$ on $[λ] ∖ {x}$ , so two tableaux with the same image are equal.

1.3L1L3given

The map is surjective onto the displayed union: let $x \in Rem (λ)$ and let $t^{-}$ be a standard tableau of shape $λ - x$ ; define $t (x) : = n$ and $t (y) : = t^{-} (y)$ for $y \in [λ - x]$ . Then $t$ is a bijection $[λ] \to {1, \dots, n}$ , because $t^{-}$ is a bijection onto ${1, \dots, n - 1}$ and $x \notin [λ - x]$ .

2.1L1L3step 1.3

The bijection $t$ of step 1.3 is standard: adjacent pairs in $[λ]$ not involving $x$ are adjacent in $[λ - x]$ and satisfy the required strict inequality by standardness of $t^{-}$ , while a pair involving $x$ has its other entry in ${1, \dots, n - 1}$ and hence satisfies $t^{-} (\cdot) \leq n - 1 < n = t (x)$ in the direction of $x$ , and the inequalities along rows and columns run into $x$ only from the left and from above, since $x$ is a corner.

2.2L1step 1.1step 1.3

The two constructions of steps 1.1 and 1.3 are inverse: starting from $t$ , the tableau reconstructed from $(x, t^{-})$ agrees with $t$ because $t (x) = n$ and $t$ restricts to $t^{-}$ ; starting from $x, t^{-}$ , the pair extracted from the reconstructed $t$ is $(x, t^{-})$ because the only entry greater than $n - 1$ is $t (x) = n$ .

3.1step 1.1step 1.2step 1.3step 2.1step 2.2L1∎

The components of the disjoint union are indexed by the distinct removable nodes $x$ , and for fixed $x$ the standard $(λ - x)$ -tableaux number $f^{λ - x}$ ; the bijection of steps 1.1–2.2 therefore gives the stated recursion, and for $λ = \emptyset$ the union is empty while $f^{\emptyset} = 1$ is the adopted convention.

LemmaStatement: Literature-sourcedProof: Literature-sourcedjudge pass (gpt-6.1-sol)Open item page →

Removing a corner changes hooks in its row and column

Statement

Let $λ ⊢ n$ with $n \geq 1$ , let $x = (a, b) \in Rem (λ)$ be a removable node (so $b = λ_{a}$ and $a = λ_{b}^{'}$ , and the arm and leg of $x$ are empty), and let $μ : = λ - x$ . Put $R_{x} : = {(a, j) : 1 \leq j < b} \cup {(i, b) : 1 \leq i < a},$ the boxes of $[μ]$ lying in row $a$ or in column $b$ ; these are exactly the boxes whose hook contains $x$ . Then:

$h_{μ} (y) = h_{λ} (y)$ for every $y \in [μ] ∖ R_{x}$ , and $h_{μ} (y) = h_{λ} (y) - 1$ for every $y \in R_{x}$ ; in particular every $y \in R_{x}$ has $h_{λ} (y) \geq 2$ .
Consequently, with $P$ the hook product of Hook, arm, leg, and hook length of a box,

$\frac{P (λ)}{P (μ)} = \prod_{y \in R_{x}} \frac{h_{λ} (y)}{h_{λ} (y) - 1} .$

Facts & Assumptions

Given: Integers $n \geq 1$ and $λ ⊢ n$ , a removable node $x = (a, b) \in Rem (λ)$ with $b = λ_{a}$ , and $μ : = λ - x$ .

[L1]

Hook lengths are $h_{ν} (i, j) = ν_{i} - j + ν_{j}^{'} - i + 1$ for a partition $ν$ and a box $(i, j) \in [ν]$ , where $ν_{j}^{'}$ is the number of rows of $[ν]$ of length at least $j$ ; a box is removable if and only if $h_{ν} = 1$ (Hook, arm, leg, and hook length of a box, Partitions, English diagrams, and conjugation).

[L2]

A node $(i, λ_{i})$ is removable if and only if $λ_{i} > λ_{i + 1}$ (with $λ_{k + 1} : = 0$ for a $k$ -part partition), and deleting a removable node leaves the diagram of a partition $λ - x ⊢ n - 1$ (Removable and addable nodes).

[L3]

The conjugate $λ^{'}$ has $λ_{j}^{'} = # {i : λ_{i} \geq j}$ ; consequently $λ_{b}^{'} = a$ when $b = λ_{a}$ and rows $a + 1, a + 2, \dots$ all have length $< b$ . For equal-index comparisons, if $i \neq a$ then $μ_{i} = λ_{i}$ , and if $j \neq b$ then $μ_{j}^{'} = λ_{j}^{'}$ (Partitions, English diagrams, and conjugation).

Proof

technique · direct

1.1L1L2L3given

For these coordinate comparisons, extend row lengths by zero beyond the last nonempty row. The row lengths of $μ$ are $μ_{a} = λ_{a} - 1 = b - 1$ and $μ_{i} = λ_{i}$ for $i \neq a$ : deleting the row-end box of row $a$ shortens exactly that row, and the result is a partition by [L2]. The column heights are $μ_{b}^{'} = λ_{b}^{'} - 1 = a - 1$ and $μ_{j}^{'} = λ_{j}^{'}$ for $j \neq b$ : column $b$ loses exactly its bottom box, since row $a$ is the last row of length at least $b$ (rows below row $a$ have length $< b$ by [L3] and removability), while a column $j \neq b$ either still meets row $a$ (if $j < b$ , when row $a$ has length $b - 1 \geq j$ ) or never met row $a$ (if $j > b$ , when row $a$ has length $b < j$ ), so its height is unchanged.

1.2L1L2given

Every $y \in R_{x}$ satisfies $h_{λ} (y) \geq 2$ : a box of row $a$ at column $j < b$ is not the end of its row, and a box $(i, b)$ with $i < a$ has the box $(i + 1, b)$ of $[λ]$ directly below it, since $λ_{i + 1} \geq λ_{a} = b$ for $i + 1 \leq a$ ; in both cases $y$ is not removable, so $h_{λ} (y) \neq 1$ and, being positive, $h_{λ} (y) \geq 2$ .

2.1step 1.1L1

For $y = (i, j) \in [μ]$ with $i \neq a$ and $j \neq b$ , both summands of $h (y) = ν_{i} - j + ν_{j}^{'} - i + 1$ are the same for $ν = λ$ and for $ν = μ$ , so $h_{μ} (y) = h_{λ} (y)$ .

2.2step 1.1L1

For $y = (a, j) \in [μ]$ with $j < b$ one has $h_{μ} (y) = μ_{a} - j + μ_{j}^{'} - a + 1 = (λ_{a} - 1) - j + λ_{j}^{'} - a + 1 = h_{λ} (y) - 1$ , because $j \neq b$ leaves the column height unchanged.

2.3step 1.1L1

For $y = (i, b) \in [μ]$ with $i < a$ one has $h_{μ} (y) = μ_{i} - b + μ_{b}^{'} - i + 1 = λ_{i} - b + (λ_{b}^{'} - 1) - i + 1 = h_{λ} (y) - 1$ , because $i \neq a$ leaves the row length unchanged.

3.1step 1.1step 2.1step 2.2step 2.3step 1.2L1∎

The multiset of hook factors: $h_{λ} (x) = 1$ , so $P (λ) = \prod_{y \in [μ]} h_{λ} (y) \cdot h_{λ} (x) = \prod_{y \in [μ]} h_{λ} (y)$ , while $P (μ) = \prod_{y \in [μ]} h_{μ} (y) = (\prod_{y \in [μ] ∖ R_{x}} h_{λ} (y)) (\prod_{y \in R_{x}} (h_{λ} (y) - 1))$ . Dividing the two finite products, all factors with $y \notin R_{x}$ cancel and the factors with $y \in R_{x}$ contribute $h_{λ} (y) / (h_{λ} (y) - 1)$ ; the division is legitimate because $h_{λ} (y) - 1 \geq 1$ on $R_{x}$ by step 1.2.

LemmaStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-6.1-sol)Open item page →

The hook-product ratios sum to the size

Statement

Let $λ ⊢ n$ and, for $x \in Rem (λ)$ , let $R (x) : = \prod_{y \in R_{x}} \frac{h_{λ} (y)}{h_{λ} (y) - 1}$ be the ratio $P (λ) / P (λ - x)$ of Removing a corner changes hooks in its row and column, where $R_{x} \subseteq [λ - x]$ is the set of boxes of row $a$ and column $b$ of $x = (a, b)$ and $h_{λ}$ is the hook length of Hook, arm, leg, and hook length of a box. Then

$\sum_{x \in Rem (λ)} R (x) = n,$

the empty sum for $λ = \emptyset$ being $0$ .

Facts & Assumptions

Given: A partition $λ = (λ_{1}, \dots, λ_{r})$ of $n$ with $r \geq 0$ parts, its removable nodes, and the numbers $R (x)$ for $x \in Rem (λ)$ ; put $h_{i, 1} : = λ_{i} + r - i$ for $1 \leq i \leq r$ .

[F1]

For $x = (a, b) \in Rem (λ)$ with $μ = λ - x$ : $R_{x} = {(a, j) : j < b} \cup {(i, b) : i < a}$ is contained in $[μ]$ , $h_{μ} (y) = h_{λ} (y) - 1$ on $R_{x}$ and $h_{μ} (y) = h_{λ} (y)$ off $R_{x}$ , and $P (λ) / P (μ) = \prod_{y \in R_{x}} h_{λ} (y) / (h_{λ} (y) - 1)$ (Removing a corner changes hooks in its row and column).

[F2]

For a box $(i, j) \in [λ]$ , $h_{λ} (i, j) = λ_{i} - j + λ_{j}^{'} - i + 1$ , where $λ_{j}^{'} = # {k : λ_{k} \geq j}$ ; in particular $h_{λ} (i, 1) = λ_{i} + r - i = h_{i, 1}$ and the hook product is $P (λ) = \prod_{(i, j) \in [λ]} h_{λ} (i, j)$ (Hook, arm, leg, and hook length of a box, Partitions, English diagrams, and conjugation).

[F3]

For a partition with $r$ parts, row $a < r$ has a removable node if and only if $λ_{a} > λ_{a + 1}$ , and row $r$ always has the removable node $(r, λ_{r})$ ; consequently the removable nodes of $λ$ are in bijection with the indices $a$ with $λ_{a} > λ_{a + 1}$ , where $λ_{r + 1} : = 0$ (Removable and addable nodes).

[F4]

$K [t]$ is a commutative ring with formal degree and leading coefficient, evaluation $g \mapsto g (z)$ , and for nonzero $f, g$ : $\deg (f + g) \leq \max (\deg f, \deg g)$ if $f + g \neq 0$ and $\deg (f g) \leq \deg f + \deg g$ if $f g \neq 0$ (The polynomial ring over a commutative ring as finitely supported coefficient sequences with convolution, Degree, leading coefficient and monic polynomial, with the zero polynomial having no degree, Evaluation and roots of a polynomial in a commutative target ring, Degree inequalities for sums and products over a commutative ring).

[F5]

A nonzero polynomial over an integral domain of degree $d$ has at most $d$ distinct roots; in particular a polynomial over a field that vanishes at $r$ distinct points has degree at least $r$ unless it is the zero polynomial (A nonzero polynomial of degree $n$ over an integral domain has at most $n$ distinct roots).

Proof

technique · direct

1.1F1F2F3given

The numbers $h_{i, 1} = λ_{i} + r - i$ are strictly decreasing in $i$ and positive, because $λ_{i} \geq λ_{i + 1}$ gives $h_{i, 1} - h_{i + 1, 1} = λ_{i} - λ_{i + 1} + 1 \geq 1$ and $h_{r, 1} = λ_{r} \geq 1$ ; for $x = (a, b) \in Rem (λ)$ we have $b = λ_{a}$ and $λ_{b}^{'} = a$ . By [F1] the value $R (x)$ is a finite product of ratios $h_{λ} (y) / (h_{λ} (y) - 1)$ over $R_{x}$ , which may be empty (for example when $λ = (1)$ ), and the sum over $Rem (\emptyset) = \emptyset$ is $0 = n$ .

1.2F2algebra

The multiset identity for row $a$ : the $h_{a, 1} = λ_{a} + (r - a)$ numbers of $L : = {h_{λ} (a, j) : 1 \leq j \leq λ_{a}} \cup {h_{a, 1} - h_{k, 1} : a < k \leq r}$ are pairwise distinct and all lie in ${1, 2, \dots, h_{a, 1}}$ , so as multisets $L = {1, \dots, h_{a, 1}}$ . Indeed $h_{λ} (a, j) = λ_{a} - j + λ_{j}^{'} - a + 1$ decreases strictly with $j$ ; the differences equal $λ_{a} - λ_{k} + k - a$ and increase strictly with $k$ , lying between $1$ and $h_{a, 1} - 1$ ; and a repetition $h_{λ} (a, j) = h_{a, 1} - h_{k, 1}$ would force $λ_{j}^{'} + λ_{k} = j + k - 1$ , which is impossible: if $λ_{k} \leq j - 1$ then the hook of $(a, j)$ does not reach row $k$ , so $λ_{j}^{'} < k$ and $λ_{j}^{'} + λ_{k} < j + k - 1$ , while if $λ_{k} \geq j$ then $(k, j)$ lies in the column of $(a, j)$ , so $λ_{j}^{'} \geq k$ and $λ_{j}^{'} + λ_{k} > j + k - 1$ .

1.3F4F5algebra

Finite identity: for pairwise distinct $z_{1}, \dots, z_{r}$ in a field $K$ with $r \geq 1$ , $\sum_{i = 1}^{r} z_{i} \prod_{j \neq i} (1 + \frac{1}{z_{j} - z_{i}}) = \sum_{i = 1}^{r} z_{i} - (\binom{r}{2}) .$ For $r = 1$ the identity is $z_{1} = z_{1}$ . Hence assume $r \geq 2$ for its coefficient calculation. Set $Q (t) : = \prod_{j = 1}^{r} (t - z_{j}) \in K [t]$ and for $g \in K [t]$ whose coefficients above $t^{r - 1}$ vanish let $Λ (g) : = \sum_{i} g (z_{i}) / \prod_{j \neq i} (z_{i} - z_{j})$ . Then $Λ (g) = [t^{r - 1}] g$ : the polynomial $g (t) - \sum_{i} g (z_{i}) \prod_{j \neq i} (t - z_{j}) / (z_{i} - z_{j})$ has no nonzero coefficient above $t^{r - 1}$ and vanishes at $z_{1}, \dots, z_{r}$ , hence is zero by [F5], and comparing coefficients of $t^{r - 1}$ gives the claim.

2.1F1F2step 1.1algebra

The column- $b$ factors of $R (x)$ : for $1 \leq i < a$ the box $(i, b)$ lies in $[μ]$ , and $h_{λ} (i, b) = λ_{i} - b + λ_{b}^{'} - i + 1 = h_{i, 1} - h_{a, 1} + 1$ , because $λ_{b}^{'} = a$ and $h_{a, 1} = b + r - a$ ; hence $\prod_{i < a} \frac{h_{λ} (i, b)}{h_{λ} (i, b) - 1} = \prod_{i < a} (1 + \frac{1}{h_{i, 1} - h_{a, 1}}) .$

2.2F1F2step 1.2algebra

The row- $a$ factors of $R (x)$ : if $b \geq 2$ , applying step 1.2 to $λ$ and to $μ = λ - x$ (which then has $r$ parts, row $a$ of length $λ_{a} - 1$ , and first-column hooks $h_{i, 1}$ for $i \neq a$ , $h_{a, 1} - 1$ for $i = a$ ) and multiplying the two identities gives $(\prod_{j < b} h_{λ} (a, j)) \cdot \prod_{k > a} (h_{a, 1} - h_{k, 1}) = h_{a, 1}!, (\prod_{j < b} (h_{λ} (a, j) - 1)) \cdot \prod_{k > a} (h_{a, 1} - h_{k, 1} - 1) = (h_{a, 1} - 1)!,$ where $h_{λ} (a, b) = 1$ by removability; dividing them yields $\prod_{j < b} \frac{h_{λ} (a, j)}{h_{λ} (a, j) - 1} = h_{a, 1} \prod_{k > a} \frac{h_{a, 1} - h_{k, 1} - 1}{h_{a, 1} - h_{k, 1}} = h_{a, 1} \prod_{k > a} (1 + \frac{1}{h_{k, 1} - h_{a, 1}}),$ since $1 + (h_{k, 1} - h_{a, 1})^{- 1} = (h_{a, 1} - h_{k, 1} - 1) / (h_{a, 1} - h_{k, 1})$ for $k > a$ . If $b = 1$ then $λ_{a} = 1$ forces $a = r$ , the product over $j < b$ is empty and $h_{a, 1} = 1$ , so the same displayed formula holds trivially.

2.3F4step 1.3algebra

Set $g (t) : = t Q (t - 1) - (t - r) Q (t) = t (Q (t - 1) - Q (t)) + r Q (t)$ . Both $Q (t)$ and $Q (t - 1)$ are monic of degree $r$ , so $[t^{r + 1}] g = 0$ . Writing $e_{1} : = \sum_{j} z_{j}$ , their $t^{r - 1}$ coefficients differ by $- r$ , while $[t^{r}] (r Q (t)) = r$ ; hence $[t^{r}] g = - r + r = 0$ . Thus all coefficients of $g$ above $t^{r - 1}$ vanish, including when $r = 0$ in $K$ or $g = 0$ . Moreover, expanding $Q (t - 1) = \prod_{j} (t - (z_{j} + 1))$ gives $[t^{r - 2}] (Q (t - 1) - Q (t)) = (r - 1) e_{1} + (\binom{r}{2})$ and $[t^{r - 1}] (r Q (t)) = - r e_{1}$ , so $[t^{r - 1}] g = (\binom{r}{2}) - e_{1}$ . Here integers are mapped into $K$ , so no division by $2$ in $K$ is used.

3.1step 2.1step 2.2F1

Combining steps 2.1 and 2.2 with [F1], for every $x = (a, b) \in Rem (λ)$ , $R (x) = h_{a, 1} \prod_{i \neq a} (1 + \frac{1}{h_{i, 1} - h_{a, 1}}) .$

3.2step 1.3step 2.3algebra

Since $Q (z_{i}) = 0$ and $Q (z_{i} - 1) = \prod_{j} (z_{i} - 1 - z_{j}) = - (- 1)^{r - 1} \prod_{j \neq i} (z_{j} - z_{i} + 1)$ , for each $i$ $\frac{g (z_{i})}{\prod_{j \neq i} (z_{i} - z_{j})} = \frac{z_{i} Q (z_{i} - 1)}{\prod_{j \neq i} (z_{i} - z_{j})} = - z_{i} \prod_{j \neq i} (1 + \frac{1}{z_{j} - z_{i}}) .$ Summing over $i$ and using $Λ (g) = [t^{r - 1}] g$ from step 1.3 together with step 2.3 gives the finite identity.

4.1step 3.1F2F3given

Rows without removable nodes contribute zero and the sum may be extended over all rows: by [F3] the removable nodes correspond to the indices $a$ with $λ_{a} > λ_{a + 1}$ , and if $a < r$ satisfies $λ_{a} = λ_{a + 1}$ , then $h_{a, 1} - h_{a + 1, 1} = 1$ and the factor of index $a + 1$ in the product of step 3.1 vanishes, so the corresponding term is $0$ . Therefore $\sum_{x \in Rem (λ)} R (x) = \sum_{a = 1}^{r} h_{a, 1} \prod_{i \neq a} (1 + \frac{1}{h_{i, 1} - h_{a, 1}}) .$

4.2step 1.1step 1.3step 3.2

Applying the finite identity of steps 1.3 and 3.2 (the $r = 1$ case being immediate in step 1.3) over $K = Q$ to the pairwise distinct numbers $z_{i} : = h_{i, 1}$ (step 1.1) gives $\sum_{a = 1}^{r} h_{a, 1} \prod_{i \neq a} (1 + \frac{1}{h_{i, 1} - h_{a, 1}}) = \sum_{i = 1}^{r} h_{i, 1} - (\binom{r}{2}) .$

5.1step 4.1step 4.2F2algebra∎

The first-column hooks sum to $n + (\binom{r}{2})$ : $\sum_{i} h_{i, 1} = \sum_{i} λ_{i} + \sum_{i} (r - i) = n + r (r - 1) / 2 = n + (\binom{r}{2})$ . Substituting this into step 4.2 and using step 4.1 yields $\sum_{x \in Rem (λ)} R (x) = n$ , and the case $λ = \emptyset$ is the empty sum $0$ ; this proves the lemma.

TheoremStatement: Literature-sourcedProof: Literature-sourcedjudge pass (gpt-6.1-sol)Open item page →

The hook length formula

Statement

For every $n \geq 0$ and every $λ ⊢ n$ , the number $f^{λ}$ of standard $λ$ -tableaux is $f^{λ} = \frac{n!}{\prod_{x \in [λ]} h (x)},$ the empty product for $λ = \emptyset$ being $1$ , so that $f^{\emptyset} = 1$ and, for $n \geq 1$ , $f^{λ} = 1$ for $λ = (n)$ and $λ = (1^{n})$ . In particular, over $C$ , $\dim_{C} S^{λ} = \frac{n!}{\prod_{x \in [λ]} h (x)}$ for the Specht module $S^{λ}$ , including $\dim_{C} S^{\emptyset} = 1$ .

Facts & Assumptions

Given: An integer $n \geq 0$ and a partition $λ ⊢ n$ , with $f^{λ}$ the number of standard $λ$ -tableaux and $P (λ) = \prod_{x \in [λ]} h (x)$ the hook product.

[F1]

$f^{λ} = \sum_{x \in Rem (λ)} f^{λ - x}$ for $n \geq 1$ , and $f^{\emptyset} = 1$ ; the boxes of $[λ]$ are the boxes of $[λ - x]$ together with $x$ for $x \in Rem (λ)$ (The removal recursion for standard tableaux).

[F2]

For $x \in Rem (λ)$ with $λ ⊢ n \geq 1$ : $P (λ) / P (λ - x) = R (x) : = \prod_{y \in R_{x}} h_{λ} (y) / (h_{λ} (y) - 1)$ (Removing a corner changes hooks in its row and column).

[F3]

$\sum_{x \in Rem (λ)} R (x) = n$ , the empty sum being $0$ (The hook-product ratios sum to the size).

[F4]

The family of standard polytabloids is a $C$ -basis of the Specht module $S^{λ}$ , so $\dim_{C} S^{λ} = f^{λ}$ for every $λ ⊢ n$ , including $n = 0$ (Standard polytabloids form a basis of a complex Specht module).

[F5]

$P (λ)$ is the product of the $n$ positive integers $h (x)$ , one for each box of $[λ]$ ; for $λ = \emptyset$ it is the empty product $1$ , for $λ = (n)$ the product is $n!$ , and for $λ = (1^{n})$ the conjugate diagram gives the same multiset of hooks (Hook, arm, leg, and hook length of a box).

Proof

technique · strong induction on $n$

1.1baseF1F5given

Base cases: for $n = 0$ the only partition is $\emptyset$ , whose set of standard tableaux is the singleton consisting of the empty tableau, so $f^{\emptyset} = 1 = 0! / 1$ with empty product $1$ ; for $n = 1$ the only partition is $(1)$ , whose single box has $h = 1$ and exactly one standard tableau, so $f^{(1)} = 1 = 1! / 1$ .

1.2ihgiven

Induction hypothesis: for every $m$ with $0 \leq m < n$ and every partition $μ ⊢ m$ , $f^{μ} = m! / P (μ)$ .

1.3F4given

The dimension clause: by [F4], $\dim_{C} S^{λ} = f^{λ}$ for every $λ ⊢ n$ , including $λ = \emptyset$ where both sides are $1$ ; this holds for all $n$ because [F4] covers every $n \geq 0$ .

2.1step 1.2F1F2F3algebra

For $n \geq 2$ and $λ ⊢ n$ , [F1] gives $f^{λ} = \sum_{x \in Rem (λ)} f^{λ - x}$ ; each $λ - x$ is a partition of $n - 1 < n$ , so step 1.2 gives $f^{λ - x} = (n - 1)! / P (λ - x)$ , and [F2] turns this into $(n - 1)! R (x) / P (λ)$ . Summing over the removable nodes and using [F3], $f^{λ} = \frac{(n - 1)!}{P (λ)} \sum_{x} R (x) = \frac{(n - 1)! n}{P (λ)} = \frac{n!}{P (λ)}$ .

3.1step 2.1F5given

The two identities $f^{(n)} = 1 = f^{(1^{n})}$ follow because the hook multiset of $(n)$ and of $(1^{n})$ is ${1, 2, \dots, n}$ by [F5], so the formula gives $n! / n! = 1$ in both cases.

4.1step 1.1step 1.2step 2.1step 1.3step 3.1discharge-induction∎

Strong induction on $n$ : the base cases are step 1.1, the inductive step is step 2.1 with the hypothesis step 1.2, and steps 1.3 and 3.1 record the dimension and endpoint clauses; hence $f^{λ} = n! / \prod_{x \in [λ]} h (x)$ and $\dim_{C} S^{λ} = f^{λ}$ hold for every $n \geq 0$ and every $λ ⊢ n$ .

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-6.1-sol)Open item page →

Row insertion and the bumping route

Definition

Let $T$ be a standard tableau whose entries are distinct real numbers (Tableaux and standard tableaux) and let $x \in R$ be a number that is not an entry of $T$ . The row insertion $T \leftarrow x$ is the following procedure. Put $x_{1} : = x$ and consider row $1$ . At row $i$ : if row $i$ is empty or $x_{i}$ is larger than every entry of row $i$ , append $x_{i}$ in a new box at the right end of row $i$ and stop; otherwise let $r_{i}$ be the position of the leftmost entry $y_{i}$ of row $i$ with $y_{i} > x_{i}$ , replace that entry by $x_{i}$ , put $x_{i + 1} : = y_{i}$ , and continue with row $i + 1$ .

For distinct real alphabets, the phrase "standard tableau" in this insertion packet means an injective filling whose rows and columns strictly increase. Its unique increasing rank relabelling is a standard tableau with entries $1, \dots, m$ in the published convention. Each comparison in this procedure is preserved and reflected by increasing relabelling, so all positions and carried labels correspond under that relabelling, by induction over the finite procedure.

The procedure terminates, and the bound is proved rather than assumed. If $r_{i}$ is defined for a nonempty row $i$ , then either row $i + 1$ has length $< r_{i}$ , in which case the next step either bumps an entry in that shorter row, at a position $r_{i + 1} \leq λ_{i + 1}$ , or appends at $r_{i + 1} = λ_{i + 1} + 1$ ; in either case $r_{i + 1} \leq r_{i}$ , or row $i + 1$ has length $\geq r_{i}$ ; in the latter case its entry in position $r_{i}$ lies strictly below $y_{i}$ and is therefore larger than $y_{i}$ , so again the next replacement position, when it exists, satisfies $r_{i + 1} \leq r_{i}$ . Hence the route positions weakly decrease, and after at most $k + 1$ row visits, where $k$ is the number of nonempty rows of $T$ , the letter is appended (at the latest in the empty row $k + 1$ ).

The output is a filling of $[shape (T)] \cup {b}$ , where the new box is $b = (s, r_{s})$ with $r_{s} = λ_{s} + 1$ in the row $s$ in which the route stopped, or $b = (k + 1, 1)$ if a new row was opened. The sequence $(r_{1}, \dots, r_{s})$ is the bumping route and $x = x_{1} < x_{2} < \dots < x_{s}$ are the bumped letters; the strict increase of the bumped letters is proved in Monotonicity of the bumping route and standardness of the output. The procedure is deterministic, so $T \leftarrow x$ is well defined; standardness of the output is not part of the definition but is proved in the same lemma.

LemmaStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-6.1-sol)Open item page →

Monotonicity of the bumping route and standardness of the output

Statement

Let $T$ be a standard tableau with distinct real entries and let $x \notin T$ be a real number, with the notation of Row insertion and the bumping route for $T \leftarrow x$ . Then:

the bumped letters strictly increase, $x = x_{1} < x_{2} < \dots < x_{s}$ , and the route positions weakly decrease, $r_{1} \geq r_{2} \geq \dots \geq r_{s} \geq 1$ ;
the new box $b = (s, r_{s})$ is an addable node of $[shape (T)]$ , and $T \leftarrow x$ is a standard tableau of shape $shape (T) + b$ whose entries are exactly the entries of $T$ together with $x$ .

Facts & Assumptions

Given: A standard tableau $T$ with distinct real entries and a real number $x$ that is not an entry of $T$ .

[L1]

At row $i$ of $T \leftarrow x$ : if row $i$ is nonempty and some entry exceeds $x_{i}$ , then $r_{i}$ is the position of the leftmost such entry $y_{i}$ , the entry is replaced by $x_{i}$ and $x_{i + 1} : = y_{i}$ ; otherwise $x_{i}$ is appended at the right end of row $i$ , at position $λ_{i} + 1$ , and the route stops (Row insertion and the bumping route).

[L2]

For the distinct real alphabets of Row insertion and the bumping route, a standard tableau is an injective filling with strictly increasing rows and columns; its rank relabelling gives a standard tableau in the published alphabet ${1, \dots, n}$ , and $(i, j) \in [λ]$ with $(i + 1, j) \in [λ]$ implies $T (i, j) < T (i + 1, j)$ (Tableaux and standard tableaux, Partitions, English diagrams, and conjugation).

[L3]

A node $(i, λ_{i} + 1)$ is addable for $λ$ if and only if $i = 1$ or $λ_{i - 1} > λ_{i}$ ; and $[λ] \cup {(i, λ_{i} + 1)}$ is then the diagram of a partition (Removable and addable nodes).

Proof

technique · direct

1.1L1given

The bumped letters increase: when the route replaces at row $i$ , the new carried letter is $x_{i + 1} = y_{i} > x_{i}$ by the leftmost-greater choice of $r_{i}$ ; hence $x = x_{1} < x_{2} < \dots < x_{s}$ .

1.2L1L2

The positions weakly decrease: supposing the route continues from row $i$ to row $i + 1$ with $r_{i}$ defined, if row $i + 1$ has length $λ_{i + 1} \geq r_{i}$ , then the entry of $T$ at $(i + 1, r_{i})$ lies below the old entry $y_{i} = x_{i + 1}$ of $(i, r_{i})$ , so it exceeds $x_{i + 1}$ ; the leftmost entry of row $i + 1$ exceeding $x_{i + 1}$ is therefore at a position $r_{i + 1} \leq r_{i}$ . If instead $λ_{i + 1} < r_{i}$ , the next step either bumps at $r_{i + 1} \leq λ_{i + 1}$ or appends at $r_{i + 1} = λ_{i + 1} + 1$ ; both give $r_{i + 1} \leq r_{i}$ .

2.1step 1.2L1

The route terminates at a well-defined row $s$ : the positions are positive integers with $r_{1} \leq λ_{1} + 1$ , they weakly decrease along the visited rows, and after the last nonempty row the next row is empty and the letter is appended, so only finitely many rows are visited and the appended new box is $b = (s, r_{s})$ with $r_{s} = λ_{s} + 1$ .

3.1step 1.2step 2.1L3

The new box is addable: if $s = 1$ then $b = (1, λ_{1} + 1)$ is addable by [L3]; if $s > 1$ , the route reached row $s$ after replacing at row $s - 1$ , so $r_{s - 1} \leq λ_{s - 1}$ and $r_{s} = λ_{s} + 1 \leq r_{s - 1}$ by step 1.2, whence $λ_{s} < λ_{s - 1}$ and $b$ is addable by [L3].

3.2step 2.1L1

The entries of the output are exactly the entries of $T$ together with $x$ : each row visit writes the carried letter $x_{i}$ into a box of row $i$ and removes the entry $y_{i} = x_{i + 1}$ from it, and the final visit appends $x_{s}$ into the new box without removing anything; thus the multiset of entries changes from that of $T$ by adding $x_{1} = x$ and deleting nothing, and the shape grows by the single box $b$ .

4.1step 1.1step 1.2step 3.1L1L2

The output is standard: the replaced entries keep strictly increasing rows because $x_{i}$ is placed at the leftmost position whose old entry exceeded it, so its left neighbour is $< x_{i}$ and its right neighbour is larger than the displaced entry and hence $> x_{i}$ , and an appended letter exceeds every entry of its row; columns remain strictly increasing because at each replaced box $(i, r_{i})$ the entry above is either a previously placed bumped letter $x_{i - 1} < x_{i}$ or an unchanged entry lying left of the old entry $x_{i}$ in row $i - 1$ , hence smaller than $x_{i}$ , and the entry below is either the newly placed $x_{i + 1} > x_{i}$ (when $r_{i + 1} = r_{i}$ ) or the unchanged entry at $(i + 1, r_{i})$ , which exceeds the old entry $y_{i} = x_{i + 1}$ and hence $x_{i}$ (when $r_{i + 1} < r_{i}$ ), while the appended box $(s, λ_{s} + 1)$ lies below either a placed $x_{s - 1} < x_{s}$ or an unchanged entry left of the old entry $x_{s}$ of $(s - 1, r_{s - 1})$ ; all other boxes are unchanged.

5.1step 3.1step 3.2step 4.1∎

The output is a standard tableau of shape $shape (T) + b$ with entries those of $T$ plus $x$ , as asserted.

LemmaStatement: Literature-sourcedProof: Literature-sourcedjudge pass (gpt-6.1-sol)Open item page →

The recording tableau is standard

Statement

Let $w = (w_{1}, \dots, w_{N})$ be a word of pairwise distinct real numbers and define $P_{0} : = \emptyset$ and $P_{k} : = P_{k - 1} \leftarrow w_{k}$ for $1 \leq k \leq N$ (Row insertion and the bumping route). Let $Q_{k}$ be the filling of $[shape (P_{k})]$ that carries the label $k$ in the box added at step $k$ and the label $j$ in the box added at step $j$ for $j < k$ ; the boxes added at the successive steps are distinct addable nodes by Monotonicity of the bumping route and standardness of the output. Then every $Q_{k}$ is a standard tableau with entries $1, \dots, k$ of the same shape as $P_{k}$ ; in particular $Q_{N}$ is a standard tableau of size $N$ .

Facts & Assumptions

Given: A word $w = (w_{1}, \dots, w_{N})$ of pairwise distinct real numbers and the tableaux $P_{0}, \dots, P_{N}$ , with the box $b_{k}$ added at step $k$ and the fillings $Q_{k}$ .

[L1]

$P_{k}$ is standard and $b_{k}$ is an addable node of $[shape (P_{k - 1})]$ ; consequently $[shape (P_{k})] = [shape (P_{k - 1})] \cup {b_{k}}$ , the node $b_{k}$ is the end of its row and of its column of $[shape (P_{k})]$ , and the shape grows by exactly one box at each step (Monotonicity of the bumping route and standardness of the output).

[L2]

A standard tableau is a bijection from its diagram to an initial segment ${1, \dots, m}$ with strictly increasing rows and columns (Tableaux and standard tableaux).

[L3]

A node $(i, λ_{i} + 1)$ addable for $λ$ satisfies $i = 1$ or $λ_{i - 1} > λ_{i}$ , so after insertion it has no box to its right and, by weak decrease of the rows, no box below it (Removable and addable nodes, Partitions, English diagrams, and conjugation).

Proof

technique · induction

1.1baseL2given

Base: $Q_{0}$ is the empty filling of the empty shape, which is standard with entry set $\emptyset$ , and $shape (Q_{0}) = shape (P_{0})$ .

1.2ihgiven

Induction hypothesis: suppose $Q_{k - 1}$ is a standard tableau with entries $1, \dots, k - 1$ of shape $shape (P_{k - 1})$ .

2.1step 1.2L1L3

The box $b_{k}$ is the end of its row and of its column in $[shape (P_{k})]$ by [L1], so in $Q_{k}$ the new label $k$ has no right and no lower neighbour; its left neighbour and its upper neighbour, if present, carry labels $< k$ , and every comparison not involving $b_{k}$ is one already present in $Q_{k - 1}$ . Hence, with $k$ the largest label, rows and columns of $Q_{k}$ are strictly increasing.

3.1step 1.2step 2.1L1

The filling $Q_{k}$ is a bijection from $[shape (P_{k})]$ onto ${1, \dots, k}$ : $Q_{k - 1}$ is a bijection onto ${1, \dots, k - 1}$ by the induction hypothesis, the shapes differ by the single node $b_{k}$ , and $Q_{k}$ agrees with $Q_{k - 1}$ off $b_{k}$ and carries label $k$ on it.

4.1step 1.1step 1.2step 2.1step 3.1discharge-induction∎

By steps 2.1 and 3.1 and the induction hypothesis, $Q_{k}$ is a standard tableau with entries $1, \dots, k$ of shape $shape (P_{k})$ , for every $k \leq N$ , and induction over $k = 0, \dots, N$ proves the assertion; in particular $Q_{N}$ is standard of size $N$ .

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-6.1-sol)Open item page →

Reverse row deletion

Definition

Let $U$ be a standard tableau with distinct real entries (Tableaux and standard tableaux) and let $b = (s, t)$ be a removable node of $[shape (U)]$ (so $t = λ_{s}$ for $λ = shape (U)$ ). The reverse row deletion $U - b$ is the following procedure. Set $i : = s$ and $x_{s + 1} : = + \infty$ (a symbol larger than every real number). While $i \geq 1$ : let $j$ be the largest index with $1 \leq j \leq λ_{i}$ and $U (i, j) < x_{i + 1}$ (for $i = s$ this is $j = λ_{s} = t$ , the box $b$ ), set $x_{i} : = U (i, j)$ and overwrite the entry of box $(i, j)$ by $x_{i + 1}$ (for $i = s$ this empties the box $b$ ); if $i = 1$ stop, otherwise replace $i$ by $i - 1$ and repeat. The procedure terminates after exactly $s$ row visits, since $i$ strictly decreases and stops at $1$ . Its result is the filling $V$ of $[shape (U)] ∖ {b}$ obtained by the overwrites, and the expelled letter is $x_{1}$ . We write $(V, x_{1}) : = U - b$ .

The index $j$ exists at every step, and $V$ is a standard tableau, so the procedure is well defined. For existence: after a row $i + 1$ has been processed, the carried letter $x_{i + 1}$ was the entry of the box $(i + 1, j_{i + 1})$ before that box was overwritten, where $j_{i + 1}$ is the position used in row $i + 1$ ; the box $(i, j_{i + 1})$ of the row above lies in the diagram, because $j_{i + 1} \leq λ_{i + 1} \leq λ_{i}$ , and by column strictness of $U$ it carries an entry strictly smaller than $x_{i + 1}$ ; hence the set over which $j$ is defined is nonempty, and it is finite, so $j$ is well defined. For standardness of $V$ : at the moment row $i$ is processed it is still the unmodified row $i$ of $U$ , and $j$ is the largest index with $U (i, j) < x_{i + 1}$ , so $U (i, j - 1) < x_{i + 1} < U (i, j + 1)$ when those neighbours exist, which keeps the row strictly increasing after the overwrite; the entry above the overwritten box is $U (i - 1, j) < U (i, j) < x_{i + 1}$ ; and the entry below, $U (i + 1, j)$ after row $i + 1$ has been processed, is larger than $x_{i + 1}$ : if $j = j_{i + 1}$ it is the overwriting letter $x_{i + 2} > x_{i + 1}$ , and if $j > j_{i + 1}$ it is the unchanged entry in column $j$ of row $i + 1$ , which exceeds the unchanged entry $U (i + 1, j_{i + 1}) = x_{i + 1}$ by row strictness. Thus all strict inequalities of a standard tableau hold in $V$ . Finally, every entry of $U$ other than $x_{1}$ survives in $V$ with multiplicity one: each row visit moves one entry upward into the box it overwrites and the single box $b$ is emptied, so the multiset of entries of $V$ is that of $U$ with $x_{1}$ deleted; in particular $x_{1}$ is not an entry of $V$ . No choice is used: the procedure is deterministic and all data are finite.

LemmaStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-6.1-sol)Open item page →

Row insertion and reverse deletion are inverse

Statement

Let $T$ be a standard tableau with distinct real entries, let $x \notin T$ be a real number, and let $U : = T \leftarrow x$ with new box $b$ (Row insertion and the bumping route). Then:

$U - b = (T, x)$ , i.e. reverse deletion from the new box returns $T$ and expels $x$ .
Conversely, if $U$ is a standard tableau, $b$ a removable node of $[shape (U)]$ , and $(V, x) : = U - b$ the result of reverse deletion (Reverse row deletion), then $x \notin V$ and $V \leftarrow x = U$ with new box $b$ .

Thus reverse deletion at the new box undoes insertion, and insertion undoes reverse deletion at any removable box.

Facts & Assumptions

Given: A standard tableau $T$ with distinct real entries, a real number $x \notin T$ , the insertion $U = T \leftarrow x$ with route positions $r_{1} \geq \dots \geq r_{s}$ and added box $b = (s, r_{s})$ , and, for the converse, a standard tableau $U$ with a removable box $b = (s, t)$ and $(V, x) : = U - b$ .

[L1]

Insertion places $x_{i}$ at position $r_{i}$ of row $i$ , bumping the old entry $x_{i + 1}$ there for $i < s$ , and appends $x_{s}$ in the new box $b$ ; rows and columns of $U$ are strictly increasing (Row insertion and the bumping route, Monotonicity of the bumping route and standardness of the output).

[L2]

Reverse deletion from $b = (s, t)$ starts at row $s$ with $x_{s + 1} : = + \infty$ and, descending, at row $i$ takes $j_{i}$ to be the largest index with $U (i, j_{i}) < x_{i + 1}$ , sets $x_{i} : = U (i, j_{i})$ , overwrites $U (i, j_{i})$ by $x_{i + 1}$ , and the result $V$ is standard with entries the entries of $U$ except $x_{1}$ (Reverse row deletion).

[L3]

In a standard tableau the entries strictly increase along rows and down columns, so an entry left of a given position is smaller and an entry right of it is larger (Tableaux and standard tableaux).

Proof

technique · direct

1.1L1L2

(First direction, row $s$ .) In $U$ the appended letter is $x_{s}$ at position $r_{s} = λ_{s} + 1$ of row $s$ , so row $s$ of $U$ equals row $s$ of $T$ followed by $x_{s}$ , and the largest index $j_{s}$ with $U (s, j_{s}) < + \infty$ is $r_{s}$ . Reverse deletion therefore sets $x_{s} = U (s, r_{s})$ , empties that cell (so that $V$ has shape $[shape (T)]$ ), and continues upward.

1.2L2L3

(Converse direction, insertion route.) If $s = 1$ , deletion removes the final entry $x_{1}$ of row1 and reinsertion appends it, so the converse is immediate. For $s \geq 2$ , let $(V, x) = U - b$ with deletion positions $j_{1}, \dots, j_{s}$ , so $j_{s} = t$ , row $i$ of $V$ agrees with row $i$ of $U$ off the single cell $(i, j_{i})$ and carries $x_{i + 1}$ there for $i < s$ (with the cell $b = (s, j_{s})$ absent), and the expelled letter is $x = x_{1}$ . In row $1$ of $V$ , the entries left of $j_{1}$ are the entries of $U$ left of $(1, j_{1})$ , hence smaller than $x_{1}$ , and the entries right of $j_{1}$ are the entries of $U$ right of it, hence larger than $x_{1}$ ; the entry at $j_{1}$ is $x_{2}$ . So inserting $x_{1}$ replaces position $j_{1}$ and bumps $x_{2}$ .

2.1step 1.1L1L2L3

(First direction, induction upward.) Suppose reverse deletion carries $x_{i + 1}$ into row $i < s$ , after restoring the lower rows. Row $i$ is still the row of $U$ : its entry at $r_{i}$ is $x_{i} < x_{i + 1}$ , its entries left of $r_{i}$ are smaller than $x_{i}$ , and its entries right of $r_{i}$ are unchanged entries of $T$ strictly greater than the old displaced value $T (i, r_{i}) = x_{i + 1}$ . Thus the rightmost entry smaller than $x_{i + 1}$ is exactly $r_{i}$ . Reverse deletion carries $x_{i}$ upward and restores $T (i, r_{i}) = x_{i + 1}$ . Inducting from the final-box deletion in step 1.1 restores every row of $T$ .

2.2step 1.2L1L2L3

(Converse direction, induction downward.) At row $i < s$ , deletion removed $x_{i}$ at $j_{i}$ and replaced it by $x_{i + 1} > x_{i}$ . The entries of $V$ left of $j_{i}$ are unchanged entries of $U$ smaller than $x_{i}$ , and those to its right are unchanged entries larger than $x_{i + 1}$ , since $j_{i}$ was the rightmost entry smaller than $x_{i + 1}$ and the entries are distinct. Therefore, when reinsertion carries $x_{i}$ into row $i$ , it chooses exactly $j_{i}$ , restores $x_{i}$ , and bumps $x_{i + 1}$ into row $i + 1$ . Starting at row1 with $x = x_{1}$ , this induction reconstructs all replaced rows. In the final row $s$ , deletion removed its row-end value $x_{s}$ , so the remaining entries are smaller than $x_{s}$ and reinsertion appends it precisely in $b = (s, j_{s})$ .

3.1step 1.1step 2.1L1

(First direction, conclusion.) By step 1.1 and downward induction in step 2.1, reverse deletion visits the rows $s, s - 1, \dots, 1$ , restores in each row $i$ the entry of $T$ at $(i, r_{i})$ , expels $x_{1} = x$ , and leaves the filling $T$ of shape $[shape (T)]$ ; that is, $U - b = (T, x)$ .

4.1step 1.2step 2.2L1L2∎

(Converse direction, conclusion.) By steps 1.2 and 2.2 the insertion of $x$ into $V$ follows the positions $j_{1}, \dots, j_{s}$ , rewrites the same entries as $U$ and appends at $b$ ; hence $V \leftarrow x = U$ with new box $b$ . Finally $x \notin V$ , because by [L2] the entries of $V$ are the entries of $U$ with $x_{1}$ deleted, and $U$ has distinct entries.

TheoremStatement: Literature-sourcedProof: AI-adaptedOpen item page →

The Robinson-Schensted correspondence

Statement

For $n \geq 0$ let $X_{n}$ be the set of words $(w_{1}, \dots, w_{n})$ of pairwise distinct real numbers with ${w_{1}, \dots, w_{n}} = {1, 2, \dots, n}$ (the permutations of ${1, \dots, n}$ written in one-line form). The Robinson-Schensted map $w \mapsto (P (w), Q (w))$ , where $P (w)$ is the iterated row insertion of $w_{1}, \dots, w_{n}$ (Row insertion and the bumping route) and $Q (w)$ the recording tableau of The recording tableau is standard, is a bijection from $X_{n}$ onto the set of pairs $(P, Q)$ of standard tableaux of the same shape $λ ⊢ n$ . The inverse map sends a pair $(P, Q)$ to the word recovered by iterated reverse deletion: for $k = n, n - 1, \dots, 1$ , delete from the current insertion tableau the box occupied by the label $k$ in the current recording tableau (a removable node, by The largest standard entry lies in a removable box and The recording tableau is standard), record the expelled letter as $w_{k}$ , and continue with the two shrunken tableaux.

Facts & Assumptions

Given: An integer $n \geq 0$ , a word $w = (w_{1}, \dots, w_{n}) \in X_{n}$ , the tableaux $P_{k}$ obtained by inserting $w_{1}, \dots, w_{k}$ , the recording tableaux $Q_{k}$ , and the iterated deletion procedure of the statement.

[F1]

Each $P_{k}$ is an injective filling with strictly increasing rows and columns and entries $w_{1}, \dots, w_{k}$ , hence is standard in the distinct-alphabet convention of the insertion packet; the box added at step $k$ makes the shape grow by one addable node (Monotonicity of the bumping route and standardness of the output, Row insertion and the bumping route).

[F2]

Each $Q_{k}$ is a standard tableau with entries $1, \dots, k$ of the same shape as $P_{k}$ (The recording tableau is standard).

[F3]

In a standard tableau of size $k \geq 1$ the box occupied by $k$ is removable, and deleting it leaves a standard tableau of size $k - 1$ (The largest standard entry lies in a removable box).

[F4]

For a standard tableau $U$ with distinct real entries and a removable box $b$ , reverse deletion $(V, x) : = U - b$ gives a standard tableau $V$ whose entries are those of $U$ with $x$ removed, and $V \leftarrow x = U$ with new box $b$ . Conversely, if $U = T \leftarrow x$ with new box $b$ , then $U - b = (T, x)$ (Reverse row deletion, Row insertion and reverse deletion are inverse).

[F5]

A standard tableau of shape $μ ⊢ k$ has exactly $k$ boxes carrying the entries $1, \dots, k$ once each, and two tableaux of the same shape with the same entries in every box are equal (Tableaux and standard tableaux, Partitions, English diagrams, and conjugation, Removable and addable nodes).

Proof

technique · direct

1.1F1F5

Each $P_{k}$ is standard on the alphabet ${w_{1}, \dots, w_{k}}$ by [F1], obtained by applying the insertion lemma once per letter. In particular $P_{n}$ has entries $1, \dots, n$ and is standard in the published convention.

1.2F2

Each $Q_{k}$ is standard with entries $1, \dots, k$ and $shape (Q_{k}) = shape (P_{k})$ : this is [F2].

1.3F3

In a standard tableau of size $k \geq 1$ the box of the largest entry $k$ is removable: this is [F3].

1.4F4

If $U$ is standard with distinct real entries and $b$ is a removable box, then reverse deletion gives $(V, x) = U - b$ with $V$ standard, its entries those of $U$ except $x$ , and $V \leftarrow x = U$ with new box $b$ : this is [F4].

2.1step 1.3step 1.4F2F5

Reinsertion restores any pair: start with standard tableaux $(U_{n}, R_{n})$ of a common shape with $n$ boxes. Recursively, let $b_{k}$ be the box of label $k$ in $R_{k}$ , set $(U_{k - 1}, v_{k}) : = U_{k} - b_{k}$ , and remove $b_{k}$ from $R_{k}$ to obtain $R_{k - 1}$ . Step 1.3 makes $b_{k}$ removable in both shapes, and step 1.4 preserves increasing rows and columns of $U_{k - 1}$ on its remaining alphabet; $R_{k - 1}$ remains standard with entries $1, \dots, k - 1$ . Thus every deletion is defined. Each reinsertion $U_{k - 1} \leftarrow v_{k}$ returns $U_{k}$ with new box $b_{k}$ , so writing recording label $k$ returns $R_{k}$ . Induction from the empty pair therefore gives the RSK pair of $(v_{1}, \dots, v_{n})$ as $(U_{n}, R_{n})$ .

3.1step 2.1F2F4

Deletion recovers the original word: the procedure is well defined by step 2.1, and in $(P_{k}, Q_{k})$ the box of label $k$ is precisely the new box of $P_{k} = P_{k - 1} \leftarrow w_{k}$ . The converse identity in [F4] therefore deletes this box to give $(P_{k - 1}, w_{k})$ ; removing its recording label leaves $Q_{k - 1}$ . Induction for $k = n, n - 1, \dots, 1$ recovers all original letters. Hence, if $P (w) = P (w^{'})$ and $Q (w) = Q (w^{'})$ , the deterministic deletion procedure recovers both words from the same pair, so $w = w^{'}$ .

3.2step 1.3step 1.4step 2.1F5

Surjectivity: let $(P, Q)$ be any pair of standard tableaux of a common shape $λ ⊢ n$ . Running the procedure of step 2.1 from $(P, Q)$ is well defined at every step by step 1.3, and produces a word $w = (w_{1}, \dots, w_{n})$ whose letters are the entries of $P$ , each expelled exactly once (the entries of $P_{k - 1}$ are those of $P_{k}$ with $w_{k}$ deleted by step 1.4), hence precisely $1, \dots, n$ ; by the induction of step 2.1 the RSK pair of $w$ is $(P, Q)$ .

4.1step 2.1step 3.1step 3.2F5∎

The map $w \mapsto (P (w), Q (w))$ is therefore a bijection from $X_{n}$ onto the set of pairs of standard tableaux of the same shape $λ ⊢ n$ : steps 2.1 and 3.1 establish both inverse identities, and step 3.2 gives surjectivity onto the stated set. For $n = 0$ both procedures have no steps and exchange the unique empty word and empty pair.

LemmaStatement: Literature-sourcedProof: Literature-sourcedjudge pass (gpt-6.1-sol)Open item page →

Basic subsequences of the first row

Statement

Let $w = (w_{1}, \dots, w_{N})$ be a word of pairwise distinct real numbers and let $P (w)$ be its insertion tableau, built by Row insertion and the bumping route. For $j \geq 1$ let $S_{j}$ be the list, in the order of insertion, of those letters which at the moment of their insertion are placed in position $j$ of the first row (equivalently, the letters that pass through the $j$ -th position of the first row). Then:

each $S_{j}$ is a strictly decreasing subsequence of $w$ ;
for every $x \in S_{j}$ with $j \geq 2$ , the entry $y$ occupying position $j - 1$ of the first row at the moment $x$ is inserted belongs to $S_{j - 1}$ , was inserted earlier than $x$ , and satisfies $y < x$ .

The lists $S_{1}, S_{2}, \dots$ are the basic subsequences of $w$ .

Facts & Assumptions

Given: A word $w = (w_{1}, \dots, w_{N})$ of pairwise distinct real numbers, its insertion tableaux $P_{k} = P (w_{1}, \dots, w_{k})$ , and for each $j \geq 1$ the list $S_{j}$ of letters placed at position $j$ of the first row at their own insertion.

[L1]

At each step the insertion of $w_{k}$ processes the first row once: either it appends $w_{k}$ at the end of the first row, at position $λ_{1} + 1$ , or it replaces the leftmost first-row entry exceeding $w_{k}$ , at some position $j \leq λ_{1}$ , and passes that displaced entry to the second row. Both alternatives place exactly one letter in the first row, and positions of the first row are filled from the left: a position $j$ can receive a letter only at a step, and thereafter its occupant is whatever was placed there last (Row insertion and the bumping route).

[L2]

$P_{k}$ is a standard tableau and its first row is strictly increasing, so its entry in position $j - 1$ is smaller than its entry in position $j$ whenever both positions exist (Monotonicity of the bumping route and standardness of the output, Tableaux and standard tableaux).

Proof

technique · direct

1.1L1

A letter is placed at position $j$ of the first row only when position $j$ already exists and is replaced, or when it is appended as the new last position $j = λ_{1} + 1$ ; in the replacement case the placed letter is strictly smaller than the entry it replaces, by the leftmost-greater rule, and in the append case position $j$ had no previous occupant.

1.2L1given

The lists $S_{j}$ consist of distinct steps of the word in increasing order, because at each step at most one letter is placed in the first row; therefore each $S_{j}$ is a subsequence of $w$ .

1.3L1L2given

Let $x \in S_{j}$ with $j \geq 2$ , inserted at step $k$ , and let $y$ be the entry occupying position $j - 1$ of the first row immediately before the insertion of $w_{k}$ . Position $j - 1$ exists because $j \leq λ_{1} + 1$ at that moment, and $y < x$ : in a replacement this follows from the leftmost entry exceeding $x$ being at position $j$ , so every earlier entry is smaller than $x$ ; in an append it follows from $x$ exceeding every old row entry.

2.1step 1.1L1

Since the occupant of position $j$ is always the last letter placed there (step 1.1), each successive element of $S_{j}$ is strictly smaller than its predecessor: the predecessor is the occupant replaced at the successor's insertion step. Hence $S_{j}$ , read in the order of insertion, is strictly decreasing.

3.1step 2.1step 1.2step 1.3L1

The entry $y$ was placed at position $j - 1$ at some earlier step $k^{'} < k$ : by step 1.1 every occupant of a position of the first row is placed there at a step, and $y$ is the current occupant before step $k$ , so its placement step precedes $k$ . Hence $y \in S_{j - 1}$ and $y$ is inserted earlier than $x$ , which together with $y < x$ proves (2).

4.1step 2.1step 1.2step 3.1∎

Consequently every element of $S_{j}$ with $j \geq 2$ has an earlier smaller predecessor in $S_{j - 1}$ , while each $S_{j}$ is strictly decreasing; this is the assertion of the lemma.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-6.1-sol)Open item page →

Column insertion

Definition

Let $T$ be a standard tableau with distinct real entries (Tableaux and standard tableaux) and let $x \notin T$ be a real number. The column insertion $x \to T$ is defined by the same rules as row insertion with rows replaced by columns: put $x_{1} : = x$ and consider column $1$ . At column $i$ : if column $i$ is empty or $x_{i}$ is larger than every entry of column $i$ , append $x_{i}$ in a new box at the bottom of column $i$ and stop; otherwise let $y_{i}$ be the topmost entry of column $i$ that is larger than $x_{i}$ , replace that entry by $x_{i}$ , put $x_{i + 1} : = y_{i}$ , and continue with column $i + 1$ . Equivalently, $x \to T = (T^{t} \leftarrow x)^{t},$ where $T^{t}$ is the transposed tableau (a standard tableau of shape $[shape (T)^{'}]$ , Partitions, English diagrams, and conjugation) and $\leftarrow$ is the row insertion of Row insertion and the bumping route; the equivalence is the observation that transposing a tableau interchanges rows and columns, so "leftmost entry of a row greater than the carried letter" becomes "topmost entry of a column greater than the carried letter".

By the equivalence, the column procedure terminates and $x \to T$ is a standard tableau with entries those of $T$ together with $x$ , of shape $[shape (T)]$ with one box added at the bottom of a column: this is Monotonicity of the bumping route and standardness of the output applied to $T^{t}$ , whose new box transposes back to a box at the bottom of a column of $T$ . The route positions weakly decrease from column to column, again by transposing the position bound for row insertion. No choice is used; the procedure is deterministic.

LemmaStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-6.1-sol)Open item page →

Row and column insertion commute

Statement

Let $T$ be a standard tableau with distinct real entries and let $x \neq y$ be real numbers not occurring in $T$ . Then $(x \to T) \leftarrow y = x \to (T \leftarrow y),$ the equality being an equality of standard tableaux on the same diagram; equivalently, in the notation of the definitional relation $x \to T = (T^{t} \leftarrow x)^{t}$ , row-inserting $y$ commutes with column-inserting $x$ .

Facts & Assumptions

Given: A standard tableau $T$ with distinct real entries, real numbers $x \neq y$ not occurring in $T$ , the row insertion $T \leftarrow y$ (Row insertion and the bumping route) and the column insertion $x \to T$ (Column insertion).

[L1]

In the row insertion $T \leftarrow y$ the route positions are $(1, c_{1}), \dots, (k, c_{k})$ with $c_{1} \geq \dots \geq c_{k} \geq 1$ and $c_{k} = λ_{k} + 1$ , the bumped labels $ω_{1} = T (1, c_{1}) < \dots < ω_{k - 1} = T (k - 1, c_{k - 1})$ strictly increase, and $T \leftarrow y$ is the standard tableau obtained by placing $y$ at $(1, c_{1})$ and moving $T (i, c_{i})$ from $(i, c_{i})$ to $(i + 1, c_{i + 1})$ for $i < k$ (Row insertion and the bumping route, Monotonicity of the bumping route and standardness of the output).

[L2]

$x \to T = (T^{t} \leftarrow x)^{t}$ ; transposing [L1] gives the route $(r_{1}, 1), \dots, (r_{l}, l)$ of $x \to T$ with rows $r_{1} \geq r_{2} \geq \dots \geq r_{l} \geq 1$ with $r_{l} = λ_{l}^{'} + 1$ (where $λ_{λ_{1} + 1}^{'} = 0$ when a new column $l = λ_{1} + 1$ is opened), strictly increasing carried labels, and $x \to T$ obtained by placing $x$ at $(r_{1}, 1)$ and moving the old label of $(r_{j}, j)$ to $(r_{j + 1}, j + 1)$ for $j < l$ (Column insertion, Partitions, English diagrams, and conjugation).

[L3]

Entries of a standard tableau strictly increase along every row and every column; all entries of $T$ , $x$ and $y$ are pairwise distinct (Tableaux and standard tableaux, Row insertion and the bumping route).

[L4]

For the finite distinct real alphabets here, an increasing tableau means an injective filling with strictly increasing rows and columns. Replacing its entries by their ranks gives a standard tableau in the published alphabet $1, \dots, m$ (Tableaux and standard tableaux). Every insertion comparison is preserved by increasing relabelling; this is the real-alphabet convention used in the statement and insertion suppliers.

Proof

technique · direct

1.1L1L2L3L4

A finite real alphabet has a unique increasing enumeration. Its rank map preserves and reflects all inequalities, so the first-greater position, each carried label, and the final shape are unchanged under relabelling, by induction over the finite procedure; compressing the entry ranks gives the published standard tableau. Thus strict-row/strict-column arguments apply to the original real labels as well. For each insertion call its activated boxes, including its final new box, its trail. A row trail has increasing row numbers and weakly decreasing columns; a column trail has increasing columns and weakly decreasing rows. At each occupied trail box the old label is replaced by the smaller preceding carried label; at the final empty box the last label is appended. Each occupied label sequence strictly increases, by [L1] and its transpose [L2].

2.1step 1.1L3

The two original trails have at most one common box. For two occupied common boxes, order them by increasing row: their labels increase along the row trail, whereas their distinct columns decrease, so their order on the column trail is reversed and their labels would decrease, a contradiction. An empty common box must be empty for both trails because only occupied boxes belong to $T$ . If it were shared along with an occupied box, that occupied box would have a smaller row than the empty box on the row trail and a smaller column on the column trail; the row trail instead requires its earlier column to be at least the final column. This is impossible.

2.2L1L2L3step 1.1algebra

Bump stability: if the entry bumped by a carried letter $z$ is unchanged, and every entry left of it is unchanged or decreased, that entry remains the leftmost entry exceeding $z$ . Thus away from a common box, sliding the other trail leaves each occupied bump of a row trail unchanged; this applies successively since the same labels are carried. A new box from the other slide lies at an old row end, so cannot interfere with an occupied bump to its left. At an append step it can interfere only if it is that same row-end box, which would be a second common box. The transposed assertions hold for columns.

3.1step 2.2L1L2

If the trails are disjoint, step 2.2 proves that each insertion into the result of the other has exactly its original trail and carried labels. The two composites therefore perform the same two slides on disjoint boxes and agree.

3.2step 1.1step 2.1L1L2L3

Suppose their common box $S = (ρ, γ)$ is occupied, with old label $s$ . Let $a$ and $i$ be the labels carried into $S$ by the column and row insertions. If there is a preceding column-trail box, call it $A = (r, γ - 1)$ , with $r \geq ρ$ and old label $a$ ; otherwise $γ = 1$ and $a = x$ . If there is a preceding row-trail box, call it $I = (ρ - 1, c)$ , with $c \geq γ$ and old label $i$ ; otherwise $ρ = 1$ and $i = y$ . Let $B$ and $J$ be the next boxes of the column and row trails, in column $γ + 1$ and row $ρ + 1$ , respectively; they may be their final empty boxes. Their old labels, when occupied, are $b > s$ and $j > s$ . Also $a < s$ , $i < s$ , and $a \neq i$ : the predecessor boxes have different coordinates, and the input letters are distinct and absent from $T$ .

4.1step 3.2step 2.1L3algebra

If $A$ is not immediately left of $S$ , then $J$ is immediately below $S$ . Indeed, if $A$ exists then $r \geq ρ + 1$ . If $J = (ρ + 1, c^{'})$ had $c^{'} < γ$ , it would lie weakly above and left of $A$ , hence be occupied and have label $j \leq a$ (with equality only if it were $A$ ). Equality is excluded by step 2.1, and strict inequality contradicts $a < s < j$ . If $A$ does not exist, $γ = 1$ already forces $c^{'} = 1$ . Transposing this argument shows that if $I$ is not immediately above $S$ , then $B$ is immediately right of $S$ . These arguments also handle empty $J$ or $B$ , since a box weakly above and left of an occupied box cannot be empty in a Young diagram.

5.1step 4.1step 2.2L1L2L3

Assume $i < a$ . Then $A$ cannot be immediately left of $S$ , since the row insertion which carries $i$ to $S$ has every old entry left of $S$ smaller than $i$ . Thus $J = (ρ + 1, γ)$ by step 4.1. Perform the column slide first. All row bumps before $S$ remain unchanged by step 2.2. At $S$ the value is now $a > i$ , while every entry to its left has remained unchanged or decreased from a value smaller than $i$ , so the row insertion places $i$ at $S$ and bumps $a$ .

5.2step 4.1step 2.1step 2.2L1L2L3

Assume $i > a$ . Then $I$ cannot be immediately above $S$ , since the column insertion carrying $a$ to $S$ has every old entry above $S$ smaller than $a$ . Hence $B = (ρ, γ + 1)$ by step 4.1. After the column slide the entries at $S, B$ are $a, s$ . The row trail before $S$ is unchanged by step 2.2. In row $ρ$ its carried label $i$ exceeds $a$ , all entries left of $S$ are smaller than $i$ , and $s > i$ , so the row insertion puts $i$ at $B$ and bumps $s$ . Its next bump is the original box $J$ , since that box is unchanged, its old label exceeds $s$ , all old entries to its left were smaller than $s$ , and the column slide only decreases them. An empty $J$ remains the append box, since a second common box is excluded. Step 2.2 gives the rest of the original row trail. Thus $S, B, J$ have labels $a, i, s$ , and all other boxes have their ordinary slid labels.

6.1step 5.1step 3.2step 2.1step 2.2L3

In row $ρ + 1$ every entry left of $J$ is smaller than $a$ after the column slide. For $γ > 1$ , its last possible entry is at $(ρ + 1, γ - 1)$ : if $A$ is lower than that box, the old value there is smaller than $a$ by column strictness; if $A$ is that box, the slide replaces $a$ by a smaller label. All other changes decrease labels. For $γ = 1$ there is no left entry. The box $J$ is unchanged by the column slide, since the only common box is $S$ ; if occupied its label $j > s > a$ , and if empty it is still the row-end box. Thus the row insertion puts $a$ at $J$ and carries $j$ onward if it exists. Step 2.2 then preserves the remaining original row trail. The final labels at $S, B, J$ are $i, s, a$ , and every other box has its ordinary slid label. The label $s$ at $B$ is not touched by the row insertion: before $S$ that row trail is unchanged, and after $S$ it lies in rows greater than $ρ$ , whereas $B$ has row at most $ρ$ .

7.1step 5.1step 6.1step 5.2L2

Transpose the tableau and exchange the roles of the inputs and trails. The same row-after-column calculation becomes the column-after-row calculation. When $i < a$ , transposition changes the inequality to the case of step 5.2 and exchanges $B, J$ , giving again $i, s, a$ at the original $S, B, J$ ; when $i > a$ , it changes to the case $i < a$ and gives again $a, i, s$ . Both composites therefore agree when the common box is occupied. The predecessor or successor may be missing: the preceding local arguments explicitly use the input label at a missing predecessor and the append rule at an empty successor, so no boundary case was omitted.

7.2step 2.2step 6.1L1L2L3algebra

Finally let $S = (ρ, γ)$ be the common empty box, and let $a, i$ be the final carried column and row labels, with the input labels used for one-box trails. The prefixes slide identically by step 2.2. If $i < a$ , filling $S$ with $a$ and then row-inserting $i$ bumps $a$ at $S$ . Its next box is $(ρ + 1, γ)$ : if $γ > 1$ , the last column predecessor $A$ is not immediately left of $S$ , because the original row append requires every entry to its left to be smaller than $i < a$ ; hence $A$ is in row at least $ρ + 1$ , the next row has exactly $γ - 1$ boxes, and its entries after the column slide are all smaller than $a$ , as in step 6.1. If $γ = 1$ that row is empty. Thus $i$ is placed at $S$ and $a$ directly below it. In the opposite order, row insertion first places $i$ at $S$ ; the final column insertion carries $a > i$ and appends it directly below $S$ , with the same result. If $i > a$ , transpose this argument: both composites place $a$ at $S$ and $i$ directly right of it. This also covers $T = \emptyset$ , where $a = x$ and $i = y$ .

8.1step 2.1step 3.1step 7.1step 7.2∎

The original trails are disjoint, share one occupied box, or share their empty box, by step 2.1. Steps 3.1, 7.1 and 7.2 prove equality of the composites in every case, with the same shape and every label specified. Hence $(x \to T) \leftarrow y = x \to (T \leftarrow y)$ for all the stated distinct letters.

LemmaStatement: Literature-sourcedProof: Literature-sourcedjudge pass (gpt-6.1-sol)Open item page →

Reversing a word transposes its insertion tableau

Statement

Let $w = (w_{1}, \dots, w_{n})$ be a word of pairwise distinct real numbers and let $P (w_{1}, \dots, w_{n})$ denote the row-insertion tableau built by inserting $w_{1}, \dots, w_{n}$ in this order (Row insertion and the bumping route). Then $P (w_{1}, \dots, w_{n}) = P (w_{n}, \dots, w_{1})^{t},$ i.e. reversing the word transposes the insertion tableau. Equivalently, the first-letter column-insertion recursion $P (x_{1}, \dots, x_{n}) = x_{1} \to P (x_{2}, \dots, x_{n})$ (Column insertion) holds for every word of distinct letters. There is no corresponding assertion for the recording tableau (Schensted's note).

Facts & Assumptions

Given: A word $(x_{1}, \dots, x_{n})$ of pairwise distinct real numbers, the tableaux $P (x_{1}, \dots, x_{k})$ obtained by inserting $x_{1}, \dots, x_{k}$ in this order, and the column insertion $\to$ of Column insertion.

[L1]

$P (x_{1}, \dots, x_{k}) \leftarrow x_{k + 1} = P (x_{1}, \dots, x_{k + 1})$ for $k \geq 1$ , and $P (x_{1}) = [x_{1}]$ is the one-box tableau; the empty word inserts to $\emptyset$ (Row insertion and the bumping route).

[L2]

$x \to T = (T^{t} \leftarrow x)^{t}$ for every standard tableau $T$ and letter $x \notin T$ ; equivalently $(x \to T)^{t} = T^{t} \leftarrow x$ (Column insertion).

[L3]

For standard tableaux $T$ with distinct real entries and letters $x \neq y$ not in $T$ one has $(x \to T) \leftarrow y = x \to (T \leftarrow y)$ (Row and column insertion commute).

[L4]

Row-inserting a letter into a standard tableau with distinct entries gives a standard tableau whose entries are those of $T$ together with the letter, and transposition is an involution carrying standard tableaux of shape $λ$ to standard tableaux of shape $λ^{'}$ (Tableaux and standard tableaux, Monotonicity of the bumping route and standardness of the output, Column insertion).

[L5]

Proof

technique · direct

1.1L1L2L5

A finite real alphabet has a unique increasing enumeration. Its rank map preserves and reflects all inequalities, so the first-greater position, each carried label, and the final shape are unchanged under relabelling, by induction over the finite procedure; compressing the entry ranks gives the published standard tableau. Thus strict-row/strict-column arguments apply to the original real labels as well. (Base case and first-letter recursion.) $P (x_{1}) = [x_{1}] = x_{1} \to \emptyset$ : by [L2] with $T = \emptyset$ one has $x_{1} \to \emptyset = (\emptyset^{t} \leftarrow x_{1})^{t}$ , the insertion appends $x_{1}$ as the only box, and a one-box tableau equals its transpose; hence for $n = 1$ the recursion holds.

1.2L1L3L4ih

(First-letter recursion, inductive step.) Let $n \geq 2$ and assume the recursion for words of length $n - 1$ . Then $P (x_{1}, \dots, x_{n}) = P (x_{1}, \dots, x_{n - 1}) \leftarrow x_{n} = (x_{1} \to P (x_{2}, \dots, x_{n - 1})) \leftarrow x_{n} = x_{1} \to (P (x_{2}, \dots, x_{n - 1}) \leftarrow x_{n}) = x_{1} \to P (x_{2}, \dots, x_{n})$ : the first and last equalities are [L1], the second is the induction hypothesis, and the third is [L3] applied to the standard tableau $T = P (x_{2}, \dots, x_{n - 1})$ with $x = x_{1}$ , $y = x_{n}$ , legitimate because the letters are pairwise distinct, so $x_{1} \notin T$ and $x_{1} \neq x_{n}$ .

1.3L1L4

(Reversal, base cases.) For $n = 0$ both sides are $\emptyset$ and $\emptyset^{t} = \emptyset$ ; for $n = 1$ the one-box tableau equals its transpose.

2.1step 1.1step 1.2discharge-induction

(First-letter recursion, conclusion.) By steps 1.1 and 1.2 the recursion $P (x_{1}, \dots, x_{n}) = x_{1} \to P (x_{2}, \dots, x_{n})$ holds for every $n \geq 1$ and every word of distinct letters.

3.1step 2.1step 1.3L1L2ih

(Reversal, inductive step.) Let $n \geq 2$ and assume $P (x_{1}, \dots, x_{k}) = P (x_{k}, \dots, x_{1})^{t}$ for all $k < n$ . Then $P (x_{n}, \dots, x_{1})^{t} = (x_{n} \to P (x_{n - 1}, \dots, x_{1}))^{t} = P (x_{n - 1}, \dots, x_{1})^{t} \leftarrow x_{n} = P (x_{1}, \dots, x_{n - 1}) \leftarrow x_{n} = P (x_{1}, \dots, x_{n})$ : the first equality is the first-letter recursion of step 2.1 applied to the reversed word, the second is the definitional identity [L2], the third is the induction hypothesis, and the fourth is [L1].

4.1step 3.1L2discharge-induction

(Conclusion.) By steps 1.3 and 3.1, $P (x_{1}, \dots, x_{n}) = P (x_{n}, \dots, x_{1})^{t}$ for every word of pairwise distinct real numbers; conversely the transpose relation for all words implies the first-letter recursion by reading the computation of step 3.1 backwards after replacing $(x_{1}, \dots, x_{n})$ by the reversed word, so the two displayed forms are equivalent.

5.1given∎

(Recording tableau.) The statement makes no assertion about the recording tableau, and indeed the transpose relation is special to the insertion tableau: the recording tableau records the order in which boxes are added, and this order is not reversed by reversing the word (Schensted's note; see the example after Lemma 7). Nothing beyond the insertion tableau is claimed or used.

TheoremStatement: Literature-sourcedProof: Literature-sourcedjudge pass (gpt-6.1-sol)Open item page →

The Schensted theorem on longest increasing and decreasing subsequences

Statement

Let $w = (w_{1}, \dots, w_{N})$ be a word of pairwise distinct real numbers and let $P (w)$ be its insertion tableau, of shape $λ$ (Row insertion and the bumping route). Call a subsequence $w_{k_{1}}, \dots, w_{k_{r}}$ (with $k_{1} < \dots < k_{r}$ ) increasing when $w_{k_{1}} < \dots < w_{k_{r}}$ and decreasing when $w_{k_{1}} > \dots > w_{k_{r}}$ . Then the length of a longest increasing subsequence of $w$ equals the number $λ_{1}$ of columns of $P (w)$ , and the length of a longest decreasing subsequence equals the number $λ_{1}^{'}$ of rows of $P (w)$ . For the empty word both longest lengths and both numbers are $0$ .

Facts & Assumptions

Given: A word $w = (w_{1}, \dots, w_{N})$ of pairwise distinct real numbers, its insertion tableaux $P_{k} = P (w_{1}, \dots, w_{k})$ of shape $λ^{(k)}$ , and the basic subsequences $S_{1}, S_{2}, \dots$ of $w$ .

[L1]

At each step $k$ the letter $w_{k}$ is placed in some position $j$ of the first row of $P_{k}$ ; each $S_{j}$ is the list, in insertion order, of the letters whose position at their own insertion is $j$ , and the $S_{j}$ form a partition of the letters of $w$ into decreasing subsequences; moreover for every $x \in S_{j}$ with $j \geq 2$ the entry $y$ occupying position $j - 1$ of the first row at the moment $x$ is inserted belongs to $S_{j - 1}$ , was inserted earlier than $x$ , and satisfies $y < x$ (Basic subsequences of the first row, Row insertion and the bumping route).

[L2]

The first row of $P_{k}$ is strictly increasing and the shape $λ^{(k)}$ is a partition, so the occupied positions of the first row are exactly $1, \dots, λ_{1}^{(k)}$ , and positions of the first row are filled and refilled from the left, a position receiving a letter only at a step when it already exists or is appended (Monotonicity of the bumping route and standardness of the output, Tableaux and standard tableaux).

[L3]

For the reversed word $w^{r} = (w_{N}, \dots, w_{1})$ one has $P (w^{r}) = P (w)^{t}$ , so the first row of $P (w^{r})$ is the first column of $P (w)$ and the number of columns of $P (w^{r})$ equals the number of rows of $P (w)$ (Reversing a word transposes its insertion tableau).

Proof

technique · direct

1.1L1L2

(Nonempty basic subsequences.) For each $j \in {1, \dots, λ_{1}}$ the final first row of $P (w) = P_{N}$ has an entry in position $j$ , which was placed there at some step, and that step's letter lies in $S_{j}$ ; hence $S_{j} \neq \emptyset$ . For $j > λ_{1}$ no step can place a letter in position $j$ , because positions of the first row never exceed $λ_{1}$ at the end; hence $S_{j} = \emptyset$ . So the nonempty basic subsequences are exactly $S_{1}, \dots, S_{λ_{1}}$ .

1.2L1given

(Decreasing property and predecessor property.) Each $S_{j}$ is strictly decreasing in the order of insertion, and each element $x$ of $S_{j}$ with $j \geq 2$ has an earlier inserted element $y \in S_{j - 1}$ with $y < x$ ; these are the two assertions of the basic subsequence lemma.

2.1step 1.1step 1.2algebra

(Upper bound for increasing subsequences.) Let $w_{k_{1}} < \dots < w_{k_{r}}$ with $k_{1} < \dots < k_{r}$ be an increasing subsequence. The letters of $w$ are partitioned by the sets $S_{j}$ (step 1.1), and within a fixed $S_{j}$ the letters occur in insertion order with strictly decreasing values (step 1.2); an increasing subsequence meets $S_{j}$ in at most one letter, since two letters of $S_{j}$ occur in the order of their positions in $w$ and their values decrease. Hence $r \leq # {j : S_{j} \neq \emptyset} = λ_{1}$ , so the longest increasing length is at most $λ_{1}$ .

2.2step 1.1step 1.2algebra

(Lower bound for increasing subsequences.) If $N \geq 1$ set $λ_{1} \geq 1$ and choose any element $x_{λ_{1}} \in S_{λ_{1}}$ , which exists by step 1.1; recursively for $j = λ_{1}, \dots, 2$ apply the predecessor property of step 1.2 to $x_{j}$ to choose $x_{j - 1} \in S_{j - 1}$ inserted earlier than $x_{j}$ with $x_{j - 1} < x_{j}$ . Reading the letters $x_{1}, \dots, x_{λ_{1}}$ in the order of the word $w$ : by construction the insertion times strictly increase from $x_{1}$ to $x_{λ_{1}}$ , so the positions in $w$ strictly increase, and the values strictly increase; hence they form an increasing subsequence of $w$ of length $λ_{1}$ .

3.1step 2.1step 2.2given

(Increasing case.) For $N \geq 1$ steps 2.1 and 2.2 give that the longest increasing subsequence length equals $λ_{1}$ ; for $N = 0$ there is no first row, $λ_{1} = 0$ , and the empty word has no nonempty subsequence, so the longest increasing length is $0 = λ_{1}$ .

4.1step 3.1algebra

(Decreasing case.) An increasing subsequence $w_{i_{1}}^{r} < \dots < w_{i_{r}}^{r}$ of the reversed word, with $i_{1} < \dots < i_{r}$ , corresponds to the index sequence $N + 1 - i_{r} < \dots < N + 1 - i_{1}$ in $w$ with $w_{N + 1 - i_{r}} > \dots > w_{N + 1 - i_{1}}$ , a decreasing subsequence of the same length; the correspondence is a bijection on subsequences, so the longest decreasing length of $w$ equals the longest increasing length of $w^{r}$ , which by step 3.1 is the number of columns of $P (w^{r})$ .

5.1step 4.1step 3.1L3∎

(Number of rows.) By [L3] the number of columns of $P (w^{r})$ equals the number of rows of $P (w)$ , namely $λ_{1}^{'}$ ; combining with step 4.1, the longest decreasing subsequence length equals $λ_{1}^{'}$ . Together with step 3.1 this is the theorem; for $N = 0$ both lengths and both $λ_{1}, λ_{1}^{'}$ are $0$ .

TheoremStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-6.1-sol)Open item page →

The RSK correspondence for two-line arrays

Statement

A two-line array is a pair of finite lists $(u; v) = ((u_{1}, \dots, u_{N}), (v_{1}, \dots, v_{N}))$ of positive integers whose columns $(u_{k}, v_{k})$ are in nondecreasing lexicographic order: $u_{1} \leq \dots \leq u_{N}$ , and $u_{k} = u_{k + 1}$ implies $v_{k} \leq v_{k + 1}$ . Row insertion is extended to arbitrary (possibly repeated) letters by the same rule as Row insertion and the bumping route: replace the leftmost entry strictly greater than the inserted letter, or append if there is none, and similarly for reverse deletion from a removable box.

Correspondence. Starting from empty tableaux and performing, for $k = 1, \dots, N$ , the insertion of $v_{k}$ and the writing of the label $u_{k}$ in the box added to the recording tableau (construction A), produces a pair $(P, Q)$ of semistandard tableaux (Semistandard tableaux and Kostka numbers) of the same shape, with content $(P)$ the multiset of the $v_{k}$ and content $(Q)$ the multiset of the $u_{k}$ . Conversely, starting from a pair $(P, Q)$ of semistandard tableaux of the same shape and performing, for $k = N, \dots, 1$ , the deletion of the box of $Q$ containing the largest entry, chosen rightmost among ties, and reverse deletion of that box from $P$ (construction B), recovers the unique lexicographically ordered two-line array with those tableaux; the two constructions are inverse, and the correspondence is a bijection.
Transpose interchange. If $(u; v)$ corresponds to $(P, Q)$ , then the lexicographically ordered rearrangement of the transposed array $(v; u)$ corresponds to $(Q, P)$ .
If $u_{k} = k$ for all $k$ (so $Q$ is standard), the correspondence is the row-insertion correspondence between words $v = (v_{1}, \dots, v_{N})$ of positive integers and pairs $(P, Q)$ with $P$ semistandard and $Q$ standard of the same shape and content $(P)$ the multiset of letters of $v$ .

Facts & Assumptions

Given: A lexicographically ordered two-line array $(u; v)$ with $N$ columns, and the tableaux $P, Q$ produced by construction A.

[F1]

Row insertion with the leftmost-strictly-greater rule places one letter per visited row and adds exactly one box at the end of the final row; for a standard tableau with distinct entries its output is standard and the route letters strictly increase and positions weakly decrease (Row insertion and the bumping route, Monotonicity of the bumping route and standardness of the output).

[F2]

A semistandard tableau of shape $λ$ has weakly increasing rows and strictly increasing columns; content records the multiplicity of each entry, and $K_{λ, μ}$ counts semistandard tableaux of content $μ$ ; a filling with content $(1^{n})$ is semistandard if and only if it is standard (Semistandard tableaux and Kostka numbers, Tableaux and standard tableaux).

[F3]

Reverse deletion from a removable box of a standard tableau is defined, is inverse to row insertion in both directions, and its output is standard with the expelled letter removed from the entry set (Reverse row deletion, Row insertion and reverse deletion are inverse).

[F4]

A node $(i, λ_{i} + 1)$ is addable for $λ$ if and only if $i = 1$ or $λ_{i - 1} > λ_{i}$ ; removable and addable nodes are the row-end nodes satisfying the corresponding strict inequality (Removable and addable nodes, Partitions, English diagrams, and conjugation).

Proof

technique · direct

1.1F1F2F4givenalgebra

Extend row insertion to weak rows and strict columns using the stated leftmost-strictly-greater rule. Carried labels strictly increase whenever a bump occurs. Route positions weakly decrease: if the old entry $x_{i + 1}$ at position $r_{i}$ of row $i$ has a box below it, that box has value $> x_{i + 1}$ by column strictness, so the next leftmost-exceeding position is at most $r_{i}$ ; if no such box exists, the next row has length $< r_{i}$ and its bump or append position is again at most $r_{i}$ . Only finitely many occupied rows can be visited, so the process terminates at an append box, which is addable: if it lies in row $s > 1$ , then $λ_{s} + 1 = r_{s} \leq r_{s - 1} \leq λ_{s - 1}$ . Exactly one box is added and the entry multiset gains the inserted letter.

1.2F2F3F4algebra

Reverse deletion also works for semistandard tableaux. Remove a corner $(s, t)$ and carry its old value upward. If the carried value from row $i + 1$ is $z$ , choose the rightmost entry $a < z$ in row $i$ and replace it by $z$ , carrying $a$ upward. Such an entry exists at the column of the just-removed or replaced cell in row $i + 1$ , by strictness of the column before that lower change; the chosen column is at least that lower column. The row remains weak, since entries left of the chosen cell are $\leq a < z$ and entries to its right are $\geq z$ . The upper neighbour is smaller than the old value $a < z$ . Any remaining lower neighbour is larger than $z$ : in the lower row the preceding reverse step replaced its carried value by a strictly larger value, and all entries to its right are at least that larger value; at the first removed corner there is no lower neighbour to its right. At the next upward replacement, the value placed above the current changed row is smaller than its carried $z$ , so strictness is preserved throughout. Thus deletion terminates with a semistandard tableau and removes one occurrence of the expelled letter, which may still occur elsewhere.

1.3givenalgebra

For transpose interchange define a directed graph on the labelled occurrences of pairs $(u, v)$ : for unequal pairs draw an arc when both coordinates weakly increase, and order occurrences of an identical pair by their original occurrence index, drawing forward arcs between them. Lexicographic order is a topological order, so the graph is acyclic. Divide it into source layers $C_{1}, \dots, C_{d}$ by successively removing all sources. A vertex lies in $C_{l}$ exactly when the longest path ending there has $l - 1$ arcs, by induction on a topological order. Within a layer the first coordinates strictly increase and the second strictly decrease when vertices are listed by first coordinate: equal coordinates or simultaneous weak increase would give an arc and different layers. Write $C_{l} = ((u_{l 1}, v_{l 1}), \dots, (u_{l n_{l}}, v_{l n_{l}}))$ in that order.

2.1step 1.1F2algebra

The output is semistandard. At a replaced box in row $i$ , left entries are $\leq x_{i}$ and right entries are at least the old displaced value $x_{i + 1} > x_{i}$ . For its upper neighbour, if $r_{i} = r_{i - 1}$ the new value above is $x_{i - 1} < x_{i}$ ; if $r_{i} < r_{i - 1}$ , the unchanged entry above lies left of the previous leftmost-exceeding position and is $\leq x_{i - 1} < x_{i}$ . Its lower neighbour is either the new carried value $x_{i + 1} > x_{i}$ if the next bump is in that column, or an unchanged value exceeding the old displaced value by column strictness. The same upper-neighbour argument applies at the appended box, whose row has all prior entries $\leq x_{s}$ and which has no box below. Hence rows stay weak and columns stay strict, including at equal input letters.

2.2step 1.1step 1.2F2algebra

These extended procedures are inverse. Along an insertion route, the resulting row has at its chosen position $x_{i} < x_{i + 1}$ , entries to the left $\leq x_{i}$ , and entries to the right $\geq x_{i + 1}$ ; hence reverse deletion carrying $x_{i + 1}$ chooses exactly that position and restores its old entry. Inducting upward from the appended box restores the input tableau. Conversely, a reverse step replacing $a$ by $z > a$ leaves all entries to its left $\leq a$ and entries to its right $\geq z$ , so reinserting $a$ chooses precisely that cell and bumps $z$ . Inducting downward restores the original tableau and corner. This proves both directions without requiring the expelled value to disappear from the entry set.

3.1step 1.1step 2.1F2F4algebra

Compare successive insertions of $x \leq x^{'}$ . On every common row, their carried values satisfy $x_{i} \leq x_{i}^{'}$ and their positions satisfy $r_{i} < r_{i}^{'}$ : after the first replacement, all entries up to $r_{i}$ are $\leq x_{i} \leq x_{i}^{'}$ , so the second bump or append is to its right. If both bump, the second displaced value is at least the first displaced value, by the old weak row order, proving the carried-value induction. The second insertion stops no lower than the first: at the first process's append row its own position would be to the right of that append, so it must append there if it has not already stopped. Its new column $t^{'}$ is strictly larger than the first new column $t$ : in the same row it appends one cell further right; in a higher row, that old row length is at least $t$ by addability of the first appended box, so its append column is at least $t + 1$ .

3.2step 1.1step 2.1F2algebra

For successive $x > x^{'}$ , the carried values satisfy $x_{i} > x_{i}^{'}$ and positions satisfy $r_{i}^{'} \leq r_{i}$ on common rows. At row $1$ the second process meets a value exceeding $x^{'}$ at or before the first chosen position, whose new value is $x > x^{'}$ . If it bumps before that position, the bumped old value is $\leq x_{i} < x_{i + 1}$ by the first leftmost-exceeding choice; if at that position, it bumps $x_{i} < x_{i + 1}$ . This proves the strict carried-value induction. At the first append row the smaller carried value bumps an entry at or before that append instead of stopping, so the second insertion ends strictly lower. Its final column $t^{'}$ is at most $t$ , since its position in the first append row is at most $t$ and subsequent route positions weakly decrease.

4.1step 1.1step 2.1step 3.1F2given

Construction A produces semistandard $P$ by step 2.1. Its contents and shape follow from step 1.1. The rows of $Q$ are weakly increasing because boxes are appended at row ends and the chronological labels $u_{k}$ weakly increase. A lower box in a column is created later, so its label is at least the upper label. All equal labels form a consecutive block of insertions, whose inputs $v_{k}$ weakly increase; step 3.1 makes their new columns strictly increase at every adjacent step, hence throughout that block. Equal labels therefore never share a column, and $Q$ has strictly increasing columns. Both contents and the common shape are as stated.

4.2F2F4step 1.2step 2.2step 3.2algebra

Construction B is defined on any semistandard pair. A rightmost maximum entry of $Q$ has no cell to its right, since that would be a larger or an equal maximum further right, and no cell below, since columns are strict. It is thus removable. Maximum entries occupy distinct columns. Removing the rightmost one leaves semistandard $Q$ , and step 1.2 allows reverse deletion in $P$ at the same corner. Repeating yields expelled letters $v_{N}, \dots, v_{1}$ and labels $u_{N} \geq \dots \geq u_{1}$ . Step 2.2 ensures that forward reinsertion rebuilds the tableaux and chosen boxes. Within each equal-label deletion block the removed columns strictly decrease, so the rebuilding insertion columns strictly increase. The contrapositive of step 3.2 then gives $v_{k} \leq v_{k + 1}$ when $u_{k} = u_{k + 1}$ . The recovered array is therefore lexicographically ordered.

5.1step 2.2step 3.1step 4.2given

For a pair produced by A, its final label block has strictly increasing insertion columns by step 3.1; the last-created box is its rightmost maximum box. Step 2.2 recovers its last input letter, and induction recovers all columns, so $B \circ A$ is the identity. For an arbitrary pair, step 4.2 and the other inverse direction in step 2.2 give $A \circ B$ as the identity. Thus the first assertion is a bijection, including the empty array and empty pair, where no operation is performed.

5.2step 1.1step 4.1step 1.3algebra

The first row of $P$ consists of $v_{1 n_{1}}, \dots, v_{d n_{d}}$ , and the first row of $Q$ of $u_{11}, \dots, u_{d 1}$ . Moreover, the events which touch first-row position $l$ are exactly the successive vertices of $C_{l}$ . Prove this simultaneously by induction on the array length. Adding the next lexicographic pair $(u, v)$ introduces no outgoing arc. A layer has a predecessor of that vertex exactly when its minimum second coordinate $v_{l n_{l}}$ is $\leq v$ ; hence the vertex's layer is $r = 1 + \max {l : v_{l n_{l}} \leq v}$ , with empty maximum $0$ . By the induction hypothesis these minima are the weakly increasing entries of the first row. Thus insertion of $v$ replaces exactly position $r$ , or appends there if $r = d + 1$ . In an existing layer its first coordinate is strictly greater than the previous member's and its second strictly smaller, since it has no predecessor in that layer; it becomes that layer's last member. Appending a new layer writes its first label $u$ in row one of $Q$ , while replacement changes no existing $Q$ label. This proves every assertion of the induction.

6.1step 3.1step 4.1step 5.2algebra

The first-row bumped pairs are exactly $(u_{l, i + 1}, v_{l i})$ for $1 \leq i < n_{l}$ , across all layers. They appear chronologically in lexicographic order: bumping labels $u$ weakly increase; within one equal-label input block step 3.1 makes first-row positions strictly increase, and the entries bumped at those successively rightward positions weakly increase, because earlier replacements in that block occur to their left. Consequently the lower rows of both tableaux are obtained by applying A to this bump array. Row two is its first row, since the labels are written precisely when that bumped letter's lower-row insertion appends. Repeat this procedure for each successive row. The bump array has $N - d < N$ columns whenever $N > 0$ , so the recursion terminates.

7.1step 1.3step 5.2step 6.1algebra

Swapping coordinates gives an isomorphism of the two initial graphs, using the same order for occurrences of identical pairs. The source layers are the same sets of occurrences, but their within-layer order reverses: the old second coordinates strictly decrease, so the swapped first coordinates increase in the reverse order. The first-row formulas of step 5.2 therefore swap $P$ and $Q$ . More importantly, the shifted pairs from a layer of the swapped graph are $(v_{l i}, u_{l, i + 1})$ for $i = n_{l} - 1, \dots, 1$ , exactly the coordinate swaps, as a multiset, of the original bump pairs $(u_{l, i + 1}, v_{l i})$ . After lexicographic sorting their bump arrays are transposes of one another. Identical pairs can again be ordered correspondingly; changing the order of identical occurrences does not change the labelled array or insertion. Thus induction on $N$ , using the smaller bump arrays in step 6.1, swaps every lower row as well. This proves that the transposed array corresponds to $(Q, P)$ .

8.1step 4.1step 5.1step 7.1F2given∎

When $u_{k} = k$ , all labels in $Q$ are distinct, and its semistandardness from step 4.1 makes it standard by [F2]. Construction A is precisely word insertion with chronological recording labels; the bijection of step 5.1 and transpose interchange of step 7.1 give all the commissioned assertions. No Choice is used: every procedure, maximum, ordering and induction here is finite and canonical, with identical pairs ordered by occurrence.

CorollaryStatement: Literature-sourcedProof: Literature-sourcedjudge pass (gpt-6.1-sol)Open item page →

RSK interchanges the insertion and recording tableaux under inversion

Statement

Let $n \geq 0$ and let $w = (w_{1}, \dots, w_{n})$ be a permutation of ${1, \dots, n}$ with RSK pair $(P (w), Q (w))$ (The Robinson-Schensted correspondence). Let $w^{- 1} = (p_{1}, \dots, p_{n})$ be the inverse permutation, where $p_{i}$ is the position of $i$ in $w$ (so $w_{p_{i}} = i$ ). Then $P (w^{- 1}) = Q (w) and Q (w^{- 1}) = P (w) .$ In particular, identifying $σ \in S_{n}$ with the word $(σ (0) + 1, \dots, σ (n - 1) + 1)$ via The finite symmetric group $S_{n}$ , one-line notation, and cycle notation, the RSK pair of $σ^{- 1}$ is $(Q, P)$ .

Facts & Assumptions

Given: An integer $n \geq 0$ , a word $w = (w_{1}, \dots, w_{n})$ of pairwise distinct real numbers with ${w_{1}, \dots, w_{n}} = {1, \dots, n}$ , its RSK pair $(P (w), Q (w))$ , and the inverse word $w^{- 1} = (p_{1}, \dots, p_{n})$ with $w_{p_{i}} = i$ .

[L1]

The Robinson-Schensted map is a bijection from the set $X_{n}$ of such words onto the set of pairs $(P, Q)$ of standard tableaux of a common shape $λ ⊢ n$ ; equivalently, two words with the same RSK pair are equal, and every such pair occurs (The Robinson-Schensted correspondence).

[L2]

For a lexicographically ordered two-line array $(u; v)$ : (a) construction A (insert $v_{k}$ , write the label $u_{k}$ in the new box) produces a pair of semistandard tableaux of common shape, and the correspondence with lexicographically ordered arrays is a bijection; (b) the lexicographically ordered rearrangement of the transposed array $(v; u)$ corresponds to $(Q, P)$ ; (c) if $u_{k} = k$ for all $k$ then construction A is exactly the row-insertion construction of The Robinson-Schensted correspondence and produces its RSK pair (The RSK correspondence for two-line arrays).

[L3]

A two-line array is a pair of finite lists of positive integers whose columns are in nondecreasing lexicographic order; the top line $u$ is strictly increasing exactly when its entries are distinct and increasing (The RSK correspondence for two-line arrays).

[L4]

$S_{n}$ acts on ${0, 1, \dots, n - 1}$ , one-line notation and cycles are as in The finite symmetric group $S_{n}$ , one-line notation, and cycle notation; a standard tableau is a filling of a Young diagram by distinct integers increasing along rows and columns (Tableaux and standard tableaux).

Proof

technique · direct

1.1L3given

The two-line array $A : = ((1, 2, \dots, n); (w_{1}, \dots, w_{n}))$ is lexicographically ordered, because its top line is strictly increasing; its top line has distinct entries and its columns are the pairs $(k, w_{k})$ for $k = 1, \dots, n$ .

1.2L2L1given

Construction A applied to $A$ inserts $v_{k} = w_{k}$ at step $k$ and writes $u_{k} = k$ in the box added at step $k$ ; by L2 the resulting pair is the RSK pair of the word $(w_{1}, \dots, w_{n})$ , namely $(P (w), Q (w))$ .

1.3L3givenalgebra

The transposed array of $A$ is $((w_{1}, \dots, w_{n}); (1, 2, \dots, n))$ , whose columns are the pairs $(w_{k}, k)$ ; since $w$ is a permutation of ${1, \dots, n}$ , each value $i$ occurs exactly once among the first coordinates, at the index $k = p_{i}$ with $w_{p_{i}} = i$ , so the lexicographically ordered rearrangement of these columns is the array $A^{- 1} : = ((1, 2, \dots, n); (p_{1}, \dots, p_{n}))$ .

1.4L4givenalgebra

For the group-theoretic form, let $σ \in S_{n}$ have one-line form $[σ (0), \dots, σ (n - 1)]$ and let $w = (σ (0) + 1, \dots, σ (n - 1) + 1)$ be the associated word; then for each $i \in {1, \dots, n}$ the position $p_{i}$ of $i$ in $w$ satisfies $p_{i} = σ^{- 1} (i - 1) + 1$ , because $w_{σ^{- 1} (i - 1) + 1} = σ (σ^{- 1} (i - 1)) + 1 = i$ ; hence the word associated with $σ^{- 1}$ is exactly $w^{- 1} = (p_{1}, \dots, p_{n})$ .

2.1L2step 1.2step 1.3

By L2 the array $A^{- 1}$ corresponds under construction A to $(Q (w), P (w))$ : it is the lexicographically ordered rearrangement of the transpose of the array $A$ of step 1.2, whose pair is $(P (w), Q (w))$ .

2.2L2L1givenstep 1.3

Construction A applied to $A^{- 1}$ inserts $p_{1}, \dots, p_{n}$ and writes the labels $1, \dots, n$ , so by L2 it produces the RSK pair $(P (w^{- 1}), Q (w^{- 1}))$ of the word $w^{- 1} = (p_{1}, \dots, p_{n})$ .

3.1L2step 2.1step 2.2

By L2 the correspondence between lexicographically ordered two-line arrays and pairs is bijective, and the array $A^{- 1}$ corresponds to exactly one pair; by steps 2.1 and 2.2 this pair is both $(Q (w), P (w))$ and $(P (w^{- 1}), Q (w^{- 1}))$ , so $P (w^{- 1}) = Q (w)$ and $Q (w^{- 1}) = P (w)$ .

4.1step 3.1step 1.4∎

Applying step 3.1 to the permutation $σ$ identified with $w$ gives $(P (σ^{- 1}), Q (σ^{- 1})) = (Q (σ), P (σ))$ , which is the stated group-theoretic form.

CorollaryStatement: Literature-sourcedProof: Literature-sourcedjudge pass (gpt-6.1-sol)Open item page →

The sum of squares of the standard tableau numbers

Statement

For every $n \geq 0$ , $\sum_{λ ⊢ n} (f^{λ})^{2} = n!,$ where $f^{λ}$ is the number of standard $λ$ -tableaux and $f^{\emptyset} = 1$ , $0! = 1$ .

Facts & Assumptions

Given: An integer $n \geq 0$ , the set $X_{n}$ of words $(w_{1}, \dots, w_{n})$ of pairwise distinct real numbers with ${w_{1}, \dots, w_{n}} = {1, \dots, n}$ , and for each partition $λ ⊢ n$ the number $f^{λ}$ of standard $λ$ -tableaux.

[L1]

The Robinson-Schensted map $w \mapsto (P (w), Q (w))$ is a bijection from $X_{n}$ onto the set of pairs $(P, Q)$ of standard tableaux of the same shape $λ ⊢ n$ (The Robinson-Schensted correspondence).

[F1]

A standard $λ$ -tableau is a filling of the Young diagram of $λ$ by $1, \dots, n$ , each once, increasing along rows and columns; $f^{λ}$ is the number of such tableaux, and $f^{\emptyset} = 1$ is the number of fillings of the empty diagram (Tableaux and standard tableaux).

[F2]

A word of $X_{n}$ is determined by the function $i \mapsto w_{i}$ , which is a bijection of ${1, \dots, n}$ ; conversely every such bijection gives a word in $X_{n}$ , and $X_{0}$ consists of the empty word alone (The Robinson-Schensted correspondence).

Proof

technique · direct

1.1F1algebra

The shapes $λ ⊢ n$ are pairwise distinct as subsets of the plane, so the sets of pairs of standard tableaux of shape $λ$ are pairwise disjoint over $λ ⊢ n$ .

1.2F1algebra

For fixed $λ ⊢ n$ the pairs $(P, Q)$ of standard $λ$ -tableaux are exactly the choices of a standard $λ$ -tableau $P$ followed by an independent choice of a standard $λ$ -tableau $Q$ , so there are $f^{λ} \cdot f^{λ} = (f^{λ})^{2}$ of them.

2.1L1F2step 1.1step 1.2algebra

By [L1] the map $w \mapsto (P (w), Q (w))$ is a bijection from $X_{n}$ onto the disjoint union over $λ ⊢ n$ of the sets counted in step 1.2; comparing cardinalities and using that the bijections of ${1, \dots, n}$ are $n!$ -in-number (with $0! = 1$ ) gives $n! = ∣ X_{n} ∣ = \sum_{λ ⊢ n} (f^{λ})^{2}$ .

3.1F1F2given∎

At $n = 0$ the only partition is $\emptyset$ and the sum is the single term $(f^{\emptyset})^{2} = 1^{2} = 1 = 0!$ , so the identity holds at the boundary.

CorollaryStatement: Literature-sourcedProof: Literature-sourcedjudge pass (gpt-6.1-sol)Open item page →

Involutions are counted by standard tableaux

Statement

Let $w$ be a permutation of ${1, \dots, n}$ with RSK pair $(P, Q)$ . Then $w = w^{- 1}$ if and only if $P = Q$ . Consequently the map $w \mapsto P (w)$ restricts to a bijection from the set of involutions of ${1, \dots, n}$ onto the set of standard tableaux with $n$ boxes, and the number of involutions of ${1, \dots, n}$ (equivalently, of $S_{n}$ ) equals $\sum_{λ ⊢ n} f^{λ} .$

Facts & Assumptions

[L1]

The Robinson-Schensted map $w \mapsto (P (w), Q (w))$ is a bijection from $X_{n}$ onto the set of pairs of standard tableaux of a common shape $λ ⊢ n$ ; in particular it is injective (The Robinson-Schensted correspondence).

[L2]

$P (w^{- 1}) = Q (w)$ and $Q (w^{- 1}) = P (w)$ (RSK interchanges the insertion and recording tableaux under inversion).

[L3]

Identifying $σ \in S_{n}$ with the word $w = (σ (0) + 1, \dots, σ (n - 1) + 1)$ , the word of $σ^{- 1}$ is $w^{- 1}$ ; thus $w = w^{- 1}$ if and only if $σ = σ^{- 1}$ , and the involutions of ${1, \dots, n}$ are the words fixed by inversion (The finite symmetric group $S_{n}$ , one-line notation, and cycle notation, RSK interchanges the insertion and recording tableaux under inversion).

[L4]

A standard tableau with $n$ boxes has shape $λ ⊢ n$ , and for each $λ ⊢ n$ there are $f^{λ}$ such tableaux; the shapes are distinct, so the total number is $\sum_{λ ⊢ n} f^{λ}$ (Tableaux and standard tableaux).

Proof

technique · direct

1.1L2given

If $w = w^{- 1}$ then $(P (w), Q (w)) = (P (w^{- 1}), Q (w^{- 1})) = (Q (w), P (w))$ by [L2], so $P (w) = Q (w)$ .

1.2L2L1given

Conversely, if $P (w) = Q (w)$ then $P (w^{- 1}) = Q (w) = P (w)$ and $Q (w^{- 1}) = P (w) = Q (w)$ by [L2], so $(P (w^{- 1}), Q (w^{- 1})) = (P (w), Q (w))$ ; injectivity of the Robinson-Schensted map [L1] gives $w^{- 1} = w$ .

2.1step 1.1step 1.2L1

(Injectivity on involutions.) If $w, w^{'}$ are fixed by inversion and $P (w) = P (w^{'})$ , then by step 1.1 and step 1.2 $Q (w) = P (w) = P (w^{'}) = Q (w^{'})$ , so the RSK pairs coincide and [L1] gives $w = w^{'}$ .

2.2L1step 1.2L4

(Surjectivity onto standard tableaux.) Let $P$ be a standard tableau with $n$ boxes, of shape $λ ⊢ n$ ; the pair $(P, P)$ is a pair of standard tableaux of common shape, so by surjectivity of the Robinson-Schensted map [L1] there is a word $w \in X_{n}$ with $(P (w), Q (w)) = (P, P)$ ; by step 1.2 $w$ is fixed by inversion, and $P (w) = P$ .

3.1step 2.1step 2.2L3L4

(The count.) By steps 2.1 and 2.2 the map $w \mapsto P (w)$ is a bijection from the involutions onto the standard tableaux with $n$ boxes; by [L4] the latter set has $\sum_{λ ⊢ n} f^{λ}$ elements, and by [L3] the involutions of ${1, \dots, n}$ are the involutions of $S_{n}$ .

4.1L1L4given∎

At $n = 0$ the empty word is the unique element of $X_{0}$ and equals its inverse, the only standard tableau with no boxes is the empty tableau, $f^{\emptyset} = 1$ , and both sides of the count are $1$ , consistent with steps 1.1 and 1.2.

5 · Examples, counterexamples and false statements

None yet.

The Hook Length Formula and Rsk Correspondence

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

Hook, arm, leg, and hook length of a box

Definition

The removal recursion for standard tableaux

Statement

Facts & Assumptions

Proof

Removing a corner changes hooks in its row and column

Statement

Facts & Assumptions

Proof

The hook-product ratios sum to the size

Statement

Facts & Assumptions

Proof

The hook length formula

Statement

Facts & Assumptions

Proof

Row insertion and the bumping route

Definition

Monotonicity of the bumping route and standardness of the output

Statement

Facts & Assumptions

Proof

The recording tableau is standard

Statement

Facts & Assumptions

Proof

Reverse row deletion

Definition

Row insertion and reverse deletion are inverse

Statement

Facts & Assumptions

Proof

The Robinson-Schensted correspondence

Statement

Facts & Assumptions

Proof

Basic subsequences of the first row

Statement

Facts & Assumptions

Proof

Column insertion

Definition

Row and column insertion commute

Statement

Facts & Assumptions

Proof

Reversing a word transposes its insertion tableau

Statement

Facts & Assumptions

Proof

The Schensted theorem on longest increasing and decreasing subsequences

Statement

Facts & Assumptions

Proof

The RSK correspondence for two-line arrays

Statement

Facts & Assumptions

Proof

RSK interchanges the insertion and recording tableaux under inversion

Statement

Facts & Assumptions

Proof

The sum of squares of the standard tableau numbers

Statement

Facts & Assumptions

Proof

Involutions are counted by standard tableaux

Statement

Facts & Assumptions

Proof

5 · Examples, counterexamples and false statements

Sources