LemmaStatement: Literature-sourcedProof: Literature-sourcedPipeline-generatedjudge pass (gpt-6.1-sol)

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 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.

Depends on

Used by

Empty and singleton RSK boundaries Example
Hook table for the shape (3,2,1) Example
The hook length formula Theorem

Dependency tree · two levels

4 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

David A. Craven, Groups, Geometries and Representation Theory (Spring Term 2013 lecture notes, 42 pp.) (standard reference, not scraped)
Charlotte Chan, Representation Theory of Symmetric Groups (Oxford Hilary Term 2011 lecture notes, 40 PDF pp.) (standard reference, not scraped)