Erdős Problem 408: distribution of iterated totient heights
A Lean proof that the least k with φ_k(n) = 1 has normal order α log n for a constant 1 / log 3 ≤ α ≤ 1 / log 2, with mean-square error O(x (log x)² / (log log x)⁵). This answers the first two questions of Erdős Problem 408. The proof formalizes extensions of Theorems 3.1 and 6.1 of OpenAI's The Poisson-Dirichlet law for prime predecessors, and uses vendored Lean proofs of the zero-free half-plane re s > 7/8 for Dirichlet L-functions (openai/math) and of the weighted dilation graph results (Yao Xu's totient-fibers-lean4).
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-19-000009
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-19-000009/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-19-000009/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'