Alphabeta Math
TheoremStatement: Literature-sourcedProof: Literature-sourcedSession-authored (Fable 5 assisted)audited 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 cycle index of the cyclic group C_n

Statement

Let Cn act on the vertices of a labelled n-gon by rotation, with n1. Then

Z(Cn)=1ndnφ(d)sdn/d.

Facts & Assumptions

Given: an integer n1 and the rotation action of Cn on the vertices of a labelled n-gon.

[A1]

A rotation by r steps sends each vertex i to i+r(modn).

[L1]

Proof

technique · direct
1.1

A rotation by r steps decomposes the n vertices into gcd(n,r) cycles, each of length n/gcd(n,r). Therefore its cycle-index monomial is sn/gcd(n,r)gcd(n,r).

A1algebra
2.1

Fix a divisor d of n. A rotation contributes the monomial sdn/d exactly when its cycles have length d, equivalently when its step size has the form r=(n/d)a with a coprime to d. Indeed, the order of the rotation by r is the least positive m with mr0(modn), and for r=(n/d)a this least m is exactly d when gcd(a,d)=1. Therefore the rotations of order d are in bijection with the units a(Z/d)×, so there are φ(d) of them by [L1].

step 1.1L1algebra
3.1

Average the monomials over all n rotations. Grouping them by the divisor d from step 2.1 yields Z(Cn)=1ndnφ(d)sdn/d.

step 2.1

Depends on

Used by

Dependency tree · two levels

13 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