ExampleConstruction: Literature-sourcedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-28

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 standard $2$ -dimensional representation of $S_{3}$ inside the permutation representation on $C^{3}$ is irreducible

Example

Let $S_{3}$ act on $C^{3}$ by permuting the standard basis vectors $e_{1}, e_{2}, e_{3}$ . The line $L : = C (1, 1, 1)$ is invariant, and its invariant complement $U : = {(x, y, z) \in C^{3} : x + y + z = 0}$ is the standard $2$ -dimensional representation. This representation is irreducible.

Facts & Assumptions

Given: The permutation representation of $S_{3}$ on $C^{3}$ .

[L1]

A permutation action on a finite set gives a permutation representation on the free vector space with that basis (The trivial representation, the regular representation, and permutation representations from finite $G$ -sets).

[L2]

A representation is irreducible exactly when it has no proper nonzero subrepresentation (Subrepresentations, direct sums of representations, and irreducibility).

Verification

technique · direct

1.1

By [L1], the action of $S_{3}$ on ${e_{1}, e_{2}, e_{3}}$ extends to $C^{3}$ by permuting coordinates. The vector $(1, 1, 1)$ is fixed by every permutation, so $L$ is invariant. The coordinate sum $x + y + z$ is also permutation-invariant, so $U$ is invariant and $C^{3} = L \oplus U$ .

L1given

2.1

Suppose $W \subseteq U$ is a nonzero invariant line, and choose $0 \neq v = (a, b, c) \in W$ . Because $W$ is invariant under the transposition $τ = (12)$ , one has $τ (v) = λ v$ for some scalar $λ$ , and $τ^{2} = 1$ forces $λ = \pm 1$ . If $λ = 1$ , then $a = b$ and the relation $a + b + c = 0$ gives $v = a (1, 1, - 2)$ . If $λ = - 1$ , then $a = - b$ and $c = 0$ , so $v = a (1, - 1, 0)$ .

step 1.1L2givenalgebra

3.1

The $3$ -cycle $σ = (123)$ sends $(1, 1, - 2)$ to $(1, - 2, 1)$ and $(1, - 1, 0)$ to $(0, 1, - 1)$ , and neither image is a scalar multiple of the original vector. Thus neither of the two possibilities from step 2.1 can span an invariant line. So $U$ has no proper nonzero invariant line, and by [L2] it is irreducible.

step 2.1L2givenalgebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

8 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

Peter Webb, A Course in Finite Group Representation Theory, Example 1.1.3 (standard reference, not scraped)
Pavel Etingof et al., Introduction to Representation Theory, Section 3.3 (standard reference, not scraped)

The standard 22-dimensional representation of S3S3​ inside the permutation representation on C3C3 is irreducible