结果族 263：The ionization and generalized ionization conjectures · 学科：Mathematical physics · 验证状态：主结果已 Lean 形式化
从一家超大的仓库（核电荷 Z 极大的原子）分批搬货：每回搬走 m 件、远少于库存，运费怎么算？定理给出精确账单：只要搬运量 m 趋于无穷而库存远大于它，拿走 m 个电子的能量代价渐近于一个普适常数乘 m 的 7/3 次方——搬得越多单价越陡；而且这个常数恰是七十年前托马斯–费米理论预言的那个。在含任意多体关联的完整量子模型里，这本账第一次被算清。
关键词卡片
@@M@@I_m(Z)@@（ionization energy）：一次拿走 m 个电子的总能量代价。@@M@@a_{\rm TF}@@（Thomas–Fermi constant）：TF 理论给出的普适系数，本文证明其精确出现。看个具体例子
能量随 m 的增长律画不如算，用公式卡。数字版定理：@@M@@I_m(Z)\sim a_{\rm TF}\,m^{7/3}@@（当 @@M@@m\to\infty@@ 且 @@M@@Z/m\to\infty@@）；代入感受量级：m 翻倍 ⇒ 费用约乘 @@M@@2^{7/3}\approx 5.0@@，m 变 8 倍 ⇒ 乘 @@M@@8^{7/3}=128@@。迭代极限版：@@M@@\lim_{m\to\infty}m^{-7/3}\limsup_{Z\to\infty}I_m(Z)=a_{\rm TF}=\frac{3}{7}\,q^{-4/3}@@。
为什么值得关心
完整库仑模型（含任意关联态）中广义电离猜想的能量部分首次获证；常数与 TF 经典预测严格吻合，是最硬的内在一致性检查。
已 Lean 形式化
结果族 263：Generalized ionization energies for full Coulomb atoms
第一级台阶
导读里”超大仓库分批搬货”的比喻，翻译过来是：对象是一个核电荷 @@M@@Z@@ 极大的原子——库存远大于搬运量；操作是一次性移走 @@M@@m@@ 个最外层电子；要算的账是这批搬运的总能量代价。经验规律是搬得越多单价越陡，而定理给出精确账单：只要 @@M@@m@@ 趋于无穷而 @@M@@Z/m@@ 也趋于无穷，总费用渐近于普适常数乘 @@M@@m^{7/3}@@，且这个常数正是七十年前托马斯–费米理论预言的那个。
第二级台阶
用精确语言说，库仑哈密顿量 @@M@@H_{Z,N}@@ 作用在反对称的双自旋 @@M@@N@@ 电子波函数上，含核吸引 @@M@@-Z/|x|@@ 与电子间排斥；@@M@@E_Z(N)@@ 是各电子数的基态能量。移走 @@M@@m@@ 个电子的费用定义为 @@M@@I_m(Z)=E_Z(Z-m)-E_Z(Z)@@。托马斯–费米泛函 @@M@@\mathcal T_Z(\rho)=T\int\rho^{5/3}-Z\int\rho/|x|+\frac12\iint\rho\rho/|x-y|@@ 是密度的变分近似，其弱电离律 @@M@@\lim_{Z\to\infty}I_m^{\rm TF}(Z)=a_{\rm TF}m^{7/3}@@（Bénilan–Brezis）给出常数 @@M@@a_{\rm TF}@@ 的经典定义。
第三级台阶
定理陈述：对完整双自旋库仑模型，只要 @@M@@m\to\infty@@ 且 @@M@@Z/m\to\infty@@，就有 @@M@@I_m(Z)/m^{7/3}\to a_{\rm TF}>0@@；由此立得 Solovej 广义电离猜想能量部分的两个迭代极限（先 @@M@@Z\to\infty@@ 再 @@M@@m\to\infty@@ 的 limsup 与 liminf 版本），联合极限是比猜想更强的陈述。假设的分工：@@M@@Z/m\to\infty@@ 保证移走的是”外层少数派”，TF 理论适用；双自旋费米统计提供动能下界；定理明确不断言固定 @@M@@m@@ 时对 @@M@@Z@@ 的收敛。证明枢纽是带价最小值 @@M@@P(\lambda)=\min_n(E_n+\lambda n)@@——允许电子数浮动、按价记账；关键的定价亏量定理断言：在 @@M@@\lambda=s^{-4}@@、@@M@@s\to0@@、@@M@@Zs^3\to\infty@@ 时，每个极小化区间都满足 @@M@@s^3(Z-n)\to q@@，@@M@@q@@ 是带价 TF 方程唯一经典解的外部电荷，且 @@M@@a_{\rm TF}=\frac37q^{-4/3}@@。
本文在完整库仑模型（双自旋、含任意关联态）中证明广义电离猜想的能量部分：移走 @@M@@m@@ 个电子的费用 @@M@@I_m(Z)\sim a_{\rm TF}m^{7/3}@@，只要 @@M@@m\to\infty@@ 且 @@M@@Z/m\to\infty@@；常数正是托马斯–费米理论预言的 @@M@@a_{\rm TF}@@，且得到猜想的两个迭代极限。
电离能衡量固定原子核下移走电子的代价。托马斯–费米（Thomas–Fermi）理论描述大电荷主阶能量，Lieb–Simon 1977 年证明它与多体薛定谔理论在 @@M@@Z^{7/3}@@ 阶一致；但两次总能量渐近相减控制不了小得多的电离能——余项足以淹没所求之差。Solovej 2016 年提出广义电离猜想（generalized ionization conjecture）：只要移走的电子数 @@M@@m@@ 远小于核电荷 @@M@@Z@@，移走 @@M@@m@@ 个电子的领头费用仍由 TF 决定，表述为先 @@M@@Z\to\infty@@ 再 @@M@@m\to\infty@@ 的迭代极限。此前 Seco–Sigal–Solovej 对 @@M@@m=1@@ 只得 @@M@@CZ^{20/21}@@ 型上界，Ivrii 的估计覆盖逐电子电离能与 TF 化学势（chemical potential）同阶的近中性区域（@@M@@Z^{5/7}\ll Z-N\ll Z@@）；均匀电离界只在 TFvW 与 Hartree–Fock 等近似变分模型中已知（Benguria–Lieb、Solovej）。完整模型需要新的屏蔽估计来对付任意关联态。
记 @@M@@I_m(Z)=E_Z(Z-m)-E_Z(Z)@@。定理（广义电离能）：对完整双自旋库仑哈密顿量，只要 @@M@@m\to\infty@@、@@M@@Z/m\to\infty@@，就有 @@M@@I_m(Z)/m^{7/3}\to a_{\rm TF}>0@@；特别地 @@M@@\lim_{m\to\infty}m^{-7/3}\limsup_{Z\to\infty}I_m(Z)=a_{\rm TF}@@，@@M@@\liminf@@ 版本同样成立——两个迭代极限正是 Solovej 公式化的能量部分，而联合极限是更强的陈述；固定 @@M@@m@@ 时对 @@M@@Z@@ 的收敛既不假设也不断言。关键中间结果（定价亏量定理）：引入带价最小值 @@M@@P(\lambda)=\min_n(E_n+\lambda n)@@，在 @@M@@\lambda=s^{-4}@@、@@M@@s\to0@@、@@M@@Zs^3\to\infty@@ 时，每个极小化区间 @@M@@n@@ 都满足 @@M@@s^3(Z-n)\to q@@；@@M@@q@@ 是方程 @@M@@\Delta F=4\pi k((F-1)_+)^{3/2}@@ 唯一经典解（原点附近被 @@M@@|x|^{-4}@@ 的倍数上下夹住、无穷远处一致趋零）的外部电荷，且 @@M@@a_{\rm TF}=\frac37q^{-4/3}@@。
定价是全文枢纽：固定 @@M@@Z@@ 时若允许电子数浮动、给每个电子记价 @@M@@\lambda@@，试验态便不必保持粒子数，价格精确记账，局部比较才可行；在尺度 @@M@@s=\lambda^{-1/4}@@ 上被移走的电荷量级为 @@M@@s^{-3}@@。证明先沿地基篇的含噪观测与空间切割做局部条件比较：把 TF 试验态与带价多体态在小球内比较，新切一刀在球外留下条件核，其条件屏蔽场在球内调和；两种后验定律严格区分、分别使用，联立得到局部密度与局部位势之间的双向蕴含。再构造障碍（barrier）传播：在最内尺度造正的次解（subsolution），逐层穿过观测尺度向外推，例外数据用期望质量趋零的误差密度支付；弱微分不等式先在保留分支的邻域上证明、后取最大值，避免在活动界面上求导。随后取极限：把条件场重标度为 @@M@@F_s(x)=s^4(V-K*\mu)(sx)@@，球面平均恒等式给出下界、帽子型上界控制正部，合成局部 @@M@@L^1@@ 控制，调和内部估计加 Arzelà–Ascoli 得紧性；极限场满足带价 TF 方程且一致衰减，障碍传递又保住正奇性 @@M@@B|x|^{-4}\le F_\infty@@。伸缩（dilation）接触论证识别出 Sommerfeld 系数 @@M@@|x|^4F\to(12/4\pi k)^2@@ 并证明唯一性（无需径向假设），从而一切极小化区间有同一亏量 @@M@@q@@。最后把价格积分回固定区间：@@M@@P@@ 关于 @@M@@\lambda@@ 是凹的，极小化区间夹住割线斜率，黎曼和加细得增量极限；零价格端的积分常数用地基篇的中性偏移界 @@M@@E_Z(Z)-E\le C@@；能量单调性把目标区间 @@M@@Z-m@@ 夹在两个极小化区间之间，得 @@M@@(E_Z(Z-m)-E_Z(Z))/m^{7/3}\to\frac37q^{-4/3}@@。TF 侧的平行计算（含精确质量伸缩 @@M@@\rho(x)=m^2\sigma(m^{1/3}x)@@，即 @@M@@I_m^{\rm TF}(Z)=m^{7/3}I_1^{\rm TF}(Z/m)@@）验证 @@M@@a_{\rm TF}=\frac37q^{-4/3}@@，与 Bénilan–Brezis 的经典弱电离律一致。
按任务标注，本文主结果已有 Lean 形式化证明，是族 263 中验证状态最强的一篇。其证明显式依赖地基篇（均匀超额电荷与外半径）的局域化、屏蔽估计与中性偏移界——带价极小化态的能量偏移可随 @@M@@s^{-7}@@ 增长，故”任意偏移下仍成立”的局部场估计不可或缺。常数与 TF 理论经典预测吻合是内在一致性检查；依 OpenAI 官方声明，未经形式化的结果可能有问题，族内尚未形式化的部分仍以社区核验为准。
结果族 263：Generalized ionization energies for full Coulomb atoms
问 1：为什么要发明”给电子标价”的带价最小值？固定粒子数不行吗？
答：不行，这是全文枢纽。固定电子数阻碍局部比较：小球内放试验态必须保持总粒子数，而带价最小值 @@M@@P(\lambda)=\min_n(E_n+\lambda n)@@ 允许电子数浮动，价格把数目变化精确记账，局部 TF 比较才可行；尺度 @@M@@s=\lambda^{-1/4}@@ 上被移走的电荷量级恰为 @@M@@s^{-3}@@。最后靠 @@M@@P@@ 的凹性与黎曼和加细把价格积分回固定区间——只用能量单调性，凸性都不需要。
问 2：证明中最脆弱的一环在哪里？
答：是障碍传播保住内部奇性：逐层平均会磨掉最内层的奇异电荷，论文在最内尺度造正次解、穿过观测尺度向外推，用期望质量趋零的误差密度支付例外数据；弱微分不等式先在保留分支邻域证明、后取最大值；两种后验定律必须严格区分使用——混用即毁掉库仑比较，这是审稿第一站。
问 3：为什么必须依赖地基篇”任意偏移”版本的局部估计？
答：带价极小化态的能量至多 @@M@@E+Cs^{-7}@@，偏移随 @@M@@s\to0@@ 增长；中性原子理论的固定偏移结论无法覆盖，引言明说”固定偏移结论本身得不出主定理”。故显式引用地基篇的局部场估计与中性偏移界 @@M@@E_Z(Z)-E\le C@@。这既是逻辑必需，也意味着本文正确性部分押在未形式化的地基篇上。
问 4：与已有结果相比真正的新意是什么？
答：此前完整模型估计都在别处：Seco–Sigal–Solovej 对首电离能只得 @@M@@CZ^{20/21}@@ 型上界；Ivrii 覆盖近中性区（@@M@@Z^{5/7}\ll Z-N\ll Z@@）；均匀电离界只在 TFvW 与 HF 等变分模型中已知。本文首次对含任意关联态的完整谱下确界证出联合极限，且常数与 TF 经典弱电离律严格吻合——最硬的内在一致性检查。
问 5：联合极限比 Solovej 的迭代极限强在哪？没证明什么？
答：迭代极限先 @@M@@Z\to\infty@@ 再 @@M@@m\to\infty@@，联合极限要求两者同时趋无穷仍收敛，蕴含迭代版且更强。定理也明说：固定 @@M@@m@@ 时 @@M@@I_m(Z)@@ 对 @@M@@Z@@ 的收敛既不假设也不断言（地基篇只给 @@M@@I_1(Z)@@ 的双侧夹逼）；读成”每个固定电离度都有 TF 极限”是错的。
问 6：主结果已 Lean 形式化，风险还剩多少？
答：形式化覆盖主定理骨架，可信度族内最高。但两点残余：一是”表述翻译”——Lean 陈述的极限模式、整数约束是否与英文一致；二是其显式依赖的地基篇尚未形式化，若形式化时把这些作为外部引理引入，验证范围未覆盖这些输入。
问 7：谁会用到它？
答：大电荷渐近分析与 TF 极限理论的研究者是直接用户；@@M@@a_{\rm TF}=\frac37q^{-4/3}@@ 的识别把多子量子电离与 Bénilan–Brezis 弱电离律接通，深电离的标度律从此有严格锚点。姊妹篇（广义外半径）与本文共享定价机制，合成 Solovej 猜想完整解答。
总评
这是广义电离猜想在完整模型上的首次完全证明（能量部分），定价技巧漂亮、常数吻合 TF 预言且有 Lean 背书，是族 263 顶点之一；最大风险是逻辑根基压在未形式化的地基篇上，形式化覆盖的边界值得用户查明。