结果族 267：Positive-temperature Bose–Einstein condensation and exact quantum depletion · 学科：Mathematical physics · 验证状态：暂无形式化证明，请以社区核验为准
低温下的齐舞：温度够低时，气体里的粒子不再各自即兴，而是一大部分同步踏进同一个”标准舞步”。这就是玻色–爱因斯坦凝聚。这篇论文首次严格证明：对固定的硬球气体和足够稀薄的密度，存在一个与容器大小无关的正温度，让这种齐舞在精确的统计平衡态中必然发生。
关键词卡片
@@M@@e^{-H/T}/\mathrm{Tr}\,e^{-H/T}@@。看个具体例子
定理的数字版：@@M@@\liminf \frac{\langle u_0,\gamma^{(1)}u_0\rangle}{N}>0@@，其中 @@M@@u_0=L^{-3/2}@@ 是常值波。取 @@M@@N=10^6@@ 个粒子：无论盒子多大，至少有某个与体积无关的固定比例——至少几万、几十万个粒子——挤在同一个波上；在动量图上，这表现为 @@M@@k=0@@ 处的巨型尖峰。
为什么值得关心
以往的严格正温凝聚定理都要借助某种”耦合极限”（比如让相互作用随容器一起缩小）；本文把排除距离、密度、温度三者固定，只让体积增大——教科书式的设定第一次被拿下。
暂无形式化证明（AI 结果待核验）
第一级台阶
导读里”低温齐舞”的比喻对应：对象是装在盒子里、两两不能靠得太近的硬球玻色气体，操作是把温度降到某个与盒子大小无关的正值。”齐舞”意味着宏观比例的粒子不再各自即兴，而同步踏进同一个标准舞步——同一个单粒子量子态；定理要证的正是：只要气体足够稀薄，这场齐舞在精确的统计平衡态中必然发生。
第二级台阶
用本科语言：硬球哈密顿量由允许构型集（任意两粒子距离超过排除距离 a）上带 Dirichlet 边界的梯度二次型定义；温度 T 的正则 Gibbs 态是 e^{−H/T}/Tr e^{−H}。热力学极限让粒子数与体积同增而密度 ρ 固定；一阶密度矩阵 γ^{(1)} 的最大特征值占总粒子数的比例即凝聚体占比（Penrose–Onsager 定义），平移不变性保证常值波 u₀=L^{−3/2} 是其特征向量。
第三级台阶
定理 1.1 的语境：固定排除距离 a，取密度 ρ 小于某阈值 ρ_*(a)，则存在正温度 T(a,ρ)——三者全部固定，只让体积趋于无穷——使 Gibbs 态的 liminf⟨u₀,γ^{(1)}u₀⟩/N 为正，凝聚落在常值轨道上。”密度充分小”挡住高密度硬核关联，”固定 a”与”体积无关的 T”分别排除了以往定理依赖的耦合极限与绑定极限；温度估值偏低，不用于定位相变点，其价值在于正温凝聚在教科书设定下首次成立。
证明三维稀薄硬球玻色气体在严格正温度下发生玻色–爱因斯坦凝聚：固定排除距离并取足够小的密度，存在与体积无关的正温度，使精确正则 Gibbs 态在热力学极限下凝聚体占比为正，且凝聚在常值轨道上。
玻色–爱因斯坦凝聚（Bose–Einstein condensation）的统计根源是 Bose 与 Einstein 在 1920 年代对理想气体的计数；Penrose 与 Onsager 在 1956 年把相互作用体系的凝聚定义为一阶密度矩阵（one-particle density matrix）的宏观特征值。此后的严格凝聚定理大多限于某种耦合极限：Lieb–Seiringer 的束缚气体 Gross–Pitaevskii 极限、Deuchert–Seiringer–Yngvason 的正温 GP 标度结果（其散射长度按 @@M@@L/N@@ 消失）、或盒子尺寸随稀薄度增长的绑定极限。硬球气体的能量理论虽已完整到 Lee–Huang–Yang 阶，但能量不等于占据：盒子增大时单粒子动能谱隙趋于零，热力学能量无法对单一轨道的占据给出体积一致的下界。把排除距离、密度、温度三者全部固定而让体积任意增长、并对精确正则 Gibbs 态（canonical Gibbs state）证明凝聚，正是本文补上的空缺。
在环面 @@M@@\Lambda_L=(\mathbb R/L\mathbb Z)^3@@ 上，硬球哈密顿量 @@M@@H_{N,L,a}@@ 由二次型 @@M@@q[f]=\sum_{i=1}^N\int_{\Omega_{N,L,a}}|\nabla_i f|^2@@ 定义，其中允许构型集 @@M@@\Omega_{N,L,a}@@ 要求任意两粒子距离超过排除距离 @@M@@a@@，波函数满足 Dirichlet 边界且对称。正温度 @@M@@T@@ 的正则 Gibbs 态为 @@M@@\Gamma_{N,L,T}=e^{-H_{N,L,a}/T}/\Tr e^{-H_{N,L,a}}@@，其一阶密度矩阵为 @@M@@\gamma^{(1)}_{N,L,T}@@。主定理（Theorem 1.1）：对每个 @@M@@a>0@@ 存在 @@M@@\rho_*(a)>0@@，使得对每个固定 @@M@@0<\rho<\rho_*(a)@@，存在正温度 @@M@@T(a,\rho)>0@@，满足
@@M@@D\liminf_{\substack{L\to\infty\\ N/L^3\to\rho}}\frac{\langle u_{0,L},\gamma^{(1)}_{N,L,T}u_{0,L}\rangle}{N}>0,@@
其中 @@M@@u_{0,L}=L^{-3/2}@@ 是常值轨道。平移不变性保证常值轨道是 @@M@@\gamma^{(1)}@@ 的特征向量，故这恰是 Penrose–Onsager 意义的凝聚。证明所得温度偏低，不用于定位相变点；其价值在于：只要气体参数 @@M@@\rho a^3@@ 足够小，温度就可以取正且与体积无关。
整体策略是把零温硬球基态的短路径比较方法移植到正温度的混合态。先做尺度变换：取单位使每个单位格含 @@M@@D\gg1@@ 个粒子、硬核半径为 @@M@@r=\alpha/D@@，在此证核心估计”占据占比 @@M@@B_{\rm occ}\ge c_*@@“。第一步是关键恒等式：把 Gibbs 核经平方根 @@M@@\Phi@@ 分解，凝聚占比恰等于”两个因子共享同一浴构型 @@M@@X'@@ 与保留构型 @@M@@W'@@、而标志粒子从 @@M@@x@@ 走到 @@M@@y@@“的积分；再把 @@M@@\Phi^2@@ 实现为短 Brown 时段上中点构型与 @@M@@W'@@ 的联合律，其条件律是避开硬核的 Brown 桥（Brownian bridge）乘积测度。于是占据问题被转化为路径水平的比较问题。接着建立联合局域估计：用熵与能量双管齐下——相对熵不等式控制密度的对角变化，一族带一致框架界的规范化插入映射控制添加粒子的自由能代价，即使存在有界吸引场也成立；再对违规路径打标记、赋予辅助粒子种类并解除其硬核约束，经热半群迹估计与外幂（exterior powers）控制一切正迹幂，得到缺陷格点数目的指数联合界。几何比较分三层推进：桥估计表明多数格点含有大量标签，其路径能以一致正概率穿过任意邻格；分组并暴露组外路径后，可用随机路线（unpredictable paths）连接大量格点对，两条独立路线相遇的指数矩有界，绕障借助 Kesten 外边界连通性定理（Timár 形式）。最终比较：沿一条路线构造中点错位的两份路径构型，从两份中各删去一个不同的标志粒子，恰好留下同一浴中点与同一 @@M@@W'@@，匹配重叠恒等式；对路线先平均再取密度的二阶矩，条件归一在两次路线相遇之外相消，使费用由相遇而非路线长度控制，格点估计把它压小，共同测度不等式对正比例的格点对给出正重叠。顺序至关重要：路径时长与组大小先于密度阈值固定，再让体积趋于无穷；最后一节换回物理单位，直接验证 @@M@@T_{\rm phys}@@ 与体积无关。
本篇暂无形式化证明，结论以社区核验为准。论文是自足的：所需的桥估计、格点路线与测度比较论证均随文附证明；其起点是两篇姊妹工作——零温硬球基态凝聚论文提供确定性短路径比较机制，有界有限程排斥势的正温凝聚论文提供热轨迹与格点路线估计——本文把二者改造为对硬核正则 Gibbs 态一阶密度矩阵的控制。同族两篇零温损耗论文与本篇共享尺度设置与路线技术，互相支撑。按 OpenAI 官方声明，未经形式化的结果可能存在问题。
问 1：证明中最关键也最脆弱的一步是什么？
（答：最终比较（sections/comparison）：沿一条随机路线构造中点错位的两份路径构型，从两份中各删去一个不同的标志粒子，恰好留下同一浴中点构型与同一保留构型 W’，匹配重叠恒等式；对路线先平均再取密度的二阶矩，条件归一在两次路线相遇之外相消，使费用由”两条独立路线相遇”而非路线长度控制。若这组删除与匹配不能精确对齐，正重叠推不出来。）
问 2：为什么以往的正温凝聚定理都要耦合极限，本文能摆脱的关键在哪？
（答：障碍在于能量不等于占据：盒子增大时单粒子动能谱隙趋于零，热力学能量无法对单一轨道的占据给出体积一致的下界。本文改把 Gibbs 核经平方根 Φ 分解，占据占比写成”两因子共享同一浴构型”的路径积分，Φ² 实现为短 Brown 时段上避开硬核的 Brown 桥联合律——占据问题变成路径比较问题。）
问 3：”密度充分小”这个假设为什么不能去掉？
（答：阈值 ρ_(a)=α₀³/(4D_²a³) 由证明常数给出：论证要求每个尺度化格子含 D≫1 个粒子、硬核半径 r=α/D，且缺陷格点数有指数联合界——高密度下硬关联渗入所有格子，局域估计与路线相遇控制都会失效。论文未讨论临界密度附近的行为。）
问 4：随机路线与绕障那一步在干什么？
（答：分组并暴露组外路径后，用不可预测路线（unpredictable paths）连接大量格点对；两条独立路线相遇的指数矩有界，绕障借助 Kesten 外边界连通性定理（Timár 形式）。这保证即使部分格点违规，仍有正比例格点对可比较，正重叠不被例外吞没。）
问 5：这类 AI 生成证明最可能的出错模式？
（答：量词顺序与尺度换算。证明明确”路径时长与组大小先于密度阈值固定，再让体积趋于无穷”；末节换回物理单位须验证 s→s∞、D→D∞、DT→1/4，使 T_phys 与体积无关；若某中间估计隐式依赖 L，结论即失效。熵—能量联合局域估计若常数失配，指数界也不成立。）
问 6：与零温硬球凝聚和有界势正温凝聚两篇姊妹工作是什么关系？
（答：本文起点是二者的机制——零温篇提供确定性短路径比较，有界势篇提供热轨迹与格点路线估计——并把它们改造为对硬核正则 Gibbs 态一阶密度矩阵的控制；硬核的 Dirichlet 边界使热半群迹估计、外幂与插入映射都要重做。论文自足，桥估计与测度比较随文给出。）
问 7：这个结果谁会用到，下一步是什么？
（答：严格统计力学的 BEC 理论自此覆盖教科书设定（固定参数、只放大体积）；后续目标是抬温逼近临界点、研究凝聚分数温度依赖与超流性；实验物理获得”正温硬核凝聚存在”的严格锚点，尽管所给温度偏低。）
总评
教科书设定下首次证明硬核玻色气体正温凝聚，是 BEC 严格理论的实质突破；最大风险在删除—匹配恒等式与多层尺度换算的长链条，未形式化前须逐节核验。