---
id: F-015
title: Low-prime loss bound for every consecutive interval
tier: lean
polarity: positive
depends_on: [F-011, F-014]
supersedes: []
verifier: export PATH="$HOME/.elan/bin:$PATH"; diff -u verified_math/F-015_low-prime-interval-loss/lean/Research/IntervalLossBound.lean workspace/experiments/experiment_2_elementary_upper_bound/lean/Research/IntervalLossBound.lean && (cd workspace/experiments/experiment_2_elementary_upper_bound/lean && lake build)
date: 2026-07-11
---

## Statement

For every interval `[k,k+n)` and prime cutoff `Z`, the contribution from primes
`p≤Z` to the total loss satisfies

\[
\sum_{p\le Z}\frac{\#\{m\in[k,k+n):p\mid m\}}{p-1}
\le \frac{\pi^2}{3}n+2\sum_{p\le Z}\frac1p.
\]

Formal theorem: `lowIntervalLoss_le`.

## Proof / verification

F-011 bounds each divisor count by `⌊n/p⌋+1`.  After casting,
`⌊n/p⌋≤n/p`; summing the repeated term invokes the first F-014 kernel bound,
and summing the one-off term invokes the second.  Lean verifies every finite
sum and denominator inequality with no `sorry`, `admit`, or axioms.
