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

Tableau stabilizers transform by conjugation

Statement

Let n≥0, let λ⊢n and let t be a λ-tableau. For every σ∈Sn, Rσ⋅t=σRtσ−1,Cσ⋅t=σCtσ−1, where Rt and Ct are the row and column stabilizers of t and σ⋅t is the tableau with entries (σ⋅t)(i,j)=σ(t(i,j)).

Facts & Assumptions

Given: An integer n≥0, a partition λ⊢n, a λ-tableau t, and a permutation σ∈Sn.

[L1]

The row sets Ai={t(i,j):1≤j≤λi} and the column sets Bj={t(i,j):1≤i≤λj′} of t each partition {1,…,n}, and Rt={γ∈Sn:γ(Ai)=Ai for every i}, Ct={γ∈Sn:γ(Bj)=Bj for every j} (Row and column stabilizers).

[L2]

The left action on tableaux is entrywise, (τ⋅t)(i,j)=τ(t(i,j)) for τ∈Sn (Row and column stabilizers).

[L3]

For n=0 there is exactly one tableau, the empty one, with Rt=Ct=S0={1} (Row and column stabilizers).

Proof

technique · direct
1.1

For every row i, the row set of σ⋅t is Ai(σ⋅t)={(σ⋅t)(i,j):1≤j≤λi}={σ(t(i,j)):1≤j≤λi}=σ(Ai) by [L2], and likewise the column set of σ⋅t in column j is Bj(σ⋅t)=σ(Bj).

givenL1L2algebra
2.1

By [L1] and step 1.1, a permutation γ∈Sn lies in Rσ⋅t exactly when γ(σ(Ai))=σ(Ai) for every row i, which after applying σ−1 to both sides is equivalent to σ−1γσ(Ai)=Ai for every i, that is to σ−1γσ∈Rt.

step 1.1L1algebra
3.1

The equivalence of step 2.1 read in the forward and the backward direction gives both inclusions Rσ⋅t⊆σRtσ−1 and σRtσ−1⊆Rσ⋅t, hence Rσ⋅t=σRtσ−1.

step 2.1
4.1

The identical computation with the column sets of step 1.1 in place of the row sets gives Cσ⋅t=σCtσ−1: γ∈Cσ⋅t exactly when γ(σ(Bj))=σ(Bj) for every column j, which is equivalent to σ−1γσ∈Ct.

step 1.1step 3.1L1
5.1

Both identities also hold for n=0: then t is the empty tableau, σ is the identity of S0={1}, and Rt=Ct=S0 by [L3], so conjugation is the identity and Rσ⋅t=Rt=σRtσ−1, likewise for Ct. In all cases, then, the row and column stabilizers of σ⋅t are the conjugates of Rt and Ct by σ. ∎

step 2.1step 4.1L3

Depends on

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