Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: Literature-sourcedprecheck 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 S4 and the class equation 24=1+6+3+8+6

Example

The conjugacy data for S4 are

cycle typerepresentativecentralizer sizeclass sizeparity
141241even
2,12(12)46odd
22(12)(34)83even
3,1(123)38even
4(1234)46odd

Facts & Assumptions

Given: The symmetric group S4.

[F2]

Sn-classes are indexed by the tuples with ∑kck=n (The conjugacy classes of Sn are indexed by the tuples (c1,…,cn) with ∑kck=n), and n!=∑n!/∏kkckck! over those tuples, the summand indexed by (ck) being the size of the corresponding class (The class equation of Sn is n!=∑∑kck=nn!/∏kkckck!).

[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 · two levels

15 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