Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04
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.

For Re⁡s>0, zeta admits the fractional-part integral formula with a simple residue-one pole at 1

Statement

For every complex number s with Re⁡s>0 and s≠1,

ζ(s)=ss−1−s∫1∞{x}x−s−1 dx,

where {x}=x−⌊x⌋ is the fractional part. The integral defines a holomorphic function on Re⁡s>0, so the right-hand side is meromorphic there with a single simple pole at s=1 of residue 1.

Facts & Assumptions

Given: A complex number s with Re⁡s>1.

[L1]

On Re⁡s>1, ζ(s)=∑n≥1n−s (The Riemann zeta function on the half-plane Re⁡s>1).

[L2]

For rational p>1, the series ∑n≥1n−p converges (For rational p>0, ∑1/kp converges iff p>1).

Proof

technique · direct
1.1givenL1algebra

For N≥2, s∫1N⌊x⌋x−s−1 dx=∑n=1N−1n ⁣∫nn+1sx−s−1 dx=∑n=1N−1n(n−s−(n+1)−s). Expanding the last sum gives s∫1N⌊x⌋x−s−1 dx=∑n=1N−1n−s−(N−1)N−s, and therefore ∑n=1Nn−s=N1−s+s∫1N⌊x⌋x−s−1 dx.

2.1step 1.1L1algebra

Since Re⁡s>1, the term N1−s tends to 0 as N→∞. Letting N→∞ in step 1.1 and using [L1] yields ζ(s)=s∫1∞⌊x⌋x−s−1 dx=s∫1∞(x−{x})x−s−1 dx. Also s∫1∞x−s dx=ss−1, so ζ(s)=ss−1−s∫1∞{x}x−s−1 dx on Re⁡s>1.

3.1step 2.1L2choosealgebra∎

Let K⊆{s∈C:Re⁡s>0} be compact, and choose σ>0 with Re⁡s≥σ on K. Because 0≤{x}<1, ∣{x}x−s−1∣≤x−σ−1(x≥1, s∈K). Taking σ rational with σ>0, [L2] implies ∫1∞x−σ−1 dx<∞, so the integral in step 2.1 converges absolutely and locally uniformly on Re⁡s>0. Hence it defines a holomorphic function there. Therefore the displayed formula continues meromorphically to Re⁡s>0, and the only singularity is the simple pole of s/(s−1) at 1, whose residue is 1.

Depends on

Used by

Dependency tree · two levels

16 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