ExampleConstruction: AI-adaptedVerification: 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.

Sign twist conjugates the $(3, 1)$ character of $S_{4}$

Example

In $S_{4}$ , the character $χ^{(3, 1)}$ has values $(3, 1, - 1, 0, - 1)$ on the cycle types $(1^{4}), (2, 1, 1), (2, 2), (3, 1), (4)$ , and multiplication by the sign character, $sgn (ρ) = (- 1)^{4 - ℓ (ρ)}$ , gives $(3, - 1, - 1, 0, 1)$ , which are the values of $χ^{(2, 1, 1)}$ . Thus $S^{(3, 1)} \otimes sgn ≅ S^{(2, 1, 1)}$ , in agreement with $ω (s_{(3, 1)}) = s_{(2, 1, 1)}$ .

Facts & Assumptions

Given: The partitions $(3, 1)$ and $(2, 1, 1) = (3, 1)^{'}$ of $4$ and the cycle types $(1^{4}), (2, 1, 1), (2, 2), (3, 1), (4)$ of $S_{4}$ .

[F1]

Jacobi–Trudi and dual Jacobi–Trudi give $s_{(3, 1)} = h_{3} h_{1} - h_{4}$ and $s_{(2, 1, 1)} = e_{3} e_{1} - e_{4}$ (Jacobi–Trudi and dual Jacobi–Trudi identities).

[F2]

$h_{4} = \sum_{ρ ⊢ 4} p_{ρ} / z_{ρ} = \frac{p_{1}^{4} + 6 p_{1}^{2} p_{2} + 8 p_{1} p_{3} + 3 p_{2}^{2} + 6 p_{4}}{24}$ , since $z_{(1^{4})} = 24$ , $z_{(2, 1, 1)} = 4$ , $z_{(2, 2)} = 8$ , $z_{(3, 1)} = 3$ , $z_{(4)} = 4$ (Complete homogeneous functions expand in power sums with cycle-distribution coefficients).

[F3]

The involution $ω$ satisfies $ω (h_{r}) = e_{r}$ and $ω (p_{r}) = (- 1)^{r - 1} p_{r}$ , and $ω (s_{λ}) = s_{λ^{'}}$ ; consequently $e_{4} = ω (h_{4}) = \frac{p_{1}^{4} - 6 p_{1}^{2} p_{2} + 8 p_{1} p_{3} + 3 p_{2}^{2} - 6 p_{4}}{24}$ and $ω (s_{(3, 1)}) = s_{(2, 1, 1)}$ (The omega involution conjugates Schur functions).

[F4]

$ch (χ^{λ}) = s_{λ}$ and $χ^{λ} (ρ)$ is the coefficient of $p_{ρ} / z_{ρ}$ in the power-sum expansion of $s_{λ}$ (The characteristic of a Specht character is a Schur function, Irreducible symmetric-group character values are power-sum coefficients).

[F5]

For $w \in S_{n}$ of cycle type $ρ$ , the sign is $sgn (w) = (- 1)^{n - ℓ (ρ)}$ , and the tensor-product character satisfies $χ_{V \otimes sgn} (w) = χ_{V} (w) sgn (w)$ ; moreover $S^{λ} \otimes sgn ≅ S^{λ^{'}}$ and $χ^{λ^{'}} (w) = (- 1)^{n - ℓ (ρ)} χ^{λ} (w)$ (A $k$ -cycle has sign $(- 1)^{k - 1}$ , and $sgn (σ) = (- 1)^{n - c (σ)}$ when fixed points are counted as cycles, Sign twist corresponds to the omega involution).

Verification

technique · direct

1.1F2F3given

The cycle types of $S_{4}$ together with their centralizer orders are $(1^{4}) ⁣ : 24$ , $(2, 1, 1) ⁣ : 4$ , $(2, 2) ⁣ : 8$ , $(3, 1) ⁣ : 3$ and $(4) ⁣ : 4$ ; hence by [F2] and [F3], $h_{4} = \frac{p_{1}^{4} + 6 p_{1}^{2} p_{2} + 8 p_{1} p_{3} + 3 p_{2}^{2} + 6 p_{4}}{24}$ and $e_{4} = \frac{p_{1}^{4} - 6 p_{1}^{2} p_{2} + 8 p_{1} p_{3} + 3 p_{2}^{2} - 6 p_{4}}{24}$ .

1.2F1F3

With $h_{1} = p_{1}$ and $h_{3} = \frac{p_{1}^{3} + 3 p_{1} p_{2} + 2 p_{3}}{6}$ and $e_{3} = ω (h_{3}) = \frac{p_{1}^{3} - 3 p_{1} p_{2} + 2 p_{3}}{6}$ , [F1] gives $s_{(3, 1)} = h_{3} h_{1} - h_{4}$ and $s_{(2, 1, 1)} = e_{3} e_{1} - e_{4}$ .

2.1F3step 1.1step 1.2algebra

Substituting step 1.1 into step 1.2: $s_{(3, 1)} = \frac{p_{1}^{4} + 3 p_{1}^{2} p_{2} + 2 p_{1} p_{3}}{6} - \frac{p_{1}^{4} + 6 p_{1}^{2} p_{2} + 8 p_{1} p_{3} + 3 p_{2}^{2} + 6 p_{4}}{24} = \frac{p_{1}^{4} + 2 p_{1}^{2} p_{2} - p_{2}^{2} - 2 p_{4}}{8}$ , and $s_{(2, 1, 1)} = \frac{p_{1}^{4} - 3 p_{1}^{2} p_{2} + 2 p_{1} p_{3}}{6} - \frac{p_{1}^{4} - 6 p_{1}^{2} p_{2} + 8 p_{1} p_{3} + 3 p_{2}^{2} - 6 p_{4}}{24} = \frac{p_{1}^{4} - 2 p_{1}^{2} p_{2} - p_{2}^{2} + 2 p_{4}}{8}$ .

3.1F4step 2.1algebra

By [F4] the values $χ^{λ} (ρ)$ are the coefficients of $p_{ρ} / z_{ρ}$ in step 2.1; with the centralizer orders of step 1.1 this gives $χ^{(3, 1)} = (3, 1, - 1, 0, - 1)$ and $χ^{(2, 1, 1)} = (3, - 1, - 1, 0, 1)$ on the cycle types $(1^{4}), (2, 1, 1), (2, 2), (3, 1), (4)$ .

4.1F3F5step 3.1algebra∎

Multiplying pointwise by the sign values $sgn (ρ) = (- 1)^{4 - ℓ (ρ)}$ , namely $(+ 1, - 1, + 1, + 1, - 1)$ , turns the values of step 3.1 into $(3 \cdot 1, 1 \cdot (- 1), (- 1) \cdot 1, 0 \cdot 1, (- 1) \cdot (- 1)) = (3, - 1, - 1, 0, 1)$ , which are exactly the values of $χ^{(2, 1, 1)}$ ; this agrees with the module isomorphism $S^{(3, 1)} \otimes sgn ≅ S^{(2, 1, 1)}$ and with $ω (s_{(3, 1)}) = s_{(2, 1, 1)}$ of [F3].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

36 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)
G. D. James, The Representation Theory of the Symmetric Groups, §6 and §16 (standard reference, not scraped)

Sign twist conjugates the (3,1)(3,1) character of S4S4​