Alphabeta Math
CorollaryStatement: Literature-sourcedProof: Literature-sourcedaudited 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 symmetric-group cycle-index series is coefficientwise exponential

Statement

In the formal power-series ring Q[s1,s2,… ]⟦t⟧,

∑n≥0Z(Sn)tn=exp⁡(∑d≥1sdtdd).

For each fixed n, the coefficient of tn depends only on s1,…,sn.

Facts & Assumptions

Given: the formal exponential and the symmetric-group cycle indices.

[L1]

The coefficient of tn in the cycle-index series of the family with one fixed structure in each degree is Z(Sn) (The cycle-index series of a graded family of S_n-actions, The cycle index of S_n is the sum over cycle types).

[L2]

Formal exponential turns finite sums into products, so for each finite truncation one may expand exp⁡ ⁣(∑d=1Nsdtd/d) as ∏d=1Nexp⁡(sdtd/d) (Formal exp⁡ and log⁡ are inverse homomorphisms and formal binomial powers obey the expected addition laws).

Proof

technique · coefficient comparison
1.1L2

Fix n≥0. Factors with d>n cannot contribute to the coefficient of tn, so that coefficient is already the coefficient of tn in the finite truncation exp⁡(∑d=1nsdtdd). By [L2], this truncation equals ∏d=1nexp⁡(sdtdd)=∏d=1n∑md≥0sdmdtdmddmdmd!.

2.1step 1.1

Expanding the finite product in step 1.1, the coefficient of tn is ∑m1,…,mn≥0∑d=1ndmd=n1∏d=1ndmdmd!∏d=1nsdmd. This depends only on s1,…,sn.

3.1step 2.1L1∎

The coefficient in step 2.1 is exactly the cycle-type formula for Z(Sn) from [L1]. Since this holds for every n, the whole series satisfies ∑n≥0Z(Sn)tn=exp⁡(∑d≥1sdtdd).

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

18 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