Alphabeta Math
LemmaStatement: Literature-sourcedProof: Literature-sourcedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05
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.

A positive integer multiple of the trivial character is an integral combination of cyclic permutation characters

Statement

Let G be a finite group. Then there is an integral linear combination of characters induced from trivial characters of cyclic subgroups whose value is G1G. Equivalently,

G1G=iaiIndCiG1Ci

for cyclic subgroups CiG and integers ai.

Facts & Assumptions

Given: A finite group G and an element gG.

[F1]

For every finite cyclic subgroup CG, the generator-indicator class function ηC on C is an integral linear combination of characters IndDC1D with DC cyclic (The generator-indicator class function of a cyclic group is obtained by Mobius inversion).

[F2]

Frobenius' formula computes induced character values (Frobenius' formula for the character of an induced representation).

[F3]

Induction is transitive along subgroup chains (Induction is transitive along subgroup chains).

Proof

technique · direct
1.1

For each cyclic subgroup CG, let ηC be the class function from [F1], and define f:=CGC cyclicIndCGηC. The sum is finite because a finite group has only finitely many subgroups.

F1givenconstruct
2.1

By [F2], for each cyclic CG one has IndCGηC(g)=1CxGx1gxCηC(x1gx). Fix xG. Among all cyclic subgroups CG, exactly one of them can make the summand indexed by x nonzero, namely C=x1gx; for that subgroup, the value of ηC is C. Therefore the double sum defining f(g) contributes exactly 1 for each xG, so f(g)=G.

F2step 1.1givenalgebra
3.1

Step 2.1 holds for every gG, hence f=G1G as class functions. Expanding each ηC by [F1] and then using [F3] to replace IndCG(IndDC1D) by IndDG1D expresses f as an integral linear combination of characters IndDG1D with D cyclic. Thus G1G has the required form.

F1F3step 1.1step 2.1algebra

Depends on

Used by

Dependency tree · two levels

10 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