primeTailBound_of_explicit
plain-language theorem explainer
For any natural number N at least 17 and real number σ₀ with 1/2 < σ₀ ≤ 1, the tail sum over primes p > N of p^{-σ₀} is bounded above by N^{1-2σ₀} / (2σ₀ - 1). Number theorists working on explicit error estimates for the Riemann hypothesis via the Christmas route would cite this result. The proof is a short tactic sequence that applies linarith to obtain 1 < 2σ₀ and then verifies the four conditions of the PrimeTailBound predicate by non-negativity of the explicit expression.
Claim. For every natural number $N ≥ 17$ and real number $σ₀$ satisfying $1/2 < σ₀ ≤ 1$, the predicate PrimeTailBound$(N, σ₀, N^{1-2σ₀}/(2σ₀-1))$ holds, where the predicate requires $σ₀ > 1/2$, non-negative tail error, and $N ≥ 1$.
background
The module supplies explicit tail bounds on sums over primes for the error budget in the Riemann hypothesis analysis. The key definition is the PrimeTailBound predicate, which requires positive σ₀ greater than 1/2, non-negative E_tail, and N at least 1, standing in for the inequality bounding the tail sum ∑_{p > N} p^{-σ₀} ≤ E_tail. Upstream, the ErrorBudget module defines this predicate as a placeholder for the actual bound involving prime reciprocals. The local setting is the Christmas-route error budget decomposition, drawing on Rosser–Schoenfeld and Dusart estimates for prime sums.
proof idea
The proof is a tactic-mode verification that directly constructs the four components of the PrimeTailBound tuple. It first establishes 1 < 2σ₀ by linarith from the hypothesis 1/2 < σ₀. Then it refines the goal to a structure with positivity of σ₀, the lower bound on σ₀, non-negativity of the explicit E_tail via rpow_nonneg and div_nonneg, and the lower bound on N by omega.
why it matters
This theorem discharges the PrimeTailBound hypothesis in the Christmas-route error budget for the Riemann hypothesis. It provides the explicit instantiation needed for the attachment-with-margin decomposition, citing Rosser–Schoenfeld (1962) and Dusart (2010). In the broader framework it supplies the concrete number-theoretic bound required to close the error estimates in the prime tail analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.