module module moderate

`IndisputableMonolith.NumberTheory.RiemannHypothesis.PrimeTailBounds`

This module supplies tail bounds and summability results for the sum over primes of p to the power minus alpha when alpha exceeds 1. It is cited by work on the Christmas-route error budget for the Riemann Hypothesis attachment. The argument assembles Mathlib comparisons to integrals and Chebyshev estimates into explicit truncation controls.

claimThe series $\sum_{p\ \rm prime} p^{-\alpha}$ converges for every real $\alpha>1$.

background

The module lives inside the NumberTheory.RiemannHypothesis hierarchy and imports Port together with ErrorBudget. ErrorBudget decomposes the attachment error norm of J_N minus J_cert,N into separate budgets, one of which is the truncation error arising from cutting the prime sum at finite N. The present file therefore supplies the concrete prime-tail estimates needed to close that budget item.

proof idea

The module is a collection of supporting lemmas rather than a single proof. It first records summability of p to the minus r via comparison with the integral of x to the minus r and with the known summability of prime reciprocals, then derives explicit tail inequalities such as prime_tail_le_integer_tail and primeTailBound_christmas by monotonicity and integral remainder estimates.

why it matters in Recognition Science

The results close the prime-tail component of the error-budget decomposition described in the ErrorBudget module doc-comment. They therefore feed directly into any higher-level formalization of the Christmas-paper route to the Riemann Hypothesis. The module does not itself contain the RH statement.

scope and limits

Does not treat the divergent case alpha less than or equal to 1.
Does not compute numerical values of the partial sums.
Does not address the full Riemann Hypothesis statement.
Does not supply bounds for non-prime integers.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.NumberTheory.Port module_import
IndisputableMonolith.NumberTheory.RiemannHypothesis.ErrorBudget module_import

declarations in this module (16)

theorem prime_rpow_summable L53
theorem prime_rpow_tsum_exists L59
theorem rpow_neg_nonneg' L73
theorem summable_nat_rpow_neg_subtype L78
theorem antitoneOn_rpow_neg L86
theorem integral_rpow_neg L96
theorem integral_rpow_neg_improper L113
theorem integer_tail_tsum_le L138
theorem prime_tail_le_integer_tail L213
theorem prime_tail_tsum_bound L228
theorem primeTailBound_christmas L252
theorem primeTailBound_of_explicit L261
structure ArithmeticApproximant L274
structure PassiveCertificate L284
def ArithmeticDeformationIdentification L301
theorem attachmentWithMargin_of_bossLemma L307