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

Primes in one reduced residue class have Dirichlet density 1 over phi(q)

Statement

Let q1 and (a,q)=1. Then the set of primes pa(modq) has relative Dirichlet density 1/φ(q) among the primes:

pa(q)ps=1φ(q)log1s1+O(1)(s1, s>1).

Facts & Assumptions

Given: A modulus q1 and a reduced residue class a modulo q.

[L1]

Character orthogonality isolates the class a modulo q (Orthogonality relations for Dirichlet characters modulo q).

[L2]

For Res>1, logL(s,χ)=p,m1χ(p)m/(mpms) by the Euler product (Euler product for Dirichlet L-functions).

[L3]

The principal factor is L(s,χ0)=ζ(s)pq(1ps). Every nonprincipal L(s,χ) is holomorphic near 1 and satisfies L(1,χ)0 (The principal Dirichlet L-function factors through zeta, Nonprincipal Dirichlet L-functions are holomorphic on Re s greater than 0, Nonprincipal Dirichlet L-functions are nonzero at one).

Proof

technique · direct
1.1

Average the logarithms with the conjugate weights of the class a: 1φ(q)χmodqχ(a)logL(s,χ)=p,m1(mpms)11φ(q)χmodqχ(a)χ(p)m. By [L1], the inner character sum is 1 exactly when pma(modq) and 0 otherwise, so the left-hand side equals pma(q)1/(mpms). The terms with m2 form a bounded tail as s1 because p,m21/(mpm)<, and therefore 1φ(q)χχ(a)logL(s,χ)=pa(q)ps+O(1).

L1L2givenalgebra
2.1

For nonprincipal χ, [L3] makes logL(s,χ)=O(1) as s1. For the principal character, [L3] gives logL(s,χ0)=logζ(s)+O(1)=log(1/(s1))+O(1), and χ0(a)=1. Hence the average on the left side of step 1.1 is φ(q)1log(1/(s1))+O(1). Comparing with step 1.1 yields the claimed asymptotic, which is exactly the Dirichlet density statement in Natural and Dirichlet density.

L3step 1.1algebra

Depends on

Used by

Dependency tree · two levels

22 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