The Colomo-Pronko 猜想：关于冻结角交错符号矩阵
The Colomo-Pronko conjecture for frozen-corner alternating sign matrices
浏览论文内容
中文总结 AI 辅助
本文证明 Colomo-Pronko 猜想对所有大小和冻结参数的角冻结交错符号矩阵成立，通过行列式核与逆恒等式建立联系，并利用 Lean 4 形式化证明，从而移除 GUE Tracy-Widom 涨落定理中的猜想假设。
中文摘要 AI 辅助
我们证明了 Colomo-Pronko 猜想对于在角部具有指定零方块的交错符号矩阵成立，适用于所有矩阵大小和冻结参数。已知的冻结角计数的多重积分公式产生了由固定多项式核构建的行列式表示。我们通过一个涉及带反转的符号 Pascal 矩阵的交换子的逆恒等式，将这些核与猜想中的行列式联系起来。在奇数维情形下，比较利用一维零空间及其上的投影来消除中心坐标。结合 Colomo 和 Pronko 的渐近分析，我们的结果从他们关于均匀随机交错符号矩阵中冻结边界与主对角线交点的 GUE Tracy-Widom 涨落定理中移除了猜想性假设。证明的有限维代数核心已在 Lean 4 中形式化。
英文摘要
We prove the Colomo-Pronko conjecture for alternating sign matrices with a prescribed square of zeros at a corner, for all matrix sizes and freezing parameters. A known multiple-integral formula for the frozen-corner count yields determinant representations built from fixed polynomial kernels. We relate these kernels to the conjectured determinant through an inverse identity for the commutator of a signed Pascal matrix with reversal. In odd dimension, the comparison uses the one-dimensional nullspace and projection along it to eliminate the central coordinate. Combined with the asymptotic analysis of Colomo and Pronko, our result removes the conjectural assumption from their GUE Tracy-Widom fluctuation theorem for the intersection of the frozen boundary with the main diagonal in uniformly random alternating sign matrices. The finite-dimensional algebraic core of the proof has been formalized in Lean 4.
