ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-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 RSK shapes of the six permutations of $S_{3}$

Example

Running Robinson-Schensted row insertion on the six permutations of ${1, 2, 3}$ gives $123 \mapsto (3), 132 \mapsto (2, 1), 213 \mapsto (2, 1), 231 \mapsto (2, 1), 312 \mapsto (2, 1), 321 \mapsto (1^{3});$ the resulting shape frequencies are $\frac{1}{6}$ for $(3)$ , $\frac{4}{6}$ for $(2, 1)$ and $\frac{1}{6}$ for $(1^{3})$ , matching $P_{3}$ of The Plancherel measure on partitions of three and confirming The RSK shape of a uniform random permutation has the Plancherel law at $n = 3$ .

Facts & Assumptions

Given: the six permutations of ${1, 2, 3}$ in one-line form, each of weight $1 / 6$ ; row insertion as defined in Row insertion and the bumping route; the insertion tableau $P (σ)$ of a permutation $σ$ and its shape $sh (σ)$ (The Robinson-Schensted correspondence).

[F1]

Row insertion is deterministic: a new letter that is larger than every entry of the current first row is appended at its right end, and otherwise the letter replaces the leftmost entry larger than it, which is bumped to the next row and processed there by the same rule (Row insertion and the bumping route).

[F2]

The shape of the insertion tableau $P (σ)$ is $sh (σ)$ ; the Robinson-Schensted map is a bijection onto pairs of standard tableaux of equal shape (The Robinson-Schensted correspondence).

[F3]

For a uniform permutation of ${1, 2, 3}$ , $sh$ has law $P_{3}$ , namely the weights $1 / 6, 4 / 6, 1 / 6$ on $(3), (2, 1), (1^{3})$ (The RSK shape of a uniform random permutation has the Plancherel law, The Plancherel measure on partitions of three).

Verification

technique · direct

1.1givenF1

Explicit insertions: applying [F1] to each word, one letter at a time, gives the following tableaux (written as the list of their rows): $123 ⇝ ((1, 2, 3))$ , shape $(3)$ ; $132$ : $(1)$ , then $(1, 3)$ , then $2$ bumps the $3$ , giving rows $(1, 2)$ and $(3)$ , shape $(2, 1)$ ; $213$ : $(2)$ , then $1$ bumps $2$ giving rows $(1)$ and $(2)$ , then $3$ is appended in the first row, shape $(2, 1)$ ; $231$ : $(2)$ , then $(2, 3)$ , then $1$ bumps $2$ , giving rows $(1, 3)$ and $(2)$ , shape $(2, 1)$ ; $312$ : $(3)$ , then $1$ bumps $3$ giving rows $(1)$ and $(3)$ , then $2$ is appended in the first row, shape $(2, 1)$ ; $321$ : $(3)$ , then $2$ bumps $3$ , giving rows $(2)$ and $(3)$ , then $1$ bumps $2$ and the expelled $2$ bumps $3$ , giving rows $(1)$ , $(2)$ , $(3)$ , shape $(1^{3})$ . Each bumping step is the deterministic rule of [F1] applied to the displayed entries.

2.1givenF2step 1.1algebra

Frequencies: by [F2] the shapes recorded in step 1.1 are the Robinson-Schensted shapes of the six permutations, so among the six words the shape $(3)$ occurs once, $(2, 1)$ four times and $(1^{3})$ once; with the uniform weight $1 / 6$ on each permutation the frequencies are $1 / 6, 4 / 6, 1 / 6$ .

3.1givenF3step 2.1algebra∎

Comparison: the frequencies of step 2.1 are exactly the Plancherel weights $P_{3} (3) = 1 / 6$ , $P_{3} (2, 1) = 4 / 6$ and $P_{3} (1^{3}) = 1 / 6$ of [F3], confirming the law of the shape of a uniform permutation at $n = 3$ ; every step was a finite computation with integer entries, and no choice principle was used.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

22 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

Dan Romik, The Surprising Mathematics of Longest Increasing Subsequences, Cambridge University Press 2015; author-hosted manuscript of 20 August 2014 (363 pp.) (standard reference, not scraped)

The RSK shapes of the six permutations of S3S3​