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 subspaces of the argument into orbits under the 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 three 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). Instantiating it for polynomial multiplication, we obtain eighteen new lower bounds over $\mathbb{F}_2$ and $\mathbb{F}_3$, for the full product, cyclic convolution, and the truncated (modulo $x^N$) and negacyclic (modulo $x^N+1$) products. Every bound is backed by a machine-checkable certificate.

翻译：暂无翻译