A full and unconditional Lean 4 / Mathlib formalization of Eric Li's paper Rank Amplification for Shifted Equal Values of Euler's Totient Function, arXiv:2606.23681v2.
v2 is the formalized version. Its Section 1.1 describes this development and how v2 differs from v1. The paper source is not distributed here.
Every numbered result of the paper — all 6 theorems, 14 propositions, 11 corollaries and 25 lemmas
— has a Lean theorem stating it or something stronger. Nothing in the library depends on an axiom
beyond Lean's own three, on a sorry, or on any result quoted from the literature.
Per-item correspondence, and every deviation, is in
docs/theorem-inventory.md.
lake exe cache get
lake build
lake lintDo not run lake update: mathlib v4.32.2 requires its dependencies at branches, so it would
re-resolve them off the revisions in lake-manifest.json. CI does not run it.
autoImplicit = false and warningAsError = true. check.sh type-checks one file against the
built oleans; it plays no part in the release audit.
Unconditional. #print axioms returns exactly propext, Classical.choice, Quot.sound for
each of the 54 flagships audited in
FoundationsAudit.lean, enforced by #guard_msgs, so
the build fails if any of them acquires another dependency. No sorry, admit, axiom, unsafe
or native_decide anywhere — rejected by CI. Every project-defined Prop used as a hypothesis of
a flagship is either the paper's own hypothesis or is discharged elsewhere in the library; see the
inventory's Foundations section for the one substantive case and for the three flagships that
quantify over a project Type.
Full. Every numbered result is stated and proved, not merely its consequences. It does not mean
character-for-character transcription: naturals stand for reals, explicit vanishing sequences for
o(1), explicit constants for ≪. Lemma 2.7 is stated at C = 1 and at integer C rather than
at general real C; Proposition 10.24 and Corollary 10.22 are stated as a conditional theorem
whose every hypothesis is separately proved here. All of this is listed in the inventory's
Deviations section.
arXiv v1 quoted two deep results without proof — the uniform smooth-totient bound of
Banks–Friedlander–Pomerance–Shparlinski (arXiv v1's Theorem 2.6), and the same-support bound of
Pollack–Pomerance–Treviño, which rests on Evertse's theorem on S-unit equations. Neither is
reachable on Mathlib at the pinned version.
Section 9 removes the Pollack–Pomerance–Treviño bound from the paper outright. Finiteness of
J_h was used only in Proposition 9.6; the five elementary clauses of the amended Lemma 9.1 —
support, reciprocal mass, counting, slope support, and parity — suffice, and give a better
dependence on h than the quoted constant.
Section 2 does not remove the BFPS estimate — it demotes it to the displayed (2.8), still
quoted in the paper. Lemma 2.6 is deduced from (2.8) there, through the envelope (2.9), and
Lemma 2.7 from the introductory form (1.5); so the paper as a standalone document rests on the
BFPS quotation exactly as v1 did. In this repository both lemmas are instead proved outright, so
the formalization has no external analytic input. The paper's remaining quotations — Mertens
and Brun–Titchmarsh, its Lemmas 2.2 and 2.3, and the Selberg sieve inside the proof of Lemma 9.5 —
are all proved here too.
The tree follows the paper's logical dependency order, not its narrative order. Two modules sit outside the root import and are excluded from CI's reachability check:
SUnitQuantitative.lean— the low-height branch of Evertse's theorem. Nothing depends on it and its high-height branch is incomplete.SupplierRecordConstructions.lean— reconstruction certificates whose slot width is super-critical: as its docstring records, the certified bound's right-hand side tends to infinity at the paper's own parameters. The root bypasses the record entirely.
Every other module is reachable, compiled by lake build, and linted by lake lint.
scripts/check-docs.py runs in CI and verifies that every Lean name cited in this file and in the
inventory resolves, that every paper-item and display citation matches the .tex, that the quoted
counts are correct, that every numbered item has an inventory row, and that each row's kind matches
the paper.
The paper's own Section 1.1 states this; the inventory has the full table. In summary: BFPS demoted
to the displayed (2.8); Lemma 9.1 replaced by elementary clauses, removing the dependence on
Evertse's theorem; Lemma 9.5 tightened to positive constant terms, 1 ≤ r ≤ R, and uniformity
through primes(2Δ); Lemma 10.10's codomain relaxed to a prime-preserving map in canonical order.
Each holds at every point where the paper applies it.
One genuine error of v1 is corrected in v2: Proposition 10.27 claimed min(c, 1/(4c)) is the
exponential size of the transfer estimate. It is only an upper bound — the proof charges every
prime the saving at the worst endpoint p = Z², while the mass concentrates at p ≈ Z. The
conclusion survives: c = 1/2 and exponent (1/2+o(1))ℛ, because c ≤ 1/2 is forced
independently by the source-height threshold.
Lean and Mathlib v4.32.2, pinned in lean-toolchain and lake-manifest.json. Root target
lake build RankAmplification; linter lake lint. No artifacts beyond .lake.
Apache 2.0. See LICENSE.