Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedverified 2026-09-26 (gpt-6-sol)
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 smoothed von Mangoldt explicit formula

Statement

Assume countable choice.

For 1<x<y and u≥0, let ϕx,y(u)=1 for u≤x, (y−u)/(y−x) for x<u<y, and 0 for u≥y. For ℜs>0 put ϕ~(s)=∫0∞ϕ(u)us−1du, and use the same symbol for its meromorphic continuation. Then ∑n≥1Λ(n)ϕx,y(n)=ϕ~(1)−∑ρϕ~(ρ)−log⁡(2π)−∑k≥1ϕ~(−2k). Both infinite sums on the right converge absolutely; zeros are counted with multiplicity. In particular, symmetric ordinate truncations give the same zero sum.

Facts & Assumptions

[L1]

For T≥0, the number of nontrivial zeros with ordinates in [T,T+1] is O(log⁡(T+2)) (A unit-interval bound for zeta zeros).

Proof

Given: Countable choice, 1<x<y, and the displayed piecewise-linear cutoff.

1.1givenalgebra

Write Φ=ϕ~. Integration by parts gives Φ(s)=ys+1−xs+1(y−x)s(s+1). Its only pole is 0, with residue 1; the apparent singularity at −1 is removable, with value −log⁡(y/x)/(y−x). On each fixed vertical strip it is Ox,y(∣ℑs∣−2) at large height, with the constant also depending on the strip.

1.2givenalgebra

We compute the constant at zero. Put γ=lim⁡N(HN−log⁡N) as in The Euler–Mascheroni constant and the harmonic asymptotic. The fractional-part formula in For Re⁡s>0, zeta admits the fractional-part integral formula with a simple residue-one pole at 1 and ∫1N{u}u2 du=log⁡N−HN+1 give ζ(1−s)=−1/s+γ+O(s). Logarithmic differentiation of the locally uniform product in The Weierstrass product for reciprocal Gamma at 1 gives −Γ′(1)Γ(1)=1+γ+∑n≥1(1n+1−1n)=γ. The same product at 1 gives Γ(1)=1, so Γ(1−s)=1+γs+O(s2). Finally The Riemann zeta function satisfies the classical sine-gamma functional equation and 2sπs−1sin⁡(πs/2)=s2(1+slog⁡(2π)+O(s2)) yield ζ(s)=−1/2−slog⁡(2π)/2+O(s2): the two Euler constants cancel. Thus ζ′(0)/ζ(0)=log⁡(2π).

2.1step 1.1algebra

To justify inversion explicitly, let J(z)=12πi∫ℜs=2zss(s+1) ds(z>0). Closing a rectangle to the left for z>1, and to the right for z<1, gives J(z)=1−z−1 and J(z)=0, respectively, by The residue theorem for a null-homologous cycle. Indeed, first let the height tend to infinity with the other vertical side fixed: the horizontal integrals are O(T−2) times a fixed width. Then let that side tend to the appropriate infinity through half-integers; its integral is O(zσ/∣σ∣) and vanishes. At z=1, continuity of the absolutely convergent initial integral gives J(1)=0. Consequently [yJ(y/u)−xJ(x/u)]/(y−x)=ϕ(u) for every u>0, including u=x,y. Combining this with step 1.1 and The logarithmic derivative of the zeta Dirichlet series is the Dirichlet series of the von Mangoldt function on Re s greater than 1 gives ∑nΛ(n)ϕ(n)=12πi∫ℜs=2−ζ′ζ(s)Φ(s) ds. The exchange of sum and integral is absolute, since ∑nΛ(n)n−2≤∑n≥2(log⁡n)n−2<∞ and Φ(2+it)=Ox,y((1+∣t∣)−2).

2.2L1L2step 1.1algebra

By [L1], [L2], and 0<ℜρ<1, step 1.1 gives absolute convergence of the zero sum: its bands at large ∣ℑρ∣≍j contribute Ox,y(log⁡(j+2)/j2). The trivial-zero sum converges absolutely since ∣Φ(−2k)∣≤Cx,yx1−2k/k2. We also choose admissible heights explicitly. Let Mj count zeros with ordinates in [j−1,j+2], with multiplicity. It is O(log⁡(j+2)). Among the 2Mj+2 equally spaced points of [j,j+1], each such ordinate excludes at most one point at distance less than 1/(4Mj+4). Choose the least remaining point Tj. Ordinates outside that larger interval are at distance at least 1, so every zero ordinate is at distance at least 1/(4Mj+4) from Tj. Conjugation gives the same separation at −Tj.

3.1step 1.2step 2.1step 2.2algebra

Fix an odd integer R≥3 and shift the integral of step 2.1 to ℜs=−R, using heights ±Tj from step 2.2. On −1≤ℜs≤2, A local formula for the logarithmic derivative of zeta bounds ζ′/ζ by O(log⁡2Tj): there are O(log⁡Tj) nearby zeros, each reciprocal is O(log⁡Tj), and the pole term is bounded. On −R≤ℜs≤−1, A left-half-plane bound for the logarithmic derivative of zeta gives OR(log⁡Tj). Thus each horizontal integral is OR,x,y(log⁡2Tj/Tj2) and tends to zero. By Residues in the von Mangoldt contour shift, −ζ′/ζ has residues 1 at 1, −m at a zero of multiplicity m, and −1 at each trivial zero. Multiplication by Φ therefore gives residues Φ(1), −mΦ(ρ), −Φ(−2k), and, by step 1.2, −log⁡(2π) at 0. There is no pole at −1. The residue theorem and absolute convergence in step 2.2 now express the initial integral as these residues for −2k>−R, the full nontrivial-zero sum, and the upward integral on ℜs=−R.

4.1step 1.1step 2.2step 3.1algebra∎

On that last line, the distance to every trivial zero is at least 1. Step 1.1 gives ∣Φ(−R+it)∣≤Cx,yx1−RR2+t2. The left-half-plane bound therefore makes its integral at most Cx,yx1−R∫Rlog⁡(R+∣t∣+2)R2+t2 dt≤Cx,y′x1−Rlog⁡(R+2)R⟶0. Letting odd R tend to infinity in step 3.1, using x>1 and the absolute convergence from step 2.2, proves the formula for every stated pair 1<x<y.

Depends on

Used by

Dependency tree · two levels

50 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