PropositionStatement: Literature-sourcedProof: 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 Kronecker coefficient is a three-character inner product

Statement

For all partitions $λ, μ, ν ⊢ n$ , $g (λ, μ, ν) = ⟨ χ^{λ} χ^{μ}, χ^{ν} ⟩ = \frac{1}{n!} \sum_{σ \in S_{n}} χ^{λ} (σ) χ^{μ} (σ) χ^{ν} (σ),$ where $χ^{λ} χ^{μ}$ is the pointwise product of class functions and the sum uses the real-valuedness of the irreducible characters, so that no conjugation appears on the third factor.

Facts & Assumptions

Given: An integer $n \geq 0$ and partitions $λ, μ, ν ⊢ n$ ; the Specht characters $χ^{λ}, χ^{μ}, χ^{ν}$ and the $S_{n}$ -module $S^{λ} \otimes_{C} S^{μ}$ .

[F1]

$g (λ, μ, ν)$ is the multiplicity of $S^{ν}$ in the completely reducible module $S^{λ} \otimes_{C} S^{μ}$ (Kronecker coefficients and the internal tensor product).

[F2]

For finite-dimensional complex representations $V, W$ of a finite group, $χ_{V \otimes W} (g) = χ_{V} (g) χ_{W} (g)$ for every $g$ (Characters add on direct sums, multiply on tensor products, and conjugate on duals).

[F3]

If $V$ is a finite-dimensional complex representation of a finite group $G$ with irreducible decomposition $V ≅ ⨁_{j} m_{j} V_{j}$ and characters $χ_{j}$ , then $m_{j} = ⟨ χ_{V}, χ_{j} ⟩_{G}$ (The multiplicity of an irreducible summand is a character inner product).

[F4]

The standard inner product of class functions on $S_{n}$ is $⟨ φ, ψ ⟩ = \frac{1}{n!} \sum_{σ \in S_{n}} φ (σ) \overline{ψ (σ)}$ (The standard inner product on $c f (G)$ ).

[F5]

Every Specht character is real-valued: $χ^{ν} (σ) = \overline{χ^{ν} (σ)}$ for every $σ \in S_{n}$ (Complex Specht modules are self-dual with real-valued characters).

Proof

technique · direct

1.1F2given

For every $σ \in S_{n}$ the tensor-product character is $χ_{S^{λ} \otimes_{C} S^{μ}} (σ) = χ^{λ} (σ) χ^{μ} (σ)$ by [F2], so the character of $S^{λ} \otimes_{C} S^{μ}$ is the pointwise product $χ^{λ} χ^{μ}$ .

2.1F1F3step 1.1

By [F1] the module $S^{λ} \otimes_{C} S^{μ}$ is completely reducible with irreducible decomposition $⨁_{ν ⊢ n} g (λ, μ, ν) S^{ν}$ ; applying [F3] to this decomposition and using step 1.1 gives $g (λ, μ, ν) = ⟨ χ^{λ} χ^{μ}, χ^{ν} ⟩$ .

3.1F4F5step 2.1algebra∎

By definition [F4] the inner product is $⟨ χ^{λ} χ^{μ}, χ^{ν} ⟩ = \frac{1}{n!} \sum_{σ \in S_{n}} χ^{λ} (σ) χ^{μ} (σ) \overline{χ^{ν} (σ)}$ ; by real-valuedness [F5] the factor $\overline{χ^{ν} (σ)}$ equals $χ^{ν} (σ)$ , so the average of the plain triple product is displayed. Combining with step 2.1 gives $g (λ, μ, ν) = \frac{1}{n!} \sum_{σ \in S_{n}} χ^{λ} (σ) χ^{μ} (σ) χ^{ν} (σ)$ .

No form of the Axiom of Choice is used: this is finite-dimensional complex character theory of a finite group.

Depends on

Used by

Dependency tree · two levels

29 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

Igor Pak and Greta Panova, Bounds on the Kronecker coefficients, arXiv:1406.2988v2 (2014) (standard reference, not scraped)
I. G. Macdonald, Symmetric Functions and Hall Polynomials, 2nd ed., Oxford University Press 1995 (standard reference, not scraped)