---
id: F-018
title: Exponential lower bound for an interval product of totient ratios
tier: lean
polarity: positive
depends_on: [F-010]
supersedes: []
verifier: export PATH="$HOME/.elan/bin:$PATH"; diff -u verified_math/F-018_interval-ratio-product-lower/lean/Research/IntervalRatioProduct.lean workspace/experiments/experiment_2_elementary_upper_bound/lean/Research/IntervalRatioProduct.lean && (cd workspace/experiments/experiment_2_elementary_upper_bound/lean && lake build)
date: 2026-07-11
---

## Statement

For every positive-start interval `[k,k+n)`,

\[
\exp\!\left(-\sum_{m=k}^{k+n-1}\sum_{p\mid m}\frac1{p-1}\right)
\le \prod_{m=k}^{k+n-1}\frac{\phi(m)}m.
\]

Formal theorem: `exp_neg_intervalLoss_le_prod`.

## Proof / verification

Apply F-010 pointwise to each nonzero interval entry, multiply the inequalities,
and use `exp(∑x)=∏exp(x)`.  Lean verifies positivity and the finite products
with no `sorry`, `admit`, or axioms.
