On the Five-Point Case of Mordell's Problem

Abstract

For five complex points $z_1,\ldots,z_5$ satisfying $\sum_i|z_i|^2=5$, Mordell's discriminant inequality states that $\prod_{i<j}|z_i-z_j|^2\leq5^5$, with equality precisely for a unit regular pentagon, up to rotation and permutation. We organize its proof around a direct comparison of discriminant values. A global maximizer gives a centered stationary configuration, whose coefficient equations reduce the generic case to two quartic branches. On each branch, the absolute value of a cubic polynomial gives the original discriminant objective after accounting for the normalization scale. Exact rational interval bounds exclude both branches from the maximum, and the exceptional coefficient cases leave the regular pentagon. The argument determines the maximizing configuration without reconstructing all stationary shapes. We have completed a full Lean formalization of the five-point inequality and both directions of its equality condition, including all reductions and finite checks used in this proof.