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

## Statement

Suppose `[k,k+n)⊆[1,X]`.  For any natural cutoff `Z`, let the high-prime loss
sum over `Z<p≤X` use the same divisor-count weights as F-012.  Then

\[
L_{>Z}(k,n;X)\,Z\log 2\le n\log X.
\]

Formal theorem: `highIntervalLoss_mul_le`.

## Proof / verification

Since `p>Z`, multiplication by `Z` cancels at most the denominator `p-1`.
Exchange the remaining divisor-count sum: it counts high prime factors across
interval entries.  This is at most each entry's total distinct-prime-factor
count, which F-013 bounds by `log m/log 2≤log X/log 2`.  Summing over the
exactly `n` entries proves the result.  Lean checks all finite-set exchanges and
casts without `sorry`, `admit`, or axioms.
