---
id: F-010
title: Exponential prime-loss lower bound for totient ratios
tier: lean
polarity: positive
depends_on: []
supersedes: []
verifier: export PATH="$HOME/.elan/bin:$PATH"; diff -u verified_math/F-010_totient-exponential-loss/lean/Research/TotientLoss.lean workspace/experiments/experiment_2_elementary_upper_bound/lean/Research/TotientLoss.lean && (cd workspace/experiments/experiment_2_elementary_upper_bound/lean && lake build)
date: 2026-07-11
---

## Statement

For nonzero `n`, define

\[
L(n)=\sum_{p\mid n}\frac1{p-1}.
\]

Then

\[
\exp(-L(n))\le \frac{\phi(n)}n.
\]

Formal theorem:

```lean
theorem exp_neg_totientLoss_le_ratio {n : ℕ} (hn : n ≠ 0) :
  exp (-totientLoss n) ≤ (Nat.totient n : ℝ) / n
```

The artifact also formalizes Euler's real-valued product formula for the ratio.

## Proof / verification

For each prime divisor, Mathlib's inequality
`1-x⁻¹ ≤ log x` gives
`exp(-1/(p-1)) ≤ 1-1/p`.  Multiply these inequalities and use Euler's
product formula
`φ(n)/n=∏_{p|n}(1-1/p)`.  Lean's kernel accepts all casts, positivity, finite
products, and exponential identities with no `sorry`, `admit`, or axioms.
