---
id: F-019
title: Arbitrarily small totient ratios at fixed multiples
tier: lean
polarity: positive
depends_on: [F-010]
supersedes: []
verifier: export PATH="$HOME/.elan/bin:$PATH"; diff -u verified_math/F-019_small-totient-ratio-at-multiples/lean/Research/SmallRatio.lean workspace/experiments/experiment_2_elementary_upper_bound/lean/Research/SmallRatio.lean && (cd workspace/experiments/experiment_2_elementary_upper_bound/lean && lake build)
date: 2026-07-11
---

## Statement

For every real decay rate `R`, there is a fixed positive natural modulus `B`
such that every nonzero multiple `m` of `B` satisfies

\[
  \frac{\phi(m)}m\le e^{-R}.
\]

Formal theorem: `exists_modulus_totientRatio_le_exp_neg`.  The artifact also
proves that the reciprocal-prime partial sums tend to infinity and the explicit
factorial estimate

```lean
theorem totientRatio_le_exp_neg_primeReciprocalBelow {N m : ℕ}
    (hm : m ≠ 0) (hdiv : N ! ∣ m) :
    (Nat.totient m : ℝ) / m ≤ exp (-primeReciprocalBelow N)
```

## Proof / verification

Mathlib's formally proved Euler theorem that the reciprocal-prime series is
not summable is converted to divergence of its nonnegative partial sums.  If
`N! ∣ m`, every prime below `N` occurs among the prime factors of `m`.  Euler's
product formula (F-010's supporting identity), monotonicity of products whose
factors lie in `[0,1]`, and `1-x≤exp(-x)` give the explicit bound.  Divergence
then supplies an `N` whose sum exceeds any prescribed `R`; take `B=N!`.

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