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.

A real nonprincipal Dirichlet L-function is nonzero at one

Statement

If χ is a real nonprincipal Dirichlet character, then L(1,χ)0.

Facts & Assumptions

Given: A real nonprincipal Dirichlet character χ modulo q.

[L1]

The principal factor is L(s,χ0)=ζ(s)pq(1ps); the continuation of ζ is holomorphic away from its simple pole at 1 (The principal Dirichlet L-function factors through zeta, The Riemann zeta function extends meromorphically to the complex plane with its only pole at 1).

[L2]

On unit classes, a real Dirichlet character takes values in {±1}, and on nonunits it is 0 (Character values on units are roots of unity).

[L3]

Every Dirichlet L-function has its Euler product on Res>1 (Euler product for Dirichlet L-functions).

[L4]

The nonprincipal factor L(s,χ) is holomorphic on Res>0 (Nonprincipal Dirichlet L-functions are holomorphic on Re s greater than 0).

[L5]

A Dirichlet series with nonnegative coefficients and finite abscissa of convergence is singular at its abscissa of convergence (Landau's theorem for Dirichlet series with nonnegative coefficients).

Proof

technique · contradiction
1.1

Suppose L(1,χ)=0, and set G(s):=L(s,χ0)L(s,χ). For Res>1, facts [L2] and [L3] give G(s)=χ(p)=1(1ps)2χ(p)=1(1p2s)1, because primes dividing q contribute the trivial local factor 1. Expanding the geometric series shows that G(s)=n1anns with an0 for every n. Moreover, if (m,q)=1, then the square coefficient am2 is positive: each local factor above has a positive coefficient at every even exponent occurring in m2.

L2L3givenassume-contraalgebra
2.1

Step 1.1 implies n1ann1/2m1(m,q)=1am2mm1(m,q)=11m=, so the abscissa of convergence σc of anns satisfies σc1/2. On the other hand, [L1] and [L4] show that G is holomorphic on the whole half-plane Res>0: the only possible singularity there is the simple pole of L(s,χ0) at 1, and the assumption of step 1.1 cancels it. Since G is represented by a Dirichlet series with nonnegative coefficients, [L5] forbids any positive abscissa of convergence. Thus σc0, contradicting σc1/2. Therefore L(1,χ)0.

L1L4L5step 1.1discharge-contradiction

Depends on

Used by

Dependency tree · two levels

24 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