ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-08

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.

RSK cells in $S_{3}$ and $S_{4}$

Facts & Assumptions

Given: The row-insertion and recording-tableau conventions for one-line permutations in $S_{3}$ and $S_{4}$ , and the corresponding Kazhdan–Lusztig cell relations.

[F1]

Row insertion replaces the leftmost entry strictly greater than the carried letter, bumps that entry to the next row, and stops by appending at the right end of a row; the recording tableau places label $k$ in the new box created by inserting the $k$ th letter (Row insertion and the bumping route, The Robinson-Schensted correspondence).

[F2]

The type-A cell theorem identifies left cells with $Q$ -fibers, right cells with $P$ -fibers, and two-sided cells with common RSK-shape fibers (Kazhdan–Lusztig cells of type A are classified by RSK tableaux).

[F3]

The right descent set is $R (w) = {s_{i} : ℓ (w s_{i}) < ℓ (w)}$ , where $w s_{i}$ swaps positions $i, i + 1$ in one-line notation; right descents are constant on a left cell ( $L$ -, $R$ - and two-sided Kazhdan–Lusztig preorders and cells).

[F4]

The length $ℓ (w)$ is the number of inversions of the one-line word, and the standard tableaux in the RSK pairs are increasing along rows and columns (Permutation Weyl group and inversion length, Tableaux and standard tableaux, Partitions, English diagrams, and conjugation).

Statement

Use the RSK correspondence of The Robinson-Schensted correspondence for the one-line word (insertion tableau $P$ , recording tableau $Q$ ; the row insertion is Row insertion and the bumping route), and write a standard tableau as its rows separated by bars. (a) In $S_{3}$ : $123 \mapsto (123, 123)$ , $132 \mapsto (12 ∣ 3, 12 ∣ 3)$ , $213 \mapsto (13 ∣ 2, 13 ∣ 2)$ , $231 \mapsto (13 ∣ 2, 12 ∣ 3)$ , $312 \mapsto (12 ∣ 3, 13 ∣ 2)$ , $321 \mapsto (1 ∣ 2 ∣ 3, 1 ∣ 2 ∣ 3)$ (pairs $(P, Q)$ ). (b) The left cells of $S_{3}$ are the four $Q$ -fibers ${123}$ , ${132, 231}$ , ${213, 312}$ , ${321}$ ; the right cells are the four $P$ -fibers ${123}$ , ${132, 312}$ , ${213, 231}$ , ${321}$ ; the two-sided cells are the three shape fibers ${123}$ , ${132, 213, 231, 312}$ , ${321}$ . (c) In $S_{4}$ the ten left cells are the ten $Q$ -fibers: $[1234] : {1234}$ ; $[12 ∣ 34] : {2413, 3412}$ ; $[123 ∣ 4] : {1243, 1342, 2341}$ ; $[124 ∣ 3] : {1324, 1423, 2314}$ ; $[13 ∣ 24] : {2143, 3142}$ ; $[134 ∣ 2] : {2134, 3124, 4123}$ ; $[12 ∣ 3 ∣ 4] : {1432, 2431, 3421}$ ; $[13 ∣ 2 ∣ 4] : {3241, 4132, 4231}$ ; $[14 ∣ 2 ∣ 3] : {3214, 4213, 4312}$ ; $[1 ∣ 2 ∣ 3 ∣ 4] : {4321}$ ; these are in bijection with the ten standard tableaux of size $4$ . (d) Right descent sets are constant on left cells but do not determine them: in $S_{4}$ the permutations $1324$ and $2413$ both have right descent set ${s_{2}}$ , while $Q (1324) = [124 ∣ 3]$ and $Q (2413) = [12 ∣ 34]$ , so $1324$ and $2413$ lie in different left cells.

Proof

technique · apply the row-insertion rule to the listed permutations and then read the cell equivalences from the type-A classification

1.1F1

The six RSK pairs in $S_{3}$ . Repeated insertion using [F1] gives $\begin{array}{ccc} w & P (w) & Q (w) \\ 123 & [123] & [123] \\ 132 & [12 ∣ 3] & [12 ∣ 3] \\ 213 & [13 ∣ 2] & [13 ∣ 2] \\ 231 & [13 ∣ 2] & [12 ∣ 3] \\ 312 & [12 ∣ 3] & [13 ∣ 2] \\ 321 & [1 ∣ 2 ∣ 3] & [1 ∣ 2 ∣ 3] \end{array}$ . For example, $132$ inserts $1$ , then appends $3$ , then inserts $2$ in place of $3$ and bumps $3$ to a new second row; the third recording label is therefore in row two. The same leftmost-greater rule gives the other displayed pairs.

1.2F1

All RSK pairs in $S_{4}$ , grouped by $Q$ . Applying [F1] to each of the $24$ one-line words gives $\begin{array}{cl} Q(w) & (w,P(w)) \\ [1234] & (1234,[1234]) \\ [12|34] & (2413,[13|24]),(3412,[12|34]) \\ [123|4] & (1243,[123|4]),(1342,[124|3]),(2341,[134|2]) \\ [124|3] & (1324,[124|3]),(1423,[123|4]),(2314,[134|2]) \\ [13|24] & (2143,[13|24]),(3142,[12|34]) \\ [134|2] & (2134,[134|2]),(3124,[124|3]),(4123,[123|4]) \\ [12|3|4] & (1432,[12|3|4]),(2431,[13|2|4]),(3421,[14|2|3]) \\ [13|2|4] & (3241,[14|2|3]),(4132,[12|3|4]),(4231,[13|2|4]) \\ [14|2|3] & (3214,[14|2|3]),(4213,[13|2|4]),(4312,[12|3|4]) \\ [1|2|3|4] & (4321,[1|2|3|4]) \end{array}$ . As a nontrivial check on the convention, insertion of $2413$ first gives rows $[2, 4]$ , then bumps $2$ below when $1$ is inserted, and finally bumps $4$ below $3$ ; thus $P (2413) = [13 ∣ 24]$ and $Q (2413) = [12 ∣ 34]$ .

2.1F2step 1.1

Cells in $S_{3}$ . By [F2] and step 1.1, grouping by equal $Q$ gives the four left fibers in part (b), grouping by equal $P$ gives the four right fibers, and grouping by the common shape gives the three two-sided fibers. The displayed RSK pairs contain all six permutations, so there are no omitted elements in any fiber.

2.2F1F2F4step 1.2

Left cells in $S_{4}$ . By [F2], each row label $Q$ in step 1.2 indexes exactly one left cell. The possible shapes of size four are $(4), (3, 1), (2, 2), (2, 1, 1), (1, 1, 1, 1)$ ; their standard tableaux are respectively $[1234]$ ; $[123 ∣ 4], [124 ∣ 3], [134 ∣ 2]$ ; $[12 ∣ 34], [13 ∣ 24]$ ; $[12 ∣ 3 ∣ 4], [13 ∣ 2 ∣ 4], [14 ∣ 2 ∣ 3]$ ; and $[1 ∣ 2 ∣ 3 ∣ 4]$ . These are exactly the ten distinct $Q$ -labels in the table. The listed fibers contain $1 + 2 + 3 + 3 + 2 + 3 + 3 + 3 + 3 + 1 = 24$ permutations, so every element of $S_{4}$ occurs and the table proves part (c) and the claimed bijection.

3.1F2F3F4step 1.2∎

Equal right descents do not determine the left cell. In one-line notation, $1324$ has length $1$ and right products $1324 s_{1} = 3124$ , $1324 s_{2} = 1234$ , $1324 s_{3} = 1342$ of lengths $2, 0, 2$ . Thus $R (1324) = {s_{2}}$ . The word $2413$ has length $3$ and right products $2413 s_{1} = 4213$ , $2413 s_{2} = 2143$ , $2413 s_{3} = 2431$ of lengths $4, 2, 4$ , so $R (2413) = {s_{2}}$ as well. But step 1.2 gives $Q (1324) = [124 ∣ 3] \neq [12 ∣ 34] = Q (2413)$ , so [F2] places them in different left cells. This proves the counterexample while [F3] records that descent sets are constant within each left cell.

The calculations concern only $S_{3}$ and $S_{4}$ ; no empty or singleton group case is asserted. All insertion procedures are finite and deterministic, so no choice principle is used.

Remarks

The classification use in [F2] is exactly its preserved $Q$ -, $P$ - and shape-fiber interface: step 2.1 uses all three in $S_{3}$ , step 2.2 uses only the $Q$ -fiber clause in $S_{4}$ , and step 3.1 uses that clause to separate the two recording tableaux. The tables and descents are computed locally; the supplier's sole cited shape-invariance implication is not replaced by a new source assumption here.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

32 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

Susumu Ariki, Robinson–Schensted correspondence and left cells, arXiv:math/9910117 (18 pp.) (standard reference, not scraped)

RSK cells in S3S3​ and S4S4​