结果族 095：Hyperbolicity cones without semidefinite lifts · 学科：Convex and metric geometry · 验证状态：暂无形式化证明，请以社区核验为准
半定规划是优化世界的”万能插座”，很多难题只要能插进去就能高效求解。一族叫”双曲锥”的好性质锥形（半正定锥是其中最出名的成员）长期被猜想都能插上这只插座；这篇论文造出一个反例锥：无论加多少辅助变量、用什么系数，都插不进去——万能插座并不万能。
关键词卡片
@@M@@L(x)\succeq 0@@ 的解集，半定规划的可行域。看个具体例子
下面的嵌套图是锥世界的地图：半正定锥 ⊂ 谱面 ⊂ 谱面影子。论文在 330 维输入空间中构造出双曲锥 @@M@@K_Q@@（矩阵块规模 @@M@@20N-1@@），并证明它落在影子区域之外——不是”还没找到插法”，而是数学上不存在任何有限插法（精确等式、任意实系数、任意多辅助变量都被排除），从而同时否定 Projected Lax 猜想与广义 Lax 猜想。
为什么值得关心
它划清了半定规划的能力边界：确实存在自然产生的凸优化问题永远无法化成半定规划，逼使人们另寻求解路线。
暂无形式化证明（AI 结果待核验）
衔接篇目：Hyperbolicity Cones Without Semidefinite Lifts（结果族 095）
第一级台阶
导读里”万能插座”的比喻落实为：插座是半定规划的可行域——由一个线性矩阵不等式的半正定性定义的集合；允许加辅助变量再投影，得到更大的”插口”族。双曲锥是一类性质优良的凸锥，半正定锥是其中最著名的成员；悬了多年的猜想说这族锥个个都能插进插口。本文造出一个双曲锥，证明无论加多少辅助变量、用什么系数，都不存在任何有限插法。
第二级台阶
术语化：齐次多项式 p 若沿某方向 e 切开、每条直线上根全为实数，称为双曲多项式；使根全非负的方向组成其闭双曲锥，Gårding 定理保证它是凸锥。谱面是仿射线性矩阵不等式 L(x)⪰0 的解集；谱面影子指再允许一组存在量词的辅助变量后的投影，等价于有限半定提升，且定义要求精确等式而非取闭包。
第三级台阶
定理断言：存在实齐次双曲多项式，其闭双曲锥没有任何有限仿射半定提升——矩阵规模、辅助变量个数任意有限，系数任意实数，全被排除。构造是高维存在性论证：从处处半正定的二次矩阵映射出发生成锥，经仿射截面化归为带 Moore–Penrose 逆刻画的三块坐标集，再用一个不必来自测度的正定矩泛函在解析 Gram 恒等式上引爆矛盾。Projected Lax 猜想（Netzer–Sanyal 2015）与更强的广义 Lax 猜想同告失败；精确等式与有限性的约定，正是把”辅助变量”这条退路一并堵死的关键。
证明了存在没有任何有限半定提升的双曲锥（hyperbolicity cone）：无论引入多少辅助变量、使用什么实系数，它都不是谱面影子（spectrahedral shadow），从而同时否定 Projected Lax 猜想与广义 Lax 猜想。
实齐次多项式 @@M@@p@@ 若在某方向 @@M@@e@@ 上使 @@M@@t\mapsto p(te-x)@@ 对每个 @@M@@x@@ 都只有实根，就称为双曲多项式（hyperbolic polynomial），其闭双曲锥 @@M@@K(p,e)@@ 由”根全非负”的点组成；Gårding 在 1959 年证明它必是凸锥。对称矩阵空间上的行列式关于单位阵双曲，锥恰为半正定锥；Güler 又证明双曲锥自带对数自协和障碍（logarithmic self-concordant barrier），因而被视为超越半定规划（semidefinite programming）的天然可行域。谱面（spectrahedron）指有限仿射线性矩阵不等式 @@M@@L(x)\succeq0@@ 的解集；谱面影子是谱面的线性投影，等价于允许辅助变量的半定提升（semidefinite lift）。广义 Lax 猜想断言每个双曲锥都是谱面；Netzer 与 Sanyal 在 2015 年提出较弱的 Projected Lax 猜想，只要求它是谱面影子。三变量情形由 Helton–Vinnikov 的行列式表示定理给出肯定答案；此后各类正面结果（初等对称族、边界光滑、Nash 光滑边界）都附加正则性假设，而 Brändén 构造的无行列式表示的多项式又不排除”换一个多项式定义同一个锥”。真正的卡点在于：如何排除允许任意多辅助变量、任意实系数的一切有限提升。
主定理（Theorem 1.1）：存在实齐次双曲多项式，其闭双曲锥没有任何形如
@@M@@DS=\Big\{x\in\mathbb{R}^d:\exists u\in\mathbb{R}^a,\ A_0+\sum_{i=1}^d x_iA_i+\sum_{j=1}^a u_jB_j\succeq0\Big\}@@
的表示——矩阵尺寸与辅助变量个数任意有限、系数任意实数，且定义要求精确等式，不允许对投影取闭包。构造是高维存在性论证：输入空间维数 @@M@@m=330@@，矩阵块规模 @@M@@r=20N-1@@（可取 @@M@@N>10\cdot 36^2@@），而非对某个具体表示的尺寸下界。两个 Lax 猜想就此同告失败。
先造锥。从一个处处半正定的二次矩阵映射 @@M@@Q:\mathbb{R}^m\to\Sym_r@@ 出发，定义 @@M@@p_Q(X,Z,y)=\det\big((\det X)Z-\Phi_y(\operatorname{adj}X)\big)@@，其中 @@M@@\Phi_y@@ 由 @@M@@Q(y)@@ 的分块公式给出、@@M@@\operatorname{adj}@@ 是经典伴随阵。固定 @@M@@y@@ 做 Gram 分解 @@M@@Q(y)=\sum_j b_jb_j^\top@@，展开得到对称行列式恒等式 @@M@@p_Q(te-(X,Z,y))=\det(tI-D_y(X,Z))@@：根全是实对称矩阵的特征值，双曲性与锥的分块刻画一并到手。再取仿射截面 @@M@@X=\diag(1,A)@@ 并投影，锥恰好映为 @@M@@E_Q=\{(A,t,y):A\succeq0,\ \operatorname{ran}Q(y)\subseteq\operatorname{ran}A,\ t\ge\operatorname{tr}(A^\dagger Q(y))\}@@，其中 @@M@@A^\dagger@@ 是 Moore–Penrose 逆。仿射截面与坐标投影都保持提升的存在性，故只需证明 @@M@@E_Q@@ 无提升。
再造障碍，难点是”@@M@@Q@@ 处处半正定”与”@@M@@E_Q@@ 有障碍”互相牵制，作者分两步绕开。第一步造有限性：令 @@M@@H@@ 为八个变量的二次型空间（36 维），四次型上的线性泛函 @@M@@y@@ 对应 Hankel 矩阵（Hankel matrix）@@M@@Y(y)(f,g)=y(fg)@@；借助附录里的有限域证书构造秩 20 的半正定”种子”矩阵 @@M@@T@@，其核满足强乘法条件。模掉平移与伸缩共八个参数后得到 185 维归一化流形，维数计数可选出子空间 @@M@@K@@ 使归一化纤维有限，于是”压缩逆的极限方向”只剩有限多个射影类 @@M@@\mathcal C@@。第二步造分离：在 @@M@@N@@ 份拷贝中用维数计数选出向量 @@M@@w\in W^N@@ 与子空间 @@M@@U\subset w^\perp@@，再对任意逼近序列按”特征值发散／趋于有限非零极限／趋于零”分组做谱分析，证明 @@M@@w@@ 不落在 Hankel 像 @@M@@(I_N\otimes Y)u@@ 的闭包中。于是存在二次型 @@M@@g@@ 在所有这些像上非负、而在 @@M@@w@@ 处严格为负；定义 @@M@@Q(y)=U^\top G(y)\,g\,G(y)U@@，则对任意向量 @@M@@a@@ 有 @@M@@a^\top Q(y)a=(G(y)Ua)^\top g\,(G(y)Ua)\ge0@@——处处半正定性免费获得，而 @@M@@g@@ 的负方向正是预埋的障碍。
最后引爆障碍。赋值泛函给出 @@M@@E_Q@@ 内一个次数至多四的多项式小块 @@M@@x(s)@@，迹不等式处处取等。再构造一个正定矩泛函（moment functional）@@M@@\Lambda@@——只要求其矩矩阵正定，完全不需要来自测度——作用在 @@M@@x(c+\eps s)@@ 上：@@M@@A@@ 坐标满足 @@M@@A_{c,\eps}\succeq a_c\eps^4I@@，而迹不等式被违反到 @@M@@-\kappa_c\eps^4@@ 阶。反设存在有限提升：半代数分层与 Sard 定理提供解析的提升坐标与 Gram 因子（Gram factor）；把 @@M@@\Lambda@@ 正延拓到 32 次，作用于 16 阶 Taylor 多项式后，pencil 值与半正定 Gram 值在 @@M@@\eps^{16}@@ 阶内一致，再与一个最大秩可行点混合，即得距测试点仅 @@M@@O(\eps^{16})@@ 的可行点。但 @@M@@A\succeq\eps^4I@@ 使逆矩阵的扰动只有 @@M@@O(\eps^8)@@，远不足以消除 @@M@@\eps^4@@ 阶的违反——矛盾。故 @@M@@E_Q@@ 及整个 @@M@@K_Q@@ 都没有有限半定提升。
本文暂无形式化证明，按 OpenAI 官方声明，未经形式化的结果可能有问题，请以社区核验为准。它与同族两篇姊妹稿互相支撑：九月底的显式反例（其主结果已 Lean 形式化）证明某个 23 变量双曲锥不是谱面，十月初的提升论文又证明该锥反而是谱面影子；只有本文的高维构造才真正切断”辅助变量”这条退路，否定 Projected Lax 猜想。技术路线上，本文与 Scheiderer 的局部平方和障碍方法一脉相承，但改用有限正矩泛函直接检验解析 Gram 恒等式，绕开了对表示测度的需求；种子矩阵的秩条件由附录中的有限域证书验证。
对象：Hyperbolicity Cones Without Semidefinite Lifts（结果族 095）
问 1：证明中最脆弱的一环是什么？
答：种子矩阵。整座构造立在”存在秩 20 的半正定 Hankel 矩阵、其核具强乘法性质”之上，而它由附录的有限域证书验证——从有限域上的秩计算过渡到实半正定矩阵是证明的一部分，此处若有缝隙，后续的有限类计数与分离论证全部悬空。次脆弱处是最终矛盾的渐近记账：ε^4 阶违反、ε^16 阶 Gram 拟合、ε^8 阶逆矩阵扰动，三个量级任何一处算错，混合可行点的构造就不再矛盾。
问 2：Brändén 早就造过没有行列式表示的多项式，为何不算解决？
答：因为”多项式无表示”不等于”锥无提升”。Kummer 证明相关的特殊化 Vámos 多项式的双曲锥反而是谱面——换一个多项式可以定义同一个锥。SOS 松弛失败也不排除所有有限提升。本文的突破恰在量词：对任意有限矩阵规模、任意实系数、任意多辅助变量，一律排除。
问 3：与 Scheiderer 2018 的局部平方和障碍相比，新意是什么？
答：Scheiderer 用局部正性障碍证明一般半代数集无提升，并在其文 5.4 节明确追问此法能否解决双曲锥问题。本文路线与之近亲，但改用有限正定矩泛函直接检验解析 Gram 恒等式——该泛函不必来自任何测度，绕开了对表示测度的需求，这正是双曲锥场景下原先迈不过去的坎。
问 4：反例锥是显式的吗？维数 330 意味着什么？
答：不是具体小维数的显式反例，而是高维存在性论证（输入维数 m=330、矩阵块规模 20N−1，N 可取大于 10·36²），因此它也不是”某个给定锥的表示尺寸下界”。三变量情形由 Helton–Vinnikov 定理永远是谱面，反例只能藏在较高维数里；找一个可手算的小反例仍是悬题。
问 5：为什么定义里咬住”精确等式、不许取闭包”？
答：半定提升的标准定义即精确等式；若允许对投影取闭包，可行性会大幅扩张，本文的反例论证依赖”提升坐标可经半代数选择与 Sard 定理取得解析”这类刚性，取闭包会消解这些工具。论文未讨论闭包版猜想的真伪，这仍是开放地带。
问 6：这篇论文最可能以什么方式出错？
答：AI 生成证明的典型风险在此具象为三处：有限域证书与实矩阵之间的转换论证、185 维归一化流形上的维数计数（选出使纤维有限的子空间）、以及逼近序列按特征值发散/有限/趋零分组的谱分析。构造嵌套极深且无形式化证明，也无姊妹篇的独立复算覆盖此主定理，须以社区核验为准。
问 7：谁会用到它？
答：它给半定规划的表达能力划出硬边界：优化界从此知道确有自然锥问题永远化不成 SDP，须转向二阶锥、其他锥规划或非凸路线；带正则性假设的正面结果（光滑边界、严格双曲等）不受影响，反而边界更清晰；实代数几何中”锥提升 ⟺ 正因子分解”的纲领获得第一批负例参照。
总评
这是把 Projected Lax 猜想正面击穿、为 SDP 万能性画上句号的工作，构造思想出色；最大风险在它未经形式化、依赖深嵌套的存在性论证与有限域证书，独立核验之前宜按”高度可信待证”对待。