Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck 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 conjugacy classes of A5: sizes 1,20,15,12,12 and the split 5-cycles

Example

The five conjugacy classes of A5 have representatives and sizes 1:1,(123):20,(12)(34):15, (12345):12,(13524):12. The last two classes are the two halves of the S5 class of 5-cycles.

Facts & Assumptions

Given: The alternating group A5.

[F1]

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); a permutation of type (ck) has centralizer cardinality ∏kkckck! (If σ∈Sn has ck cycles of length k, then ∣CSn(σ)∣=∏k=1nkckck!); 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!).

[F2]

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).

[F3]

For n≥2 and σ∈An, the Sn-class of σ splits into two An-classes of equal size exactly when all cycle lengths in its decomposition, including 1-cycles for fixed points, are odd and no two are equal (For n≥2, an Sn-class of an even permutation splits in An exactly when all cycle lengths, including 1-cycles, are odd and distinct).

Verification

technique · counting
1.1

By [F1] and [F2], the even S5 types are 15, 3,12, 22,1, and 5, with symmetric class sizes 1,20,15,24.

F1F2algebra
2.1

By [F3], the first three stay single classes, while the 5-cycle class splits into two equal classes of size 12.

F3step 1.1
3.1

Put s=(12345). The permutation q=(2 3 5 4) satisfies qsq−1=s2=(13524) and is odd by [F2]. Every other conjugator from s to s2 differs from q by an element centralizing s; such a centralizer element is determined by the image of 1 and is therefore a power of the even 5-cycle s. Thus every conjugator is odd, so s and s2 lie in the two different halves from step 2.1.

F2step 2.1algebra
4.1

The total 1+20+15+12+12=60 agrees with [F4].

F4step 1.1step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

23 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