结果族 087：The Mahler conjectures, functional inequalities and polar-product symplectic width · 学科：Convex and metric geometry · 验证状态：主结果已 Lean 形式化
往箱子里塞球谁都懂，但物理里的”箱子”是相空间——位置坐标乘上动量坐标——而”塞”必须遵守一套保护面积的特殊规则（辛几何）。这篇论文证明：把对称凸体 @@M@@K@@ 当位置范围、其对偶 @@M@@K^\circ@@ 当动量范围，拼成的相空间恰好能塞进大小为 4 的标准辛球，再多一点都不行。妙处在于：数字 4 与 @@M@@K@@ 的形状完全无关。
关键词卡片
@@M@@\omega_0=\sum dq_j\wedge dp_j@@，哈密顿力学的几何语言。@@M@@U_K=\operatorname{int}K\times\operatorname{int}K^\circ@@，位置块与对偶动量块相乘而成的相空间。看个具体例子
容量 @@M@@c@@ 的 @@M@@2n@@ 维标准球体积为 @@M@@c^n/n!@@。取 @@M@@n=2@@、@@M@@K=[-1,1]^2@@（面积 4），@@M@@K^\circ@@ 是菱形（面积 2），相空间体积 @@M@@4\times2=8@@；容量 4 的球体积恰为 @@M@@\tfrac{4^2}{2!}=8@@。数字版定理：
@@M@@c_G(\operatorname{int}K\times\operatorname{int}K^\circ)=4\quad\Longrightarrow\quad \operatorname{vol}(K)\operatorname{vol}(K^\circ)\ \ge\ \frac{4^n}{n!}@@
塞到 4 就顶格：对正方体这个例子，容量 4 的球体积已与整个相空间一样大，再大一点体积本身就装不下。而且构造对任何对称凸体 @@M@@K@@ 都成立：每个容量 @@M@@c<4@@ 的标准球都能光滑地塞进去。
为什么值得关心
它把悬置八十余年的对称 Mahler 猜想变成”一行体积计算”：塞得进容量 4 的球，体积就至少有 @@M@@4^n/n!@@；这是与姊妹篇相互独立的另一条证明路线。
已 Lean 形式化
第一级台阶
导读的”往相空间里塞球”可以落地说：箱子不是一个，而是两块拼成的——把对称凸块当作位置的活动范围，把它的价格对偶块当作动量的活动范围，位置乘动量就是物理学家眼中的相空间。”塞”也不是随便放：搬运过程必须遵守一套保护”位置–动量面积”的特殊规则，球在搬运中不能被压扁成细管。要问的是：这个拼装箱子最多能装多大的标准球。惊人的是答案与块的形状完全无关。
第二级台阶
| 用本科术语精确化：标准辛形式 ω₀=Σ dq_j∧dp_j 度量相空间的面积结构；光滑嵌入若保持辛形式（e*ω₀=ω₀）则称辛嵌入；一个域的 Gromov 宽度定义为可辛嵌入其中的标准球容量的上确界，容量 c 的球即 {(q,p)：π( | q | ²+ | p | ²)<c}。极体 K°={p：对一切 q∈K 有 ⟨q,p⟩≤1}，极积为开域 U_K=int K×int K°。辛嵌入必然保体积。 |
第三级台阶
| 定理在 n≥2、对每个原点对称凸体陈述——不要求光滑、严格凸、无条件对称或乘积结构——Gromov 宽度 c_G(U_K)=4：对每个 c<4 都给出光滑辛嵌入，顶点容量无须达到。上界一侧由 Gromov 非挤压定理封死；下界一侧是真正的构造：一个”全纯消失产生球”原理提供容量 πk 以下的球，一个平面共形映射逆的高次幂一致切片估计把动量尺度控制在 (1+o(1))πk/4，两个尺度相除即凑出任意 c<4。保体积性随后把对称 Mahler 猜想变成一行计算：容量趋于 4 的球体积 c^n/n! 不得超过相空间体积 | K | K° | 。 |
论文证明：对每个 @@M@@n\ge2@@ 与每个原点对称凸体 @@M@@K@@，相空间极积 @@M@@\operatorname{int}K\times\operatorname{int}K^\circ@@ 的 Gromov 宽度恰为 4——每个容量 @@M@@c<4@@ 的标准球都能光滑辛地嵌入其中且 4 不可超越；由辛嵌入保体积立刻重新推出对称 Mahler 猜想。
Gromov 1985 年的非挤压定理（nonsqueezing）表明辛嵌入受体积之外的约束，容量（capacity）自此成为辛几何的核心不变量；Viterbo 进而提出凸域的体积–容量猜想。Artstein-Avidan–Karasev–Ostrover（2014）把它与对称 Mahler 猜想联系起来，证得 Hofer–Zehnder 容量 @@M@@c_{\mathrm{HZ}}(K\times K^\circ)=4@@，这给出 Gromov 宽度的上界，但下界需要真实构造球嵌入，此前仅在 @@M@@\ell_p@@ 单位球（@@M@@1<p<\infty@@，Karasev）、立方体–交叉多胞体积（Ramos–Sepe）等特殊族上实现。Vicente 提出”无限制对称极积宽度”问题，本文给出肯定回答。另注：Haim-Kislev–Ostrover 用正五边形否定了一般 Viterbo 猜想，但五边形非中心对称，与本文无冲突。
定理：对每个整数 @@M@@n\ge2@@、每个原点对称凸体 @@M@@K\subset\mathbb R^n@@，把 @@M@@K@@ 放入位置坐标、@@M@@K^\circ@@ 放入动量坐标，标准辛形式 @@M@@\omega_0=\sum_j dq_j\wedge dp_j@@，则 @@M@@U_K=\operatorname{int}K\times\operatorname{int}K^\circ@@ 的 Gromov 宽度（Gromov width）@@M@@c_G(U_K)=4@@：对每个 @@M@@0<c<4@@ 存在光滑辛嵌入 @@M@@B^{2n}(c)\hookrightarrow U_K@@。推论一：对称 Mahler 不等式 @@M@@\operatorname{vol}_n(K)\operatorname{vol}_n(K^\circ)\ge 4^n/n!@@（辛嵌入保体积而 @@M@@\operatorname{vol}(B^{2n}(c))=c^n/n!@@，令 @@M@@c\uparrow4@@ 即得），立方体表明常数精确；推论二：@@M@@n\ge3@@ 时满足严格体积和与两两容量条件的有限球组可不相交地装入 @@M@@U_K@@。
下界来自两个解析部件的配合。第一个是”全纯消失产生球”原理：若全纯映射 @@M@@f:\Omega\subset\mathbb C^n\to\mathbb C^m@@ 以原点为唯一公共零点、@@M@@|f(z)|=O(|z|^k)@@ 且 @@M@@|f|^2@@ 的次水平集在 @@M@@\Omega@@ 中紧，则域 @@M@@V=\{|f|^2<1\}@@ 连同辛形式 @@M@@\omega=dd^c(|z|^2+|f|^2)@@ 包含每个容量 @@M@@<\pi k@@ 的标准球。其证明分四步：先用光滑递增修正把 @@M@@\log|f|^2@@ 的对数奇性削成斜率受控的仿射行为；再用正则化极大（regularized maximum，Richberg 粘合技巧）以径向位势 @@M@@\mu\log(|z|^2+\delta)-M@@ 替换奇点而不改变边界附近的形式；然后用紧支集的 Moser 形变（Moser deformation）把光滑化的形式拉回原形式；最后在径向模型 @@M@@R(z)=\sqrt{1+\mu/(|z|^2+\delta)}\,z@@ 下显式读出一个标准球。
第二个部件控制动量尺度：沿用透镜共形映射 @@M@@F:\mathbb D\to D@@（Gross 均匀分布映射的旋转，尖端在 @@M@@\pm i@@），其逆 @@M@@g@@ 的高次幂的水平原函数满足一致界 @@M@@|J_k|\le(\pi k/4)|g|^{2k}+o(k)@@，且一致性一直保持到尖端——这一点必不可少，因为切片高度会随 @@M@@k@@ 增大而逼近 @@M@@\pm1@@。组合时把条带体 @@M@@K=\{x:|b_j\cdot x|\le1\}@@ 的实约束复线性延拓，令 @@M@@f_j(z)=g(b_j\cdot z)^k@@，则全纯球原理适用。相空间实现 @@M@@\Phi_k@@ 把 @@M@@z=u+ix@@ 的虚部送入位置 @@M@@q=x@@，动量取 @@M@@p=-u-\sum_j J_k(b_j\cdot u,\,b_j\cdot x)\,b_j@@，其中带符号切片积分修正标准动量：直接拉回计算给出 @@M@@\Phi_k^*\omega_0=\omega@@，偏导数 @@M@@\partial_v J_k\ge0@@ 保证整体单射，一致界保证动量落在 @@M@@S_k\operatorname{int}K^\circ@@ 内，且 @@M@@S_k=(1+o(1))\pi k/4@@。动量除以 @@M@@S_k@@、源球做补偿性伸缩，两尺度相除后对充分大的 @@M@@k@@ 就凑出每个给定的容量 @@M@@c<4@@；整个过程对每个 @@M@@c@@ 是一次有限构造，无需嵌入的极限。最后用极体中的有限条带体逼近把下界推广到任意对称凸体。上界则用 AAKO 的支撑柱面论证：取 @@M@@\langle q_0,p_0\rangle=1@@ 的配对作辛线性变换，把 @@M@@U_K@@ 嵌入 @@M@@(-1,1)^2\times\mathbb R^{2n-2}@@，再等面积地映入 @@M@@B^2(4)\times\mathbb R^{2n-2}@@，由 Gromov 非挤压定理宽度不得超过 4。
主结果已由 Lean 形式化。本篇与对称 Mahler 姊妹篇共用透镜映射与逆映射高次幂技术，但论文明确声明其证明既不使用姊妹篇的体积积定理也不使用等号分类，是独立路线；等号情形本篇不作断言。同族一般凸体篇给出非对称常数与单纯形等号。按 OpenAI 官方声明，未经形式化的结果可能有问题；本篇主结果已形式化，球装填推论引用了同集另一篇球装填定理，以社区核验为准。
问 1：证明里最脆弱的一步在哪？
| 答：一致切片估计”一直到尖端”。透镜映射之逆 g 的高次幂的水平原函数满足 | J_k | ≤(πk/4) | g | ^{2k}+o(k)，这个界必须在透镜全域一致——而切片高度会随 k 增大逼近尖端 ±1，端点在移动。论文明言”uniformity near the tips is essential”，planar 一节专为此证了动端点界。若尖端一致性失效，动量修正项失控，嵌入就溢出极体。 |
问 2：为什么只证每个 c<4，不证 c=4？
答：U_K 是开域，容量恰为 4 的闭球不可能嵌入开集且达到上确界；定理只须对每个严格小于 4 的容量给出嵌入，宽度作为上确界即等于 4。Mahler 推论靠 c↑4 取极限完成，无需顶点嵌入。
问 3：与已有工作相比真正的新意是什么？
答：Artstein-Avidan–Karasev–Ostrover 已证 Hofer–Zehnder 容量 c_HZ(K×K°)=4，它给 Gromov 宽度上界；难点在下界——需要真实构造球嵌入，此前只在 ℓp 球（Karasev）与立方体–交叉多胞体积（Ramos–Sepe）等特殊族实现。本文对无任何结构假设的对称凸体完成构造，”全纯消失产生球”原理（Richberg 正则化极大＋紧支集 Moser 形变）是方法学上新工具。
问 4：哪个假设最不能去掉？
答：中心对称性。极积与极体的定义都围绕原点；非对称体须先取 Santaló 点，其相空间结构与本文的透镜对称性不匹配。引言也强调不对等号情形作断言——Gromov 宽度是上确界量，等号分类须另走凸几何路线（姊妹篇的 Hanner 分类）。Haim-Kislev–Ostrover 的五边形 Viterbo 反例不冲突，正因五边形非中心对称。
问 5：作为 AI 生成证明，最可能出错的模式是什么？
答：软分析的边界控制。Moser 形变要求支集远离边界（紧次水平集保证），切片单调性 ∂_v J_k≥0 保证整体单射——这类”技术条件恰好够用”的环节是生成式证明的高危区。本文主结果已 Lean 形式化，风险可控；但球装填推论引用同集另一篇装填定理，属未形式化的下游。
问 6：谁会用这个结果？
答：辛几何与凸几何的交叉社区：它把对称 Mahler 猜想降为一行体积计算，给出了与透镜姊妹篇完全独立的第三条路线；n≥3 时的有限球组装填推论直接服务辛装填问题。Viterbo 体积–容量猜想的对称情形也被此结果强化。
总评
“宽度恰为 4”这个形状无关的普适常数是漂亮且分量十足的定理，Lean 背书加上与姊妹篇的路线独立性使其可信度居前；最大残留风险在未形式化的装填推论与尖端估计的软分析细节。