ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-27

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.

Removable nodes versus row endpoints

Example

For the shapes $λ = (3, 3, 1)$ , $μ = (3, 2, 1)$ and the empty shape $\emptyset$ the removable and addable nodes are as follows.

$λ = (3, 3, 1)$ has two removable nodes, the row endpoints $(2, 3)$ and $(3, 1)$ , while the row endpoint $(1, 3)$ is not removable because the node $(2, 3)$ lies directly below it. Its addable nodes are $(1, 4)$ , $(3, 2)$ and $(4, 1)$ .
$μ = (3, 2, 1)$ has all three of its row endpoints $(1, 3)$ , $(2, 2)$ , $(3, 1)$ removable, and its addable nodes are $(1, 4)$ , $(2, 3)$ , $(3, 2)$ and $(4, 1)$ .
$\emptyset$ has no removable node and exactly one addable node, $(1, 1)$ , whose insertion produces the partition $(1)$ .

Thus ending a row is necessary but not sufficient for removability, and the first shape above exhibits the difference.

Facts & Assumptions

Given: The partitions $(3, 3, 1)$ of $7$ and $(3, 2, 1)$ of $6$ and the empty partition $\emptyset$ .

[F1]

A node of $[λ]$ is removable when deleting it leaves a Young diagram and a point outside $[λ]$ is addable when inserting it leaves a Young diagram; for $λ = (λ_{1}, \dots, λ_{k})$ with $λ_{k + 1} : = 0$ the removable nodes are exactly the row endpoints $(i, λ_{i})$ with $λ_{i} > λ_{i + 1}$ , and the addable nodes are exactly the points $(i, λ_{i} + 1)$ with $i = 1$ or $λ_{i - 1} > λ_{i}$ , together with $(k + 1, 1)$ ; deleting a removable node leaves the diagram of a partition of $n - 1$ , and $Rem (\emptyset) = \emptyset$ , $Add (\emptyset) = {(1, 1)}$ (Removable and addable nodes).

Verification

technique · direct

1.1

For $λ = (3, 3, 1)$ the row lengths are $3, 3, 1$ , so the row endpoints are $(1, 3), (2, 3), (3, 1)$ ; by [F1] the removable ones are those with $λ_{i} > λ_{i + 1}$ , and with $λ_{4} : = 0$ these are $(2, 3)$ , because $3 > 1$ , and $(3, 1)$ , because $1 > 0$ , while $λ_{1} = λ_{2}$ excludes $(1, 3)$ : deleting $(1, 3)$ would leave the row lengths $2, 3, 1$ , which are not weakly decreasing, so this row endpoint is not removable. Deleting the two removable nodes instead gives the partitions $(3, 2, 1)$ and $(3, 3)$ of size $6$ .

givenF1

1.2

For $λ = (3, 3, 1)$ the addable points of the form $(i, λ_{i} + 1)$ are $(1, 4)$ , which is in the first row, and $(3, 2)$ , because $λ_{2} = 3 > λ_{3} = 1$ , while $(2, 4)$ fails the test $λ_{1} > λ_{2}$ since $3 = 3$ ; the point $(4, 1)$ opens a new row and is addable by [F1]. Inserting these three points gives the partitions $(4, 3, 1)$ from $(1, 4)$ , $(3, 3, 2)$ from $(3, 2)$ and $(3, 3, 1, 1)$ from $(4, 1)$ .

givenF1

1.3

For $μ = (3, 2, 1)$ the row lengths are strictly decreasing, $3 > 2 > 1 > 0$ , so by [F1] all three row endpoints are removable: $(1, 3)$ with deletion $(2, 2, 1)$ , $(2, 2)$ with deletion $(3, 1, 1)$ , and $(3, 1)$ with deletion $(3, 2)$ , each of size $5$ .

givenF1

1.4

For $μ = (3, 2, 1)$ the addable points are $(1, 4)$ in the first row, $(2, 3)$ because $μ_{1} = 3 > μ_{2} = 2$ , $(3, 2)$ because $μ_{2} = 2 > μ_{3} = 1$ , and $(4, 1)$ opening a new row, and no other point of the form $(i, μ_{i} + 1)$ passes the test of [F1]; inserting $(2, 3)$ and $(3, 2)$ gives the partitions $(3, 3, 1)$ and $(3, 2, 2)$ of size $7$ .

1.5

For $\emptyset$ the diagram has no nodes, so $Rem (\emptyset) = \emptyset$ ; a point $(i, j)$ outside the empty diagram leaves a Young diagram after insertion only for $(i, j) = (1, 1)$ , since the diagrams ${(i, j)}$ with $j \geq 2$ or $i \geq 2$ are not left-justified, so $Add (\emptyset) = {(1, 1)}$ and the resulting partition is $(1)$ , in agreement with [F1].

2.1

The three shapes are thus completely described: $Rem (3, 3, 1) = {(2, 3), (3, 1)}$ with the non-removable row endpoint $(1, 3)$ , $Rem (3, 2, 1) = {(1, 3), (2, 2), (3, 1)}$ , $Rem (\emptyset) = \emptyset$ , together with the addable sets $Add (3, 3, 1) = {(1, 4), (3, 2), (4, 1)}$ , $Add (3, 2, 1) = {(1, 4), (2, 3), (3, 2), (4, 1)}$ and $Add (\emptyset) = {(1, 1)}$ . ∎

step 1.1step 1.2step 1.3step 1.4step 1.5

Depends on

Removable and addable nodes

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

2 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 Craven, Groups, Geometries and Representation Theory - Definition 1.10, printed p. 7 (PDF p. 9) (standard reference, not scraped)
Charlotte Chan, Representation Theory of Symmetric Groups - Chapter 2, printed pp. 7-8 (PDF pp. 8-9) (standard reference, not scraped)