Equality Cases Establish the Strict Uniqueness of the Regular Simplex

In a preprint first uploaded on August 19, 2026, Mengwei Su, Kaiwen Yang, Hao Xu, and Chih-Lin I resolve Mulgund's Open Problem 8.1 on the equality cases of the Weak Simplex Conjecture. For $n+1$ equiprobable equal-energy signals in $\mathbb{R}^n$ under additive white Gaussian noise, they prove that every nonregular signal set has strictly lower correct-decoding probability than the regular simplex at every positive signal-to-noise ratio. Equality at even one positive operating point therefore forces the regular simplex, up to relabeling and an orthogonal transformation.

The result also rules out attainment in ambient dimension below $n$, proves uniqueness when blocklength is unrestricted under a per-codeword energy budget, and shows that every optimal codeword uses all available energy. In convex-geometric language, it determines the equality case of the Simplex Mean Width Conjecture: an $n$-simplex in the Euclidean unit ball has the regular simplex's mean width only if it is an orthogonal image of that simplex.

The proof strengthens an input in Mulgund's argument using Royen's correlation theorem. A Lean 4 companion checks the single-parameter moment-generating rigidity by an independent route and reports only the standard Lean axioms, but the authors state that Royen's theorem—and therefore the full single-threshold result—has not been formalized.