结果族 370：The Lane–Emden and Hénon–Lane–Emden conjectures · 学科：Partial differential equations · 验证状态：主结果已 Lean 形式化
两片互相加热的暖宝宝：u 的热度由 v 的 @@M@@p@@ 次幂决定，v 又由 u 的 @@M@@q@@ 次幂决定，还带”越靠近原点火力越猛”的位置权重。这样的互相取暖，能否在整个空间维持一个处处为正、处处有限的稳态？论文证明：只要”火力”越过一条只含维度、权重与幂次的简单分数线，答案必然是否——正的整体解根本不存在。分数线背后是朴素的直觉：火力与扩散散热比赛，火力占上风时温度必然失控。
关键词卡片
@@M@@-\Delta u=|x|^A v^p@@ 与 @@M@@-\Delta v=|x|^B u^q@@ 联立的方程组。@@M@@|x|^A@@，发热强度随位置改变，破坏平移对称性。@@M@@\frac{n+A}{p+1}+\frac{n+B}{q+1}\gt n-2@@。看个具体例子
代入数字：@@M@@n=5@@、@@M@@A=B=3@@、@@M@@p=q=4@@ 时左边 @@M@@=\frac85+\frac85=3.2\gt3=n-2@@，故无正整体解；若去掉权重（@@M@@A=B=0@@），同样的 @@M@@p,q@@ 只给 @@M@@\frac15+\frac15=\frac25\lt\frac35=(n-2)/n@@，不在无解区——加权与否本质不同。当 @@M@@n\ge3@@、@@M@@A,B\gt-2@@ 时，不等号翻转即存在径向正解（Phan 猜想 C），二者合成”有解无解”的精确分界线。还值得注意假设之弱：解只需在原点连续、别处经典，无穷远处完全不设任何有界性或衰减条件，结论照样成立。
为什么值得关心
Liouville 定理是导出先验估计、分析奇性的标准工具，此结果把带权方程组遗留的高维空白一次填满。它也是研究相应方程组解的有界性与爆破行为的必备输入。
已 Lean 形式化
第一级台阶
导读把方程组比作”两片互相加热的暖宝宝”。翻译成半数学语言：对象是铺满整个空间、处处为正的两个温度分布；供热规则是一方的热量由另一方的幂次决定，还要乘上一个随位置变化的火力权重——越靠近原点火力越猛；扩散则扮演散热。问题是：这种互相取暖能否在全空间维持一个处处有限的稳态？
第二级台阶
精确化三个概念。Hénon–Lane–Emden 方程组写作 @@M@@-\Delta u=|x|^A v^p@@、@@M@@-\Delta v=|x|^B u^q@@，其中 @@M@@\Delta@@ 是 Laplace 算子（刻画扩散散热），@@M@@|x|^A@@ 是以原点为中心的权重；整体正解指在全空间处处取正值、在原点只要求连续的解；次临界条件指不等式 @@M@@\frac{n+A}{p+1}+\frac{n+B}{q+1}\gt n-2@@。
第三级台阶
定理设维数 @@M@@n\ge2@@、幂次 @@M@@p,q\gt0@@、实权重 @@M@@A,B@@，假设解在原点连续、在别处满足方程，且在无穷远处完全不设任何条件；结论是次临界条件一旦成立，整体正解不存在。该不等式正是”火力压过散热”的精确分数线；无对称性、无衰减假设体现定理强度。把权重取为零，还立即顺带得到经典无权 Lane–Emden 猜想。再结合 Bidaut-Véron–Giacomini 的径向存在定理，进一步得到 @@M@@n\ge3@@、@@M@@A,B\gt-2@@ 时解存在与否的完整二分法（Phan 猜想 C）：不等号翻转时径向正解确实存在，分数线两侧严丝合缝。
证明了次临界 Hénon–Lane–Emden 猜想：当 @@M@@\frac{n+A}{p+1}+\frac{n+B}{q+1}\gt n-2@@ 时，方程组 @@M@@-\Delta u=|x|^A v^p@@、@@M@@-\Delta v=|x|^B u^q@@ 在全空间没有正整体解，且不需要任何对称性或无穷远条件；结合经典径向存在性定理，进一步给出了解存在的精确判据。
Lane–Emden 型方程组的 Liouville 定理（Liouville theorem，即”无非平凡正整体解”类结论）是非线性椭圆方程的基石：它是导出先验估计与奇性分析的爆破（blow-up）论证的标准输入。标量情形由 Gidas 与 Spruck 在 1981 年解决；方程组情形困难得多，Mitidieri 的 Rellich 恒等式、Serrin–Zou、Poláčik–Quittner–Souplet 与 Souplet 的工作逐步解决了低维无权情形，Li–Li–Wei 又把无权非存在区域推广到 @@M@@n\ge5@@。带权 @@M@@|x|^A@@、@@M@@|x|^B@@ 的 Hénon 推广更加棘手：权函数以原点为中心，破坏了方程的平移不变性，而传统 Liouville 证明恰恰依赖平移与平移不变的伸缩分析。此前 Bidaut-Véron–Giacomini 在径向理论中确定了临界双曲线，Phan 把无限制的问题表述为猜想 C，Li–Zhang 解决了三维，Li 覆盖了四、五维的部分指数范围，Huang–Zou 的猜想 B 则只在附加稳定性、衰减或能量假设时成立——高维全区域一直是空白。
主定理：设 @@M@@n\ge2@@、@@M@@p,q\gt0@@、@@M@@A,B\in\mathbb{R}@@ 且 @@M@@\frac{n+A}{p+1}+\frac{n+B}{q+1}\gt n-2@@，则不存在 @@M@@u,v\in C^2(\mathbb{R}^n\setminus\{0\})\cap C(\mathbb{R}^n)@@ 的严格正函数在 @@M@@x\ne0@@ 处满足上述方程组。假设之弱值得强调：只要求解在原点连续（不必可微），在无穷远处不加任何有界性、可积性或增长衰减条件。取 @@M@@A=B=0@@ 立即得到经典无权 Lane–Emden 猜想：@@M@@n\ge3@@ 且 @@M@@\frac1{p+1}+\frac1{q+1}\gt\frac{n-2}{n}@@ 时无非平凡正解。注意加权结论无法由无权结论推出——例如 @@M@@n=5@@、@@M@@p=q=4@@、@@M@@A=B=3@@ 满足加权次临界条件，但对应的无权分数 @@M@@2/5\lt3/5@@。分类推论（Phan 猜想 C）：当 @@M@@n\ge3@@、@@M@@A,B\gt-2@@ 时，”无正整体解”当且仅当上述严格不等式成立；反向弱不等式（含临界双曲线上）时存在径向正整体解，此部分由 Bidaut-Véron–Giacomini 的径向定理给出，二者合成完整的存在—不存在二分法。
先做归约：仅凭正性即可排除 @@M@@n=2@@、@@M@@A@@ 或 @@M@@B\le-2@@ 以及 @@M@@pq\le1@@，工具是球面平均通量 @@M@@(r^{n-1}\bar u')'@@ 的严格单调性与积分。随后是全文的关键观察：权以原点为中心，故平移不保持方程，但以原点为中心的伸缩 @@M@@u_R(x)=R^\alpha u(Rx)@@ 保持方程；据此在 @@M@@B_1@@ 上对源质量作自举估计（@@M@@M_f\ge cM_g^q@@、@@M@@M_g\ge cM_f^p@@ 结合 @@M@@pq\gt1@@）得到通用中心估计 @@M@@\int_{B_R}f\le CR^{n-2-\beta}@@，并证明 @@M@@u,v@@ 恰为 Newton 位势 @@M@@u=K*g@@、@@M@@v=K*f@@。定义次临界间隙 @@M@@\gamma=a(n+B)+b(n+A)-(n-2)@@，恒等式 @@M@@\gamma=(1-a-b)(\alpha+\beta+2-n)@@ 表明 @@M@@\gamma\gt0@@ 蕴含能量伸缩指数 @@M@@\alpha+\beta+2-n\gt0@@。于是整个证明归约为一个目标：给局部能量 @@M@@E=\int\eta(fu+gv)@@ 一个不依赖于解的一致上界——对 @@M@@u_R,v_R@@ 用该界并令 @@M@@R\to\infty@@，@@M@@B_1@@ 内能量以 @@M@@R^{\alpha+\beta+2-n}@@ 增长，必与一致界矛盾。
再建立局部化 virial 恒等式：引入相互作用测度 @@M@@\dd\pi(x,y)=f(x)g(y)K(x-y)\dd x\dd y@@，其两个边缘恰为 @@M@@fu@@ 与 @@M@@gv@@；对紧支撑向量场 @@M@@X=x\eta@@ 分部积分得 @@M@@a(n+B)E_f+b(n+A)E_g-aW_f-bW_g=(n-2)\int\Phi\,\dd\pi@@。Taylor 展开与位势尾部估计显示 @@M@@\Phi@@ 可近似为 @@M@@\eta(x)-w(x)D(x,y)@@，误差被 @@M@@\eps E+C_\eps@@ 吸收；整理后左端系数之和恰为 @@M@@\gamma@@，于是只欠”压强”估计 @@M@@aW_f+bW_g-(n-2)\int wD\,\dd\pi\le\eps E+C_\eps@@。
最后是最技术性的一步：把源 @@M@@f@@ 沿方向 @@M@@e@@ 按水平集 @@M@@\{f\gt t\}@@ 切成区间分量，只保留足够短的区间，其权重取帽权 @@M@@h_e@@ 的区间内下确界，方向 @@M@@e@@ 被限制在径向 @@M@@\omega_x@@ 附近的小帽内。两条平行线上的纯几何区间比较引理——由分部积分的中点恒等式加上差 @@M@@h=s-s'@@ 的分布关于中点分离的对称性证明——给出核积分的端点控制；层端点值 @@M@@(t/|x|^B)^{1/q}@@ 不是常数 @@M@@t^{1/q}@@，这一障碍用区间长度不超过 @@M@@2\delta d@@ 来压小；被丢弃的长区间由极坐标积分源质量并作高/低水平分解控制。合并全部误差即得压强估计，进而 @@M@@\frac\gamma2E\le\eps E+C@@，取 @@M@@\eps@@ 充分小便有 @@M@@E\le C@@，再由伸缩导出最终矛盾。
据任务元数据，本文主结果已通过 Lean 形式化证明，可信度属最高一档，结果族条目亦附有 Lean 文档链接。本批解读即结果族 370 的核心论文：非存在性定理是本文新贡献，分类推论的存在性一半则直接引用 Bidaut-Véron–Giacomini 的经典径向定理，属可靠引用而非新构造。仍需记住 OpenAI 官方声明”未经形式化的结果可能有问题”——好在本文核心定理已形式化，但文中引用的历史结论仍应以原始文献为准。
问 1：证明里最关键、也最脆弱的一步在哪里？
（答：从局部化 virial 恒等式到压强估计的收口。恒等式整理后左端系数之和恰为次临界间隙 @@M@@\gamma@@，于是只欠”压强估计” @@M@@aW_f+bW_g-(n-2)\int wD\,d\pi\le\eps E+C_\eps@@；能量 @@M@@E@@ 一旦有不依赖解的一致上界，对以原点为中心的伸缩解 @@M@@u_R@@ 用它并令 @@M@@R\to\infty@@，单位球内能量按 @@M@@R^{\alpha+\beta+2-n}@@ 增长即得矛盾。若任一误差项不是”相对 @@M@@E@@ 任意小加通用常数”，这一矛盾就凑不出来。）
问 2：哪个假设为什么不能去掉？
（答：严格不等号本身：在临界双曲线上不等号取等，而那里存在径向正解（Bidaut-Véron–Giacomini），非存在性必须严格次临界。另外 @@M@@pq\gt1@@ 是进入主论证的前提——@@M@@pq\le1@@ 及 @@M@@n=2@@、@@M@@A@@ 或 @@M@@B\le-2@@ 的情形已由球面平均通量的严格单调性另行排除，属归约部分而非主定理假设。）
问 3：与已有工作相比，真正的新意是什么？
（答：直面的两个老大难：其一，权以原点为中心使平移不再保持方程，而传统 Liouville 证明恰恰依赖平移与平移不变的伸缩，本文改用以原点为中心的伸缩并保留精确的空间权系数；其二，水平集层的端点值 @@M@@(t/|x|^B)^{1/q}@@ 不是常数，本文用”保留区间长度不超过 @@M@@2\delta d@@“压小端点权重变化。空间变化的定向截断、区间内取权下确界、相对能量的分层误差这套组合是方法层面的新机器；此前 Li–Zhang 只到三维，Li 覆盖四五维部分范围，Huang–Zou 则需稳定性/衰减/能量假设。）
问 4：这类 AI 生成证明最可能以什么方式出错？
（答：最可能在区间比较引理与压强估计的误差记账：几何区间比较（分部积分中点恒等式加差分布关于中点分离的对称性）与丢弃长区间的极坐标、高低水平分解层层交织，常数若在某层失去”相对 @@M@@E@@ 可控”性质则收口失败。不过据任务元数据，本文主定理已通过 Lean 形式化，此类风险被大幅压缩——这是同批论文中可信度最高的一篇。）
问 5：为什么加权结论不能由无权结论直接推出？
（答：论文明言：@@M@@n=5@@、@@M@@p=q=4@@、@@M@@A=B=3@@ 满足加权次临界条件，但对应无权分数 @@M@@2/5\lt3/5@@ 落在无权定理的适用范围之外；Phan 的迁移论证所需的无权输入也必须保持在其真实范围内。加权与无权的临界双曲线本质不同。）
问 6：这个结果谁会用、用在哪？
（答：Liouville 定理是先验估计与奇性分析中爆破论证的标准输入：相应带权方程组解的有界性、爆破行为研究都会直接引用；取 @@M@@A=B=0@@ 立得经典无权 Lane–Emden 猜想（文中推论）。非线性椭圆方程与抛物方程社区是主要用户。）
总评
次临界 Hénon–Lane–Emden 猜想在全维数、全权重范围的完整解决，且主定理已 Lean 形式化，分量与可信度俱高；残余风险仅在被引用的历史结果与形式化的覆盖边界，引用时以原始文献核对即可。