← All papers
First page of The Equality Cases of the Weak Simplex Conjecture

The Equality Cases of the Weak Simplex Conjecture

Mengwei Su, Kaiwen Yang, Hao Xu, Chih-Lin I

cs.IT Aug 19, 2026 · v1
A single-parameter rigidity step in the equality-case proof of the Weak Simplex Conjecture is machine-checked in Lean 4.
Among $n+1$ equiprobable equal-energy signals in $\R^n$ under additive white Gaussian noise with maximum-likelihood decoding, which arrangement maximizes the probability of correct decoding? The question is Shannon's, recorded by Rice in 1950. Mulgund proved in 2026 that the regular-simplex value bounds the correct-decoding probability of every signal set at every signal-to-noise ratio, leaving open whether the simplex is the only maximizer. This paper determines the equality cases in a form stronger than uniqueness. A signal set other than a regular simplex falls strictly below the bound at every positive signal-to-noise ratio. Hence a code meeting the bound at one positive operating point is already a regular simplex, up to vertex relabeling and an orthogonal map. In probabilistic form, among the correlation matrices that signal sets induce, any matrix other than the identity gives a lower-orthant probability strictly above its independent counterpart at every finite threshold, leaving no room for a nontrivial equality. No code of ambient dimension below $n$ attains the bound. Under an energy budget $E$ with unrestricted blocklength the optimal codebook is uniquely the regular simplex of circumradius $\sqrt{E}$. Every optimal codeword therefore exhausts its allowance. Equality in the Simplex Mean Width Conjecture likewise occurs only at the regular simplex. The proof strengthens the first self-convolution step of Mulgund's argument with Royen's correlation theorem. The single-parameter rigidity is machine-checked in Lean 4.

The Weak Simplex Conjecture asks which arrangement of n+1 equal-energy signals maximizes correct-decoding probability over a Gaussian channel; optimality of the regular simplex was proved, but the equality (uniqueness) cases remained open.

The correlation-domination framework is strengthened using a strict Šidák–Khatri rectangle inequality and Royen's Gaussian correlation theorem to sharpen the first self-convolution step of Mulgund's argument. This yields strict inequalities showing any non-simplex code falls strictly below the bound at every positive signal-to-noise ratio. A single-parameter rigidity argument underlying the equality characterization is machine-checked in Lean 4.

A code meeting the regular-simplex bound at one positive operating point must itself be a regular simplex up to relabeling and orthogonal maps; no code of ambient dimension below n attains the bound, and the equality case of the Simplex Mean Width Conjecture occurs only at the regular simplex.