arXiv++ Combinatorics

How many equilateral points can $\ell_p^n$ contain beyond $n+1$? For every fixed real $p>4$, we construct equilateral sets for which the number of points beyond $n+1$ grows at least linearly with $n$. For every fixed dimension, we prove that the maximum is $n+1$ at all sufficiently large finite $p$, with an explicit threshold. The least dimension admitting any fixed number of extra points is $p^{1+o(1)}$ as $p\to\infty$. The constructions and finite bounds are formalised in Lean. Thus $p=4$ marks the boundary: $n+1$ is exact in every dimension for $2\leq p\leq4$, while at every fixed finite $p>4$ the excess grows at least linearly with dimension.