# An asymptotic formula for the number of totients

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [An asymptotic formula for the number of totients](../../preprints/An-asymptotic-formula-for-the-number-of-totients-September-25-2026/An-asymptotic-formula-for-the-number-of-totients-September-25-2026.pdf)

## Scope

Let $V(x)$ count the distinct values of Euler's totient function up to $x$. The formalization constructs the paper's explicit positive main term from finite arithmetic approximants and proves that their ratio tends to one. In particular, $V(cx)/V(x)\to c$ for every fixed $c>0$, answering the Erdős–Hall regular-variation question.

The formalization also gives asymptotics for totients $v\le x$ whose least preimage $\ell(v)=\min\{n\ge1:\varphi(n)=v\}$ lies between $kx$ and $(k+1)x$. The associated coefficient is positive under the stated existence condition; when no totient $d$ satisfies $kd<\ell(d)$, the count and coefficient are identically zero. The cases $k=1,2$ have positive coefficients.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Totient-count asymptotics and regular variation | [TotientAsymptotic.lean](../ComparatorChallenges/TotientAsymptotic.lean) |
| Exact zero case for the companion totient counts | [TotientCompanionZero.lean](../ComparatorChallenges/TotientCompanionZero.lean) |