ExampleConstruction: Literature-sourcedVerification: 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.

Boundary behavior can agree or differ for Dirichlet-series abscissae

Example

The ordinary zeta series $\sum_{n \geq 1} n^{- s}$ has

$σ_{c} = σ_{a} = 1,$

while the alternating eta series

$\sum_{n \geq 1} (- 1)^{n - 1} n^{- s}$

has $σ_{c} = 0$ and $σ_{a} = 1$ .

Facts & Assumptions

Given: The two displayed Dirichlet series.

[L1]

The abscissae $σ_{c}$ and $σ_{a}$ are defined by half-plane convergence and absolute convergence (The convergence and absolute-convergence abscissae of a Dirichlet series).

[L2]

Convergence at one point forces convergence on the open half-plane to its right (Convergence at one point of a Dirichlet series forces local uniform convergence on the open half-plane to its right).

[L3]

Absolute convergence at one point forces absolute convergence on every closed half-plane to its right (Absolute convergence at one point forces absolute and locally uniform convergence on closed half-planes to the right).

[L4]

Abel summation for complex series rewrites tails through bounded partial sums (Abel summation by parts for complex coefficients and their partial sums).

[L5]

For rational $q > 1$ , the series $\sum_{n \geq 1} n^{- q}$ converges, while the $p = 1$ case, the harmonic series, diverges (For rational $p > 0$ , $\sum 1 / k^{p}$ converges iff $p > 1$ ).

[L6]

A series whose terms do not tend to $0$ diverges (If a series converges then its terms tend to $0$ ).

Verification

technique · direct

1.1

For the zeta series, fix $s$ with $ℜ s > 1$ and choose a rational $q$ with $1 < q < ℜ s$ . Then $∣ n^{- s} ∣ = n^{- ℜ s} \leq n^{- q}$ , so [L5] gives absolute convergence. At $s = 1$ the same series is the harmonic series and diverges by [L5]. Therefore [L1], [L2], and [L3] force both abscissae to equal $1$ : convergence at any point with real part $< 1$ would imply convergence at $1$ , and absolute convergence at any point with real part $< 1$ would imply absolute convergence at $1$ .

L1L2L3L5givenchoosealgebra

2.1

For the eta series, fix $s$ with $σ : = ℜ s > 0$ . The partial sums of $\sum (- 1)^{n - 1}$ are bounded by $1$ . Applying [L4] to the tail weights $b_{n} = n^{- s}$ gives $\sum_{n = M}^{N} (- 1)^{n - 1} n^{- s} = A_{N} N^{- s} - A_{M - 1} M^{- s} + \sum_{n = M}^{N - 1} A_{n} (n^{- s} - (n + 1)^{- s}),$ with $∣ A_{n} ∣ \leq 1$ . Since $n^{- s} - (n + 1)^{- s} = O_{s} (n^{- σ - 1})$ and $N^{- s} \to 0$ , the right-hand side tends to $0$ as $M, N \to \infty$ , so the eta series converges for every $ℜ s > 0$ . Its absolute series is $\sum n^{- ℜ s}$ , so step 1.1 shows $σ_{a} = 1$ . At $s = 0$ the terms are $(- 1)^{n - 1}$ , which do not tend to $0$ , so [L6] gives divergence. Therefore [L1] and [L2] force $σ_{c} = 0$ .

step 1.1L1L2L4L6givenalgebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

29 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

Leonard Tomczak, Analytic Number Theory, Chapter 3 (standard reference, not scraped)