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

Orthogonality relations for Dirichlet characters modulo q

Statement

Let G=(Z/qZ)×, and let the sum range over all Dirichlet characters modulo q.

  1. For unit classes a,bG, χmodqχ(a)χ(b)={φ(q),a=b,0,ab.
  2. For Dirichlet characters χ,ψ modulo q, aGχ(a)ψ(a)={φ(q),χ=ψ,0,χψ.

Facts & Assumptions

Given: The finite abelian group G=(Z/qZ)×.

[L1]

Dirichlet characters modulo q are exactly the one-dimensional complex characters of G (Dirichlet characters modulo q, Every irreducible representation of a finite abelian group over a splitting field is one-dimensional).

[L2]

Irreducible complex characters satisfy χ,ψ=δχψ (The first orthogonality relation for irreducible complex characters).

[L3]

For a finite group, the column orthogonality sum is iχi(g)χi(h)=CG(g) when g,h are conjugate and 0 otherwise (The second orthogonality relation for irreducible complex characters).

[L4]

The sum of the squares of the irreducible character degrees is G (The regular character gives a second proof of the sum-of-squares formula).

Proof

technique · direct
1.1

By [L1], every irreducible complex character of G has degree 1, and then [L4] shows that their number is G=φ(q) because G=i12. Thus the irreducible complex characters of G are exactly the Dirichlet characters modulo q. Since G is abelian, every conjugacy class is a singleton and every centralizer is all of G.

L1L4givenalgebra
2.1

Applying [L2] to the character group of G gives 1GaGχ(a)ψ(a)=δχψ, which is exactly the second displayed formula because G=φ(q). Applying [L3] to the same irreducible character list and using step 1.1 turns the centralizer size into G=φ(q) and conjugacy into literal equality of elements, which yields the first displayed formula.

L2L3step 1.1algebra

Depends on

Used by

Dependency tree · two levels

19 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