ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-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.

A complete RSK insertion and reverse deletion run

Example

Let $σ$ be the permutation of ${1, \dots, 6}$ with $σ = (1 6 3) (2 4)$ , so its one-line form is the word $w = (6, 4, 1, 2, 5, 3)$ . Running row insertion gives $P_{1} = \begin{array}{l} 6 \end{array}, P_{2} = \begin{array}{l} 4 \\ 6 \end{array}, P_{3} = \begin{array}{l} 1 \\ 4 \\ 6 \end{array}, P_{4} = \begin{array}{ll} 1 & 2 \\ 4 \\ 6 \end{array}, P_{5} = \begin{array}{lll} 1 & 2 & 5 \\ 4 \\ 6 \end{array}, P_{6} = \begin{array}{lll} 1 & 2 & 3 \\ 4 & 5 \\ 6 \end{array}$ and the recording tableaux $Q_{1} = \begin{array}{l} 1 \end{array}, Q_{2} = \begin{array}{l} 1 \\ 2 \end{array}, Q_{3} = \begin{array}{l} 1 \\ 2 \\ 3 \end{array}, Q_{4} = \begin{array}{ll} 1 & 4 \\ 2 \\ 3 \end{array}, Q_{5} = \begin{array}{lll} 1 & 4 & 5 \\ 2 \\ 3 \end{array}, Q_{6} = \begin{array}{lll} 1 & 4 & 5 \\ 2 & 6 \\ 3 \end{array} .$ Reverse deletion from $(P_{6}, Q_{6})$ in the order of the labels $6, 5, 4, 3, 2, 1$ removes the boxes $(2, 2), (1, 3), (1, 2), (3, 1), (2, 1), (1, 1)$ and expels the letters $3, 5, 2, 1, 4, 6$ , which is $w$ read backwards, restoring $(\emptyset, \emptyset)$ .

Facts & Assumptions

Given: The word $w = (6, 4, 1, 2, 5, 3)$ of pairwise distinct reals, the tableaux $P_{k}$ obtained by inserting $w_{1}, \dots, w_{k}$ by row insertion, and the recording tableaux $Q_{k}$ carrying the label $k$ in the box added at step $k$ .

[L1]

Row insertion at each step places the carried letter in the first row by appending it at the end when it is larger than every entry, and otherwise replacing the leftmost entry exceeding it and passing that entry to the next row, until an append occurs; the new box is the appended box (Row insertion and the bumping route).

[L2]

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

[L3]

For a standard tableau $U$ and a removable box $b = (s, t)$ , reverse deletion $(V, x) : = U - b$ satisfies $V \leftarrow x = U$ with new box $b$ ; conversely, deleting the new box of $T \leftarrow y$ returns $(T, y)$ . Deletion visits rows $s, s - 1, \dots, 1$ , moving upwards from $b$ , taking at each row the largest entry smaller than the carried letter (Reverse row deletion, Row insertion and reverse deletion are inverse).

[L4]

The RSK pair of $w$ is $(P_{6}, Q_{6})$ and the deletion procedure of the correspondence recovers $w$ backwards (The Robinson-Schensted correspondence).

Verification

technique · direct

1.1L1given

(Insertion steps.) Inserting $6$ into the empty tableau gives $P_{1} = [6]$ . Inserting $4$ replaces $6$ in row $1$ and appends the displaced $6$ in the empty row $2$ , giving $P_{2}$ . Inserting $1$ replaces $4$ in row $1$ , carries $4$ into row $2$ where it replaces $6$ , and appends that displaced $6$ in the empty row $3$ , giving $P_{3}$ . These are the displayed columns.

2.1L1step 1.1algebra

(Steps $4$ and $5$ .) Inserting $2$ into $P_{3}$ , whose first row is $[1]$ and second row $[4]$ , appends $2$ at the end of the first row, giving $P_{4}$ ; inserting $5$ into $P_{4}$ appends it at the end of the first row as $5 > 2$ , giving $P_{5}$ ; the new boxes are $(1, 2)$ at step $4$ and $(1, 3)$ at step $5$ .

3.1L1step 2.1algebra

(Step $6$ .) Inserting $3$ into $P_{5}$ , whose first row is $[1, 2, 5]$ and second row $[4]$ : the leftmost entry exceeding $3$ is $5$ at position $3$ , so $3$ replaces it and $5$ is carried to the second row, where it is larger than $4$ and is appended; hence $P_{6} = \begin{array}{lll} 1 & 2 & 3 \\ 4 & 5 \\ 6 \end{array}$ , with new box $(2, 2)$ .

4.1L2step 1.1step 2.1step 3.1

(Recording tableaux.) At each step $k$ the label $k$ is written in the new box of that step, which is $(1, 1), (2, 1), (3, 1), (1, 2), (1, 3), (2, 2)$ for $k = 1, \dots, 6$ ; these boxes are exactly those filled in the displayed $Q_{1}, \dots, Q_{6}$ , and by [L2] each $Q_{k}$ is standard of the shape of $P_{k}$ .

5.1L3L4step 3.1step 4.1

(First deletion.) The box of the label $6$ in $Q_{6}$ is $(2, 2)$ , the bottom-right corner; reverse deletion starts there with the carried letter $+ \infty$ , takes in row $2$ the entry $5$ (the largest entry smaller than $+ \infty$ ), empties $(2, 2)$ and carries $5$ ; in row $1$ the largest entry smaller than $5$ is $3$ at position $3$ , which is overwritten by $5$ and expelled. The result is $P_{5}$ , and the expelled letter $3$ is $w_{6}$ .

6.1L3L4step 5.1given

(Remaining deletions.) Repeating step 5.1 for the labels $5, 4, 3, 2, 1$ : deleting the box $(1, 3)$ of label $5$ expels $5$ and restores $P_{4}$ ; deleting the box $(1, 2)$ of label $4$ expels $2$ and restores $P_{3}$ ; deleting the box $(3, 1)$ of label $3$ expels $1$ and restores $P_{2}$ ; deleting the box $(2, 1)$ of label $2$ expels $4$ and restores $P_{1}$ ; deleting the box $(1, 1)$ of label $1$ expels $6$ and leaves $\emptyset$ . Each deletion reverses the corresponding insertion by [L3], and the recorded labels are the boxes listed in the statement.

7.1L4step 5.1step 6.1∎

(Conclusion.) The expelled letters in the order $3, 5, 2, 1, 4, 6$ are $w_{6}, w_{5}, w_{4}, w_{3}, w_{2}, w_{1}$ , i.e. $w$ read backwards; both tableaux are restored to the empty tableau, so the run illustrates the inverse procedure of the Robinson-Schensted correspondence.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

10 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)
Jeremy L. Martin, Lecture Notes on Algebraic Combinatorics (263 pp.) (standard reference, not scraped)