ExampleConstruction: Literature-sourcedVerification: Literature-sourcedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13

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 five conjugacy classes of $S_{4}$ and the class equation $24 = 1 + 6 + 3 + 8 + 6$

Example

The conjugacy data for $S_{4}$ are

cycle type	representative	centralizer size	class size	parity
$1^{4}$	$1$	$24$	$1$	even
$2, 1^{2}$	$(12)$	$4$	$6$	odd
$2^{2}$	$(12) (34)$	$8$	$3$	even
$3, 1$	$(123)$	$3$	$8$	even
$4$	$(1234)$	$4$	$6$	odd

Facts & Assumptions

Given: The symmetric group $S_{4}$ .

[F1]

A cycle type $(c_{k})$ has centralizer size $\prod k^{c_{k}} c_{k}!$ (If $σ \in S_{n}$ has $c_{k}$ cycles of length $k$ , then $∣ C_{S_{n}} (σ) ∣ = \prod_{k = 1}^{n} k^{c_{k}} c_{k}!$ ).

[F2]

$S_{n}$ -classes are indexed by the tuples with $\sum k c_{k} = n$ (The conjugacy classes of $S_{n}$ are indexed by the tuples $(c_{1}, \dots, c_{n})$ with $\sum k c_{k} = n$ ), and $n! = \sum n! / \prod_{k} k^{c_{k}} c_{k}!$ over those tuples, the summand indexed by $(c_{k})$ being the size of the corresponding class (The class equation of $S_{n}$ is $n! = \sum_{\sum k c_{k} = n} n! / \prod_{k} k^{c_{k}} c_{k}!$ ).

[F3]

A $k$ -cycle has sign $(- 1)^{k - 1}$ , and $sgn (σ) = (- 1)^{n - c (σ)}$ when fixed points are included as $1$ -cycles (A $k$ -cycle has sign $(- 1)^{k - 1}$ , and $sgn (σ) = (- 1)^{n - c (σ)}$ when fixed points are counted as cycles).

Verification

technique · counting

1.1

The five partitions of $4$ give exactly the five cycle types in the table.

F2algebra

2.1

Applying [F1] gives centralizer sizes $24, 4, 8, 3, 4$ ; dividing $24$ by them gives class sizes $1, 6, 3, 8, 6$ .

F1F2step 1.1algebra

3.1

Their sum is $24 = 1 + 6 + 3 + 8 + 6$ , which verifies [F2].

F2step 2.1algebra

4.1

Applying [F3] to the representatives gives the parity column.

F3step 1.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 55 results over 11 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

K. Conrad, Conjugacy Classes (standard reference, not scraped)

The five conjugacy classes of S4S4​ and the class equation 24=1+6+3+8+624=1+6+3+8+6