---
id: F-020
title: A decreasing low-ratio tail forces linear interval loss
tier: lean
polarity: positive
depends_on: [F-018]
supersedes: []
verifier: export PATH="$HOME/.elan/bin:$PATH"; diff -u verified_math/F-020_decreasing-tail-forces-loss/lean/Research/DecreasingProduct.lean workspace/experiments/experiment_2_elementary_upper_bound/lean/Research/DecreasingProduct.lean && (cd workspace/experiments/experiment_2_elementary_upper_bound/lean && lake build)
date: 2026-07-11
---

## Statement

Let `q>0`.  Suppose every totient on `[q,q+ℓ)` is at most `φ(q)`, and
`φ(q)/q≤exp(-R)`.  Then

\[
 \prod_{m=q}^{q+\ell-1}\frac{\phi(m)}m\le e^{-R\ell}
 \quad\text{and consequently}\quad
 R\ell\le \sum_{m=q}^{q+\ell-1}\sum_{p\mid m}\frac1{p-1}.
\]

Formal theorems: `interval_ratio_prod_le_exp_neg_mul` and
`rate_mul_le_intervalLoss_of_decreasing_anchor`.  The artifact also proves the
monotonicity lemma `totientRatio_anti_of_totient_le`.

## Proof / verification

If `q≤m` and `φ(m)≤φ(q)`, cross multiplication gives
`φ(m)/m≤φ(q)/q`.  Multiply this pointwise estimate over the interval and use
`exp(-R)^ℓ=exp(-Rℓ)`.  F-018 bounds the same product below by
`exp(-intervalLoss q ℓ)`; strict monotonicity of the exponential then gives the
linear loss inequality.

Artifact: `lean/Research/DecreasingProduct.lean`.  Lean accepts it with no
`sorry`, `admit`, or axioms.
