ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passaudited 2026-10-02

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 Young graph through size four

Statement

Consider the Young graph of The Young graph of partitions, in which the vertices are all partitions, the rank of the vertex $λ$ is $∣ λ ∣$ , and the edges $λ \to ν$ are the pairs with $ν = λ + y$ for an addable node $y$ of $[λ]$ . Then:

(Vertices at ranks $0$ to $4$ .) The vertices of rank $n$ for $0 \leq n \leq 4$ are exactly $\emptyset; (1); (2), (1, 1); (3), (2, 1), (1, 1, 1); (4), (3, 1), (2, 2), (2, 1, 1), (1, 1, 1, 1),$ so there are $1, 1, 2, 3, 5$ of them at ranks $0, 1, 2, 3, 4$ .
(Edges.) The edges whose source has rank at most $3$ are exactly $\emptyset \to (1); (1) \to (2), (1) \to (1, 1); (2) \to (3), (2) \to (2, 1), (1, 1) \to (2, 1), (1, 1) \to (1, 1, 1);$ $(3) \to (4), (3) \to (3, 1), (2, 1) \to (3, 1), (2, 1) \to (2, 2), (2, 1) \to (2, 1, 1), (1, 1, 1) \to (2, 1, 1), (1, 1, 1) \to (1, 1, 1, 1),$ that is $1, 2, 4, 7$ edges between consecutive ranks $0$ - $1$ , $1$ - $2$ , $2$ - $3$ and $3$ - $4$ . The vertex $(2, 1)$ has the two incoming edges from $(2)$ and $(1, 1)$ and the three outgoing edges to $(3, 1)$ , $(2, 2)$ and $(2, 1, 1)$ .
(Branching along the edges, each edge once.) For every $λ ⊢ n$ with $1 \leq n \leq 4$ , restriction gives an isomorphism of $C S_{n - 1}$ -modules ${Res}_{S_{n - 1}}^{S_{n}} S_{C}^{λ} ≅ ⨁_{x \in Rem (λ)} S_{C}^{λ - x}$ , one summand per incoming edge of $λ$ ; for every $λ ⊢ n$ with $0 \leq n \leq 3$ , induction gives an isomorphism of $C S_{n + 1}$ -modules ${Ind}_{S_{n}}^{S_{n + 1}} S_{C}^{λ} ≅ ⨁_{y \in Add (λ)} S_{C}^{λ + y}$ , one summand per outgoing edge of $λ$ . For instance $Res S_{C}^{(2, 2)} ≅ S_{C}^{(2, 1)}$ and $Ind S_{C}^{(2, 1)} ≅ S_{C}^{(3, 1)} \oplus S_{C}^{(2, 2)} \oplus S_{C}^{(2, 1, 1)}$ .
(Standard tableaux and dimensions.) The numbers $f^{λ}$ of standard $λ$ -tableaux of ranks up to $4$ are $f^{\emptyset} = f^{(1)} = f^{(2)} = f^{(1, 1)} = 1, f^{(3)} = 1, f^{(2, 1)} = 2, f^{(1, 1, 1)} = 1,$ $f^{(4)} = 1, f^{(3, 1)} = 3, f^{(2, 2)} = 2, f^{(2, 1, 1)} = 3, f^{(1, 1, 1, 1)} = 1,$ with $\dim_{C} S_{C}^{λ} = f^{λ}$ , and they satisfy $\sum_{λ ⊢ n} (f^{λ})^{2} = n!$ for $n = 0, 1, 2, 3, 4$ , that is $1, 1, 2, 6, 24$ .

Facts & Assumptions

Given: the Young graph of partitions with its rank function and addable-node edges, the complex Specht modules $S_{C}^{λ}$ for $∣ λ ∣ \leq 4$ , and the partitions of $0, 1, 2, 3, 4$ .

[F1]

The Young graph has all partitions as vertices; its edges $α \to β$ are exactly the pairs with $[β] = [α] \cup {y}$ for an addable node $y$ of $α$ , distinct addable nodes giving distinct edges; every edge raises the rank by one, and paths of length $k$ from $\emptyset$ end at partitions of size $k$ (The Young graph of partitions).

[F2]

A node $(i, λ_{i})$ is removable exactly when $λ_{i} > λ_{i + 1}$ (with $λ_{k + 1} : = 0$ ); a node $(i, λ_{i} + 1)$ is addable exactly when $i = 1$ or $λ_{i - 1} > λ_{i}$ , and the node $(k + 1, 1)$ opening a new row is always addable; also $Rem (\emptyset) = \emptyset$ and $Add (\emptyset) = {(1, 1)}$ (Removable and addable nodes).

[F3]

A partition of $n$ is a weakly decreasing finite sequence of positive integers summing to $n$ , with $[λ]$ its Young diagram (Partitions, English diagrams, and conjugation); a standard $λ$ -tableau is a filling of $[λ]$ by $1, \dots, n$ , each once, increasing along rows and down columns, and $f^{λ}$ denotes their number (Tableaux and standard tableaux).

[F4]

For every $λ ⊢ n$ the standard polytabloids form a $C$ -basis of the complex Specht module $S_{C}^{λ}$ , so $\dim_{C} S_{C}^{λ} = f^{λ}$ (Standard polytabloids form a basis of a complex Specht module, Column antisymmetrizers, polytabloids, and Specht modules).

[F5]

For $m \geq 1$ and $ν ⊢ m$ one has ${Res}_{S_{m - 1}}^{S_{m}} S_{C}^{ν} ≅ ⨁_{x \in Rem (ν)} S_{C}^{ν - x}$ , each removable node contributing one summand (The complex Specht restriction branching rule).

[F6]

For $n \geq 0$ and $λ ⊢ n$ one has ${Ind}_{S_{n}}^{S_{n + 1}} S_{C}^{λ} ≅ ⨁_{y \in Add (λ)} S_{C}^{λ + y}$ , each addable node contributing one summand (Multiplicity-free complex Specht induction).

[F7]

The modules ${S_{C}^{λ} : λ ⊢ n}$ form a complete irredundant list of the irreducible complex $S_{n}$ -representations (Specht modules classify the complex irreducibles of $S_{n}$ ), and for a finite group $G$ over an algebraically closed field $k$ with $char k ∤ ∣ G ∣$ a complete list $V_{1}, \dots, V_{r}$ of the irreducibles satisfies $\sum_{i} (\dim_{k} V_{i})^{2} = ∣ G ∣$ (If $k$ is algebraically closed and $char k ∤ ∣ G ∣$ , then $\sum_{i} (\dim_{k} V_{i})^{2} = ∣ G ∣$ ); moreover $∣ S_{n} ∣ = n!$ (The Lehmer code gives $∣ S_{n} ∣ = n!$ again).

All computations below range over the finitely many partitions of $n \leq 4$ and the finite groups $S_{0}, \dots, S_{4}$ , so no choice principle is used.

Proof

technique · direct

1.1F1F3given

The partitions of $0, 1, 2, 3, 4$ are listed by size directly from the definition [F3]: $\emptyset$ ; $(1)$ ; $(2), (1, 1)$ ; $(3), (2, 1), (1, 1, 1)$ ; $(4), (3, 1), (2, 2), (2, 1, 1), (1, 1, 1, 1)$ , giving $1, 1, 2, 3, 5$ vertices of ranks $0, 1, 2, 3, 4$ , which is claim 1.

2.1F1F2step 1.1algebra

Addable nodes by the criterion of [F2]: for $\emptyset$ the node $(1, 1)$ gives $(1)$ ; for $(1)$ the nodes $(1, 2)$ and $(2, 1)$ give $(2)$ and $(1, 1)$ ; for $(2)$ the nodes $(1, 3)$ and $(2, 1)$ give $(3)$ and $(2, 1)$ ; for $(1, 1)$ the nodes $(1, 2)$ and $(3, 1)$ give $(2, 1)$ and $(1, 1, 1)$ ; for $(3)$ the nodes $(1, 4)$ and $(2, 1)$ give $(4)$ and $(3, 1)$ ; for $(2, 1)$ the nodes $(1, 3)$ (here $i = 1$ ), $(2, 2)$ (here $λ_{1} = 2 > λ_{2} = 1$ ) and $(3, 1)$ (a new row) give $(3, 1)$ , $(2, 2)$ and $(2, 1, 1)$ ; and for $(1, 1, 1)$ the nodes $(1, 2)$ (here $i = 1$ ) and $(4, 1)$ (a new row) give $(2, 1, 1)$ and $(1, 1, 1, 1)$ . By [F1] each addable node gives exactly one edge, so the edges out of ranks $0, 1, 2, 3$ are exactly the $1, 2, 4, 7$ edges displayed in claim 2; in particular $(2, 1)$ has the three outgoing edges to $(3, 1), (2, 2), (2, 1, 1)$ .

2.2F3step 1.1

Standard tableaux by explicit enumeration in the sense of [F3]: rank $0$ has the empty tableau; rank $1$ has $1$ ; rank $2$ has $12$ and $1 / 2$ ; rank $3$ has $123$ , the two tableaux $\begin{matrix} 1 & 2 \\ 3 \end{matrix}$ , $\begin{matrix} 1 & 3 \\ 2 \end{matrix}$ and $1 / 2 / 3$ ; rank $4$ has $1234$ , the three tableaux $\begin{matrix} 1 & 2 & 3 \\ 4 \end{matrix}$ , $\begin{matrix} 1 & 2 & 4 \\ 3 \end{matrix}$ , $\begin{matrix} 1 & 3 & 4 \\ 2 \end{matrix}$ , the two tableaux $\begin{matrix} 1 & 2 \\ 3 & 4 \end{matrix}$ , $\begin{matrix} 1 & 3 \\ 2 & 4 \end{matrix}$ , the three tableaux $\begin{matrix} 1 & 2 \\ 3 \\ 4 \end{matrix}$ , $\begin{matrix} 1 & 3 \\ 2 \\ 4 \end{matrix}$ , $\begin{matrix} 1 & 4 \\ 2 \\ 3 \end{matrix}$ and $1 / 2 / 3 / 4$ . Counting these gives the values $f^{λ}$ displayed in claim 4.

3.1F1F2step 2.1algebra

Removable nodes by the criterion of [F2], read in the reverse direction: $(1)$ has the removable node $(1, 1)$ with $(1) - (1, 1) = \emptyset$ ; $(2)$ has $(1, 2)$ giving $(1)$ ; $(1, 1)$ has $(2, 1)$ giving $(1)$ ; $(3)$ has $(1, 3)$ giving $(2)$ ; $(2, 1)$ has $(1, 2)$ giving $(1, 1)$ and $(2, 1)$ giving $(2)$ ; $(1, 1, 1)$ has $(3, 1)$ giving $(1, 1)$ ; $(4)$ has $(1, 4)$ giving $(3)$ ; $(3, 1)$ has $(1, 3)$ giving $(2, 1)$ and $(2, 1)$ giving $(3)$ ; $(2, 2)$ has $(2, 2)$ giving $(2, 1)$ only; $(2, 1, 1)$ has $(1, 2)$ giving $(1, 1, 1)$ and $(3, 1)$ giving $(2, 1)$ ; and $(1, 1, 1, 1)$ has $(4, 1)$ giving $(1, 1, 1)$ . In every case the resulting partition has one box fewer, and the incoming edges so obtained are exactly the edges of step 2.1 read backwards: for example the two incoming edges of $(2, 1)$ come from $(2)$ and $(1, 1)$ , and the only incoming edge of $(2, 2)$ comes from $(2, 1)$ .

3.2F4F7step 2.2algebra

By [F4] each $\dim_{C} S_{C}^{λ}$ equals the corresponding value $f^{λ}$ of step 2.2. Substituting these dimensions into [F7] with $G = S_{n}$ over $k = C$ gives $\sum_{λ ⊢ n} (f^{λ})^{2} = ∣ S_{n} ∣ = n!$ by [F7]; explicitly $1^{2} = 1$ , $1^{2} = 1$ , $1^{2} + 1^{2} = 2$ , $1^{2} + 2^{2} + 1^{2} = 6$ and $1^{2} + 3^{2} + 2^{2} + 3^{2} + 1^{2} = 24$ for $n = 0, 1, 2, 3, 4$ .

4.1F5F6step 2.1step 3.1

Claim 3 follows from the two branching rules: by [F5], for each $λ ⊢ n$ with $1 \leq n \leq 4$ the restriction of $S_{C}^{λ}$ is the direct sum of one copy of $S_{C}^{λ - x}$ for each removable node $x$ , that is one summand per incoming edge of step 3.1; by [F6], for each $λ ⊢ n$ with $0 \leq n \leq 3$ the induction of $S_{C}^{λ}$ is the direct sum of one copy of $S_{C}^{λ + y}$ for each addable node $y$ , that is one summand per outgoing edge of step 2.1. The two displayed instances are the cases $λ = (2, 2)$ with the single removable node and $λ = (2, 1)$ with its three addable nodes.

5.1F1F2F7step 2.1step 4.1step 3.2∎

Boundary and consistency audit. Rank $0$ carries the single vertex $\emptyset$ , whose unique standard tableau is the empty one, and the empty product $n! = 0! = 1$ matches $f^{\emptyset} = 1$ ; every partition of $n \geq 1$ has at least one removable node and at least one addable node by [F2] (for the addable case take the node opening a new row), so both branching sums are nonempty and each of the $1, 2, 4, 7$ edges between consecutive ranks is counted exactly once in each direction; and the edge counts agree with the two enumerations of the same edge set, since summing the number of incoming edges over the partitions of $n$ for $n = 1, 2, 3, 4$ gives $1, 2, 4, 7$ , the same numbers as in step 2.1. All sets involved are finite and explicitly listed, so no choice principle enters. This proves claims 1 to 4 and hence the Statement.

Remarks

The graph is the branching rule. Reading claim 3 along claim 2 says that the Young graph is exactly the bookkeeping device for the two branching rules: the neighbours one rank below a vertex $λ$ index the summands of the restriction of $S_{C}^{λ}$ , and the neighbours one rank above index the summands of its induction, always with multiplicity one on this finite piece of the graph.
Two convenient checks. The numbers of edges between consecutive ranks $0$ - $1$ , $1$ - $2$ , $2$ - $3$ and $3$ - $4$ computed in step 2.1 are $1, 2, 4, 7$ , while the vertex counts at ranks $1, 2, 3, 4$ are the partition numbers $1, 2, 3, 5$ : the edge count exceeds the vertex count exactly because a vertex such as $(2, 1)$ or $(2, 1, 1)$ has two removable corners and hence two incoming edges. And the sum-of-squares identity of step 3.2, $\sum_{λ ⊢ n} (f^{λ})^{2} = n!$ , is the numerical shadow of the decomposition of the regular representation of $S_{n}$ into Specht modules.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

60 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

Charlotte Chan, Representation Theory of Symmetric Groups, Theorem 4.16, printed pp. 18-19, and Theorem 6.8, printed p. 26 (standard reference, not scraped)
David A. Craven, Groups, Geometries and Representation Theory, Sections 2.2 and 2.4, printed pp. 22-23 and 28-31 (standard reference, not scraped)