---
id: F-029
title: Exact logarithmic totient loss and cutoff decomposition
tier: lean
polarity: positive
depends_on: [F-010, F-028]
supersedes: []
verifier: export PATH="$HOME/.elan/bin:$PATH"; diff -u verified_math/F-029_exact-log-totient-loss/lean/Research/ExactLogLoss.lean workspace/experiments/experiment_3_adjacent_equal_density/lean/Research/ExactLogLoss.lean && (cd workspace/experiments/experiment_3_adjacent_equal_density/lean && lake build)
date: 2026-07-11
---

## Statement

For nonzero `n`, the exact additive prime loss satisfies

\[
 \sum_{p\mid n}-\log(1-1/p)=-\log\frac{\phi(n)}n.
\]

It splits exactly into prime factors at most and above every cutoff `Z`; each
prime contribution is nonnegative and at most `1/(p-1)`.  If `n>0` and
`φ(n)=φ(n+1)`, then

\[
 L(n+1)-L(n)=\log(n+1)-\log n.
\]

Formal theorems include `exactLogLoss_eq_neg_log_ratio`,
`exactLogLoss_eq_truncated_add_tail`, `primeLogLoss_nonneg_le`, and
`exactLogLoss_succ_sub_of_totient_eq`.

## Proof / verification

Take logarithms in Euler's finite product formula, proving every factor
positive.  The cutoff identity is a finite-set partition.  The upper bound on
`-log(1-1/p)` follows from `log x≤x-1` applied to the reciprocal Euler factor.
For equal neighboring totients, expand both logarithms of quotients and cancel
the common totient value.

Artifact: `lean/Research/ExactLogLoss.lean`; Lean accepts it with no `sorry`,
`admit`, native evaluator axiom, or project-declared axiom.
