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

Arithmetic characterization of Dirichlet characters modulo q

Statement

A function χ:ZC comes from a Dirichlet character modulo q if and only if all of the following hold:

  1. χ is q-periodic.
  2. χ(mn)=χ(m)χ(n) for all integers m,n.
  3. χ(n)=0 exactly when (n,q)>1.
  4. χ(1)=1.

Facts & Assumptions

Given: A positive integer q and a function χ:ZC.

[L1]

Every Dirichlet character modulo q is extended by zero from a homomorphism on (Z/qZ)× (Dirichlet characters modulo q).

[L2]

That extension is representative-independent, q-periodic, and vanishes exactly on the nonunits modulo q (Extension by zero is well defined and periodic).

Proof

technique · direct
1.1

Assume first that χ comes from a Dirichlet character modulo q. Periodicity and the support condition are exactly [L2]. If (m,q)>1 or (n,q)>1, then both χ(mn) and χ(m)χ(n) are 0 by [L2]. If both are coprime to q, then [L1] gives χ(mn)=χˉ(mˉnˉ)=χˉ(mˉ)χˉ(nˉ)=χ(m)χ(n). Also χ(1)=χˉ(1ˉ)=1 because every homomorphism sends the identity to the identity.

L1L2givenalgebra
1.2

Conversely, assume properties 1-4. If (n,q)=1, define χˉ(nˉ):=χ(n). This is well defined because property 1 makes χ constant on residue classes modulo q, and property 3 shows that only unit classes receive nonzero values. For unit classes mˉ,nˉ, property 2 gives χˉ(mˉnˉ)=χ(mn)=χ(m)χ(n)=χˉ(mˉ)χˉ(nˉ), so χˉ is a homomorphism (Z/qZ)×C×; property 4 makes it unital. Extending this homomorphism by zero recovers the original χ by property 3.

givenalgebra
2.1

Step 1.1 proves necessity and step 1.2 proves sufficiency.

step 1.1step 1.2

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · one level

2 results within one dependency step 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