Equilateral sets in $\ell_p^n$ beyond $n+1$: Linear excess and dimension cost
Logan R. Chalmers, Aran S. Ziegler
math.MG
Sep 23, 2026 · v1
math.CO
TL;DR
The equilateral-set constructions and finite bounds in ℓ_p^n are formalised in Lean, with the formalisation archived on Zenodo.
Abstract
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.
Problem
Kusner's conjecture that ℓ_p^n has at most n+1 equilateral points fails for p>4. That raises two questions: how fast the excess beyond n+1 grows with dimension at fixed p, and what happens at fixed dimension as p grows.
Approach
Copies of a spherical seed built from the 8×8 Walsh matrix are joined, using a spherical amplification lemma, to produce equilateral sets with linearly growing excess. For large p, a rank obstruction is applied to an approximate distance matrix of coordinate powers to rule out n+2 points. The constructions and finite bounds are formalised in Lean.
Results
For every p>4, e(ℓ_p^n) ≥ (1+c_p)n for large n. For p ≥ max{6, 2n(log n)^2}, e(ℓ_p^n) = n+1. The least dimension D_k(p) admitting k extra points satisfies p/(2(log p)^2) < D_k(p) ≤ (256/9)kp, so D_k(p) = p^{1+o(1)}.
