CorollaryStatement: 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.

Irreducible symmetric-group character values are power-sum coefficients

Statement

For all $λ, ρ ⊢ n$ ,

$χ^{λ} (ρ) = ⟨ s_{λ}, p_{ρ} ⟩_{H},$

the coefficient of $p_{ρ} / z_{ρ}$ in the power-sum expansion of $s_{λ}$ . Equivalently,

$s_{λ} = \sum_{ρ ⊢ n} χ^{λ} (ρ) \frac{p_{ρ}}{z_{ρ}} .$

Facts & Assumptions

Given: An integer $n \geq 0$ and partitions $λ, ρ ⊢ n$ .

[F1]

$ch (χ^{λ}) = s_{λ}$ in $Λ^{n}$ , where $χ^{λ}$ is the character of the Specht module $S^{λ}$ and all its values are integers (The characteristic of a Specht character is a Schur function).

[F2]

$ch (f) = \sum_{σ ⊢ n} f (σ) p_{σ} / z_{σ}$ for $f \in c f (S_{n})$ , where $z_{σ} = \prod_{i} i^{m_{i} (σ)} m_{i} (σ)! > 0$ (The Frobenius characteristic map).

[F3]

The Hall form is the $Z$ -bilinear form with $⟨ h_{α}, m_{β} ⟩_{H} = δ_{α β}$ and $Q$ -bilinear extension to $Λ_{Q}$ , and $⟨ p_{σ}, p_{ρ} ⟩_{H} = δ_{σ ρ} z_{ρ}$ (The Hall inner product on symmetric functions, Power sums are orthogonal for the Hall form).

Proof

technique · direct

1.1F1F2

By [F1] and the definition of the characteristic [F2], $s_{λ} = ch (χ^{λ}) = \sum_{σ ⊢ n} χ^{λ} (σ) p_{σ} / z_{σ}$ in $Λ_{Q}^{n}$ .

2.1F3step 1.1algebra

Pairing both sides of step 1.1 with $p_{ρ}$ and using $Q$ -bilinearity of the Hall form and the orthogonality $⟨ p_{σ}, p_{ρ} ⟩_{H} = δ_{σ ρ} z_{ρ}$ of [F3], $⟨ s_{λ}, p_{ρ} ⟩_{H} = \sum_{σ ⊢ n} \frac{χ^{λ} (σ)}{z_{σ}} ⟨ p_{σ}, p_{ρ} ⟩_{H} = \frac{χ^{λ} (ρ)}{z_{ρ}} z_{ρ} = χ^{λ} (ρ)$ .

3.1step 1.1step 2.1∎

Step 2.1 is the first displayed identity; step 1.1 exhibits $χ^{λ} (ρ)$ as the coefficient of $p_{ρ} / z_{ρ}$ in the expansion of $s_{λ}$ in the basis ${p_{σ} / z_{σ} : σ ⊢ n}$ of $Λ_{Q}^{n}$ , which is the equivalent second display.

Depends on

Used by

Dependency tree · two levels

27 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

I. G. Macdonald, Symmetric Functions and Hall Polynomials, 2nd ed., Chapter I §7 (standard reference, not scraped)