单位球面上八个点的能量最小化
Energy minimization for eight points on the sphere
- University of North Florida（北佛罗里达大学）
- Bar-Ilan University（巴伊兰大学）
- University of Oxford（牛津大学）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
本文研究单位球面上八点的能量最小化，证明了对数、库仑及充分大的Riesz s-能量下正方形反棱柱为唯一全局极小点，并给出反例否定Cohn-Woo普适性猜想。
AI中文摘要：
我们研究了单位球面上八个点的能量最小化问题。对于对数能量和库仑能量，我们证明了在合同意义下唯一的全局极小点是正方形反棱柱，其高度由唯一的驻点方程刻画。该证明是计算机辅助的，并在 Lean 中完全验证。此后，我们考虑将该结果推广到其他重要的能量。对于 Riesz $s$-能量，我们提供了一个经 Lean 验证的非计算机辅助证明，表明对于所有充分大的 $s$，高度依赖于 $s$ 的正方形反棱柱是唯一的全局极小点，并提供了一个计算机辅助证明，表明这实际上对所有 $s\geq 0$ 成立。我们还给出了由完全单调势产生的能量的例子，对于这些能量，正方形反棱柱不是全局极小点，从而否定了 Cohn 和 Woo 的一个普适性问题。
英文摘要：
We study the energy minimization problem for eight points on the unit sphere. For the logarithmic and Coulomb energies, we show that the unique global minimizer up to congruence is a square antiprism with height characterized by a unique stationarity equation. The proof is computer-assisted and fully verified in Lean. After this, we consider generalizations of the result to other important energies. For the Riesz $s$-energies, we provide a Lean-verified, non-computer-assisted proof that the square antiprism with height depending on $s$ is the unique global minimizer for all sufficiently large $s$, and a computer-assisted proof that this in fact holds for all $s\geq 0$. We also give examples of energies arising from completely monotonic potentials for which the square antiprism is not a global minimizer, answering in the negative a universality question of Cohn and Woo.
