Lieb 永久积支配猜想对普通 immanant 在阶数至 15 时的证明
Lieb's Permanental Dominance Conjecture for Ordinary Immanants through Order Fifteen
浏览论文内容
中文总结 AI 辅助
本文解决了 Pate 遗留的 (4,4,3,3)、(5,4,3,3) 和 (3^5) 三个情形，从而证明了 n≤15 时所有普通 immanant 的 Lieb 永久积支配猜想，并给出超越有限前沿的族结果及 Lean 4 形式化验证。
中文摘要 AI 辅助
Pate 证明了阶数至 13 的普通不可约 immanant 永久积支配，并确定 (4,4,3,3) 为阶数 14 的唯一剩余情形，而 (5,4,3,3) 和 (3^5) 构成阶数 15 的前沿。这三个情形在此得到解决；因此，对于每个满足 n≤15 的划分 λ⊢n 以及每个复 Hermitian 半正定矩阵 A，有 d_λ(A)/f^λ ≤ per(A)。该论证还产生了超越此有限前沿的结果：针对 (4,4,3,3) 的精确四项桥接，一致族 (m,4,3,3)，满足 a≥b≥4 且 5a≥8b 的双参数族 (a,b,3,3)，以及针对任意固定尾部的长首行准则。这些结果源于对 Pate 的 W-函数正性框架的显式特化，使用了部分交换、Young 投影子、Pieri-内容恒等式和分支数据。对于 (3^5)，一个精确的 Farkas 证书表明中心投影子部分交换锥不足；一个分支细化的单交换构造绕过了此障碍，并产生一个正的 106+19 见证证书。边界压缩和节点移动结果进一步描述了局部过滤方法的可达范围和局限性。所有有限证书均通过精确整数或有理数算术检查，并作为辅助材料提供。阶数 14 的桥接还在 Lean 4 中对所有复 Hermitian 半正定矩阵进行了形式化和核检查，包括精确系数归一化以及从四个明确陈述的 Pate 不等式推导出 (4,4,3,3) 永久积支配。
英文摘要
Pate proved ordinary irreducible-immanant permanental dominance through order $13$ and identified $(4,4,3,3)$ as the sole remaining order-$14$ case, with $(5,4,3,3)$ and $(3^5)$ forming the order-$15$ frontier. These three cases are settled here; consequently $d_λ(A)/f^λ\le \operatorname{per}(A)$ for every partition $λ\vdash n$ with $n\le15$ and every complex Hermitian positive-semidefinite matrix $A$. The argument also yields results beyond this finite frontier: an exact four-term bridge for $(4,4,3,3)$, the uniform family $(m,4,3,3)$, a two-parameter family $(a,b,3,3)$ for $a\ge b\ge4$ and $5a\ge8b$, and a long-first-row criterion for arbitrary fixed tails. These results arise from explicit specializations of Pate's $W$-function positivity framework using partial swaps, Young projectors, Pieri--content identities, and branching data. For $(3^5)$, an exact Farkas certificate shows that the central-projector partial-swap cone is insufficient; a branching-refined one-swap construction escapes this obstruction and yields a positive $106+19$-witness certificate. Boundary-compression and node-moving results further describe the reach and limitations of the local-filter method. All finite certificates are checked by exact integer or rational arithmetic and are supplied as ancillary material. The order-$14$ bridge is additionally formalized and kernel-checked in Lean 4 for all complex Hermitian positive-semidefinite matrices, including the exact coefficient normalization and the deduction of $(4,4,3,3)$ permanental dominance from four explicitly stated Pate inequalities.
