LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30

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.

Nonzero antisymmetrizer image detects dominance

Statement

For every $n \geq 0$ , partitions $λ, μ ⊢ n$ , and $λ$ -tableau $t$ , if $κ_{t} M^{μ} \neq 0$ , then $λ$ dominates $μ$ in the published order $λ ⊵ μ$ .

Facts & Assumptions

Given: $n \geq 0$ , $λ, μ ⊢ n$ , a $λ$ -tableau $t$ , and the hypothesis $κ_{t} M^{μ} \neq 0$ .

[F1]

The $μ$ -tabloids form a basis of $M^{μ}$ , with the linear extension of the left action of $S_{n}$ (Young subgroups, tabloids, and permutation modules).

[F2]

The column antisymmetrizer is the group-algebra element $κ_{t} = \sum_{γ \in C_{t}} sgn (γ) γ$ (Column antisymmetrizers, polytabloids, and Specht modules).

[F3]

If two entries in one row of $s$ lie in one column of $t$ , then $κ_{t} \cdot {s} = 0$ (Column collision cancels antisymmetrization).

[F4]

If every row of $s$ meets each column of $t$ in at most one entry, then for tableaux of shapes $λ$ and $μ$ one has $λ ⊵ μ$ (Basic row-column incidence lemma).

[F5]

The notation $λ ⊵ μ$ means that every prefix sum of $λ$ is at least the corresponding prefix sum of $μ$ , with both partitions padded by zeros (Dominance order on partitions).

Proof

technique · direct

1.1givenF1F2construct

By [F1,F2], $κ_{t}$ acts linearly on $M^{μ}$ . If it killed every $μ$ -tabloid, it would kill their span $M^{μ}$ , contrary to the hypothesis; therefore some $μ$ -tabloid ${s}$ satisfies $κ_{t} \cdot {s} \neq 0$ .

2.1step 1.1givenF3F4F5construct∎

By the contrapositive of [F3], no row of $s$ contains two entries from one column of $t$ . Thus the basic combinatorial lemma [F4] applies to these tableaux and gives $λ ⊵ μ$ ; by [F5] this is exactly the published dominance order in the statement.

Depends on

Used by

Homomorphisms from Specht to Young permutation modules obey dominance Theorem

Dependency tree · two levels

11 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

Charlotte Chan, Representation Theory of Symmetric Groups - Theorem 4.1(a) and proof, printed p. 15 (standard reference, not scraped)