---
id: F-017
title: Combined low/high prime bound for total interval loss
tier: lean
polarity: positive
depends_on: [F-012, F-015, F-016]
supersedes: []
verifier: export PATH="$HOME/.elan/bin:$PATH"; diff -u verified_math/F-017_combined-interval-loss/lean/Research/CombinedIntervalLoss.lean workspace/experiments/experiment_2_elementary_upper_bound/lean/Research/CombinedIntervalLoss.lean && (cd workspace/experiments/experiment_2_elementary_upper_bound/lean && lake build)
date: 2026-07-11
---

## Statement

For `[k,k+n)⊆[1,X]` and `0<Z≤X`,

\[
\sum_{m=k}^{k+n-1}\sum_{p\mid m}\frac1{p-1}
\le \frac{\pi^2}{3}n+2\sum_{p\le Z}\frac1p
 +\frac{n\log X}{Z\log 2}.
\]

Formal theorem: `intervalLoss_le_combined`.  The artifact also proves the exact
identity `intervalLoss = lowIntervalLoss + highIntervalLoss`.

## Proof / verification

F-012's all-prime sum is partitioned exactly at `Z`.  F-015 controls the low
part and F-016 controls the high part; positivity of `Z log 2` permits division
in the latter.  Lean verifies the finite-set partition, denominator signs, and
algebra with no `sorry`, `admit`, or axioms.
