We present a general, automated framework for proving lower bounds on the bilinear complexity (tensor rank) of multiplication problems over a finite field $\mathbb{F}_q$. The framework is parameterized only by the multiplication tensor and by a group of rank-preserving symmetries acting on one argument: it classifies the orbits of constraint subspaces under that group, runs a dynamic program over the orbits combining four lower-bound techniques, and emits a proof certificate that a verifier rechecks, typically faster than the search. Instantiating the framework for matrix multiplication, we improve the lower bounds for several small formats over $\mathbb{F}_2$, most notably showing that the bilinear complexity of multiplying two $3 \times 3$ matrices over $\mathbb{F}_2$ is at least $20$ -- raising the bound of $19$ that had stood since Bläser (2003). The search algorithm finds this proof in under an hour on a laptop, and the certificate verifies in seconds. Instantiating it for polynomial multiplication, we obtain eight new lower bounds for full and cyclic multiplication over $\mathbb{F}_2$ and $\mathbb{F}_3$. Every bound in this paper is backed by a machine-checkable certificate.

翻译：暂无翻译