On the Erdős-Moser Diophantine Equation

On the Erdős-Moser Diophantine Equation: A Detailed Treatise on Power Sum Dynamics, Moser's Prime Sieve, Small Modulus Exclusions, and Certified Proofs This preprint provides an exhaustive mathematical treatise on the Erdős-Moser conjecture (Problem #11 in Paul Erdős' collection), which asserts that the only positive integer solution $(m, k) \in \mathbb{N}_{\ge 2} \times \mathbb{N}_{\ge 1}$ to the power sum Diophantine equation: $$\sum_{i=1}^{m-1} i^k = 1^k + 2^k + 3^k + \dots + (m-1)^k = m^k$$ is the trivial linear identity $1^1 + 2^1 = 3^1$ (corresponding to $m = 3, k = 1$). Key Mathematical Results & Contributions Continuous Asymptotics & Critical Diagonal: Analytical comparison of the discrete sum $S_k(m) = \sum_{i=1}^{m-1} i^k$ with the continuous integral $\int_0^m x^k dx = \frac{m^{k+1}}{k+1}$, proving that any hypothetical non-trivial solution must satisfy the critical diagonal balance $m \approx k + 1$. Formal Inductive Exclusion for $m = 4$: Complete, non-elliptical mathematical induction proving that $1 + 2^k + 3^k < 4^k$ for all $k \ge 2$, establishing the unconditional non-existence of integer solutions for $m = 4$ ($\forall k \ge 1$). Formal Inductive Exclusion for $m = 5$: Complete step-by-step induction proving that $1 + 2^k + 3^k + 4^k < 5^k$ for all $k \ge 3$, establishing the unconditional non-existence of integer solutions for $m = 5$ ($\forall k \ge 1$). Leo Moser's Modular Sieve: Detailed arithmetic exposition of Moser's modular reductions modulo $m - 1$ and $m$, proving by pairing symmetries that the exponent $k$ must necessarily be an even integer ($k = 2h$). 100% Machine-Checked Verification in Lean 4: All inductive bounds and exclusion theorems are formally verified with 0 axioms, 0 linter warnings, and 0 sorry placeholders via the Lean 4 interactive theorem prover and Mathlib. Repository and Verification Artifacts The companion machine-checked code and formal verification artifacts are publicly hosted on GitHub: https://github. com/flouzzy/erdos-problems Primary MSC (2020): 11D41, 11B68, 68V20, 11A07, 11B83.Keywords: Erdős-Moser Conjecture, Diophantine Equations, Power Sums, Mathematical Induction, Modular Sieves, Formal Verification, Lean 4, Mathlib.