AI 中文总结
该研究解决弱单纯形猜想的等号情形，证明正则单纯形是唯一在任意正信噪比下达到正确译码概率上界的信号集，相关结论经Lean 4机器验证。
AI 中文摘要
在加性高斯白噪声（AWGN）环境下，于n维实空间（$\boldsymbol{\text{R}}^n$）中存在n+1个等概率、等能量的信号，采用最大似然译码时，何种信号排列能最大化正确译码概率？这是Shannon提出的问题，由Rice于1950年记录。Mulgund在2026年证明，正则单纯形值在任意信噪比（SNR）下都对所有信号集的正确译码概率构成上界，但仍未明确单纯形是否为唯一的最大化器。本文以强于唯一性的形式确定了等号情形：除正则单纯形外的信号集，在所有正信噪比下的性能都严格低于该上界。因此，在任意正工作点达到该上界的码，经顶点重标记和正交变换后必为正则单纯形。以概率形式表述：在信号集诱导的相关矩阵中，除单位矩阵外的任意矩阵，在所有有限阈值下的下象限概率都严格高于其独立对应值，不存在非平凡等号情形。环境维度低于n的码无法达到该上界。在能量预算E、码长无限制的条件下，最优码本唯一为外接圆半径$\boldsymbol{\text{R}}^n$的正则单纯形，所有最优码字均耗尽能量配额。单纯形平均宽度猜想的等号同样仅在正则单纯形处出现。该证明通过Royen的相关定理强化了Mulgund论证的首次自卷积步骤，单参数刚性在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.
