certified
If V(x) counts distinct Euler totient values up to x, then V(2x)/V(x) tends to 2. This establishes part (i), not every part of Problem 416.
Submitted by JenW1N
The PDF is a working mathematical exposition. Lean verification applies to the formal source, not the prose.
Certified 16 Sept 2026, published by conjectures.io.
Review decision
Approved in reviewREVIEW_APPROVED
Approved under submission-time policy v3: REVIEW_APPROVED, for the full locked task bounty. The submission proves Erdős 416(i): V(2x)/V(x) tends to 2 as real x tends to infinity. V counts distinct positive totient values up to x, with unrestricted natural-number preimages. The final theorem supplies the coverage, collision and prime-counting estimates needed for convergence. It does not assume the desired limiting relation. This decision concerns part (i), the doubling limit. The submission was accepted on 14 September 2026 at 04:31:57.787556 UTC. The earlier 29 July [proof claim](https://www.erdosproblems.com/forum/thread/416/proof-claims) and its [source repository](https://github.com/rafikmath15/fixed-scale-totient-limit-points) claim subsequential near-hits and a cluster interval. They explicitly leave the interval's width uncontrolled; the stronger conditional result requires an additional hypothesis. They do not establish convergence for the exact submitted target. [Ford's paper, page 3](https://arxiv.org/pdf/1104.3264#page=3), explicitly distinguishes its bounded-factor estimates from the unresolved scaling limit. The submission uses Ford-related mathematics, but that paper does not already solve this direct problem. The submitted supporting prime-number-theorem formalization retains the [PNT project](https://github.com/AlexKontorovich/PrimeNumberTheoremAnd) source and contributor notices; reuse of such auxiliary results does not itself establish a prior formalization of the exact reward target. The bounded prior-source review found no qualifying earlier complete solution, exact external formalization, misattribution evidence or earlier eligible same-target holder. Two separately conducted Codex agent assessments recommend REVIEW_APPROVED. The formal assessment checked exact task/proof/report commitments, statement fidelity, static policy compliance and selected parts of the proof architecture. The prior-source assessment checked dated public sources, proof claims, correspondence and eligibility. No material disagreement was identified. The agents used independent contexts in the same model family; no distinct-model consensus is claimed. The review relies on the successful hash-matched production Lean and Comparator verification. No fresh Lean replay, separate complete axiom export, exhaustive line-by-line audit of the 64,775-line proof or proof of originality is claimed. No material formalization defect or published disqualification reason was established. The miner may submit contrary evidence or request reconsideration from the review team, citing this submission ID.
Approved · decided 15 Sept 2026
Formal statement
Filter.Tendsto (fun x => Erdos416.V (2 * x) / Erdos416.V x) Filter.atTop (nhds 2)Verification report
Every box below had to hold before the proof counted. They are grouped in the order the verifier reaches them.
Manifest valid — Passed
The task bundle held together: the exact file set, a strict manifest, and every trusted hash matching the bytes on disk.
Task commitment matches — Passed
The bundle digest the submission committed to is the digest of the bundle that was actually verified.
Production task — Passed
The task came from the production pool rather than a test fixture.
Trusted file hashes match — Passed
The pinned dependencies agree across the manifest, the lockfile and the checkout, down to the same Formal Conjectures commit.
Submission policy respected — Passed
The submitted source passed the static scan: no imports, no axiom declarations, no sorry, no native_decide, no unsafe options.
Production sandbox — Passed
The run happened under real isolation, Landrun with seccomp, and the sandbox passed its own live self-test before the proof was touched.
Challenge built — Passed
The trusted Challenge.lean, which contains no miner code, compiled on its own.
Source type hash matches — Passed
The source theorem in the compiled environment still hashes to the type recorded in the task, so the statement has not drifted upstream.
Solution built — Passed
The submitted Solution.lean compiled.
Statement unchanged — Passed
The theorem the proof establishes has exactly the same canonical type as the task's target - it was not weakened or restated.
Only permitted axioms — Passed
The transitive axiom closure of the proof stays inside the axioms this task permits.
Lean kernel accepted — Passed
The Lean kernel replayed the proof and accepted it.
Nanoda accepted — Not run
A second kernel, written independently of Lean's, also accepted the proof.
One kernel, not two
This task does not require a second, independent kernel, so Nanoda was not run. The verdict rests on a single kernel implementation.
Theorems established
Stage COMPLETED · Axioms permitted: propext, Quot.sound, Classical.choice