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 and . Then the set of primes has relative Dirichlet density among the primes:
Facts & Assumptions
Given: A modulus and a reduced residue class modulo .
Character orthogonality isolates the class modulo (Orthogonality relations for Dirichlet characters modulo q).
For , by the Euler product (Euler product for Dirichlet L-functions).
The principal factor is . Every nonprincipal is holomorphic near and satisfies (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
Average the logarithms with the conjugate weights of the class : . By [L1], the inner character sum is exactly when and otherwise, so the left-hand side equals . The terms with form a bounded tail as because , and therefore .
For nonprincipal , [L3] makes as . For the principal character, [L3] gives , and . Hence the average on the left side of step 1.1 is . Comparing with step 1.1 yields the claimed asymptotic, which is exactly the Dirichlet density statement in Natural and Dirichlet density.
Depends on
- Natural and Dirichlet density
- Orthogonality relations for Dirichlet characters modulo q
- Euler product for Dirichlet L-functions
- 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
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
- Kiran S. Kedlaya, Notes on Analytic Number Theory, Theorem 4.11 (standard reference, not scraped)
- Andrew V. Sutherland, Number Theory I, Lecture 18 (standard reference, not scraped)