结果族 095：Hyperbolicity cones without semidefinite lifts · 学科：Convex and metric geometry · 验证状态：主结果已 Lean 形式化
想象用一张”机器体检表”描述一块地皮：把坐标填进一个对称矩阵，只要矩阵保持”非负”（半正定），点就在地内——数学里许多漂亮的凸区域都能这么写。这篇论文造出一块形状很规整的凸区域，并严格证明：无论换多大的矩阵、多聪明的填法，都写不出它。”所有这类凸区域都能这样描述”的广义 Lax 猜想，就此被推翻。
关键词卡片
@@M@@x^2-y^2-z^2@@。@@M@@L(x)\succeq0@@ 解集的凸集。看个具体例子
数字版定理（对照着看）
冰激凌锥可以：@@M@@x^2-y^2-z^2@@ 的双曲锥恰好等于 @@M@@\{(x,y,z):\begin{pmatrix}x+y&z\\z&x-y\end{pmatrix}\succeq0\}@@，一个 @@M@@2\times2@@ 矩阵就搞定。
本文反例不行：@@M@@p(X,Z,y)=\det((\det X)Z-\Phi_y(\operatorname{adj}X))@@ 是 23 个实变量上的双曲多项式（20 次；除以 @@M@@\det X@@ 后可整理成 16 次，锥不变），但对任何矩阵尺寸 @@M@@N@@、任何实线性映射 @@M@@L@@，它的闭双曲锥 @@M@@K\ne\{x:L(x)\succeq0\}@@。
证明的妙处：假设存在矩阵表示，就能从锥的几何里”榨出”一个范数恒等式，让以”弱极端性”著称的 Choi–Lam 型原样现身，再由它推出恒为零的矛盾。
为什么值得关心
双曲锥是比半定规划更一般的优化舞台，它能否写成矩阵不等式，直接决定”双曲规划能否归约为半定规划”。这个 23 变量的显式反例给出了否定回答。
已 Lean 形式化
第一级台阶
入门导读把谱面比作”机器体检表”：给一块地皮配一台机器，把坐标填进一个对称矩阵，矩阵保持”非负”就表示点在地内。现在把比喻拧干一些：我们关心的对象是一类形状规整的凸区域；操作是”设计喂料规则”——事先约定每个坐标往矩阵哪些格子填、填多少倍，然后问这块地是否恰好等于机器亮绿灯的集合。导读里的冰激凌锥说明，确有不少地皮能这样描述。
第二级台阶
用本科语言精确化。齐次多项式称为关于方向 e 双曲，若从任一点沿 e 切开，所得直线上的一元多项式零点全为实数；其闭双曲锥由”所有根非负”的点组成，Gårding 定理保证它是凸闭锥，是冰激凌锥的高维推广。另一边，若凸锥等于某个线性矩阵不等式的解集——即把坐标线性填入固定大小的实对称矩阵后要求半正定——则称它为谱面。
第三级台阶
主定理在 23 维语境下陈述：变量取两个四阶对称矩阵加三个标量，把 Choi–Lam 双二次型经一个保持半正定性的线性映射织进一个行列式，得到 20 次齐次双曲多项式（除去一个行列式因子后为 16 次，锥不变）。关键在于假设给对手完全的自由：矩阵尺寸任意、线性填法任意、Hermitian 铅笔也无济于事。结论是它的闭双曲锥不等于任何这种解集，于是”每个双曲锥都是谱面”的几何版广义 Lax 猜想被一个显式反例推翻；而证明手法不是比对行列式，而是从锥的几何中逼出范数恒等式，让 Choi–Lam 型自己现身。
构造了 23 个实变量、16 次的显式齐次双曲多项式，其闭双曲锥不能写成任何有限实对称线性矩阵不等式，从而推翻几何版广义 Lax 猜想。
1958 年 Lax 提出：三变量的双曲多项式是否都有对称行列式表示？Helton–Vinnikov 定理与 Lewis–Parrilo–Ramana 的等价性给出肯定答案，因此三元双曲锥都是谱面（spectrahedron）。高维情形，广义 Lax 猜想断言每个齐次双曲多项式的闭双曲锥（hyperbolicity cone）——Gårding 证明其为凸——都能由有限线性矩阵不等式 @@M@@L(x)\succeq0@@ 定义。由于双曲锥在凸优化中扮演超越半定规划的角色，这一表示问题直接关系到”双曲规划能否归约为半定规划”。此前的相关反例停留在多项式层面：某个多项式没有行列式表示，并不能排除同一个锥被另一个多项式或另一支铅笔表示。卡点在于：必须对任意有限矩阵尺寸、任意实系数的铅笔，从锥自身的几何中提炼出刚性矛盾。
定理 1.1：设 @@M@@Q(y)@@ 为由系数一的 Choi–Lam 双二次型（Choi–Lam biquadratic form）@@M@@b(z,y)=z^\top Q(y)z@@ 决定的 @@M@@3\times3@@ 矩阵，@@M@@\Phi_y@@ 为由它诱导的 @@M@@\Sym^4@@ 上的线性映射，则
@@M@@Dp(X,Z,y)=\det\big((\det X)Z-\Phi_y(\operatorname{adj}X)\big),\qquad (X,Z,y)\in\Sym^4\times\Sym^4\times\mathbb{R}^3@@
是 20 次齐次多项式，关于 @@M@@e=(I_4,I_4,0)@@ 双曲且 @@M@@p(e)=1@@；其闭双曲锥 @@M@@K=\Lambda_+(p,e)@@ 不是谱面：对任意有限 @@M@@N@@ 与任意实线性映射 @@M@@L:\Sym^4\times\Sym^4\times\mathbb{R}^3\to\Sym^N@@，都有 @@M@@K\ne\{(X,Z,y):L(X,Z,y)\succeq0\}@@。推论 1.2：商 @@M@@q=p/\det X@@ 可延拓为同样 23 个变量的 16 次齐次双曲多项式且锥不变，故得到 16 次反例。作者不声称维数或次数极小；实对称框架也已覆盖 Hermitian 铅笔。
整条证明链围绕一个标量刚性展开：Choi–Lam 型 @@M@@b@@ 非负非零，却具有弱极端性（weak extremality）——任何满足 @@M@@\ell(z,y)^2\le b(z,y)@@ 的双线性型 @@M@@\ell@@ 必须恒为零。作者先给出短证明：@@M@@b@@ 的零点直接消去 @@M@@\ell@@ 的非对角系数，再沿使 @@M@@b@@ 以四阶速度消失的曲线消去对角系数。
先证多项式性质良好。对秩一矩阵有恒等式 @@M@@u^\top\Phi_y(vv^\top)u=b(v_0u'-u_0v',y)\ge0@@，故 @@M@@\Phi_y@@ 是保持半正定的正线性映射（positive linear map）。双曲性用上半平面论证：取 @@M@@t=a+i\eta@@，@@M@@(tI_4-X)^{-1}@@ 的虚部负定，经 @@M@@\Phi_y@@ 的正性传导后目标矩阵虚部正定从而可逆，故 @@M@@p(te-(X,Z,y))@@ 无复根。随之算出两个切片：@@M@@X\succ0@@ 时属于 @@M@@K@@ 当且仅当 @@M@@Z\succeq\Phi_y(X^{-1})@@；@@M@@y=0@@ 时当且仅当 @@M@@X\succeq0@@ 且 @@M@@Z\succeq0@@。
再压榨假设的铅笔。设 @@M@@K@@ 有表示 @@M@@L=L_1(X)+L_2(Z)+L_3(y)@@。先除去公共核并把 @@M@@L(e)@@ 归一化为严格正定；@@M@@y=0@@ 切片迫使 @@M@@L_1,L_2@@ 是正映射，分块后得到单态（unital）正映射 @@M@@D:\Sym^4\to\Sym^a@@、@@M@@E:\Sym^4\to\Sym^c@@ 与线性映射 @@M@@B:\mathbb{R}^3\to\mathbb{R}^{a\times c}@@。关键一步是重标度：由 @@M@@\Phi_{sy}=s^2\Phi_y@@，整条点列 @@M@@(I_4,s^2Z_0,sy)@@ 落在 @@M@@K@@ 内；用 @@M@@\diag(I_a,s^{-1}I_c)@@ 做同余变换并令 @@M@@s\to0@@，可得 @@M@@G(y)=0@@，且块矩阵 @@M@@\begin{pmatrix}D(X)&B(y)\\B(y)^\top&E(Z)\end{pmatrix}\succeq0@@ 与 @@M@@Z\succeq\Phi_y(X^{-1})@@ 等价，取 Schur 补即 @@M@@E(Z)\succeq B(y)^\top D(X)^{-1}B(y)@@。
然后取秩一极限。令 @@M@@X_t=vv^\top+t(I-vv^\top)@@、@@M@@Z_t=uu^\top+t(I-uu^\top)@@ 趋于秩一投影，把两个等价条件分别化成闭射线的阈值，对齐得 @@M@@\lambda_{\max}(A_t)=\|C_t\|_{\op}^2@@；令 @@M@@t\to\infty@@，@@M@@D(X_t)^{-1/2}@@ 收敛到 @@M@@D(I-vv^\top)@@ 核上的投影 @@M@@P(v)@@，@@M@@E@@ 侧同理得 @@M@@R(u)@@，于是出现精确的范数恒等式
@@M@@Db(v_0u'-u_0v',y)=\big\|P(v)B(y)R(u)\big\|_{\op}^2@@
——Choi–Lam 型从锥的几何中原样浮现。
最后一步切向微分。核投影 @@M@@R(u)@@ 在秩最大的开集上光滑；在基点 @@M@@u=v@@ 处左边为零，强迫 @@M@@P(v)B(y)R(v)=0@@。沿球面路径 @@M@@u_s=(v+sh)/\sqrt{1+s^2\|h\|^2}@@ 求导，左边变成 @@M@@b(Jh,y)@@，右边变成 @@M@@\|P(v)B(y)\,dR_v(h)\|_{\op}^2@@，其中 @@M@@J:v^\perp\to\mathbb{R}^3@@ 是同构。于是矩阵 @@M@@F(z,y)=P(v)B(y)dR_v(J^{-1}z)@@ 的每个元素都是双线性型，且其平方不超过 @@M@@\|F\|_{\op}^2=b(z,y)@@；由弱极端性这些元素全部为零，从而 @@M@@b@@ 恒为零，与 @@M@@b(e_1,e_1)=1@@ 矛盾。
本文主结果已有 Lean 形式化证明（见结果族 095 的 Lean 文档），是同族三篇中验证最扎实的一环。姊妹稿关系密切：本文只排除原坐标下的铅笔表示；十月初的姊妹篇进一步证明这同一个锥其实拥有 @@M@@100\times100@@、含 307 个辅助变量的精确半定提升，即它是谱面影子而非谱面；而族内另一篇高维构造则说明确有双曲锥连影子都不是。三者合起来把 Lax 猜想的各个层级逐一切断。按 OpenAI 官方声明，未经形式化的结果可能有问题——本文主结果不在其列。
问 1：整条证明链里哪一步最要害、也最脆弱？
答：第 6 节的切向微分。秩一极限先给出范数恒等式 b(v₀u′−u₀v′,y)=‖P(v)B(y)R(u)‖²_op，随后要在核投影 R(u) 的常数秩邻域内沿球面路径求一阶变分，得到元素均为双线性型、逐元素平方不超过 b 的矩阵 F。可微性论证是全文技术最密、最容易出细节问题的一环；所幸主定理已有 Lean 形式化背书。
问 2：为什么必须对”任意矩阵尺寸、任意线性填法”一并否定？
答：几何版广义 Lax 猜想断言的是存在某个有限尺寸的表示；只排除小矩阵或特定填法都不算推翻。定理 1.1 对每个有限 N 与每个实线性映射 L 都否定，且引言明确实对称框架已覆盖 Hermitian 铅笔（经 A+iB 到分块实对称的等价），堵住了换数域的绕行。
问 3：与已有工作相比真正的新意是什么？
答：以往反例停留在多项式层面：某个双曲多项式没有行列式表示，但同一个锥仍可能被另一支铅笔定义。本文首次在锥的层面工作，且不比较假设铅笔的行列式与 p，而是经重标度 (I₄,s²Z₀,sy) 与核投影变分，从锥的几何中逼出 Choi–Lam 型本身，再由其弱极端性收网。
问 4：为什么弱极端性是收网的那一环，换别的性质行吗？
答：Choi–Lam 型 b 非负、非零，但并不极端；它满足的是弱极端性——平方处处不超过 b 的双线性型必恒为零。证明恰好只需要这条：F 的每个元素平方 ≤‖F‖²_op=b。若只知 b 非负，矩阵元素可以非零，矛盾链就断了。第 2 节用零点与四阶消失曲线给出的短证明，是这条性质的来源。
问 5：23 个变量、16 次是精挑细选的吗？
答：不是，论文明确声明不主张维数或次数极小。20 次由公式自然给出，推论 1.2 除掉因子 det X 得到 16 次同锥多项式，属顺手加固。最小维数与最小次数问题论文未展开。
问 6：这类 AI 参与生成的证明最可能在哪里出错？
答：典型风险是”局部代数看似显然”的步骤：双曲性的上半平面论证、切片 X≻0 当且仅当 Z⪰Φ_y(X⁻¹) 的计算、伴随矩阵展开中的符号错误。这些地方一旦写错，全局矛盾仍可能”形式上通”。本文的保险是主结果已形式化，未形式化的部分（如次数归约）风险相对集中。
问 7：这个反例杀死了什么、又没杀死什么？谁会用到它？
答：杀死的只是”原坐标下的谱面表示”。姊妹篇证明同一个锥其实有 100×100、307 个辅助变量的精确半定提升，即它是谱面影子；同族另一构造则给出连影子都不是的锥。做双曲规划、谱图理论的优化理论学者会用它校准”双曲规划可否归约为半定规划”这一问题的答案边界。
总评
这是几何版广义 Lax 猜想的第一个锥级显式反例，且有 Lean 形式化托底，分量实打实。最大风险在切向微分一步的未形式化细节，以及把”非谱面”误读为”与半定世界彻底无关”的过度引申。