关于 $\mathbb F_2$ 上 $3\times3$ 矩阵乘法下界 21 的结构性证明
A Structural Proof of the Lower Bound 21 for $3\times3$ Matrix Multiplication over $\mathbb F_2$
浏览论文内容
中文总结 AI 辅助
本文通过结构性证明，利用占用约束、商秩界和有限几何，证明了 $\mathbb F_2$ 上 $3\times3$ 矩阵乘法张量秩至少为 21，并在 Lean 中形式化验证。
中文摘要 AI 辅助
我们证明了 $\mathbb F_2$ 上 $3\times3$ 矩阵乘法的张量秩至少为 $21$。该结构性证明由 Qiushi Engine 独立开发，将单个张量因子上的占用约束转化为耦合所有三个因子的代数关系。经过认证的商秩界和有限几何迫使任何假设的 $20$ 项分解具有第一因子矩阵秩轮廓 $(16,1,3)$。因此，相应的分裂展平和项秩之和为 $27$，恰好等于完整分裂展平的秩。秩次可加性中的等式迫使它们的像形成直和；通过逆展平归一化后，使各项成为成对湮灭的幂等元。矩阵乘法的显式乘积恒等式意味着至多一个第一因子可逆，这与轮廓所强制的三个可逆因子相矛盾。同样的障碍约束了达到分裂秩界的 $22$ 项分解。完整证明（包括有限商界）已在 Lean 中形式化。随附的研究轨迹记录了 Qiushi Engine 从数值实验和商构造到结构性证明的长期自主研究过程。
英文摘要
We prove that the tensor rank of $3\times3$ matrix multiplication over $\mathbb F_2$ is at least $21$. The structural proof, independently developed by Qiushi Engine, converts occupation constraints on a single tensor factor into algebraic relations coupling all three factors. Certified quotient-rank bounds and finite geometry force any hypothetical $20$-term decomposition to have first-factor matrix-rank profile $(16,1,3)$. The ranks of the corresponding split-flattened summands therefore sum to $27$, exactly the rank of the full split flattening. Equality in rank subadditivity forces their images to form a direct sum; normalization by the inverse flattening then makes the summands pairwise annihilating idempotents. An explicit product identity for matrix multiplication implies that at most one first factor can be invertible, contradicting the three forced by the profile. The same obstruction constrains $22$-term decompositions attaining the split-rank bound. The complete proof, including the finite quotient bounds, is formalized in Lean. The accompanying research trajectory records Qiushi Engine's long-horizon autonomous research, from numerical experiments and quotient constructions to the structural proof.
发表机构
- College of Information Science and Electronic Engineering, Zhejiang University（浙江大学信息科学与工程学院）
机构由 AI 辅助整理，请以论文原文为准。
