prime_rpow_summable
plain-language theorem explainer
The declaration shows that the series summing p to the power negative alpha over all primes converges for every real alpha greater than 1. Number theorists supplying tail bounds for prime sums in Riemann-hypothesis error budgets would cite it as the convergence anchor. The argument is a one-line wrapper that rewrites directly to the Mathlib fact on summable prime powers and closes the inequality with linear arithmetic.
Claim. For every real number $α > 1$, the series $∑_{p prime} p^{-α}$ converges.
background
The result belongs to the module that supplies explicit prime-sum bounds for the attachment-with-margin error budget in the Recognition Science treatment of the Riemann hypothesis. The module decomposes that budget into three parts: convergence of prime sums for α > 1, explicit upper bounds on the tail sums via partial summation, and discharge of the PrimeTailBound predicate. The local setting uses only the standard ordering on the reals together with the definition of the set of primes; no additional Recognition Science primitives enter the statement.
proof idea
The proof is a one-line wrapper. It rewrites the goal by the Mathlib lemma Nat.Primes.summable_rpow, which asserts summability of the indicated series whenever α > 1, then closes the resulting arithmetic goal with linarith.
why it matters
The theorem supplies the convergence fact required by the immediate downstream result prime_rpow_tsum_exists in the same file. That existence statement in turn feeds the explicit tail bounds and the discharge of PrimeTailBound_of_explicit, which closes the Christmas-route error-budget decomposition referenced in Riemann-Christmas.tex. Within the monolith it anchors the number-theoretic estimates that precede any appeal to the phi-ladder or eight-tick octave structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.