---
id: F-012
title: Prime-by-prime rearrangement of consecutive totient loss
tier: lean
polarity: positive
depends_on: [F-010]
supersedes: []
verifier: export PATH="$HOME/.elan/bin:$PATH"; diff -u verified_math/F-012_interval-loss-prime-rearrangement/lean/Research/IntervalLoss.lean workspace/experiments/experiment_2_elementary_upper_bound/lean/Research/IntervalLoss.lean && (cd workspace/experiments/experiment_2_elementary_upper_bound/lean && lake build)
date: 2026-07-11
---

## Statement

If `0<k` and `k+n≤X`, then the total loss from F-010 on `[k,k+n)` can be
rearranged exactly as

\[
\sum_{m=k}^{k+n-1}\sum_{p\mid m}\frac1{p-1}
=\sum_{p\le X}\frac{\#\{m\in[k,k+n):p\mid m\}}{p-1}.
\]

Formal theorem: `intervalLoss_eq_sum_divisorCounts` in
`lean/Research/IntervalLoss.lean`.

## Proof / verification

Every prime factor of a nonzero `m≤X` lies in `X.primesLE`; filtering that
finite prime set by divisibility gives exactly `m.primeFactors`.  Lean then
checks the exchange of the two finite sums and turns the indicator sum into the
cardinality of divisible interval entries.  There are no omitted primes,
floating-point operations, `sorry`, `admit`, or axioms.
