Alphabeta Math
TheoremStatement: Literature-sourcedProof: 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.

If σ∈Sn has ck cycles of length k, then ∣CSn(σ)∣=∏k=1nkckck!

Statement

If σ∈Sn has ck cycles of length k, including fixed points when k=1, then ∣CSn(σ)∣=∏k=1nkckck!. The formula uses the empty product 1 when n=0.

Facts & Assumptions

Given: A permutation σ∈Sn of cycle type (c1,…,cn).

[F1]

The centralizer consists of the permutations commuting with σ (The conjugacy class Cl⁡G(x) and centralizer CG(x) of an element).

[F2]

Every permutation has a disjoint-cycle decomposition unique up to reordering and cyclic rotation, and its cycle type counts the orbits of each length, including fixed points as 1-cycles (Every permutation of a finite set is a product of pairwise disjoint cycles, uniquely up to reordering and cyclic rotation, Support, fixed points, disjoint cycles, cycle length, disjoint-cycle decompositions, and cycle type).

[F4]

The cardinality of a finite product of finite choice sets is the product of their cardinalities, with the empty product having cardinality 1 (The product rule: ∣A×B∣=∣A∣ ∣B∣, and ∣∏i<mAi∣=∏i<m∣Ai∣).

Proof

technique · counting
1.1

If gσ=σg and O is a ⟨σ⟩-orbit, then g(O) is another orbit of the same size.

F1F2algebra
2.1

For the ck orbits of size k, g may permute those orbits in ck! ways by [F3]. Once a target orbit is chosen, the image of one marked point has k choices, and commutation forces all other images; hence there are kckck! choices at length k.

F1F2F3step 1.1
3.1

Conversely, arbitrary orbit permutations and cyclic offsets from step 2.1 assemble on the disjoint orbits to a unique bijection g, and the forced-image rule makes gσ=σg.

F2step 2.1algebra
4.1

Choices for distinct lengths are independent, so [F4] and steps 2.1--3.1 give the displayed product. If ck=0 its factor is k00!=1; for the identity the result is n!, and for n=0 it is the empty product 1.

F3F4step 2.1step 3.1∎

Depends on

Used by

Dependency tree · two levels

27 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