---
id: F-014
title: Uniform bounds for the two prime-loss kernels
tier: lean
polarity: positive
depends_on: [F-008]
supersedes: []
verifier: export PATH="$HOME/.elan/bin:$PATH"; diff -u verified_math/F-014_prime-loss-kernel-bounds/lean/Research/LossBounds.lean workspace/experiments/experiment_2_elementary_upper_bound/lean/Research/LossBounds.lean && (cd workspace/experiments/experiment_2_elementary_upper_bound/lean && lake build)
date: 2026-07-11
---

## Statement

For every natural cutoff `Z`,

\[
\sum_{p\le Z}\frac1{p(p-1)}\le\frac{\pi^2}{3},
\qquad
\sum_{p\le Z}\frac1{p-1}\le 2\sum_{p\le Z}\frac1p.
\]

Formal theorems: `sum_primesLE_inv_mul_pred_le` and
`sum_primesLE_inv_pred_le`.

## Proof / verification

For primes `p≥2`, kernel terms satisfy
`1/(p(p-1))≤2/p²` and `1/(p-1)≤2/p`.  The first finite sum is bounded by the
formally known convergent square-reciprocal series (`hasSum_zeta_two`); the
second is exactly compared to F-008's finite prime-reciprocal sum.  Lean checks
all denominator signs and summation comparisons without `sorry`, `admit`, or
axioms.
