---
id: F-022
title: Uniform linear-plus-triple-log interval loss bound
tier: lean
polarity: positive
depends_on: [F-009, F-017]
supersedes: []
verifier: export PATH="$HOME/.elan/bin:$PATH"; diff -u verified_math/F-022_interval-loss-triplelog-upper/lean/Research/AsymptoticIntervalLoss.lean workspace/experiments/experiment_2_elementary_upper_bound/lean/Research/AsymptoticIntervalLoss.lean && (cd workspace/experiments/experiment_2_elementary_upper_bound/lean && lake build)
date: 2026-07-11
---

## Statement

There is `A>0` such that, for all sufficiently large natural `X`, every
positive-start interval `[q,q+ℓ)⊆[1,X]` satisfies

\[
 \operatorname{intervalLoss}(q,\ell)
 \le \left(\frac{\pi^2}{3}+\frac{2}{\log 2}\right)\ell
      +A\log\log\log X.
\]

Formal theorem: `exists_eventually_intervalLoss_le_linear_add_tripleLog`.

## Proof / verification

In F-017 choose the natural prime cutoff `Z=⌊log X⌋`.  Eventually
`(log X)/2≤Z≤log X≤X`, so the high-prime term is at most
`2ℓ/log 2`.  F-009 applies along `Z→∞`; monotonicity of two logarithms gives
`log log Z≤log log log X`, so the remaining reciprocal-prime term is at most
`A log log log X`.  Lean checks the floor bounds, filter compositions, and all
denominator signs.

Artifact: `lean/Research/AsymptoticIntervalLoss.lean`.  The full project builds
with no `sorry`, `admit`, or axioms.
