\documentclass[11pt]{amsart} \pdfsuppressptexinfo=-1 \usepackage[margin=1.1in]{geometry} \usepackage{amsmath,amssymb,amsthm,mathtools} \usepackage{booktabs,enumitem} \usepackage[hidelinks]{hyperref} \hypersetup{pdftitle={The rank of 3x3 matrix multiplication over F2 is 23}, pdfauthor={Tejasvi Singh Tomar}} \newtheorem{theorem}{Theorem}[section] \newtheorem{lemma}[theorem]{Lemma} \newtheorem{proposition}[theorem]{Proposition} \newtheorem{corollary}[theorem]{Corollary} \theoremstyle{definition} \newtheorem{definition}[theorem]{Definition} \theoremstyle{remark} \newtheorem{remark}[theorem]{Remark} \numberwithin{equation}{section} \setlength{\emergencystretch}{2em} \newcommand{\F}{\mathbb{F}_2} \newcommand{\Z}{\mathbb{Z}} \newcommand{\GL}{\mathrm{GL}_3(\F)} \newcommand{\mm}{\langle 3,3,3\rangle} \newcommand{\rk}{\operatorname{rank}} \newcommand{\lb}{\operatorname{lb}} \newcommand{\cp}{\operatorname{cap}} \newcommand{\cS}{\mathcal{S}} \newcommand{\cK}{\mathcal{K}} % \newcommand{\TBD}[1]{\textbf{[#1]}} % \newcommand{\RUN}[1]{\textbf{[run: \detokenize{#1}]}} \begin{document} \title{The rank of $3\times 3$ matrix multiplication over $\F$ is $23$} \author{Tejasvi Singh Tomar} \renewcommand{\urladdrname}{{\itshape ORCID}} \urladdr{\href{https://orcid.org/0000-0003-4668-3639}{https://orcid.org/0000-0003-4668-3639}} \subjclass[2020]{68Q17, 15A69; 68V05, 68V15} \keywords{Matrix multiplication, tensor rank, bilinear complexity, lower bounds, finite fields, substitution method, computer-assisted proof, formal verification, Lean} \begin{abstract} The rank of the tensor of $3\times 3$ matrix multiplication over the field with two elements is at most $23$ by Laderman's algorithm, and Rudich and Rousseau recently proved that it is at least $22$. We prove that it equals $23$. Hence Laderman's algorithm uses the fewest multiplications among all bilinear algorithms over $\F$ and among all bilinear algorithms with integer coefficients. The proof uses the substitution method in the form developed by D'Ambrosio, Wang and Yang et al., which bounds the number of first factors of a decomposition that lie in a given subspace of the space of first factors. We sharpen these bounds for $111$ of Wang's $496$ classes of subspaces, constrain the ranks of the first factors through a $27\times 27$ flattening of the tensor, and list, up to symmetry, all sets of $22$ first factors that satisfy these constraints. An exact completion search shows that none of them is the set of first factors of a decomposition. The computation emits certificates, which are checked in the Lean~4 proof assistant. In one formal proof the largest checks are evaluated as compiled code, and in a second one the kernel evaluates every check, so that its final theorem depends only on the three standard axioms of Lean. The Lean proofs build on the formalization of Rudich and Rousseau and import their table of bounds and their reduction for block algorithms. \end{abstract} \maketitle \section{Introduction}\label{sec:intro} Let $\mm$ be the tensor of $3\times 3$ matrix multiplication. Its rank $R_K(\mm)$ over a field $K$ is the smallest number of multiplications in a bilinear algorithm over $K$ that computes the product of two $3\times 3$ matrices \cite[Ch.~14]{BCS97}. Laderman's algorithm \cite{Lad76} uses $23$ multiplications. It does not use commutativity and its coefficients are $0$ and $\pm1$, so it works over any ring, and $R_K(\mm)\le 23$ for all fields $K$. For $2\times 2$ matrices the question was settled half a century ago: Strassen's algorithm uses $7$ multiplications \cite{Str69}, and Hopcroft and Kerr \cite{HK71} and Winograd \cite{Win71} proved that $7$ are necessary. For $3\times 3$ matrices, however, the best lower bound valid over all fields is $19$, due to Bläser \cite{Bla03}, and whether Laderman's $23$ multiplications are necessary has been open since 1976. Over $\F$ the lower bound has risen several times in 2026. C.~Wang proved $R_{\F}(\mm)\ge 20$ with an automated method that splits the problem into $496$ classes of subspaces \cite{Wan26a}, and Beuchert checked his certificate independently \cite{Beu26}. Wang \cite{Wan26b} and, independently, Yang et al.\ \cite{Yan26} then proved $R_{\F}(\mm)\ge 21$, and Yang et al.\ formalized their proof in Lean. Tahir independently obtained $21$ conditionally on bounds from Wang's table \cite{Tah26}. Rudich and Rousseau proved $R_{\F}(\mm)\ge 22$, also in Lean \cite{RR26}. This left the question whether $22$ multiplications suffice over $\F$, and we show that they do not. \begin{theorem}\label{thm:main} $R_{\F}(\mm)=23$. \end{theorem} A bilinear algorithm with integer coefficients becomes a bilinear algorithm over $\F$ with the same number of multiplications when its coefficients are reduced modulo $2$. An algorithm with integer constants that can be applied to blocks of matrices cannot use commutativity, and by the argument of Hopcroft and Kerr \cite{HK71} a lower bound over $\F$ applies to it as well. Rudich and Rousseau explain this reduction and formalize it in Lean \cite{RR26}. Theorem~\ref{thm:main} therefore has the following consequence. \begin{corollary}\label{cor:integer} A bilinear algorithm over $\F$ or with integer coefficients that multiplies two $3\times 3$ matrices uses at least $23$ multiplications. In particular $R_{\Z}(\mm)=23$, and no recursive $3\times3$ algorithm with integer constants has an exponent below $\log_3 23\approx 2.854$. \end{corollary} Over fields of characteristic zero the rank of $\mm$ is still unknown. It lies between $19$ and $23$. \subsection*{The method} The proof is a computation organized by the substitution method \cite{Pan66,AFT11,LM17,Bla03,Bla13}. Let $A$ be the space of first factors. For a subspace $S\subseteq A$ let $R(S)$ be the rank of $\mm$ modulo $S$, that is, the rank of the problem in which the first input is restricted to the annihilator of $S$. In a decomposition of length $r$ at most $r-R(S)$ terms have their first factor in $S$ (Lemma~\ref{lem:cap}). For $r=22$ this bounds the number of first factors that each subspace can contain, the \emph{capacity} of the subspace. Wang bounded $R(S)$ for representatives of the $496$ orbits of subspaces under the symmetries of $\mm$ \cite{Wan26a}, and Rudich and Rousseau improved these bounds \cite{RR26}. In Section~\ref{sec:raise} we raise the lower bound for $111$ classes of their table. For most of them we enumerate the possible first factors of a hypothetical shorter decomposition of the quotient and refute each candidate. The others follow from these by monotonicity. The most useful new bound is $R(S)\ge 21$ for a point $S$ spanned by a matrix of rank one. With the bounds of \cite{RR26} for the other two classes of points it shows that the $22$ first factors of a decomposition of length $22$ are distinct. By Lemma~\ref{lem:cap}, decompositions of length $23$ give upper bounds, and those of a collection of Kauers \cite{Kau} show that most of the new bounds are best possible. Section~\ref{sec:types} constrains the numbers $n_1,n_2,n_3$ of first factors of rank $1$, $2$ and~$3$. These constraints come from a $27\times 27$ flattening of $\mm$ to which each term contributes the rank of its first factor, and hence $n_1+2n_2+3n_3\ge 27$. A Gram-matrix form of the identity behind this inequality excludes eight types $(n_1,n_2,n_3)$, three of them by short arguments and five by an exhaustive computation. Section~\ref{sec:l479} shows that, if at least $14$ first factors have rank one, no line in a certain orbit of $441$ lines contains two first factors, although the capacity of these lines is $2$. The proof assumes two first factors on such a line, enumerates the possible projections of the other $20$ terms and shows that none of them lifts back to a decomposition of $\mm$. With these constraints we enumerate, up to the symmetry group of order $56{,}448$, all sets of $22$ nonzero matrices in $\F^{3\times 3}$ that satisfy them (Section~\ref{sec:search}). An exact search then tries to complete each set to a decomposition (Section~\ref{sec:tsolve}), and fails for every one of them. \subsection*{Relation to earlier work} Capacities, coset profiles, the symmetry-reduced enumeration of first factors and the deduction that the first factors are distinct come from the work of D'Ambrosio \cite{DAm26}, Wang \cite{Wan26a,Wan26b} and Yang et al.\ \cite{Yan26}, and the split flattening is due to Yang et al. In the proofs of $R_{\F}(\mm)\ge 21$ the conditions on the first factors alone exclude all cases. At $r=22$ they do not, and most of the work lies in refuting the sets of first factors that survive, by an exhaustive search for the second and third factors (Section~\ref{sec:tsolve}). Certificates that branch on these factors also occur in the Lean proof of \cite{RR26}. What is new here is this refutation step, applied to all $75{,}327{,}600$ sets that survive the search at $r=22$ (Table~\ref{tab:search}), the new lower bounds of Table~\ref{tab:raise}, the type exclusions of Proposition~\ref{prop:types} and Theorem~\ref{thm:l479}. \subsection*{Verification} Sections~\ref{sec:verify} and~\ref{sec:kernel} describe the verification. The searches emit certificates, which are verified by checkers written in Lean. The soundness of each checker is a theorem of Lean proved with its three standard axioms. There are two formal proofs. In the first, the checks for the search at $r=22$ and for the largest enumerations are evaluated as compiled code through \texttt{native\_decide}, which adds one axiom for each evaluation. This proof therefore depends on the Lean compiler and runtime as well as on the kernel. In the second (Section~\ref{sec:kernel}), the kernel evaluates every check, and its final theorem depends only on the axioms \texttt{propext}, \texttt{Classical.choice} and \texttt{Quot.sound}. Laderman's algorithm is also checked in Lean, which makes the equality $R_{\F}(\mm)=23$ a theorem there, and the bound of Corollary~\ref{cor:integer} for algorithms with integer constants that can be applied to blocks is derived in the formulation of \cite{RR26}. Statements marked with $\dagger$ depend on a computation. \section{Preliminaries}\label{sec:prelim} \subsection{The tensor} Let $A=B=C=\F^{3\times 3}$ and let $e_{ij}$ be the matrix units. We write \[ T=\mm=\sum_{i,j,k=1}^{3} e_{ij}\otimes e_{jk}\otimes e_{ki}\in A\otimes B\otimes C . \] A \emph{decomposition of length $r$} is an expression $T=\sum_{s=1}^{r}a_s\otimes b_s\otimes c_s$, and the rank of $T$ is the least such $r$. We call $a_s$ the \emph{first factors}. When $T$ has a decomposition of length $r$ it also has one of length $r+1$: replace a term $a\otimes b\otimes c$ by $a\otimes b\otimes c'+a\otimes b\otimes(c+c')$ with $c'\notin\{0,c\}$. In a decomposition of length $22$ all factors are nonzero, since otherwise $T$ would have a decomposition of length $21$, contrary to \cite{RR26}. For a first factor $a$ we write $B$ and $C$ for the second and third factors read as matrices in the index order of $T$. Thus $b=\sum B_{jk}e_{jk}$ and $c=\sum C_{ki}e_{ki}$, and the triple $(a,b,c)$ is identified with $(a,B,C)$. \subsection{Symmetries} For $P,Q,R\in\GL$ the map \begin{equation}\label{eq:sym} (a,B,C)\mapsto (PaQ^{-1},\ QBR^{-1},\ RCP^{-1}) \end{equation} fixes $T$, because $Q^{-1}$ and $Q$ cancel on the index $j$ shared by the first two factors, and $R$ and $P$ cancel in the same way on $k$ and $i$. So does $(a,B,C)\mapsto(a^{\mathsf T},C^{\mathsf T},B^{\mathsf T})$, which permutes the terms of $T$. Both maps send decompositions to decompositions of the same length. On first factors they generate the group $G$ of maps $a\mapsto PaQ$ and $a\mapsto Pa^{\mathsf T}Q$ with $P,Q\in\GL$. It has order $2\cdot 168^2=56{,}448$ and preserves the rank of a matrix. The space $A$ contains $511$ nonzero matrices, of which $49$ have rank one, $294$ rank two and $168$ rank three. The group $G$ acts transitively on each of these three sets. \subsection{Quotients and capacities}\label{subsec:quot} For a subspace $S\subseteq A$ let $\pi_S\colon A\to A/S$ be the projection and $T_S=(\pi_S\otimes 1\otimes 1)(T)$. We write $R(S)$ for the rank of $T_S$. If $S\subseteq S'$ then $R(S')\le R(S)$, and $R(gS)=R(S)$ for $g\in G$. \begin{lemma}[{\cite[\S4]{DAm26}}, {\cite[Lemma~2.1]{Wan26b}}, {\cite[Lemma~2.2]{Yan26}}]\label{lem:cap} If $T=\sum_{s=1}^{r}a_s\otimes b_s\otimes c_s$, then for every subspace $S\subseteq A$ \[ \#\{s : a_s\in S\}\le r-R(S). \] \end{lemma} \begin{proof} Applying $\pi_S\otimes 1\otimes 1$ removes the terms with $a_s\in S$ and leaves a decomposition of $T_S$ of length $\#\{s:a_s\notin S\}$. \end{proof} We call a subspace of dimension $1$ a \emph{point} and one of dimension $2$ a \emph{line}. Wang sorted the subspaces of $A$ into $496$ classes up to the action of $G$ \cite{Wan26a}. A \emph{table} assigns to each class a number $\lb(S)\le R(S)$. At $r=22$ the \emph{capacity} of $S$ is $\cp(S)=22-\lb(S)$, and Lemma~\ref{lem:cap} says that a subspace contains at most $\cp(S)$ first factors of a decomposition of length $22$. We start from the table of Rudich and Rousseau, which gives $R(S)$ exactly for $359$ classes and lower bounds for the others \cite{RR26}. In this table $R(\{0\})\ge 22$, and $R(S)\ge 21$ for the points spanned by matrices of rank two and three. In our data the classes are numbered as in the Lean table of \cite{RR26}, which lists a basis of a representative of each class. The case $S=\ker\varphi$ of a hyperplane will be used often. Here $\varphi\colon A\to\F$ is a nonzero linear form, which we write as $\varphi(a)=\sum_{i,j}x_{ij}a_{ij}$ with a matrix $x\ne 0$, and we set $\rk\varphi=\rk x$. Contracting $T$ with $\varphi$ gives the $9\times 9$ matrix $T(\varphi)=\sum_{i,j,k}x_{ij}\, e_{jk}\otimes e_{ki}$. It consists of three copies of $x^{\mathsf T}$, one for each value of $k$, and so has rank $3\rk\varphi$. Hence $R(\ker\varphi)=3\rk\varphi$, and Lemma~\ref{lem:cap} becomes the statement that at least $3\rk\varphi$ first factors satisfy $\varphi(a_s)=1$. \section{Lower bounds for quotients}\label{sec:raise} \subsection{Coset profiles}\label{subsec:profiles} Let $S$ be a subspace and $\ell$ an integer. To prove $R(S)\ge\ell$ we assume that $T_S$ has a decomposition of length $\ell-1$, which we may take with all factors nonzero (Section~\ref{sec:prelim}). Its first factors are nonzero cosets $\bar a_1,\dots,\bar a_{\ell-1}$ of $S$. Let $n(x)$ be the number of $t$ with $\bar a_t=x$. Applying Lemma~\ref{lem:cap} to the decomposition of $T_S$ and a superspace $S'\supseteq S$ gives (compare \cite[Lemma~2.2]{Yan26}) \begin{equation}\label{eq:coset} \sum_{0\ne x\in S'/S} n(x)\le \ell-1-R(S')\le \ell-1-\lb(S'). \end{equation} We call a function $n$ with $\sum_x n(x)=\ell-1$ that satisfies \eqref{eq:coset} for all $S'$ a \emph{coset profile}. The coset profiles are the integer points of a polytope with one coordinate per nonzero coset. We enumerate them up to the stabilizer of $S$ in $G$, or for six classes up to a subgroup of it, by an orderly branch and bound in which linear-programming bounds prune the branches. We then refute each coset profile by the completion search of Section~\ref{sec:tsolve} with target $T_S$. If all coset profiles are refuted, then $R(S)\ge\ell$. The bounds $\lb(S')$ used in \eqref{eq:coset} belong to strict superspaces of $S$, so we establish new bounds in decreasing order of $\dim S$. \subsection{Points} \begin{theorem}[$\dagger$]\label{thm:point} If $S$ is spanned by a matrix of rank one, then $R(S)\ge 21$. \end{theorem} Here $A/S$ has $255$ nonzero cosets and the stabilizer of $S$ in $G$ has order $1152$. The enumeration of coset profiles of size $20$ has $809{,}336{,}049$ nodes and $7{,}409{,}768$ leaves, and all leaves are refuted. \begin{corollary}[$\dagger$]\label{cor:distinct} The $22$ first factors of a decomposition of length $22$ are pairwise distinct. \end{corollary} \begin{proof} A repeated first factor $a$ would put two first factors in the point $\F a$. By Theorem~\ref{thm:point} and \cite{RR26} all points have $R\ge 21$ and therefore capacity at most $1$. \end{proof} \subsection{The other classes} Table~\ref{tab:raise} lists the new bounds by dimension. We proved $88$ of them, among them Theorem~\ref{thm:point}, by the method of Section~\ref{subsec:profiles}. The other $23$ follow by monotonicity: for each of them some $gS$ with $g\in G$ is contained in a subspace $S'$ of larger dimension whose new bound is at least as large, and $R(S)=R(gS)\ge R(S')$. These are the bound $19\to 20$ for one class of dimension $2$, the bound $18\to 19$ for eight classes of dimension $3$, the bound $16\to 17$ for three classes of dimension $4$, and the bound $17\to 18$ for eleven classes of dimension $4$. For $106$ of the $111$ classes the new bound equals the upper bound of \cite{RR26}. \begin{proposition}[$\dagger$]\label{prop:raise} The lower bounds of Table~\ref{tab:raise} hold. \end{proposition} \begin{table}[ht] \caption{New lower bounds on $R(S)$, by $\dim S$. A class is listed under the bound of \cite{RR26} and the new bound. The number in parentheses in the second column counts the classes whose new bound follows by monotonicity. The last two columns give the size of the enumerations of Section~\ref{subsec:profiles}.}\label{tab:raise} \centering \small \begin{tabular}{@{}ccp{0.36\textwidth}rr@{}} \toprule $\dim S$ & classes & bounds & enumeration nodes & leaves\\ \midrule $1$ & $1$ & $20\to 21$ & $809{,}336{,}049$ & $7{,}409{,}768$\\ $2$ & $4$ ($1$) & $19\to 20$ (1), $20\to 21$ (3) & $26{,}301{,}783{,}827$ & $5{,}211{,}895{,}431$\\ $3$ & $35$ ($8$) & $18\to 19$ (17), $19\to 20$ (18) & $3{,}654{,}254{,}117$ & $969{,}245{,}867$\\ $4$ & $50$ ($14$) & $16\to 17$ (8), $17\to 18$ (23), $18\to 19$ (19) & $46{,}041{,}278$ & $15{,}998{,}835$\\ $5$ & $21$ & $16\to 17$ (5), $16\to 18$ (1), $17\to 18$ (15) & $1{,}089{,}004$ & $349{,}120$\\ \bottomrule \end{tabular} \end{table} \subsection{Upper bounds}\label{subsec:upper} Lemma~\ref{lem:cap} also gives upper bounds: if a decomposition of length $23$ has $k$ first factors in $S$, then $R(S)\le 23-k$. We apply this to the collection of schemes of length $23$ that Kauers made available \cite{Kau}. It consists of the $64{,}150$ schemes in the data set of \cite[\S6]{KM22}, which extends that of \cite{HKS21}, and nine named schemes. Of its $64{,}159$ files, $62{,}239$ are decompositions over $\F$,\footnote{Each of the other $1{,}920$ files becomes a decomposition when one factor of one product is changed. These changes are listed in our data.} and we use each of them three times, once with each of its three factors in the role of the first factor. For $406$ of the $496$ classes, among them $103$ of the $111$ classes of Table~\ref{tab:raise}, one of these decompositions has $23-\lb(S)$ first factors in a subspace of the class, and hence $R(S)=\lb(S)$. For classes $293$ and $488$ in the numbering of \cite{RR26}, which keep the bounds of \cite{RR26}, the upper bounds obtained in this way are new, and they give $R(S)=17$ and $R(S)=20$, respectively. For class $473$ of Table~\ref{tab:raise} the new upper bound is $20$, which equals its new lower bound. Hence $R(S)$ is now known exactly for $107$ of the $111$ classes of Table~\ref{tab:raise}, namely class $473$ and the $106$ whose new bound equals the upper bound of \cite{RR26}. For class $468$ the collection gives $R(S)\le 20$, against the lower bound $19$. For example, one decomposition in the collection has the three matrices $I$, $e_{12}+e_{13}+e_{31}$ and their sum among its first factors. They are the three nonzero elements of a line of class $488$ and lie in planes of classes $468$ and $473$. By Lemma~\ref{lem:cap} this gives the bound $20$ for these three classes. For every class, our data list a decomposition with the largest number of first factors in a subspace of the class. \section{The ranks of the first factors}\label{sec:types} In this section we consider a decomposition $T=\sum_{t=1}^{r}a_t\otimes b_t\otimes c_t$ with all factors nonzero. Its \emph{type} is $(n_1,n_2,n_3)$, where $n_q$ is the number of first factors of rank $q$. We write $r_t=\rk(a_t)$ and $\Delta=\sum_t r_t-27$. \subsection{The split flattening} Index the rows of a $27\times 27$ matrix by pairs $(i,\beta)$ and the columns by pairs $(j,\gamma)$, where $i,j\in\{1,2,3\}$ and $\beta,\gamma$ run over the nine matrix positions. For $a\in A$, $b\in B$, $c\in C$ let $M(a,b,c)$ be the matrix with entries $a_{ij}b_\beta c_\gamma$. Its rank is $\rk(a)$ when $b,c\ne 0$, since $M(a,b,c)$ is the Kronecker product of $a$ and $bc^{\mathsf T}$ up to the order of indices. Let $P=\sum_t M(a_t,b_t,c_t)$. By linearity $P$ depends only on $T$, and its only nonzero entries are $P_{(i,jk),(j,ki)}=1$. Thus $P$ is a permutation matrix. \begin{lemma}[{\cite[(4.2)]{Yan26}}]\label{lem:split} $\sum_t\rk(a_t)\ge 27$, that is, $\Delta\ge 0$. \end{lemma} \begin{proof} $27=\rk P\le\sum_t\rk M(a_t,b_t,c_t)=\sum_t\rk(a_t)$. \end{proof} For a decomposition of length $22$ we have $\Delta=n_2+2n_3-5$, so Lemma~\ref{lem:split} gives $n_2+2n_3\ge 5$. \subsection{The Gram form} The inequality of Lemma~\ref{lem:split} does not use how the terms fit together. The following factorization of $P$ records this information as equations between pairs of terms. Factor each first factor as $a_t=L_tR_t^{\mathsf T}$ with $L_t,R_t\in\F^{3\times r_t}$. Let $X$ be the $27\times(27+\Delta)$ matrix whose column blocks are $L_t\otimes b_t$, with rows indexed like the rows of $P$, and let $Y$ be the $27\times(27+\Delta)$ matrix with column blocks $R_t\otimes c_t$, with rows indexed like the columns of $P$. Then $M(a_t,b_t,c_t)=(L_t\otimes b_t)(R_t\otimes c_t)^{\mathsf T}$, so $P=XY^{\mathsf T}$. \begin{lemma}\label{lem:gram} The matrix $\Gamma=Y^{\mathsf T}P^{-1}X$ is idempotent of rank $27$, and $\Pi=I+\Gamma$ is idempotent of rank $\Delta$. Its blocks are \begin{equation}\label{eq:gram} \Gamma_{ts}=R_t^{\mathsf T}B_sC_tL_s . \end{equation} \end{lemma} \begin{proof} $\Gamma^2=Y^{\mathsf T}P^{-1}(XY^{\mathsf T})P^{-1}X=\Gamma$. The rank of $\Gamma$ is at most $27$, and $X\Gamma Y^{\mathsf T}=P$ has rank $27$, so $\rk\Gamma=27$. Over $\F$ the matrix $I+\Gamma=I-\Gamma$ is the complementary idempotent, of rank $(27+\Delta)-27$. For \eqref{eq:gram}, $P^{-1}=P^{\mathsf T}$ and $P^{\mathsf T}_{(j,\gamma),(i,\beta)}=1$ exactly when $\beta=jk$ and $\gamma=ki$ for some $k$. Hence the $(\alpha,\alpha')$ entry of $\Gamma_{ts}$ is $\sum_{i,j,k}(R_t)_{j\alpha}(B_s)_{jk}(C_t)_{ki}(L_s)_{i\alpha'}$. \end{proof} Write $\Pi=UV^{\mathsf T}$ with $U,V$ of size $(27+\Delta)\times\Delta$ and let $U_t,V_t$ be their row blocks. Multiplying \eqref{eq:gram} by $L_t$ on the left and by $R_s^{\mathsf T}$ on the right, and setting $l_t=L_tU_t$ and $m_s=R_sV_s$, we obtain \begin{equation}\label{eq:excess} a_tB_sC_ta_s=\delta_{ts}\,a_t+l_tm_s^{\mathsf T}\qquad\text{for all }t,s, \end{equation} with $l_t,m_t\in\F^{3\times\Delta}$ whose columns lie in the column spaces of $a_t$ and $a_t^{\mathsf T}$. For $\Delta=0$ this is the rank-additive saturation lemma of Yang et al.\ \cite[Lemma~5.1]{Yan26}. Its solutions are invariant under the symmetries \eqref{eq:sym}, and under the change $(l_t,m_t)\mapsto(l_tg,m_tg^{-\mathsf T})$ with $g\in\mathrm{GL}_\Delta(\F)$. \subsection{Excess zero} \begin{lemma}\label{lem:S} If $\Delta=0$ and some first factor is invertible, then $r=25$. In particular, a decomposition of length $22$ with $\Delta=0$ has type $(17,5,0)$. \end{lemma} \begin{proof} For $\Delta=0$, \eqref{eq:excess} reads $a_tB_sC_ta_s=\delta_{ts}a_t$. Let $a_0$ be invertible. Then $a_0B_0C_0a_0=a_0$ gives $B_0C_0=a_0^{-1}$, so $C_0$ is invertible. For $s\ne 0$ the equation $a_0B_sC_0a_s=0$ shows that $B_s$ vanishes on $C_0\,\mathrm{col}(a_s)$, a space of dimension $r_s$. Hence $\rk B_s\le 3-r_s$. The equation $a_sB_sC_sa_s=a_s$ gives $r_s\le\rk B_s$. Therefore $r_s\le 3-r_s$, that is $r_s=1$, for all $s\ne 0$. Then $27=\sum_tr_t=3+(r-1)$. For $r=22$ there is therefore no invertible first factor, and $n_1+n_2=22$, $n_1+2n_2=27$ give $(17,5,0)$. \end{proof} Lemma~\ref{lem:S} sharpens \cite[Proposition~5.3 and Corollary~6.1]{Yan26}, by which a decomposition with $\sum_tr_t=27$ has at most one invertible first factor. The same argument for $\langle 2,2,2\rangle$ shows that a decomposition with $\sum_t r_t=8$ and an invertible first factor has length $7$ and all other first factors of rank one, as in Strassen's algorithm. \subsection{Three invertible first factors} \begin{lemma}\label{lem:S3} A decomposition with three distinct invertible first factors has $\Delta\ge 2$. \end{lemma} \begin{proof} By Lemma~\ref{lem:S} we may assume $\Delta=1$, so that $\Pi=pq^{\mathsf T}$ with $q^{\mathsf T}p=1$. Let $x,y$ range over the indices of the three invertible terms, take $L_x=a_x$ and $R_x=I$, and let $p_x,q_x\in\F^3$ be the blocks of $p$ and $q$. Since $\Gamma=I+\Pi$, \eqref{eq:gram} gives \[ Z_{yx}:=B_yC_x=(\delta_{xy}I+p_xq_y^{\mathsf T})\,a_y^{-1}. \] The $9\times 9$ matrix $[Z_{yx}]_{y,x}$ is the product of the block column $[B_y]_y$ and the block row $[C_x]_x$, so its rank is at most $3$. (i) Each $Z_{xx}$ is singular. Otherwise, for $y\ne x$, the $6\times 6$ submatrix on the blocks $x,y$ has rank $3+\rk(Z_{yy}-Z_{yx}Z_{xx}^{-1}Z_{xy})\ge 3+(2-1)$, because $Z_{yy}$ has rank at least $2$ and the correction has rank at most $1$. This contradicts the bound $3$. Hence $\det(I+p_xq_x^{\mathsf T})=1+q_x^{\mathsf T}p_x=0$, so $q_x^{\mathsf T}p_x=1$, $\rk Z_{xx}=2$ and $\mathrm{im}\,Z_{xx}=q_x^{\perp}$. (ii) $\rk B_x=\rk C_x=2$. Both ranks are at least $\rk Z_{xx}=2$. If $C_x$ were invertible, then $Z_{yx}=B_yC_x$ would have rank at least $2$ for $y\ne x$, but $Z_{yx}=p_xq_y^{\mathsf T}a_y^{-1}$ has rank at most $1$. The same argument applies to $B_y$. (iii) $q_y^{\mathsf T}p_x=\delta_{xy}$. By (i) and (ii), $\mathrm{im}\,B_y=\mathrm{im}\,Z_{yy}=q_y^{\perp}$. For $x\ne y$ the matrix $Z_{yx}=p_xq_y^{\mathsf T}a_y^{-1}$ is nonzero and its image $\F p_x$ lies in $\mathrm{im}\,B_y$, so $q_y^{\mathsf T}p_x=0$. (iv) Let $V$ be the row space of $[C_x]_x$, of dimension at most $3$. Each block row $B_y[C_x]_x$ has its rows in $V$. For $z\ne y$ the row $q_z^{\mathsf T}B_y[C_x]_x$ has $q_z^{\mathsf T}a_y^{-1}$ in block $y$, $q_y^{\mathsf T}a_y^{-1}$ in block $z$, and $0$ in the third block. Call it $v_{y,z}$. (v) Fix a block $x_0$ and let $y,z$ be the other two indices. The projection of $V$ to block $x_0$ contains $q_z^{\mathsf T}a_{x_0}^{-1}$ for both $z\ne x_0$, and these are independent. Hence the vectors of $V$ that vanish on block $x_0$ form a space of dimension at most $1$. It contains the nonzero vectors $v_{y,z}$ and $v_{z,y}$, which are therefore equal. This gives $q_z^{\mathsf T}a_y^{-1}=q_z^{\mathsf T}a_z^{-1}$ and $q_y^{\mathsf T}a_y^{-1}=q_y^{\mathsf T}a_z^{-1}$. (vi) Over the three choices of $x_0$ we get $q_x^{\mathsf T}a_t^{-1}=q_x^{\mathsf T}a_s^{-1}=q_x^{\mathsf T}a_w^{-1}$ for all $x$, where $t,s,w$ are the three indices. The $q_x$ form a basis by (iii), so the three first factors are equal, a contradiction. \end{proof} \subsection{An exhaustive computation} For larger configurations we solve \eqref{eq:excess} by computer. Fix a type and a value of $\Delta$. Using \eqref{eq:sym} and the action of $\mathrm{GL}_\Delta(\F)$ we bring one term, the \emph{anchor}, to $a_0=I$ (or to a fixed matrix of rank two when there is no invertible term) and its data $(B_0,C_0,l_0,m_0)$ to one of finitely many orbit representatives: $7$ for $\Delta=1$ and $36$ for $\Delta=2$ with an invertible anchor, and $4$ for $\Delta=0$ with an anchor of rank two. The other terms become \emph{vertices}: tuples $(a,B,C,l,m)$ that satisfy \eqref{eq:excess} with themselves and with the anchor. For fixed $a$ these conditions are linear in $B$ once $m$ is fixed and linear in $C$ once $B$ and $l$ are fixed, so the vertices are found by solving linear systems. Two vertices are adjacent when their first factors differ and \eqref{eq:excess} holds for the pair. A decomposition of the given type yields a clique with the prescribed number of vertices of each rank. We first list the cliques formed by the anchor's companions of rank two and three (the \emph{cores}). For each core we then bound the largest set of pairwise adjacent rank-one vertices compatible with the core and having distinct first factors, using a colouring of the compatibility graph as the certificate. \begin{proposition}[$\dagger$]\label{prop:types} No decomposition of length $22$ has type $(17,5,0)$, $(18,2,2)$, $(17,4,1)$, $(17,3,2)$ or $(18,1,3)$. \end{proposition} \begin{table}[ht] \caption{The computation behind Proposition~\ref{prop:types}. The last column is the number of rank-one terms by which a core would have to be extended, and no core extends that far.}\label{tab:types} \centering \small \begin{tabular}{@{}cccrc@{}} \toprule type & $\Delta$ & anchor orbits & cores & needed\\ \midrule $(17,5,0)$ & $0$ & $4$ & $23{,}175$ & $17$\\ $(18,2,2)$ & $1$ & $7$ & $0$ & $18$\\ $(17,4,1)$ & $1$ & $7$ & $708$ & $17$\\ $(17,3,2)$ & $2$ & $36$ & $96{,}717$ & $17$\\ $(18,1,3)$ & $2$ & $36$ & $68$ & $18$\\ \bottomrule \end{tabular} \end{table} Lemmas~\ref{lem:S} and~\ref{lem:S3} exclude $(18,3,1)$, $(19,1,2)$ and $(19,0,3)$. Since $\Delta=0$ forces one of the types $(17,5,0)$, $(18,3,1)$, $(19,1,2)$, we obtain the following. \begin{corollary}[$\dagger$]\label{cor:types} Every decomposition of length $22$ satisfies $\sum_t\rk(a_t)\ge 28$, and none has type $(19,0,3)$, $(18,2,2)$, $(17,4,1)$, $(17,3,2)$ or $(18,1,3)$. \end{corollary} \section{Two first factors on a line}\label{sec:l479} Let $L_0$ be the line spanned by $e_{11}$ and $e_{12}+e_{21}$. Its orbit under $G$ consists of $441$ lines, each containing one matrix of rank one and two of rank two. By Table~\ref{tab:raise} we have $R(L_0)\ge 20$, and Rudich and Rousseau prove $R(L_0)\le 20$ in Lean \cite{RR26}. The capacity of $L_0$ is therefore $2$, so Lemma~\ref{lem:cap} allows two first factors of a decomposition of length $22$ in a line of this orbit. We show that this does not happen when at least $14$ first factors have rank one, which is case (II) of the search in Section~\ref{sec:search}. \begin{theorem}[$\dagger$]\label{thm:l479} In a decomposition of length $22$ with at least $14$ first factors of rank one, each line in the $G$-orbit of $L_0$ contains at most one first factor. \end{theorem} The proof uses a criterion for lifting a decomposition of a quotient $T_L$ to a decomposition of $T$. Let $L$ be a line with nonzero elements $p$, $q$ and $p+q$, and choose linear forms $\chi_0,\chi_1$ on $A$ with $\chi_0(p)=1$, $\chi_0(q)=0$, $\chi_1(p)=0$ and $\chi_1(q)=1$. Let \[ T_L=\sum_{t=1}^{20}\bar a_t\otimes b_t\otimes c_t \] be a decomposition with nonzero factors. For a linear form $\varphi$ on $A$ put \[ V_\varphi=\Bigl\{\,T(\varphi)-\sum_{t=1}^{20}\varphi(a_t)\,b_tc_t^{\mathsf T}\ :\ a_t\in\bar a_t\text{ for all }t\,\Bigr\}, \] a set of $9\times 9$ matrices, where $T(\varphi)$ is the contraction of Section~\ref{sec:prelim}. \begin{lemma}[Lifting criterion]\label{lem:lift} The following are equivalent. \begin{enumerate}[label=(\alph*)] \item There are $a_t\in\bar a_t$ and two further terms with distinct first factors in $L$ that together with the terms $a_t\otimes b_t\otimes c_t$ form a decomposition of $T$ of length $22$. \item At least two of the sets $V_{\chi_0}$, $V_{\chi_1}$ and $V_{\chi_0+\chi_1}$ contain a matrix of rank one. \end{enumerate} \end{lemma} \begin{proof} Fix representatives $a_t^0\in\bar a_t$ and write $a_t=a_t^0+e_t$ with $e_t\in L$. As $e_t$ runs through $L$, the pair $(\chi_0(e_t),\chi_1(e_t))$ takes each value in $\F^2$ once. For a choice of the $e_t$ the tensor $T-\sum_ta_t\otimes b_t\otimes c_t$ maps to $0$ in $(A/L)\otimes B\otimes C$, so it equals $p\otimes M_p+q\otimes M_q$ for some matrices $M_p$ and $M_q$. Contracting with $\chi_0$, $\chi_1$ and $\chi_0+\chi_1$ shows that $M_p$, $M_q$ and $M_p+M_q$ are the elements of $V_{\chi_0}$, $V_{\chi_1}$ and $V_{\chi_0+\chi_1}$ given by this choice. Two terms with distinct first factors $x,y\in L$ and nonzero second and third factors have the form $x\otimes N_x+y\otimes N_y$ with $\rk N_x=\rk N_y=1$. Since \[ p\otimes M_p+q\otimes M_q=p\otimes(M_p+M_q)+(p+q)\otimes M_q=q\otimes(M_p+M_q)+(p+q)\otimes M_p , \] the two terms exist for this choice exactly when two of $M_p$, $M_q$ and $M_p+M_q$ have rank one. The element of $V_{\chi_0}$ depends only on the bits $\chi_0(e_t)$, that of $V_{\chi_1}$ only on the bits $\chi_1(e_t)$, and that of $V_{\chi_0+\chi_1}$ only on their sums. Any two of these three families of bits can be chosen independently. Hence two of the three matrices can be made of rank one by the same choice if and only if each of them can be made of rank one by some choice. \end{proof} For a single term whose slice has rank one, a related statement is part of \cite[Proposition~3.1]{LM17}, and Wang's forced-product technique \cite{Wan26a} also enumerates the free coefficients of a residual and tests its rank. To test whether $V_\varphi$, an affine space of matrices, contains a matrix $bc^{\mathsf T}$ of rank one, we solve for each of the $511$ nonzero vectors $b$ a linear system in $c$ and the coefficients. \begin{proof}[Proof of Theorem~\ref{thm:l479}] By symmetry it suffices to treat $L_0$. Suppose two first factors lie in $L_0$. They are distinct by Corollary~\ref{cor:distinct}, and the capacity of $L_0$ is $2$, so the third nonzero matrix of $L_0$ is not a first factor. The other $20$ terms project to a decomposition of $T_{L_0}$ of length $20$ with nonzero factors, and its coset profile $n$ satisfies \eqref{eq:coset} with $\ell-1=20$. At most one of the two first factors in $L_0$ has rank one, so at least $13$ of the other $20$ have rank one. Only $39$ of the $127$ nonzero cosets of $L_0$ contain a matrix of rank one, which gives the additional inequality \[ \sum_{x\in C_1}n(x)\ge 13, \] where $C_1$ is the set of these $39$ cosets. We enumerate the coset profiles that satisfy these inequalities, as in Section~\ref{subsec:profiles}, and run the completion search with target $T_{L_0}$ on each. When it finds decompositions of $T_{L_0}$ with a given profile, we list all of them and check that for each at most one of the three sets in Lemma~\ref{lem:lift}(b) contains a matrix of rank one. By Lemma~\ref{lem:lift} no profile comes from a decomposition of $T$ of length $22$. The enumeration has $737{,}787{,}637{,}822$ nodes and $189{,}298{,}650{,}178$ leaves. For $10$ of the profiles the completion search finds decompositions of $T_{L_0}$, $540$ in all, and none of them lifts. \end{proof} The reduction to coset profiles works for any subspace in place of $L_0$ and any number of first factors in it, with the inequality for $C_1$ adjusted to the matrices of rank one in the subspace. The formalization proves it in this generality, together with the refutation of profiles that admit no decomposition of the quotient. \section{The search at \texorpdfstring{$r=22$}{r=22}}\label{sec:search} \subsection{Admissible sets} By Corollary~\ref{cor:distinct} the first factors of a decomposition of length $22$ form a set $F\subset A\setminus\{0\}$ with $|F|=22$. Let $k$ be the number of elements of rank one in $F$. We split the proof into three cases: (I) $k\le 12$, (I$'$) $k=13$ and (II) $k\ge 14$, which is the range of Theorem~\ref{thm:l479}. \begin{definition}\label{def:adm} A set $F\subset A\setminus\{0\}$ with $|F|=22$ is \emph{admissible} if \begin{enumerate}[label=(\alph*)] \item $|F\cap S|\le\cp(S)$ for every subspace $S$ in the family $\cK$ described below, and \item $|\{a\in F: \varphi(a)=1\}|\ge 3\rk\varphi$ for every nonzero linear form $\varphi$ on $A$, \end{enumerate} and, in case (II), in addition \begin{enumerate}[label=(\alph*),resume] \item the type of $F$ is not excluded by Corollary~\ref{cor:types}, and \item each line in the $G$-orbit of $L_0$ (Section~\ref{sec:l479}) contains at most one element of $F$. \end{enumerate} \end{definition} The family $\cK$ consists of the subspaces whose capacity is not implied by the capacity of another subspace, about $3.8\cdot 10^{6}$ of them. For a subspace $S$ of dimension at most $4$ the capacity can be lowered further. Since the elements of $F$ are distinct, $|F\cap S|\le k$ whenever no $k+1$ nonzero elements of $S$ respect the capacities of all subspaces of $S$. We use the bound obtained in this way for five classes of subspaces, for which it is smaller than $\cp(S)$. By Lemma~\ref{lem:cap}, Corollary~\ref{cor:types} and Theorem~\ref{thm:l479}, the set of first factors of a decomposition of length $22$ is admissible, and so are its images under $G$. \subsection{Orderly generation}\label{subsec:orderly} We order the $511$ nonzero matrices by rank, and matrices of equal rank by the integer $\sum_{i,j}a_{ij}2^{3i+j-4}$. In case (II) the order is rank one, rank two, rank three. In cases (I) and (I$'$) it is rank three, rank two, rank one, which keeps the search tree small when there are few elements of rank one. For finite sets $F\ne F'$ of the same size we write $F