在Lean 4中机器检查的非奇异方阵的Kannan - Bachem史密斯标准型的算术位复杂度
Machine-Checked Arithmetic Bit Complexity of the Kannan-Bachem Smith Normal Form in Lean 4
浏览论文内容
中文总结 AI 辅助
研究非奇异方阵的Kannan - Bachem史密斯标准型算法，在Lean 4中形式化，通过递归减小枢轴二进制大小实现稳定终止，生成算术叶跟踪，用自定界编解码器定义输入输出大小，给出跟踪成本和矩阵编码长度的多项式界。
中文摘要 AI 辅助
我们在Lean 4中形式化了非奇异方阵的Kannan - Bachem史密斯标准型算法。该程序返回\(S,U,U^{-1},V,V^{-1}\)并证明\(UAV = S\)，\(U^{-1}SV^{-1}=A\)等。稳定终止是因为每次递归严格减小活动枢轴的二进制大小。计算还生成指定符号大小算术叶的扁平跟踪。通过连接子执行返回的电荷列表形成复合阶段的跟踪。验证的自定界编解码器定义输入和输出大小。系数和工作递归给出跟踪成本和五个输出矩阵编码长度的固定多项式界。
英文摘要
We formalize in Lean 4 the Kannan-Bachem Smith normal form algorithm for nonsingular square integer matrices. The program returns $S,U,U^{-1},V,V^{-1}$ and proves $UAV=S$, $U^{-1}SV^{-1}=A$, four inverse identities, the Smith divisibility conditions, and equality of $S$ with a canonical reference matrix. Stabilization terminates because each recursive pass strictly decreases the binary size of the active pivot; the outer algorithm recurses on the lower-right block. The computation also emits a flat trace of designated sign-magnitude arithmetic leaves. Branch conditions, quotients, Bezout data, and matrix entries are taken from the recorded primitive runs. Composite phases form their traces by concatenating the charge lists returned by the executed children. Verified self-delimiting codecs define the input and output sizes. Coefficient and work recurrences, closed by a kernel-checked polynomial-envelope calculus, give fixed polynomial bounds for both trace cost and the encoded length of the five output matrices. The theorem concerns these arithmetic primitives; structural operations and compiled Lean runtime are outside the model.
