Alphabeta Math
CorollaryStatement: Literature-sourcedProof: Literature-sourcedPipeline-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.

Involutions are counted by standard tableaux

Statement

Let w be a permutation of {1,…,n} with RSK pair (P,Q). Then w=w−1 if and only if P=Q. Consequently the map w↦P(w) restricts to a bijection from the set of involutions of {1,…,n} onto the set of standard tableaux with n boxes, and the number of involutions of {1,…,n} (equivalently, of Sn) equals ∑λ⊢nfλ.

Facts & Assumptions

Given: An integer n≥0, a word w=(w1,…,wn) of pairwise distinct real numbers with {w1,…,wn}={1,…,n}, its RSK pair (P(w),Q(w)), and the inverse word w−1=(p1,…,pn) with wpi=i.

[L1]

The Robinson-Schensted map w↦(P(w),Q(w)) is a bijection from Xn onto the set of pairs of standard tableaux of a common shape λ⊢n; in particular it is injective (The Robinson-Schensted correspondence).

[L2]

P(w−1)=Q(w) and Q(w−1)=P(w) (RSK interchanges the insertion and recording tableaux under inversion).

[L3]

Identifying σ∈Sn with the word w=(σ(0)+1,…,σ(n−1)+1), the word of σ−1 is w−1; thus w=w−1 if and only if σ=σ−1, and the involutions of {1,…,n} are the words fixed by inversion (The finite symmetric group Sn, one-line notation, and cycle notation, RSK interchanges the insertion and recording tableaux under inversion).

[L4]

A standard tableau with n boxes has shape λ⊢n, and for each λ⊢n there are fλ such tableaux; the shapes are distinct, so the total number is ∑λ⊢nfλ (Tableaux and standard tableaux).

Proof

technique · direct
1.1L2given

If w=w−1 then (P(w),Q(w))=(P(w−1),Q(w−1))=(Q(w),P(w)) by [L2], so P(w)=Q(w).

1.2L2L1given

Conversely, if P(w)=Q(w) then P(w−1)=Q(w)=P(w) and Q(w−1)=P(w)=Q(w) by [L2], so (P(w−1),Q(w−1))=(P(w),Q(w)); injectivity of the Robinson-Schensted map [L1] gives w−1=w.

2.1step 1.1step 1.2L1

(Injectivity on involutions.) If w,w′ are fixed by inversion and P(w)=P(w′), then by step 1.1 and step 1.2 Q(w)=P(w)=P(w′)=Q(w′), so the RSK pairs coincide and [L1] gives w=w′.

2.2L1step 1.2L4

(Surjectivity onto standard tableaux.) Let P be a standard tableau with n boxes, of shape λ⊢n; the pair (P,P) is a pair of standard tableaux of common shape, so by surjectivity of the Robinson-Schensted map [L1] there is a word w∈Xn with (P(w),Q(w))=(P,P); by step 1.2 w is fixed by inversion, and P(w)=P.

3.1step 2.1step 2.2L3L4

(The count.) By steps 2.1 and 2.2 the map w↦P(w) is a bijection from the involutions onto the standard tableaux with n boxes; by [L4] the latter set has ∑λ⊢nfλ elements, and by [L3] the involutions of {1,…,n} are the involutions of Sn.

4.1L1L4given∎

At n=0 the empty word is the unique element of X0 and equals its inverse, the only standard tableau with no boxes is the empty tableau, f∅=1, and both sides of the count are 1, consistent with steps 1.1 and 1.2.

Depends on

Used by

Dependency tree · two levels

15 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