\documentclass[11pt]{article}

\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{lmodern}
\usepackage[margin=1in]{geometry}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{mathtools}
\usepackage{booktabs}
\usepackage{array}
\usepackage{tabularx}
\usepackage{enumitem}
\usepackage{microtype}
\usepackage[hidelinks]{hyperref}
\usepackage{etoolbox}
\apptocmd{\thebibliography}{\setlength{\itemsep}{1pt plus 0.5pt}}{}{}

\hypersetup{
  pdftitle={Local optimality of rank-47 schemes for 4x4 matrix multiplication over F2},
  pdfauthor={Tejasvi Singh Tomar (ORCID 0000-0003-4668-3639)},
}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{remark}[theorem]{Remark}
\newtheorem{example}[theorem]{Example}

\newcommand{\F}{\mathbb{F}}
\newcommand{\Ft}{\mathbb{F}_2}
\newcommand{\Rk}{\mathrm{R}}
\newcommand{\bRk}{\underline{\mathrm{R}}}
\newcommand{\mm}[3]{\langle #1,#2,#3\rangle}
\newcommand{\GL}{\mathrm{GL}}
\newcommand{\Aut}{\operatorname{Aut}}
\newcommand{\spn}{\operatorname{span}}
\newcommand{\rk}{\operatorname{rk}}
\newcommand{\core}{\operatorname{core}}
\newcommand{\LO}{\mathrm{LO}}
\newcommand{\cv}{\textsuperscript{$\dagger$}}
\newcommand{\lean}[1]{\texttt{#1}}
\newcommand{\cp}{\operatorname{cap}}
\newcommand{\lb}{\operatorname{lb}}

\renewcommand{\topfraction}{0.9}
\renewcommand{\bottomfraction}{0.8}
\renewcommand{\textfraction}{0.07}
\renewcommand{\floatpagefraction}{0.8}

\title{Local optimality of rank-47 schemes for $4\times4$ matrix multiplication over $\mathbb{F}_2$}
\author{Tejasvi Singh Tomar\thanks{ORCID: \href{https://orcid.org/0000-0003-4668-3639}{0000-0003-4668-3639}.}}
\date{}

\begin{document}
\maketitle

\begin{abstract}
The tensor $\mm444$ of $4\times4$ matrix multiplication has rank at most 47 over $\Ft$, and as it is not known whether 47 is optimal, we ask how far the known decompositions of rank 47 are from one of rank 46. A decomposition is locally optimal to depth $D$ if no $D$ or fewer of its rank-one terms can be replaced by fewer rank-one terms. We prove that five pairwise inequivalent decompositions of rank 47 over $\Ft$ are locally optimal to depth 18, as is every decomposition equivalent to one of them, so a decomposition of rank 46 over $\Ft$ shares at most 28 terms with any decomposition in these five classes. The five classes include the scheme of Fawzi et al. and every public decomposition of rank 47 over $\Ft$ known to us; one of them, found in our flip-graph searches, is new. The proof rests on a peeling lemma and, for four sets of terms that resist the other bounds, on a refinement of the substitution method, which we call substitution over subspaces with lifting. Local optimality to depth 18 is also proved in Lean~4.
\end{abstract}

\begin{quote}\small
\textbf{Keywords:} matrix multiplication; tensor rank; local optimality; substitution method; flip graphs; SAT solving; Lean~4.\\[2pt]
\textbf{MSC2020:} 68Q17, 15A69 (primary); 68V05, 68V15, 68V20 (secondary).
\end{quote}

\section{Introduction}\label{sec:intro}

Let $\mm nmp$ denote the tensor of the bilinear map that multiplies an $n\times m$ matrix by an $m\times p$ matrix. Its rank over a field $\F$ is the least number of multiplications in a bilinear algorithm for this product, and the ranks of the square formats determine the exponent of matrix multiplication~\cite{BCS1997,Blaser2013survey}. Strassen's algorithm~\cite{Strassen1969} gives $\Rk(\mm222)\le 7$ and hence $\Rk(\mm444)\le 49$ over any field. Fawzi et al.~\cite{FawziEtAl2022} found a decomposition (or scheme) of $\mm444$ of rank 47 that is valid in characteristic~2. Kauers and Moosbauer~\cite{KauersMoosbauer2023flip} introduce flip graphs and report more than 100,000 decompositions of rank 47 over $\Ft$, none of rank 46; the web collection of Kauers~\cite{KauersSchemes444x47} contains only four distinct decompositions up to the order of the terms (Appendix~\ref{app:search}). Later flip-graph searches, including adaptive and symmetric variants~\cite{AraiIchikawaHukushima2024,MoosbauerPoole2025}, found no decomposition of $\mm444$ over $\Ft$ of rank below 47. Over rings that contain $1/2$ the best known rank is 48~\cite{DumasPernetSedoglavic2025}, and AlphaEvolve found a decomposition of rank 48 over $\mathbb{C}$~\cite{NovikovEtAl2025AlphaEvolve}; these decompositions use the coefficient $1/2$, so they do not apply over $\Ft$. In the other direction, Bl\"aser's bound $\Rk(\mm nmn)\ge 2mn+2n-m-2$ for $m\ge n\ge3$~\cite{Blaser2003} gives $\Rk(\mm444)\ge34$ over every field, with $m=n=4$, and to our knowledge no better lower bound over $\Ft$ has been published; the recent result $\Rk_{\Ft}(\mm333)=23$~\cite{Tomar2026rank23} gives the same value (Remark~\ref{rem:lower}). Whether $\Rk_{\Ft}(\mm444)=47$ is open.

This paper asks how far the known decompositions of rank 47 are from one of rank 46. Let $S$ be a decomposition of rank 47, viewed as a list of rank-one terms. If a decomposition of rank 46 shares $m$ terms with $S$, then the other $47-m$ terms of $S$ sum to a tensor of rank at most $46-m$. We call $S$ \emph{locally optimal to depth $D$} if every set of at most $D$ terms of $S$ has \emph{full rank}, that is, sums to a tensor whose rank over $\Ft$ equals the number of terms. A decomposition of rank 46 then shares at most $46-D$ terms with $S$ (Lemma~\ref{lem:share}). Local optimality to depth $D$ excludes any move that replaces at most $D$ terms of $S$ by fewer terms, such as the reductions used in flip-graph search, and it excludes such moves from every decomposition equivalent to $S$ as well (Section~\ref{sec:lo}). Here two decompositions are \emph{equivalent} if they are related by the symmetries of $\mm444$ listed in Section~\ref{sec:sym}, up to the order of the terms.

We study five decompositions of $\mm444$ of rank 47 over $\Ft$. AT47 is the decomposition of Fawzi et al.~\cite{FawziEtAl2022}, and KM47 is a decomposition from the data of Kauers and Moosbauer~\cite{KauersMoosbauer2023flip,KauersMoosbauerFlipsRepo}. C3 is equivalent to a decomposition in another web collection of Kauers~\cite{KauersSchemes444r47}, and C5 to the second decomposition of rank 47 of Zaru~\cite{Zaru2026}. C4 was found by our flip-graph searches. By Theorem~\ref{thm:classes}, the five are pairwise inequivalent, and none of them admits a flip or a reduction. Every public decomposition of rank 47 over $\Ft$ known to us is equivalent to AT47, KM47, C3 or C5, and none is equivalent to C4 (Appendix~\ref{app:search}). We mark with a dagger ($\dagger$) the numbered statements whose proofs rely on computer calculation (Section~\ref{sec:verif}).

\begin{theorem}[$\dagger$]\label{thm:main}
Let $S$ be a decomposition of $\mm444$ over $\Ft$ that is equivalent to one of AT47, KM47, C3, C4 and C5.
Then $S$ is locally optimal to depth $18$.
\end{theorem}

\begin{corollary}[$\dagger$]\label{cor:main}
A decomposition of $\mm444$ of rank $46$ over $\Ft$ shares at most $28$ terms with any decomposition equivalent to one of the five.
\end{corollary}

The proof rests on a \emph{peeling lemma} (Lemma~\ref{lem:peel}): if one term of a sum of rank-one terms has factors in two of the three positions outside the spans of the other terms' factors in those positions, then removing this term lowers the rank by exactly one. Repeated removal ends in a unique \emph{core}, so local optimality to depth $D$ holds if and only if all subsets of size at most $D$ without such a term, the \emph{non-peelable} subsets, have full rank (Corollary~\ref{cor:reduction}). We enumerate these subsets up to the automorphism group of the decomposition and bound their ranks from below with flattenings, the Koszul flattenings of Landsberg and Ottaviani~\cite{LandsbergOttaviani2013,LandsbergOttaviani2015} and the substitution method~\cite{AFT2011}, mostly with the peeling lemma applied again in every branch of the substitution. Four subsets $Y$ of C3 resist these bounds. For them we eliminate first factors along arbitrary linear forms and record the subspaces spanned by the eliminated first factors, so the proof becomes a directed acyclic graph (DAG) of subspaces whose nodes carry statements about the minimal decompositions of the subset's sum. At some leaves SAT instances on that sum, with the first factors prescribed only modulo the subspace, settle the node; hence the name substitution over subspaces with lifting (Section~\ref{sec:gsl}). The method is stated there for any tensor over $\Ft$ that is concise in one position.

The independent checks of the computations and the Lean~4 proofs of Theorems~\ref{thm:main}, \ref{thm:classes}(a) and~\ref{thm:Y}, in which most computations are evaluated as compiled code, are described in Section~\ref{sec:verif}.

\paragraph{Related work.} Decompositions of small matrix multiplication tensors over $\Ft$ are found with SAT solvers~\cite{HeuleKauersSeidl2019,HeuleKauersSeidl2021}, with flip graphs~\cite{KauersMoosbauer2023flip} and their variants~\cite{AraiIchikawaHukushima2024,MoosbauerPoole2025,KauersWood2025meta}, and with GPU search~\cite{MedleyEtAl2026}. Kauers and Moosbauer call a scheme reducible if, among terms with a common factor in one position, the factors in another position are linearly dependent~\cite[Def.~2]{KauersMoosbauer2023flip}. Arai, Ichikawa and Hukushima reduce a set of terms with a common factor whose sum has rank below the size of the set~\cite[Def.~2.6]{AraiIchikawaHukushima2024}. Local optimality to depth $D$ excludes such a rank drop for all subsets of size at most $D$, with or without a common factor. So a scheme that is locally optimal to depth $D$ has no reduction of either kind on $D$ or fewer terms. The converse fails: the eight terms of the standard algorithm for $\mm222$ admit no reduction of either kind, although their sum has rank at most 7~\cite{Strassen1969}. Moosbauer~\cite[Sec.~4.8]{Moosbauer2023thesis} studies tensor identities, which exchange a set of terms for another set of terms. Zaru~\cite{Zaru2026} searches with a SAT solver for decompositions of $\mm444$ of rank 47 over $\Ft$ that are invariant under the symmetry group of AT47. The search finds a second such decomposition, and Zaru shows that both are flip-isolated and that no decomposition of rank 46 invariant under this group keeps 8 or more of the 10 orbits of terms of either. Agarwal~\cite{Agarwal2026} studies the question of this paper for a decomposition of $\mm444$ with 48 terms over $\mathbb{C}$, and shows that every shorter decomposition differs from it in at least 13 terms. On the side of lower bounds, the substitution method goes back to Pan~\cite{Pan1966}, and we use the form of Alexeev, Forbes and Tsimerman~\cite{AFT2011}. Substitution over subspaces with lifting is compared in Section~\ref{sec:gsl-prior} with automated frameworks for certified rank lower bounds over finite fields and with capacity inequalities.

\paragraph{Organization.} Section~\ref{sec:prelim} recalls the lower-bound methods, and Section~\ref{sec:classes} presents the five decompositions. Sections~\ref{sec:peel} and~\ref{sec:method} give the peeling lemma, the enumeration and the certification. Section~\ref{sec:results} proves Theorem~\ref{thm:main}, with Section~\ref{sec:gsl} for the four subsets of C3. Section~\ref{sec:verif} describes the independent checks and the formal proof, and Section~\ref{sec:open} closes with open questions. Appendix~\ref{app:schemes} lists the decompositions, and Appendix~\ref{app:checks} collects the details of the computations.

\section{Preliminaries}\label{sec:prelim}

We fix notation and recall the two lower-bound methods that we use: flattenings and the substitution method.

\subsection{Tensors and decompositions}

Let $A$, $B$, $C$ be finite-dimensional vector spaces over a field $\F$. A tensor $T\in A\otimes B\otimes C$ has rank one if $T=a\otimes b\otimes c$ with $a$, $b$, $c$ nonzero. The \emph{rank} $\Rk(T)$ is the least $r$ such that $T$ is a sum of $r$ tensors of rank one. The \emph{border rank} $\bRk(T)$ is the least $r$ such that $T$ lies in the Zariski closure, over the algebraic closure $\overline{\F}$, of the set of tensors of rank at most $r$. Thus $\bRk(T)\le\Rk(T)$. We follow~\cite{BCS1997,Landsberg2012TGA}.

We index rows, columns and basis vectors from 0. We write $E_{ij}$ for the matrix units and use the cyclic convention
\[
  \mm nmp=\sum_{i=0}^{n-1}\sum_{j=0}^{m-1}\sum_{k=0}^{p-1} E_{ij}\otimes E_{jk}\otimes E_{ki}
  \in \F^{n\times m}\otimes\F^{m\times p}\otimes\F^{p\times n}.
\]
A \emph{decomposition} (or scheme) of rank $r$ is a list $S$ of $r$ rank-one tensors $a_t\otimes b_t\otimes c_t$ whose sum is $\mm nmp$. We call $a_t$, $b_t$, $c_t$ the factors of the term $t$ in the first, second and third position. For $X\subseteq S$ we write
\[
  \Sigma_X=\sum_{t\in X} a_t\otimes b_t\otimes c_t .
\]

\subsection{Symmetry}\label{sec:sym}

For $P,Q,R\in\GL_4(\Ft)$ the map
\[
  a\otimes b\otimes c\ \longmapsto\ PaQ^{-1}\otimes QbR^{-1}\otimes RcP^{-1}
\]
fixes $\mm444$, and so do the cyclic shift $a\otimes b\otimes c\mapsto b\otimes c\otimes a$ and the map $a\otimes b\otimes c\mapsto c^{\mathsf T}\otimes b^{\mathsf T}\otimes a^{\mathsf T}$, as one checks directly. They generate a group $G\cong\GL_4(\Ft)^3\rtimes S_3$ of order $6\cdot 20160^3\approx 4.9\cdot10^{13}$, which acts on decompositions of $\mm444$ term by term. Under this action exactly the scalar triples $(\alpha I,\beta I,\gamma I)$ act trivially. Over $\Ft$ the only such triple is the identity, so the map from $\GL_4(\Ft)^3$ to $G$ is injective. Two decompositions are \emph{equivalent} if one is the image of the other under $G$, up to the order of the terms. The automorphism group $\Aut(S)$ is the stabilizer of $S$ in $G$. It permutes the terms of $S$.

\subsection{Local optimality}\label{sec:lo}

\begin{definition}\label{def:lo}
A list $S$ of rank-one tensors is \emph{locally optimal to depth $D$}, written $\LO(D)$, if $\Rk(\Sigma_X)=|X|$ for all $X\subseteq S$ with $|X|\le D$.
\end{definition}

We say that a set $X$ of terms has \emph{full rank} if $\Rk(\Sigma_X)=|X|$. Invertible linear maps on each factor and permutations of the three positions preserve rank. Therefore $\LO(D)$ is invariant under these maps, and in particular under equivalence.

\begin{lemma}\label{lem:share}
Let $S$ and $S'$ be decompositions of the same tensor, of ranks $r$ and $r-1$. If $S$ is $\LO(D)$, then $S$ and $S'$ have at most $r-1-D$ terms in common.
\end{lemma}

\begin{proof}
Let $Y$ be the common part of $S$ and $S'$, counted with multiplicity. Then $\Sigma_{S\setminus Y}=\Sigma_{S'\setminus Y}$, so $\Rk(\Sigma_{S\setminus Y})\le r-1-|Y|<|S\setminus Y|$. Hence $|S\setminus Y|>D$, that is, $|Y|\le r-1-D$.
\end{proof}

\subsection{Flattening bounds}\label{sec:flat}

Let $T\in A\otimes B\otimes C$. The flattening $T_A\colon A^*\to B\otimes C$ has rank at most $\Rk(T)$, and the same holds for $T_B$ and $T_C$. We also use the Koszul flattenings of Landsberg and Ottaviani~\cite{LandsbergOttaviani2013,LandsbergOttaviani2015}, a special case of their Young flattenings. Fix a linear map $\pi\colon A\to V=\F^{2p+1}$ with $p\ge1$, and let $M_0,\dots,M_{2p}$ be the slices of $(\pi\otimes1\otimes1)T$, viewed as maps $B^*\to C$. Define
\[
  T^{\wedge p}_{\pi}\colon \Lambda^pV\otimes B^*\to\Lambda^{p+1}V\otimes C,\qquad
  \omega\otimes\beta\mapsto\sum_{k=0}^{2p}(e_k\wedge\omega)\otimes M_k(\beta).
\]
A term $a\otimes b\otimes c$ with $\pi(a)\ne0$ contributes $(\pi(a)\wedge\cdot)\otimes(\beta\mapsto\beta(b)c)$. The map $\omega\mapsto\pi(a)\wedge\omega$ from $\Lambda^pV$ to $\Lambda^{p+1}V$ has rank $\binom{2p}{p}$ over any field. Hence
\begin{equation}\label{eq:young}
  \Rk(T)\ \ge\ \Bigl\lceil \rk T^{\wedge p}_{\pi}\big/\tbinom{2p}{p}\Bigr\rceil .
\end{equation}
We use $p=1$ (divisor 2), $p=2$ (divisor 6) and $p=3$ (divisor 20). Landsberg and Ottaviani call all of these Koszul flattenings, and so do we. For $p=1$ and $\F=\Ft$, the matrix of $T^{\wedge1}_\pi$ is the block matrix
\[
  K=\begin{pmatrix}0&M_2&M_1\\ M_2&0&M_0\\ M_1&M_0&0\end{pmatrix},
\]
since signs vanish in characteristic~2. A term with $\pi(a)=0$ contributes nothing. So if $\pi$ kills a term of a list $X$, the bound~\eqref{eq:young} for $\Sigma_X$ is at most $|X|-1$.

Matrix ranks do not change under field extension, and the tensors for which one of these maps has rank at most $m$ form a Zariski-closed set, defined by minors. Hence the bounds above are lower bounds for $\bRk(T)$ as well as for $\Rk(T)$. None of them, however, can prove $\Rk(T)\ge r$ when $\bRk(T)<r$. We call this the \emph{border-rank barrier}.

\subsection{The substitution method}\label{sec:subst}

The substitution method goes beyond the border-rank barrier. We use the following form, due to Alexeev, Forbes and Tsimerman~\cite{AFT2011}.

\begin{lemma}[\cite{AFT2011}]\label{lem:subst}
Let $T=\sum_{i=0}^{n-1}e_i\otimes M_i\in\F^n\otimes B\otimes C$, and suppose that $M_0,\dots,M_{k-1}$ are linearly independent. Then
\[
  \Rk(T)\ \ge\ k+\min_{c}\ \Rk\Bigl(\sum_{i=k}^{n-1}e_i\otimes\Bigl(M_i+\sum_{j=0}^{k-1}c_{ij}M_j\Bigr)\Bigr),
\]
where $c$ runs over all $(n-k)\times k$ matrices over $\F$, with rows indexed by $i\in\{k,\dots,n-1\}$ and columns by $j\in\{0,\dots,k-1\}$.
\end{lemma}

The proof is short. Take an optimal decomposition $T=\sum_{l=1}^{r}\alpha_l\otimes\beta_l\otimes\gamma_l$. Since $M_0,\dots,M_{k-1}$ are independent, the first $k$ coordinates of the $\alpha_l$ span $\F^k$. A projection of $\F^n$ onto $\spn(e_k,\dots,e_{n-1})$ can therefore kill $k$ of the $\alpha_l$. It maps $T$ to one of the tensors on the right, which therefore has rank at most $r-k$.

We apply the lemma in any position, after permuting the positions. For $k=1$ and a pivot $j$ with $M_j\ne0$, it reads
\begin{equation}\label{eq:onestep}
  \Rk(T)\ \ge\ 1+\min_{u}\ \Rk\Bigl(\sum_{i\ne j}e_i\otimes(M_i+u_iM_j)\Bigr),
\end{equation}
with $u$ running over $\F^{n-1}$. The hypothesis $M_j\ne0$ is essential. If $M_j=0$, every branch is $T$ with a zero slice removed, and~\eqref{eq:onestep} would spuriously raise the bound by one. Over $\Ft$ the minimum has $2^{n-1}$ branches. Applying~\eqref{eq:onestep} recursively, in any position and with any pivot, gives a tree of tensors with bounds from Section~\ref{sec:flat} at the leaves. We call this \emph{plain substitution}.

\begin{example}\label{ex:W}
The tensor $W=e_0\otimes e_0\otimes e_1+e_0\otimes e_1\otimes e_0+e_1\otimes e_0\otimes e_0$ has border rank 2. It is the value at $\varepsilon=0$ of the curve $\varepsilon^{-1}\bigl((e_0+\varepsilon e_1)^{\otimes3}-e_0^{\otimes3}\bigr)$, whose other values have rank at most 2. Its first-position slices are $M_0=\bigl(\begin{smallmatrix}0&1\\1&0\end{smallmatrix}\bigr)$ and $M_1=\bigl(\begin{smallmatrix}1&0\\0&0\end{smallmatrix}\bigr)$. With pivot $1$, the bound~\eqref{eq:onestep} gives $\Rk(W)\ge1+\min_{u}\rk(M_0+uM_1)=3$.
\end{example}

\begin{remark}\label{rem:lower}
Over $\Ft$ the rank of $\mm333$ is 23~\cite{Tomar2026rank23}, and this value also gives $\Rk_{\Ft}(\mm444)\ge34$. Lemma~\ref{lem:subst}, applied to the $m$ independent slices of the last column of the second matrix, and setting the last row of the third matrix to zero give $\Rk(\mm nmp)\ge\Rk(\mm nm{p-1})+m$. With the symmetries of matrix multiplication, the bound 23 then improves to 26, 30 and 34 in turn. By the same step, Wang's automated bound $\Rk_{\Ft}(\mm344)\ge29$~\cite{Wang2026automated} yields only 33.
\end{remark}

\section{Five decompositions of rank 47}\label{sec:classes}

We encode a matrix $(m_{ij})\in\Ft^{4\times4}$ by the integer $\sum_{i,j}m_{ij}2^{4i+j}$. We list the five decompositions in this encoding in Appendix~\ref{app:schemes}, with terms numbered from 0. AT47 and KM47 are named after their sources, and the further classes are numbered C3, C4 and C5 in the order in which our searches found them. For AT47 we read the decomposition of~\cite{FawziEtAl2022} over $\Ft$ in its index convention, which is the cyclic convention.

\begin{theorem}[$\dagger$]\label{thm:classes}
\leavevmode
\begin{enumerate}[label=\textup{(\alph*)},nosep]
\item Each of AT47, KM47, C3, C4 and C5 is a decomposition of $\mm444$ over $\Ft$ with $47$ terms.
\item The five decompositions are pairwise inequivalent.
\item Their automorphism groups have orders $12$, $2$, $4$, $12$ and $12$.
\item In each of them, the $47$ factors in each position are pairwise distinct.
\end{enumerate}
\end{theorem}

\begin{proof}
Part (a) is a direct expansion. For (b), let $\rho(S)=\sum_{t\in S}(\rk a_t+\rk b_t+\rk c_t)$ be the sum of the matrix ranks of all $141$ factors. An element of $G$ maps every factor to a matrix $PaQ^{-1}$ or to a transpose, of the same rank, and permutes the three positions. Thus $\rho$ is constant on equivalence classes. The five values of $\rho$ in Table~\ref{tab:classes} are distinct. We computed the automorphism groups in (c) by an exhaustive search over $G$. For each of the six permutations of the positions and each pair $(P,Q)\in\GL_4(\Ft)^2$, the search keeps the pair only if the transformed first-position factors are, as a multiset, the first-position factors of $S$. For each surviving pair it tries every $R$. Part~(d) can be read off from Appendix~\ref{app:schemes}.
\end{proof}

By part (d), in each position the 47 factors of each of the five are pairwise distinct, and a flip or a reduction needs two terms with equal factors in one position, so in the flip graph of~\cite{KauersMoosbauer2023flip} no flip and no reduction starts at the five, and no flip ends at them.

\begin{table}[ht]
\centering
\caption{The five decompositions of rank 47 (sources in Section~\ref{sec:intro}).}\label{tab:classes}
\begin{tabular}{lcc}
\toprule
Decomposition & $|\Aut(S)|$ & $\rho(S)$\\
\midrule
AT47 & 12 & 278\\
KM47 & 2 & 276\\
C3 & 4 & 272\\
C4 & 12 & 282\\
C5 & 12 & 274\\
\bottomrule
\end{tabular}
\end{table}

\begin{remark}[$\dagger$]\label{rem:search}
Every decomposition from the first $41{,}809$ descents (search runs) of our flip-graph searches is equivalent to one of the five. The later decompositions of these searches carry the invariant hash of one of the five classes, and a random sample of $4{,}083$ of them was matched explicitly (Appendix~\ref{app:search} defines the hash and gives the details).
\end{remark}

\section{The peeling lemma}\label{sec:peel}

Throughout this section we fix a finite list $L$ of rank-one tensors $a_s\otimes b_s\otimes c_s$ in $A\otimes B\otimes C$ over any field $\F$, and we write $\Sigma_L$ for their sum. For $t\in L$ we write $L-t$ for the list without $t$.

\begin{definition}\label{def:peel}
A term $t\in L$ is \emph{free in the first position} if $a_t\notin\spn\{a_s : s\in L-t\}$, that is, if $t$ is a coloop of the vector configuration $(a_s)_{s\in L}$. Freeness in the second and third positions is defined in the same way. A term is \emph{peelable} in $L$ if it is free in at least two positions, and $L$ is \emph{non-peelable} if none of its terms is peelable.
\end{definition}

The following lemma is a direct consequence of the substitution lemma~\cite[Lemma~2]{HopcroftKerr1971}, \cite[Lemma~B.1]{AFT2011}, \cite[Prop.~5.3.1.1]{Landsberg2017GCT}, combined with a projection in a second position. The same two-position argument appears for direct sums in~\cite[Thm.~4.1]{LandsbergMichalek2017abelian} and~\cite[Lemma~7.1]{Blaser2013survey}. We include the short proof because we need the lemma in the form below, where the third factor is unrestricted.

\begin{lemma}[Peeling lemma]\label{lem:peel}
If $t$ is peelable in $L$, then $\Rk(\Sigma_L)=\Rk(\Sigma_{L-t})+1$.
\end{lemma}

\begin{proof}
Clearly $\Rk(\Sigma_L)\le\Rk(\Sigma_{L-t})+1$. For the converse we may assume that $t$ is free in the first two positions. Let $r=\Rk(\Sigma_L)$ and $\Sigma_L=\sum_{i=1}^r\alpha_i\otimes\beta_i\otimes\gamma_i$. Choose $a^*\in A^*$ with $a^*(a_t)=1$ and $a^*(a_s)=0$ for $s\ne t$. Contracting the first factor with $a^*$ gives
\[
  b_t\otimes c_t=\sum_{i=1}^r a^*(\alpha_i)\,\beta_i\otimes\gamma_i .
\]
The left side is nonzero, so $a^*(\alpha_i)\ne0$ for some $i$. After renumbering and rescaling we may assume $a^*(\alpha_1)=1$. The map $\varphi(v)=v-a^*(v)\alpha_1$ kills $\alpha_1$ and fixes $a_s$ for $s\ne t$. Hence
\[
  (\varphi\otimes1\otimes1)\Sigma_L=\Sigma_{L-t}+(a_t-\alpha_1)\otimes b_t\otimes c_t=\sum_{i=2}^{r}\varphi(\alpha_i)\otimes\beta_i\otimes\gamma_i
\]
has rank at most $r-1$. Now choose $b^*\in B^*$ with $b^*(b_t)=1$ and $b^*(b_s)=0$ for $s\ne t$, and let $\psi(w)=w-b^*(w)\,b_t$. The map $\psi$ kills $b_t$ and fixes $b_s$ for $s\ne t$. So $1\otimes\psi\otimes1$ maps the tensor above to $\Sigma_{L-t}$. Linear maps do not increase rank, and therefore $\Rk(\Sigma_{L-t})\le r-1$.
\end{proof}

Two free positions are needed: in the list $L=(e_0\otimes e_0\otimes e_0,\ e_1\otimes e_0\otimes e_0)$ the second term is free in the first position only, and both $\Sigma_L$ and $\Sigma_{L-t}$ have rank one.

Freeness is monotone. If $t$ is free in some position within $L$, then it is free in that position within any sublist of $L$ that contains $t$. This makes the result of repeated peeling canonical.

\begin{lemma}\label{lem:core}
Delete peelable terms from $L$ one at a time until no peelable term is left. The final list $\core(L)$ does not depend on the order of deletion. It is the largest non-peelable sublist of $L$, and
\[
  \Rk(\Sigma_L)=\Rk(\Sigma_{\core(L)})+|L|-|\core(L)|.
\]
\end{lemma}

\begin{proof}
Let $t_1,\dots,t_m$ be the terms deleted in one run, and let $N\subseteq L$ be a non-peelable sublist. Suppose some $t_i$ lies in $N$, and take the least such $i$. Then $N\subseteq L-\{t_1,\dots,t_{i-1}\}$, and $t_i$ is peelable in this list, hence in $N$ by monotonicity. This is a contradiction. Hence $N$ is contained in the final list of the run. The final list is itself non-peelable, so it is the largest non-peelable sublist of $L$ and does not depend on the run. The rank formula follows from Lemma~\ref{lem:peel}.
\end{proof}

\begin{corollary}\label{cor:reduction}
A list $S$ is $\LO(D)$ if and only if $\Rk(\Sigma_X)=|X|$ for all non-peelable $X\subseteq S$ with $|X|\le D$.
\end{corollary}

\begin{proof}
One direction is trivial. For the other, let $X\subseteq S$ with $|X|\le D$. The list $\core(X)$ is non-peelable of size at most $D$, so $\Rk(\Sigma_{\core(X)})=|\core(X)|$. Lemma~\ref{lem:core} then gives $\Rk(\Sigma_X)=|X|$.
\end{proof}

\begin{lemma}\label{lem:equiv}
Let $h$ be an invertible linear map on each position composed with a permutation of the positions, for example an element of $G$, and write $h(L)$ for the list of images of the terms of $L$. Let $\tau$ be the permutation of the positions. Then $t$ is free in position $k$ in $L$ if and only if $h(t)$ is free in position $\tau(k)$ in $h(L)$. Moreover, $t$ is peelable in $L$ if and only if $h(t)$ is peelable in $h(L)$, $\core(h(L))=h(\core(L))$, and $\Rk(\Sigma_{h(L)})=\Rk(\Sigma_L)$.
\end{lemma}

\begin{proof}
The map $h$ preserves linear dependence among the factors in each position, up to the permutation of positions, and it preserves rank.
\end{proof}

\subsection{Peeling inside substitution}\label{sec:peelsubst}

Let $L$ be a list with first factors in $\F^n$, and let $j$ be a pivot such that the slice $M_j$ of $\Sigma_L$ is nonzero. For $u\in\F^{n-1}$ let $\varphi_u\colon\F^n\to\F^{n-1}$ map $e_j$ to $\sum_{i\ne j}u_ie_i$ and fix $e_i$ for $i\ne j$. The branch tensor in~\eqref{eq:onestep} is
\[
  (\varphi_u\otimes1\otimes1)\Sigma_L=\sum_{s\in L}\varphi_u(a_s)\otimes b_s\otimes c_s .
\]
After the terms with $\varphi_u(a_s)=0$ are deleted, this is again a list $L_u$ of rank-one terms. Lemma~\ref{lem:core} therefore applies to every branch. To prove that a branch has rank at least $k$, it suffices to prove $\Rk(\Sigma_{\core(L_u)})\ge k-|L_u|+|\core(L_u)|$. We call substitution with this peeling step at all nodes \emph{peeled substitution}. It can be much cheaper than plain substitution. For example, the computation of depth 16 without peeling (Table~\ref{tab:summary}) treats each subset of size 16 in full. For one subset of C5 there, the shortest plain-substitution certificate known to us has four levels and about $9\cdot10^7$ branches. That subset has two peelable terms, so the peeling enumeration never lists it. It lists the core of 14 terms instead, and peeled substitution certifies that core with three levels.

\section{Enumeration and certification}\label{sec:method}

We now fix one of the five decompositions $S$ and a depth $D$. By Corollary~\ref{cor:reduction} and the invariance of $\LO(D)$ under equivalence (Section~\ref{sec:lo}), Theorem~\ref{thm:main} reduces to two tasks for each of the five: list the non-peelable subsets $X\subseteq S$ with $|X|\le D$, and prove $\Rk(\Sigma_X)\ge|X|$ for each of them.

\subsection{Enumeration}\label{sec:enum}

We search depth first over increasing sequences of term indices. A node is a set $Y\subseteq S$, and its subtree consists of the sets $Y\cup Z$ with $Z$ a set of indices larger than $\max Y$.

\paragraph{Symmetry.} The search numbers the terms in its own order: the $\Aut(S)$-orbits of terms in order of decreasing size, with ties broken by the least index, and within an orbit by increasing index in Appendix~\ref{app:schemes}. Lexicographic comparisons refer to this order, and we compare sets as sorted sequences. Since $\Aut(S)$ permutes the terms and preserves ranks and non-peelability (Lemma~\ref{lem:equiv}), we list only the lexicographically least set of each $\Aut(S)$-orbit of subsets. If $\sigma(Y)$ precedes $Y$ for some $\sigma\in\Aut(S)$, then no set in the subtree of $Y$ is lexicographically least, and we skip the subtree. Indeed, let $X=Y\cup Z$ with $Z>\max Y$, and let $i$ be the first position where the sorted sequences $\sigma(Y)$ and $Y=(y_1,y_2,\dots)$ differ. Then $\sigma(X)$ has at least $i$ elements below $y_i$, while $X$ has exactly $i-1$, and $\sigma(X)$ agrees with $X$ or lies below it at the earlier positions. So $\sigma(X)$ precedes $X$. A listed set $X$ carries the size $|\Aut(S)|/|\mathrm{Stab}(X)|$ of its orbit as a weight, where $\mathrm{Stab}(X)$ is the stabilizer of $X$ in $\Aut(S)$. The pruning is sound for any group of automorphisms of $S$, so it does not depend on knowing the full group. The subsets in Tables~\ref{tab:open} and~\ref{tab:hardest} are the representatives that the search found, written in the numbering of Appendix~\ref{app:schemes}. In that numbering the first subset of AT47 in Table~\ref{tab:hardest} is not lexicographically least in its orbit.

\paragraph{Free terms.} A term is free in a position if and only if it lies in no linear dependency among the factors in that position. Along the current search path we keep echelon forms of the factors in the three positions. Each row carries a tag, the set of terms it combines, and tags combine by symmetric difference, so a tag is exactly the support of the combination. A factor that reduces to zero gives a dependency, whose support is its tag. These dependencies form a basis of the space of all dependencies, since each involves a term that the earlier ones do not. The union of the supports of a basis is the union of the supports of all dependencies, which is the set of terms that are not free. We therefore know the free terms of $Y$ at constant cost per node.

\paragraph{Universe pruning.} All sets in the subtree of $Y$ lie in the universe $W=Y\cup\{s\in S: s>\max Y\}$. If a term of $Y$ is free in two positions within $W$, then by monotonicity it is peelable in every set of the subtree, and we skip the subtree. To test this, we store a basis of the linear dependencies among the factors of the terms in $W$, separately in the three positions, as matrices with columns indexed by $W$. A term is free within $W$ if and only if its column is zero. When an index leaves $W$, the update is one elimination step, a contraction in the dual matroid. In our C++ implementation of the enumeration, the correctness of this update is supported by the agreement of counts (Table~\ref{tab:summary}).

\subsection{Certification}\label{sec:cert}

Let $X$ be a listed non-peelable set with $|X|=k$. We write $T=\Sigma_X$ in reduced coordinates: in each position, the factors of $X$ are expressed in a basis of their span. For a list of terms, the greedy reduced coordinates are defined position by position: a factor of a term, taken in list order, becomes a basis vector if it is not in the span of the factors kept before it. We try the following bounds in this order and stop at the first one that gives $\Rk(T)\ge k$.
\begin{enumerate}[nosep]
\item The three flattening ranks.
\item Koszul flattenings with $p=1$ for four fixed projections $\pi\colon\Ft^{4\times4}\to\Ft^3$ of the first position. They are chosen so that $\pi(a_s)\ne0$ for all $s\in S$, since a projection that kills a term of $X$ cannot certify $X$ (Section~\ref{sec:flat}). In ambient coordinates their matrices change by one term per step of the search, so we update them incrementally.
\item Koszul flattenings with $p=1$ and $p=2$, for random projections in reduced coordinates.
\end{enumerate}
We call tests 1--3 the in-line tests, since they run during the enumeration. In the depth-16 run and in the first part of the depth-18 run they also included one level of substitution. We pass the sets left after the in-line tests to post-processing, which has three stages. In the first two we apply peeled substitution with the bounds above at the leaves, first with two levels and then with three or four levels and all pivots. In the third, for the few sets left after that, we use up to five levels of peeled substitution with the leaf bounds above, or of plain substitution with Koszul flattenings for $p=3$ at the leaves.

\paragraph{Certificates.} Apart from the four subsets of C3 (Section~\ref{sec:gsl}), every bound except one is found by a deterministic certifying program, with fixed seeds, that can emit it as an explicit certificate (Appendix~\ref{app:formats}); the exception is the subset of C4 (Section~\ref{sec:hardest}).

\subsection{Counts}

The numbers of non-peelable subsets of each size $k\le18$, weighted by orbit size, are in Table~\ref{tab:counts}. The outcome of the post-processing is in Appendix~\ref{app:runs}.

For the five decompositions the reduction to non-peelable subsets removes almost all subsets. About $98.4\%$ of the subsets of size 16 have an empty core, and the non-peelable subsets are about $0.05\%$ of the subsets of size 16. Over the five decompositions there are about $3.5\cdot10^9$ non-peelable subsets of size 16 (Table~\ref{tab:counts}). For comparison, about $6.46\cdot10^{12}$ of the $5\binom{47}{16}\approx7.52\cdot10^{12}$ subsets of size 16, or $86\%$, have all three flattenings rank-deficient, so the flattening test does not certify them.

\begin{table}[ht]
\centering
\caption{Non-peelable subsets of size $k$, weighted by orbit size. There are no nonempty ones with $k\le6$. All of them have full rank.}\label{tab:counts}
\small
\begin{tabular}{rrrrrr}
\toprule
$k$ & AT47 & KM47 & C3 & C4 & C5\\
\midrule
7 & 0 & 8 & 0 & 26 & 0\\
8 & 183 & 198 & 204 & 180 & 219\\
9 & 188 & 145 & 178 & 158 & 182\\
10 & 1{,}827 & 1{,}723 & 1{,}807 & 1{,}721 & 1{,}985\\
11 & 7{,}735 & 7{,}887 & 7{,}761 & 7{,}626 & 7{,}875\\
12 & 73{,}106 & 76{,}875 & 73{,}892 & 70{,}885 & 76{,}369\\
13 & 593{,}114 & 638{,}232 & 617{,}673 & 582{,}344 & 633{,}839\\
14 & 5{,}663{,}006 & 6{,}189{,}240 & 5{,}925{,}614 & 5{,}588{,}900 & 6{,}113{,}109\\
15 & 59{,}345{,}163 & 65{,}789{,}884 & 61{,}773{,}855 & 58{,}027{,}883 & 63{,}924{,}882\\
16 & 680{,}464{,}489 & 750{,}094{,}461 & 692{,}083{,}701 & 671{,}378{,}921 & 722{,}958{,}867\\
17 & 7{,}362{,}510{,}297 & 7{,}977{,}283{,}543 & 7{,}358{,}929{,}678 & 7{,}517{,}279{,}220 & 7{,}788{,}773{,}768\\
18 & 63{,}184{,}632{,}311 & 66{,}992{,}981{,}254 & 62{,}635{,}166{,}253 & 67{,}371{,}750{,}921 & 66{,}540{,}556{,}157\\
\bottomrule
\end{tabular}
\end{table}

\section{Proof of the main theorem}\label{sec:results}

\subsection{Depth 18}\label{sec:d18}

\begin{table}[ht]
\centering
\caption{The four hardest subsets of C3 (term numbers as in Table~\ref{tab:schemes}). Spans gives the dimensions of the spans of the factors in the three positions.}\label{tab:open}
\begin{tabular}{clcc}
\toprule
 & Terms & $|Y|$ & Spans\\
\midrule
$Y_1$ & 0 5 8 9 10 11 13 15 16 19 24 25 28 34 35 39 44 45 & 18 & $10\times11\times10$\\
$Y_2$ & 0 3 4 5 9 15 17 19 23 25 26 35 38 41 42 44 45 46 & 18 & $9\times12\times10$\\
$Y_3$ & 0 3 4 5 9 15 17 19 23 26 35 36 37 38 41 42 44 46 & 18 & $9\times10\times12$\\
$Y_4$ & 0 5 8 10 11 13 16 19 24 25 28 32 34 35 39 44 45 & 17 & $9\times11\times9$\\
\bottomrule
\end{tabular}
\end{table}

\begin{proof}[Proof of Theorem~\ref{thm:main}]
As in Section~\ref{sec:method}, we only need to prove $\Rk(\Sigma_X)=|X|$ for the non-peelable subsets $X$ of size at most 18 of the five decompositions, up to their automorphism groups, which preserve non-peelability (Lemma~\ref{lem:equiv}). We list these subsets with the enumeration (Section~\ref{sec:enum}; their numbers are in Table~\ref{tab:counts}). All of them except nine orbits are certified by the in-line tests or in post-processing (Section~\ref{sec:cert}). Five of the nine, the subsets of Table~\ref{tab:hardest}, are settled in Section~\ref{sec:hardest}. The other four are the orbits of Table~\ref{tab:open}, which have full rank by Theorem~\ref{thm:Y} and Lemma~\ref{lem:equiv}.
\end{proof}

\begin{proof}[Proof of Corollary~\ref{cor:main}]
Apply Lemma~\ref{lem:share} with $r=47$ and $D=18$.
\end{proof}

\begin{remark}[$\dagger$]\label{rem:d16}
Local optimality to depth 16, which Theorem~\ref{thm:main} implies, was also proved in a separate run of the same argument, in which every listed subset was certified by the in-line tests or in post-processing. At depth 16 there are two further checks: an enumeration without peeling, with an independent checker on all of its post-processing certificates, and a Lean proof with 40 compiled evaluations (Table~\ref{tab:summary}).
\end{remark}

\subsection{The hardest settled subsets}\label{sec:hardest}

We settle the five subsets of Table~\ref{tab:hardest} as follows.

For the subset $X$ of C4, write $\Sigma_X$ in the reduced coordinates of the second position, with the greedy basis (Section~\ref{sec:cert}) of its second-position factors taken in the term order 0, 1, 11, 17, 3, 22, 38, 15, 39, 40, 6, 26, 9, 14, 4, 31, 36, 32. Its first two vectors $b_0$ and $b_1$ are the second factors of terms 0 and 1. In these coordinates $\Sigma_X$ has 16 linearly independent slices $M_0,\dots,M_{15}$ in the second position. We apply Lemma~\ref{lem:subst} in this position with $M_2,\dots,M_{15}$ as the $k=14$ independent slices. The tensors in the minimum are then the pencils $e_0\otimes s_0+e_1\otimes s_1$ with $s_0\in M_0+\spn(M_2,\dots,M_{15})$ and $s_1\in M_1+\spn(M_2,\dots,M_{15})$. Each pair $(s_0,s_1)$ comes from exactly one matrix $c$, so there are $2^{28}$ pencils. Equivalently, the pencils are $\bigl((1\otimes f_0\otimes1)\Sigma_X,(1\otimes f_1\otimes1)\Sigma_X\bigr)$, where $f_0$ and $f_1$ range over the linear forms on the span of the second factors with $f_i(b_j)=\delta_{ij}$ for $i,j\in\{0,1\}$. The two families therefore depend only on $b_0$ and $b_1$. The count 57 below refers to this choice of $b_0$ and $b_1$. A pencil has rank at least the matrix rank of each of its slices, and only 57 of the $2^{14}$ matrices in each of the two families have rank at most 3. For each of the remaining $57\cdot57=3{,}249$ pairs, one of the flattenings $[\,s_0\ s_1\,]$ and $\bigl[\begin{smallmatrix}s_0\\ s_1\end{smallmatrix}\bigr]$ has rank at least 4. Hence every pencil has rank at least 4, and $\Rk(\Sigma_X)\ge14+4=18$.

The other four subsets of Table~\ref{tab:hardest} were certified with the methods of the third stage of post-processing, in further runs of the certifying programs with other fixed seeds: the two subsets of AT47 by peeled substitution with four and three levels, and the two subsets of KM47 by plain substitution with all pivots, with two and four levels.

\begin{table}[ht]
\centering
\caption{The five hardest settled subsets, all of size 18 (term numbers as in Table~\ref{tab:schemes}, Spans as in Table~\ref{tab:open}). Size is the number of nodes of the certificate as counted by the checkers, and for C4 the number of pencils.}\label{tab:hardest}
\footnotesize
\begin{tabular}{@{}l>{\raggedright\arraybackslash}p{4.2cm}cll@{}}
\toprule
Scheme & Terms & Spans & Method & Size\\
\midrule
C4 & 0 1 3 4 6 9 11 14 15 17 22 26 31 32 36 38 39 40 & $10\times16\times10$ & Lemma~\ref{lem:subst}, $k=14$ & $2^{28}$ pencils\\
\addlinespace
AT47 & 13 14 15 17 20 21 24 26 29 32 33 34 37 42 43 44 45 46 & $10\times10\times11$ & peeled, 4 levels & $1.3\cdot10^6$ nodes\\
\addlinespace
AT47 & 13 14 15 17 18 19 20 24 26 28 32 34 36 37 40 43 44 45 & $12\times10\times11$ & peeled, 3 levels & $1.8\cdot10^8$ nodes\\
\addlinespace
KM47 & 0 2 10 11 12 16 17 18 19 20 22 24 27 32 33 35 41 42 & $10\times15\times10$ & plain, 2 levels & $1.3\cdot10^8$ nodes\\
\addlinespace
KM47 & 4 5 6 8 10 11 12 16 20 21 23 25 30 33 34 36 37 44 & $9\times11\times12$ & plain, 4 levels & $1.4\cdot10^7$ nodes\\
\bottomrule
\end{tabular}
\end{table}

\section{Substitution over subspaces with lifting}\label{sec:gsl}

This section develops a lower-bound method for any tensor $T$ over $\Ft$ that is concise in one position and any bound $c$. It proves $\Rk(T)\ge c$ through statements about the minimal decompositions of $T$. Neither these statements, one for each node of a certificate, nor the capacity, rank and lifting leaves (Section~\ref{sec:gsl-leaves}) bound the border rank, so the method can pass the border-rank barrier. Compared with the substitution certificates (Section~\ref{sec:cert}), its certificates (i) substitute in one position only, with an arbitrary nonzero linear form as pivot, and record the subspace spanned by the eliminated first factors; (ii) pass from each node to its parent a statement about the decompositions of the whole tensor, where plain substitution would pass a lower bound for the rank of a quotient; and (iii) settle some leaves by SAT instances on the whole tensor. We apply the method to the four subsets of C3 in Table~\ref{tab:open} (Section~\ref{sec:gsl-result}).

Throughout this section the field is $\Ft$, $T\in A\otimes B\otimes C$, and $c\ge1$ is the bound to be proved. For the subsets of C3 we take $T=\Sigma_Y$ in reduced coordinates (Section~\ref{sec:cert}) and $c=|Y|$. Any of the three positions of $Y$ may serve as $A$.

\subsection{Quotients and the invariant}\label{sec:gsl-setting}

We assume that $A\ne0$ and that $T$ is \emph{concise} in the first position, that is, $T\notin A'\otimes B\otimes C$ for every proper subspace $A'\subset A$. In particular $T\ne0$. The first factors of every decomposition of $T$ span $A$, since otherwise $T$ would lie in $A'\otimes B\otimes C$ for their span $A'$. For a subspace $U\subseteq A$ let $\pi_U\colon A\to A/U$ be the quotient map, and let $T/U=(\pi_U\otimes1\otimes1)T$. A decomposition $T=\sum_l\alpha_l\otimes\beta_l\otimes\gamma_l$ gives
\begin{equation}\label{eq:quot}
  T/U=\sum_{l:\ \alpha_l\notin U}\pi_U(\alpha_l)\otimes\beta_l\otimes\gamma_l ,
\end{equation}
because the terms with $\alpha_l\in U$ vanish. Applied to $T=\Sigma_Y$, \eqref{eq:quot} writes $T/U$ as the sum of the list $L_U$ of the rank-one terms $\pi_U(a_t)\otimes b_t\otimes c_t$ with $t\in Y$ and $a_t\notin U$, in the order of $Y$.

A set $E$ of terms of a decomposition \emph{spans} $U$ if the first factors of the terms in $E$ span $U$. A decomposition of $T$ is \emph{minimal} if it has $\Rk(T)$ terms. Over $\Ft$ the terms of a minimal decomposition are pairwise distinct, since two equal terms cancel.

\begin{definition}\label{def:N}
For a subspace $U\subseteq A$, let $N(U)$ be the statement that if $\Rk(T)<c$, then no minimal decomposition of $T$ has a set of terms that spans $U$.
\end{definition}

\begin{lemma}\label{lem:N}
Let $U\subseteq A$ be a subspace of dimension $d$.
\begin{enumerate}[label=\textup{(\alph*)},nosep]
\item $N(0)$ holds if and only if $\Rk(T)\ge c$.
\item If $\Rk(T/U)\ge c-d$, then $N(U)$ holds. In particular, $N(U)$ holds if $d\ge c$.
\end{enumerate}
\end{lemma}

\begin{proof}
(a) Minimal decompositions exist, and in each of them the empty set of terms spans $0$. Hence $N(0)$ fails exactly when $\Rk(T)<c$. (b) Let $\Delta$ be a minimal decomposition of $T$ with $|\Delta|<c$, and let $E\subseteq \Delta$ span $U$. Then $|E|\ge d$, and by~\eqref{eq:quot} the terms of $\Delta\setminus E$ give a decomposition of $T/U$ with at most $c-1-d$ terms. Hence $\Rk(T/U)\le c-1-d$.
\end{proof}

The converse of (b) fails, because $N(U)$ concerns only those decompositions of $T/U$ that come from a decomposition of $T$ with a set of terms spanning $U$. Thus $\Rk(T/U)$ can be smaller than $c-d$ while $N(U)$ holds, and Section~\ref{sec:gsl-result} gives many such subspaces for $Y_4$.

\subsection{Substitution with general pivots}\label{sec:gsl-sub}

For a nonzero point $p$ of $A/U$ let $U_p=\pi_U^{-1}(\langle p\rangle)$. This is the subspace $U+\langle\alpha\rangle$ for any $\alpha\in A$ with $\pi_U(\alpha)=p$, and it has dimension $\dim U+1$. Distinct points give distinct subspaces, since over $\Ft$ the line $\langle p\rangle$ has only one nonzero point.

\begin{lemma}\label{lem:gsub}
Let $U\subsetneq A$ be a subspace, and let $f$ be a nonzero linear form on $A/U$. If $N(U_p)$ holds for every $p\in A/U$ with $f(p)=1$, then $N(U)$ holds.
\end{lemma}

\begin{proof}
Suppose that $N(U)$ fails, so that some minimal decomposition $\Delta$ of $T$ with $|\Delta|<c$ has a set $E$ of terms that spans $U$. The linear form $f\circ\pi_U$ on $A$ is nonzero, and the first factors of $\Delta$ span $A$ because $T$ is concise. Hence $f(\pi_U(\alpha_t))=1$ for some term $t$ of $\Delta$, with first factor $\alpha_t$. Then $\alpha_t\notin U$, so $t\notin E$, and $E\cup\{t\}$ spans $U+\langle\alpha_t\rangle=U_p$ with $p=\pi_U(\alpha_t)$. Since $f(p)=1$, this contradicts $N(U_p)$.
\end{proof}

There are $2^{\dim(A/U)-1}$ points $p$ with $f(p)=1$, and as many children $U_p$. If $f$ is a coordinate function $x_j$ for a basis $e_0,e_1,\dots$ of $A/U$, the points with $f(p)=1$ are $p=e_j+\sum_{i\ne j}u_ie_i$, and $T/U_p=(T/U)/\langle p\rangle$ is the branch tensor of~\eqref{eq:onestep} for $T/U$, with pivot $j$ and parameter $u$, once $(A/U)/\langle p\rangle$ is identified with the span of the $e_i$ with $i\ne j$. So for a coordinate function the lemma is one step of plain substitution, and for a general $f$ it is the same step in another basis of $A/U$.

Suppose that $N(U_p)$ is known for every point $p$ outside a set $Q$. Then Lemma~\ref{lem:gsub} applies with some $f$ if and only if $Q$ does not span $A/U$, since $f$ must vanish on $Q$. With coordinate functions only, $Q$ would have to lie in a coordinate hyperplane, so general pivots settle more nodes.

\begin{definition}\label{def:dag}
A \emph{DAG certificate} for $(T,c)$ is a finite set $\mathcal N$ of subspaces of $A$ with $0\in\mathcal N$, in which every $U\in\mathcal N$ carries a label. The label is either a substitution label $f$, where $f$ is a nonzero linear form on $A/U$ such that $U_p\in\mathcal N$ for every $p$ with $f(p)=1$, or a leaf label (Section~\ref{sec:gsl-leaves}). A leaf label at $U$ is \emph{valid} if the corresponding rule proves $N(U)$.
\end{definition}

The edges from a node $U$ with a substitution label $f$ to its children $U_p$ form a directed acyclic graph, because the dimension rises by one along each edge. Since the statement $N(U)$ depends only on $U$, whatever sequence of pivots a search follows to reach it, a subspace reached along several paths is a single node with a single label.

\begin{theorem}\label{thm:dag}
If all leaf labels of a DAG certificate for $(T,c)$ are valid, then $N(U)$ holds for every $U\in\mathcal N$. In particular, $\Rk(T)\ge c$.
\end{theorem}

\begin{proof}
We prove $N(U)$ by downward induction on $\dim U$. Let $U\in\mathcal N$, and assume $N(U')$ for all $U'\in\mathcal N$ with $\dim U'>\dim U$. If $U$ has a leaf label, $N(U)$ holds because the label is valid. If $U$ has a substitution label $f$, all its children $U_p$ with $f(p)=1$ lie in $\mathcal N$ and have dimension $\dim U+1$, so $N(U_p)$ holds, and Lemma~\ref{lem:gsub} gives $N(U)$. For $U=0$, Lemma~\ref{lem:N}(a) gives $\Rk(T)\ge c$.
\end{proof}

The nodes reachable from $0$ form a DAG certificate by themselves, so the other nodes play no role and need not carry valid labels.

\subsection{Leaves}\label{sec:gsl-leaves}

Let $U\in\mathcal N$ have dimension $d$, and let $k=c-d$. Lemma~\ref{lem:core}, applied to the list $L_U$, gives
\[
  \Rk(T/U)=p_U+\Rk(X_U),\qquad\text{where } X_U=\Sigma_{\core(L_U)}\ \text{and}\ p_U=|L_U|-|\core(L_U)| .
\]
We write $X_U$ in the greedy reduced coordinates of $\core(L_U)$, with first position $\Ft^{e}$. The rank of $X_U$ is the same in these coordinates as in $(A/U)\otimes B\otimes C$, because projecting a decomposition of $X_U$ onto the spans of the factors of $X_U$, along fixed complements, gives a decomposition of $X_U$ with at most as many terms. A minimal decomposition therefore stays minimal under the projection, so none of its factors vanishes and its terms stay distinct. The first three kinds of leaves prove $\Rk(X_U)\ge k-p_U$, which gives $N(U)$ by Lemma~\ref{lem:N}(b). The fourth proves $N(U)$ directly.

\paragraph{Flattening leaves.} A flattening bound for $X_U$ with target $k-p_U$, given and checked as at the leaves of substitution certificates.

\paragraph{Capacity leaves.} Let $X\in\Ft^e\otimes B'\otimes C'$ be a tensor. For a subspace $K\subseteq\Ft^e$ we form $X/K$ as above, and for a linear form $g$ on $\Ft^e$ we write $X(g)=(g\otimes1\otimes1)X$, a matrix in $B'\otimes C'$. A \emph{multiset} on a set $P$ is a map $m\colon P\to\mathbb{Z}_{\ge0}$. Its size is $|m|=\sum_{p\in P}m(p)$, and we write $m(P')=\sum_{p\in P'}m(p)$ for $P'\subseteq P$. The first factors of a decomposition of $X$, counted with multiplicity, form a multiset on $\Ft^e\setminus\{0\}$.

\begin{lemma}\label{lem:count}
Let $K\subseteq\Ft^e$ be a subspace. In every decomposition of $X$, at least $\Rk(X/K)$ of the first factors lie outside $K$.
\end{lemma}

\begin{proof}
By~\eqref{eq:quot}, applied to $X$ and $K$, the terms whose first factors lie outside $K$ give a decomposition of $X/K$.
\end{proof}

Let $\lb$ assign to each proper subspace $K\subsetneq\Ft^e$ an integer $\lb(K)\le\Rk(X/K)$. A multiset $m$ on $\Ft^e\setminus\{0\}$ is \emph{admissible} if $m(\Ft^e\setminus K)\ge\lb(K)$ for every proper subspace $K$. The \emph{capacity} $\cp(X)$ is the least size of an admissible multiset. For $e=0$ the empty multiset is admissible and $\cp(X)=0$.

\begin{proposition}\label{prop:cap}
The first factors of every decomposition of $X$ form an admissible multiset. Hence $\Rk(X)\ge\cp(X)$.
\end{proposition}

\begin{proof}
For the multiset $m$ of first factors, $m(\Ft^e\setminus K)$ is the number of first factors outside $K$, which is at least $\Rk(X/K)\ge\lb(K)$ by Lemma~\ref{lem:count}. A minimal decomposition gives an admissible multiset of size $\Rk(X)$.
\end{proof}

For $e\ge1$ the subspace $K=0$ gives the constraint $|m|\ge\lb(0)$, so $\cp(X)\ge\lb(0)$, and the constraints for $K\ne0$ can raise the capacity further. Let $K$ have codimension $j\ge1$. The linear forms $g$ that vanish on $K$ are the forms on $\Ft^e/K$, and $X(g)$ is a quotient of $X/K$. If $j=1$, then $X/K\cong X(g)$ for the nonzero such $g$, and we take $\lb(K)=\rk X(g)=\Rk(X/K)$. If $j\ge2$, we take for $\lb(K)$ the maximum of the following lower bounds for $\Rk(X/K)$:
\begin{enumerate}[label=\textup{(\roman*)},nosep]
\item the ranks $\rk X(g)$ for the nonzero forms $g$ that vanish on $K$;
\item the \emph{averaging bound} $\bigl\lceil 2^{1-j}\sum_{g}\rk X(g)\bigr\rceil$, where $g$ runs over the $2^j-1$ nonzero forms that vanish on $K$;
\item the three flattening ranks of $X/K$ and, if $j\ge3$, the bounds~\eqref{eq:young} with $p=1$ for $X/K$ and all surjections $\pi\colon\Ft^e/K\to\Ft^3$;
\item if $3\le j<e$, the capacity of $X/K$, computed with the same rules for the quotients of $X/K$.
\end{enumerate}
Bound (i) holds because rank does not increase under linear maps, (iii) is Section~\ref{sec:flat}, and (iv) is Proposition~\ref{prop:cap} for $X/K$, whose quotients are quotients of $X$. For (ii), let $X/K=\sum_{l=1}^{r}\alpha_l\otimes\beta_l\otimes\gamma_l$ with $r=\Rk(X/K)$ and all $\alpha_l\ne0$. For each $g$, the matrix $X(g)=\sum_l g(\alpha_l)\,\beta_l\otimes\gamma_l$ has rank at most the number of $l$ with $g(\alpha_l)=1$. Each nonzero $\alpha_l$ has $g(\alpha_l)=1$ for exactly $2^{j-1}$ of the $2^j$ linear forms $g$ on $\Ft^e/K$. Summing over $g$ gives $\sum_g\rk X(g)\le 2^{j-1}r$.

The averaging bound counts points over $\Ft$, and it can exceed the border rank: for the tensor $W$ of Example~\ref{ex:W}, the three nonzero forms on the first position give slices of ranks 2, 1 and 2, so (ii) with $K=0$ gives $\Rk(W)\ge\lceil5/2\rceil=3$, whereas $\bRk(W)=2$.

A capacity leaf asserts $\cp(X_U)\ge k-p_U$. We use such leaves only for $e\le5$. The capacity is then the optimum of an integer program with at most $31$ variables $m(p)$ and $373$ constraints, one for each proper subspace of $\Ft^5$. The checker decides feasibility by a depth-first search over the variables with a node limit. A search that reaches the limit counts as undecided. Inside rule (iv) this only weakens a bound, so the capacities used are exact or lower bounds, and a capacity leaf, or the condition $\cp(X_U)\ge r$ of a rank leaf, counts only if the search proves it. A listing of the admissible multisets of a given size that reaches the node limit, or exceeds a cap on the number of instances, fails instead of being truncated.

\paragraph{Rank leaves.} Let $r=k-p_U-1$ and suppose that $e\le5$ and $\cp(X_U)\ge r$. Then $\Rk(X_U)\ge r+1$ unless $X_U$ has a decomposition with exactly $r$ terms. Such a decomposition is minimal, so its terms are distinct, and its first factors form an admissible multiset of size $r$ by Proposition~\ref{prop:cap}. A rank leaf therefore asserts that for every admissible multiset $m$ of size $r$ the following instance is unsatisfiable: $X_U=\sum_{l=1}^{r}\alpha_l\otimes\beta_l\otimes\gamma_l$, where $\alpha_1,\dots,\alpha_r$ are the points of $m$, repeated according to their multiplicities, and the $\beta_l$ and $\gamma_l$ are nonzero. Since the terms are distinct, we may require the terms with equal $\alpha_l$ to be in strictly increasing order of $(\beta_l,\gamma_l)$, for a fixed total order. A SAT solver decides these instances.

\paragraph{Lifting leaves.} A lifting leaf uses the whole tensor $T$. We use such leaves only for $\dim(A/U)\le5$, so that the admissible multisets for $T/U$ can be enumerated. Fix a lower bound $s_0\le\Rk(T/U)$, for instance $\max\bigl(\cp(T/U),\ p_U+\cp(X_U)\bigr)$. For an integer $s$ and a multiset $m$ of size $s$ on $(A/U)\setminus\{0\}$, let $\mathrm{Lift}(s,m)$ be the statement:
\begin{quote}
$T=\sum_{l=1}^{c-1}\alpha_l\otimes\beta_l\otimes\gamma_l$ with pairwise distinct terms, where exactly $s$ of the $\alpha_l$ lie outside $U$, their images $\pi_U(\alpha_l)$ are the points of $m$, counted with multiplicity, and the other $c-1-s$ of the $\alpha_l$ lie in $U\setminus\{0\}$.
\end{quote}
We call the $s$ terms with $\alpha_l\notin U$ the outer terms and the others the inner terms. The statement requires exactly $c-1$ terms. A decomposition with fewer terms is brought to this size by splitting terms.

\begin{lemma}[Padding]\label{lem:pad}
Let $\Delta$ be a list of pairwise distinct rank-one terms in $A\otimes B\otimes C$ with $|\Delta|\le c-2$, and suppose that $2^{\dim C-1}\ge c-1$. Let $x\otimes y\otimes z$ be a term of $\Delta$. Then there is a $z'\in C\setminus\{0,z\}$ such that replacing $x\otimes y\otimes z$ by the two terms $x\otimes y\otimes z'$ and $x\otimes y\otimes(z+z')$ gives a list of $|\Delta|+1$ pairwise distinct rank-one terms with the same sum. The same holds with $B$ in place of $C$.
\end{lemma}

\begin{proof}
The pairs $\{z',z+z'\}$ with $z'\notin\{0,z\}$ partition $C\setminus\{0,z\}$ into $2^{\dim C-1}-1$ pairs. Over $\Ft$ a rank-one tensor determines its three factors. So a new term coincides with another term of $\Delta$ only if that term has the form $x\otimes y\otimes z''$ with $z''$ in the chosen pair, and each of the other $|\Delta|-1\le c-3$ terms of $\Delta$ excludes at most one pair. Since $2^{\dim C-1}-1\ge c-2$, some pair is not excluded. Its two terms are nonzero, they differ from each other because $z\ne0$, and they differ from the remaining terms of $\Delta$.
\end{proof}

\begin{proposition}\label{prop:lift}
Suppose that $2^{\max(\dim B,\dim C)-1}\ge c-1$, and that $\mathrm{Lift}(s,m)$ fails for every $s$ with $s_0\le s\le c-1-d$ and every admissible multiset $m$ of size $s$ for $T/U$. Then $N(U)$ holds.
\end{proposition}

\begin{proof}
Suppose that $N(U)$ fails. Then some minimal decomposition $\Delta$ of $T$ with $|\Delta|<c$ has a set $E$ of terms that spans $U$. Let $J$ be the set of terms of $\Delta$ whose first factors lie in $U$, so that $E\subseteq J$ and $|J|\ge d$. Let $s=|\Delta|-|J|$, and let $m$ be the multiset of the points $\pi_U(\alpha_t)$ for the terms $t\notin J$. By~\eqref{eq:quot} these $s$ terms give a decomposition of $T/U$. Hence $s\ge\Rk(T/U)\ge s_0$, and $m$ is admissible by Proposition~\ref{prop:cap}. Moreover $s\le|\Delta|-d\le c-1-d$. If $|\Delta|=c-1$, then $\Delta$ satisfies $\mathrm{Lift}(s,m)$, because its terms are distinct.

If $|\Delta|<c-1$, we apply Lemma~\ref{lem:pad} repeatedly, in the larger of the second and third positions, until there are $c-1$ terms. If $J\ne\emptyset$, we always split a term of $J$. The two new terms have the same first factor, which lies in $U\setminus\{0\}$, so $s$ and $m$ do not change. If $J=\emptyset$, then $d=0$, and we split terms with first factors outside $U$, which exist because $T\ne0$. Splitting such a term with image $p$ replaces $(s,m)$ by $(s+1,m+\{p\})$. Adding a point keeps a multiset admissible, and at the end $s=c-1=c-1-d$. In both cases the final list satisfies $\mathrm{Lift}(s,m)$ for some admissible $m$ and some $s$ in the stated range. This contradicts the hypothesis.
\end{proof}

The condition on $\dim B$ and $\dim C$ cannot be dropped. Let $T=e_0\otimes e_0\otimes e_0\in\Ft\otimes\Ft\otimes\Ft$, $c=3$ and $U=0$. Since $T$ is the only rank-one tensor in this space, no two terms can be distinct, so every statement $\mathrm{Lift}(s,m)$ fails, and without the condition Proposition~\ref{prop:lift} would give $\Rk(T)\ge3$. In our certificates $c-1\le17$, and the larger of $\dim B$ and $\dim C$ is at least 11, so the condition holds with a wide margin.

The statement $\mathrm{Lift}(s,m)$ is a SAT instance. In a basis of $A$ whose first $d$ vectors form the reduced echelon basis of $U$ and whose other vectors are unit vectors mapping to a basis of $A/U$, an outer term has first factor $(x_l;p_l)$ with $p_l$ prescribed by $m$ and $x_l\in\Ft^d$ free, an inner term has first factor $(x_l;0)$ with $x_l\ne0$, and all $\beta_l$ and $\gamma_l$ are free nonzero vectors. Since the terms are distinct, the outer terms with equal $p_l$ may be required to be in strictly increasing order of $(x_l,\beta_l,\gamma_l)$, and the inner terms likewise.

The instance for $(s,m)$ can often be refuted more cheaply through the \emph{quotient relaxation}: $T/U=\sum_{l=1}^{s}p_l\otimes\beta_l\otimes\gamma_l$ with $p_1,\dots,p_s$ the points of $m$ and nonzero $\beta_l$, $\gamma_l$, where equal terms are allowed. If this relaxation is unsatisfiable, so is $\mathrm{Lift}(s,m)$, since $\pi_U$ maps a solution of $\mathrm{Lift}(s,m)$ to a solution of the relaxation by~\eqref{eq:quot}. Two outer terms that differ only in $x_l$ give equal terms of the relaxation, so we allow equal terms there. The proof of Proposition~\ref{prop:lift} would also work with relaxations that forbid equal terms. The decomposition it constructs has no two outer terms with the same image $p$ and the same $\beta_l$ and $\gamma_l$: in a minimal decomposition such terms would merge into one inner term, and padding never creates such a pair. If the relaxations for all $(s,m)$ are unsatisfiable, then $\Rk(T/U)\ge c-d$. So lifting instances are needed exactly at the nodes where some relaxation has a solution.

The format of the DAG certificates and the steps of their check are given in Appendix~\ref{app:formats}.

\subsection{The subsets of C3}\label{sec:gsl-result}

All four subsets of Table~\ref{tab:open} are non-peelable. Koszul flattenings with $p=2,3$ give $\Rk(\Sigma_{Y})\ge|Y|-2$ for all four, that is, 16 for $Y_1$, $Y_2$, $Y_3$ and 15 for $Y_4$, and none of the flattening bounds (Section~\ref{sec:flat}) that we know goes further. Substitution trees of up to five levels with randomized pivot orders did not settle these subsets. Their DAG certificates and the outcome of their check are described in Appendix~\ref{app:dag}. The check itself is specified in Appendix~\ref{app:formats}.

\begin{theorem}[$\dagger$]\label{thm:Y}
The subsets $Y_1$, $Y_2$, $Y_3$ and $Y_4$ of C3 in Table~\ref{tab:open} have full rank. In particular $\Rk(\Sigma_{Y_4})=17$, and $\Rk(\Sigma_Y)=18$ for the other subsets $Y$ in the statement.
\end{theorem}

\begin{proof}
The sum $\Sigma_Y$ has $|Y|$ terms, so $\Rk(\Sigma_Y)\le|Y|$. For the lower bound, $\Sigma_Y$ is concise in the position used as $A$, and the nodes of its certificate (Table~\ref{tab:dag}) that are reachable from $0$ form a DAG certificate for $(\Sigma_Y,|Y|)$ whose leaf labels are all valid: the DAG checker recomputed every reachable node, checked its flattening and capacity leaves, and settled by the rank or the lifting rule every other reachable leaf (Appendix~\ref{app:formats}). Theorem~\ref{thm:dag} gives $\Rk(\Sigma_Y)\ge|Y|$.
\end{proof}

In the certificate for $Y_4$, $122{,}003$ nodes have two or more parents, and unfolded into a tree the certificate would have $803{,}089$ nodes. At $491$ of the lifting leaves no leaf that uses Lemma~\ref{lem:N}(b) can settle the node, because $\Rk(\Sigma_{Y_4}/U)=c-d-1$ there: the checker found a decomposition of $X_U$ with $k-p_U-1$ terms, while $\cp(X_U)\ge k-p_U-1$. At the other $70$ lifting leaves $\cp(X_U)<k-p_U-1$, which excludes the rank rule.

\subsection{Relation to earlier work}\label{sec:gsl-prior}

Wang~\cite{Wang2026automated} gives an automated framework for certified rank lower bounds over finite fields, with forced products and substitution with backtracking, for formats up to $\mm344$. Forced products use rank-one slices of the tensor and enumerate the remaining coefficients, whereas peeling uses the known terms of a subset and needs no enumeration. Two parts of our construction also occur in Wang's framework. Its substitution lemma~\cite[Lemma~3]{Wang2026automated} eliminates first factors in arbitrary directions, several in turn: in our notation it passes from $T/U$ to $T/U_p$ for arbitrary points $p$, and Lemma~\ref{lem:gsub} is the one-form step, stated for $N(U)$. Subspaces also index its dynamic program, which assigns certified lower bounds to the ranks of all restrictions of the first argument of a bilinear map, up to symmetry. In our notation such a restriction is a quotient $T/U$, whereas a DAG certificate is evaluated at exactly the nodes reachable from $0$.

Bounds for small formats over $\Ft$ also combine capacity inequalities, by which the number of first factors of a decomposition outside a subspace is at least the rank of the quotient of the tensor by that subspace, with an enumeration of the multisets of first factors that satisfy all of them~\cite{Wang2026automated,DAmbrosio2026,Wang2026rank21,YangEtAl2026,Tomar2026rank23}. Lemma~\ref{lem:count} and Proposition~\ref{prop:cap} are the capacity inequality and the admissible profiles of D'Ambrosio~\cite[Sec.~4, (8)]{DAmbrosio2026} and Wang~\cite[Lemma~2.1]{Wang2026rank21}. The substitution with backtracking of Wang~\cite[Sec.~5.4]{Wang2026automated} already combines the inequality, for subspaces spanned by first factors, with an exhaustive search over multisets of first factors. Yang et al.~\cite[Lemma~2.2]{YangEtAl2026} call the inequality the occupation inequality, and they exclude multisets of first factors by integer programming with Farkas-type certificates~\cite[Sec.~3.3]{YangEtAl2026}. The averaging bound for a subspace $K$ of codimension $j$ is their cover inequality~\cite[(3.6)--(3.7)]{YangEtAl2026} for the $2^j-1$ hyperplanes that contain $K$, since every nonzero point of $\Ft^e/K$ lies in exactly $2^{j-1}-1$ of them. Earlier, Shpilka's lower bounds for $n\times n$ matrices over finite fields~\cite{Shpilka2003} discard the products whose linear forms vanish on suitably chosen matrices (Lemmas 3 and~6 in the numbering of its arXiv text). Over $\Ft$ a code argument bounds the remaining products, and over $\mathrm{GF}(p)$ they are bounded by an inequality of the above kind for a three-dimensional space of matrices, due to Bl\"aser~\cite{Blaser1999FOCS} (Lemma 9 in the arXiv text of~\cite{Shpilka2003}). For a subspace $K$ of codimension one, Lemma~\ref{lem:count} is the correspondence between bilinear algorithms and linear codes~\cite{BrockettDobkin1978,LempelWinograd1977}. The first factors are the columns of a generator matrix, and the codeword of the form $g$ that vanishes on $K$ has weight at least $\rk X(g)$. For larger codimension, Lemma~\ref{lem:count} bounds the support of a subcode, in the sense of the generalized Hamming weights of Wei~\cite{Wei1991}.

The completion search of~\cite{Tomar2026rank23} decides instances like those of the rank leaves, in which all first factors are prescribed, by an exhaustive search for the second and third factors, and D'Ambrosio~\cite{DAmbrosio2026} mentions SAT instances with a fixed profile of first factors as diagnostics. In $\mathrm{Lift}(s,m)$ only the images of the first factors in $A/U$ are prescribed, and the instance concerns $T$ itself. D'Ambrosio~\cite[Sec.~5]{DAmbrosio2026} and Wang~\cite[Sec.~4]{Wang2026rank21} exclude by hand the few multisets of first factors that satisfy all capacities in their problems, with arguments on the second and third factors, and Yang et al.~\cite[Sec.~1.1]{YangEtAl2026} refute the profile of first factors forced by their occupation bounds with relations between the factors of the whole tensor. We are not aware of earlier lower-bound arguments that propagate statements such as $N(U)$ instead of rank bounds for quotients, or that use instances such as $\mathrm{Lift}(s,m)$, in which the first factors are prescribed only modulo a subspace.

\section{Verification}\label{sec:verif}

The statements marked with a dagger rest on computations: the search over $G$ and the matching, the enumeration, the certificates produced by the deterministic certifying programs, the direct computation for the subset of C4 and the DAG certificates. Table~\ref{tab:summary} summarizes how the main statements are certified and checked.

\begin{table}[ht]
\centering
\caption{How the main computer-assisted statements are certified and checked. All further checks agree with the certification.}\label{tab:summary}
\footnotesize
\begin{tabularx}{\textwidth}{@{}>{\raggedright\arraybackslash}p{2cm}>{\raggedright\arraybackslash}X>{\raggedright\arraybackslash}X>{\raggedright\arraybackslash}p{2.3cm}@{}}
\toprule
Statement & Certified by & Further checks & Lean\\
\midrule
Theorem~\ref{thm:classes} & (a) expansion; (b) the invariant $\rho$; (c) a search over $G$; (d) inspection & -- & (a) proved\\
\addlinespace[1pt]
Remark~\ref{rem:search} & explicit equivalences and invariant hashes (Appendix~\ref{app:search}) & -- & --\\
\addlinespace[1pt]
Table~\ref{tab:counts} & the enumeration (Section~\ref{sec:enum}) & count-only program; a separate sampler ($k=16,17,18$), within two standard errors & --\\
\addlinespace[1pt]
$\LO(16)$, Remark~\ref{rem:d16} & in-line tests and post-processing (Section~\ref{sec:cert}) & enumeration without peeling (sizes 5 to 16), an independent checker on all of its post-processing certificates and a sample of its in-line ones & proved, 40 compiled evaluations\\
\addlinespace[1pt]
Theorem~\ref{thm:main} & as for $\LO(16)$, with Section~\ref{sec:hardest} and Theorem~\ref{thm:Y} for nine orbits & all post-processing certificates, samples of the in-line ones, the four certificates of Table~\ref{tab:hardest}, all $2^{28}$ pencils for C4 & proved; the subset of C4 kernel-only\\
\addlinespace[1pt]
Theorem~\ref{thm:Y} & DAG certificates (Section~\ref{sec:gsl}) & DAG checker, with LRAT proofs checked by \texttt{lrat-check} & proved, with LRAT proofs checked in Lean\\
\bottomrule
\end{tabularx}
\end{table}

\subsection{Independent checks}\label{sec:checks}

Independently written checkers, developed from specifications separately from the enumeration and certifying programs, checked the certificates as listed in Table~\ref{tab:summary}. The other further checks there come from a count-only program for the non-peelable subsets and an enumeration of all pencils for the subset of C4, both written from specifications in the same way, from a sampler that shares no code with the enumeration, and from an earlier enumeration program, run without peeling. The DAG checker counts an unsatisfiable instance only if \texttt{lrat-check}~\cite{WetzlerHeuleHunt2014DRATtrim} verifies its LRAT proof~\cite{CruzFilipeEtAl2017LRAT}, which CaDiCaL~\cite{BiereEtAl2024CaDiCaL} produced, against the formula that was solved. Certificates other than the checked ones rely on the correctness of the certifying programs. For the DAG certificates the LRAT proofs certify that the formulas are unsatisfiable; the encoding of the instances, the node computations and the enumeration of the admissible multisets rest on the DAG checker, on the scripts that distributed its runs and carried results over between runs and certificate versions, and on the tests of these programs, which are in the archive (see Data and code availability).

\subsection{Formal proofs in Lean}\label{sec:lean}

We formalize Theorems~\ref{thm:classes}(a), \ref{thm:main} and~\ref{thm:Y}, as well as local optimality to depth 16, in Lean~4 with Mathlib~\cite{deMouraUllrich2021,mathlib2020}; on the way to depth 18 the development also proves local optimality to depth 17 of the five decompositions. Tensors are taken over $\Ft$, the rank of a tensor is the least $r$ such that it is a sum of $r$ outer products, and equivalence allows invertible linear maps of $\Ft^{16}$ on each factor, a permutation of the three factors and a reordering of the terms, so it contains the action of $G$. No proof uses \lean{sorry}, Lean's placeholder for a missing proof. The kernel checks the flattening, Koszul and substitution bounds, the peeling lemma, the soundness of a certificate checker, the soundness of the enumeration with symmetry and universe pruning, and the transfer to equivalent lists. Lean runs its own enumeration, which follows Sections~\ref{sec:peel} and~\ref{sec:enum} but recomputes the universe matrices instead of updating them, so the theorems depend neither on the C++ enumeration nor on the contraction update. In the Lean runs a non-peelable set gets a Koszul certificate, a certificate from an in-line search or, at depths 17 and 18, a peeled-substitution certificate from a Lean version of the search of Section~\ref{sec:cert}, and a proved checker verifies it. Data from the C++ searches enter only as certificates that proved checkers verify. A run may also accept, without a certificate, the sets in the orbits of finitely many listed sets, among them the nine orbits that remain after post-processing (Section~\ref{sec:d18}). Lean proves their full rank separately: by substitution certificates that proved checkers verify, by a proof for the subset of C4 that follows Section~\ref{sec:hardest}, and, for the subsets of C3, by the proof of Theorem~\ref{thm:Y}. For that proof Lean formalizes substitution over subspaces with lifting (Section~\ref{sec:gsl}), with the standing assumption $A\ne0$: it proves Lemma~\ref{lem:gsub}, Theorem~\ref{thm:dag}, the leaf rules (Section~\ref{sec:gsl-leaves}) with the capacity bound and the search that computes it, Lemma~\ref{lem:pad} and Proposition~\ref{prop:lift}, and it recomputes the nodes of each certificate as in Appendix~\ref{app:formats}. It also proves that every decomposition described by a rank instance, a lifting instance or a relaxation gives a satisfying assignment of its CNF formula, so the encoding is not trusted. The refutations are LRAT proofs for CNF formulas generated by the same Lean function that the soundness proof uses, and the verified LRAT checker of Lean core checks them.

Apart from the evaluations by \lean{native\_decide}, which runs a decision procedure as compiled code, the kernel checks every step of the Lean proofs of this section, and each evaluation adds an axiom. The trusted base of a theorem with such axioms is therefore the Lean kernel and the compiled code of its evaluations. That code depends on the Lean compiler and runtime and, for precompiled modules, on Lean's C toolchain. In the proofs for the subsets of C3, the evaluated code includes the LRAT checker of Lean core, whose soundness is a theorem of Lean core. The proof for the subset of C4 is kernel-only, and so is the proof of local optimality to depth 8 for every decomposition equivalent to one of the five. The formalization does not cover parts (b)--(d) of Theorem~\ref{thm:classes}, that is, the pairwise inequivalence of the five decompositions, the orders of their automorphism groups and the distinctness of their factors, nor that the Lean data for AT47 and KM47 are the decompositions of~\cite{FawziEtAl2022} and~\cite{KauersMoosbauerFlipsRepo}. The symmetry pruning uses automorphisms checked by Lean.

\section{Concluding remarks}\label{sec:open}

Whether $\Rk_{\Ft}(\mm444)=47$ is itself a question of local optimality: it holds if and only if one, or equivalently every, decomposition $S$ of rank 47 is locally optimal to depth 47, since $X=S$ sums to $\mm444$ itself, and a set $X\subseteq S$ with $\Rk(\Sigma_X)<|X|$ would give a decomposition of $\mm444$ with fewer than 47 terms. Is any of the five decompositions locally optimal to depth 19? If one of them is not, then $\Rk_{\Ft}(\mm444)\le46$. What limits the depth is the number of non-peelable subsets, which grows roughly tenfold with each size from 11 to 18 in Table~\ref{tab:counts} and reaches about $6.3\cdot10^{10}$ to $6.7\cdot10^{10}$ per decomposition at size 18, weighted by orbit size, together with the cost of certifying all of them.

Do the sums of the four subsets of C3 in Table~\ref{tab:open} have border rank below their size? We do not know. If they do, no flattening bound can prove that they have full rank, which would be consistent with the bound $|Y|-2$ that Koszul flattenings give for them (Section~\ref{sec:gsl-result}).

\section*{Data and code availability}

The archive at \url{https://doi.org/10.5281/zenodo.23652770} contains the five decompositions; the programs for the enumeration and the certification; the certificate checkers, two in Python and two in C++, with their specifications and tests; the count-only program, the sampler, the script for the bound for the subset of C4 and the independent program that checks it (Appendix~\ref{app:pencils}); the result tables; the stored certificates, which are samples of the depth-18 run, certificates of the hardest subsets and the DAG certificates (the three largest stored substitution certificates and the four DAG certificates are separate data files of the same record, listed in its \texttt{MANIFEST.md}); the search program for the DAG certificates and the DAG checker with its driver, specification, tests (listed in \texttt{repo/gsublift/checker/README.md}) and reports, together with per-instance outcome tables derived from the journals of the checks; and the Lean development. The README files of the archive give the commands, the runs and their costs, the tests of the checkers, and the Lean theorems with their axioms.

\section*{Acknowledgment}

This research received no specific funding.

\section*{Use of AI tools}

Generative AI tools contributed to this work as follows. They did not contribute to choosing the topic, the rank of $4\times4$ matrix multiplication over $\Ft$, a long-standing open problem that the author chose to work on. They helped with the conceptual approach and made central technical contributions: they were used to find and prove the results, including the peeling lemma and the enumeration and certification methods, and to write the programs, the certificate checkers and the Lean formalization. They were also used for writing and exposition (drafting and revising the text), for checking for errors (reviewing the proofs, the programs and the text), and for other supporting tasks (searching the literature and running the computations). The author takes full responsibility for the content of the paper, including the parts produced with these tools.

\bibliographystyle{plain}
\begingroup\footnotesize
\bibliography{refs}
\endgroup

\appendix

\section{The five decompositions}\label{app:schemes}

The five decompositions are in Table~\ref{tab:schemes}. A matrix $M=(m_{ij})$ with $0\le i,j\le3$ has the code $\sum_{i,j}m_{ij}2^{4i+j}$ in hexadecimal, so the last digit encodes row 0, with bit $j$ for column $j$. With $\mm444=\sum_{i,j,k}E_{ij}\otimes E_{jk}\otimes E_{ki}$, each of the five sums to $\mm444$ over $\Ft$.

\begin{table}[!htbp]
\centering
\caption{The five decompositions. Row $t$ gives the codes of $a_t$, $b_t$, $c_t$ for each decomposition.}\label{tab:schemes}
\scriptsize
\renewcommand{\arraystretch}{0.85}
\setlength{\tabcolsep}{2.2pt}
\begin{tabular}{r@{\hspace{9pt}}ccc@{\hspace{9pt}}ccc@{\hspace{9pt}}ccc@{\hspace{9pt}}ccc@{\hspace{9pt}}ccc}
\toprule
 & \multicolumn{3}{c}{AT47} & \multicolumn{3}{c}{KM47} & \multicolumn{3}{c}{C3} & \multicolumn{3}{c}{C4} & \multicolumn{3}{c}{C5} \\
\cmidrule(l{6pt}r{0pt}){2-4} \cmidrule(l{6pt}r{0pt}){5-7} \cmidrule(l{6pt}r{0pt}){8-10} \cmidrule(l{6pt}r{0pt}){11-13} \cmidrule(l{6pt}r{0pt}){14-16}
$t$ & $a_t$ & $b_t$ & $c_t$ & $a_t$ & $b_t$ & $c_t$ & $a_t$ & $b_t$ & $c_t$ & $a_t$ & $b_t$ & $c_t$ & $a_t$ & $b_t$ & $c_t$ \\
\midrule
0 & \texttt{0004} & \texttt{0100} & \texttt{0013} & \texttt{0008} & \texttt{edee} & \texttt{baa8} & \texttt{0555} & \texttt{9b90} & \texttt{9ef1} & \texttt{00b0} & \texttt{ccac} & \texttt{1e3d} & \texttt{0001} & \texttt{0001} & \texttt{0001} \\
1 & \texttt{0064} & \texttt{0890} & \texttt{1002} & \texttt{7048} & \texttt{6d66} & \texttt{bba8} & \texttt{94d3} & \texttt{b994} & \texttt{929d} & \texttt{df62} & \texttt{0343} & \texttt{9909} & \texttt{2000} & \texttt{2212} & \texttt{0078} \\
2 & \texttt{0054} & \texttt{0405} & \texttt{0102} & \texttt{d000} & \texttt{38b3} & \texttt{8008} & \texttt{c0cc} & \texttt{8990} & \texttt{6606} & \texttt{3333} & \texttt{fc0f} & \texttt{d0d0} & \texttt{9800} & \texttt{b282} & \texttt{b000} \\
3 & \texttt{0044} & \texttt{0d95} & \texttt{0002} & \texttt{0409} & \texttt{0303} & \texttt{4554} & \texttt{a00a} & \texttt{8a20} & \texttt{5e0d} & \texttt{9b22} & \texttt{0353} & \texttt{55c9} & \texttt{0800} & \texttt{1888} & \texttt{b004} \\
4 & \texttt{0001} & \texttt{0001} & \texttt{0105} & \texttt{98a0} & \texttt{62b9} & \texttt{4ea8} & \texttt{9579} & \texttt{0008} & \texttt{eee0} & \texttt{0090} & \texttt{1cac} & \texttt{0033} & \texttt{0230} & \texttt{4272} & \texttt{0b00} \\
5 & \texttt{0101} & \texttt{039b} & \texttt{0004} & \texttt{6000} & \texttt{6db6} & \texttt{0800} & \texttt{1001} & \texttt{202a} & \texttt{00e0} & \texttt{9944} & \texttt{1206} & \texttt{44dd} & \texttt{c06e} & \texttt{0200} & \texttt{2850} \\
6 & \texttt{0501} & \texttt{0302} & \texttt{0014} & \texttt{0400} & \texttt{0ed3} & \texttt{4958} & \texttt{0cc0} & \texttt{0dd0} & \texttt{dd0d} & \texttt{ff42} & \texttt{fc4c} & \texttt{3330} & \texttt{953e} & \texttt{4280} & \texttt{2840} \\
7 & \texttt{0367} & \texttt{0090} & \texttt{1000} & \texttt{0159} & \texttt{0202} & \texttt{4444} & \texttt{6acc} & \texttt{8d90} & \texttt{9609} & \texttt{1c91} & \texttt{bc0c} & \texttt{3300} & \texttt{950d} & \texttt{0008} & \texttt{1000} \\
8 & \texttt{3002} & \texttt{0045} & \texttt{0108} & \texttt{540a} & \texttt{0dd0} & \texttt{4d58} & \texttt{0222} & \texttt{fdf0} & \texttt{9e4d} & \texttt{5055} & \texttt{6006} & \texttt{45dd} & \texttt{4500} & \texttt{4d84} & \texttt{7000} \\
9 & \texttt{6002} & \texttt{0320} & \texttt{0018} & \texttt{98c0} & \texttt{b2b9} & \texttt{0220} & \texttt{6066} & \texttt{8a90} & \texttt{9e01} & \texttt{2022} & \texttt{0060} & \texttt{a536} & \texttt{903b} & \texttt{0002} & \texttt{0010} \\
10 & \texttt{2002} & \texttt{0375} & \texttt{0008} & \texttt{5000} & \texttt{3de3} & \texttt{4558} & \texttt{944b} & \texttt{202d} & \texttt{9edd} & \texttt{ff72} & \texttt{fc7f} & \texttt{7eed} & \texttt{4600} & \texttt{4484} & \texttt{7800} \\
11 & \texttt{3057} & \texttt{0005} & \texttt{0100} & \texttt{0800} & \texttt{c213} & \texttt{4aa8} & \texttt{844a} & \texttt{505d} & \texttt{0e00} & \texttt{bb00} & \texttt{3053} & \texttt{158d} & \texttt{a800} & \texttt{2282} & \texttt{b040} \\
12 & \texttt{6507} & \texttt{0300} & \texttt{0010} & \texttt{070a} & \texttt{0210} & \texttt{4551} & \texttt{8468} & \texttt{0558} & \texttt{d00d} & \texttt{cccc} & \texttt{6c06} & \texttt{fedd} & \texttt{9080} & \texttt{b288} & \texttt{00d0} \\
13 & \texttt{1000} & \texttt{3046} & \texttt{0c08} & \texttt{0739} & \texttt{0209} & \texttt{0202} & \texttt{955c} & \texttt{9090} & \texttt{9e0e} & \texttt{cc00} & \texttt{1071} & \texttt{f566} & \texttt{0100} & \texttt{4d8d} & \texttt{0004} \\
14 & \texttt{9008} & \texttt{3002} & \texttt{0cd8} & \texttt{0049} & \texttt{0308} & \texttt{1302} & \texttt{2ec2} & \texttt{8dd0} & \texttt{d60d} & \texttt{9f22} & \texttt{0303} & \texttt{ccc0} & \texttt{0537} & \texttt{0004} & \texttt{0100} \\
15 & \texttt{8008} & \texttt{7402} & \texttt{0ca8} & \texttt{704e} & \texttt{0b00} & \texttt{1100} & \texttt{1011} & \texttt{b993} & \texttt{0060} & \texttt{9922} & \texttt{fc53} & \texttt{40dd} & \texttt{9b30} & \texttt{4282} & \texttt{0040} \\
16 & \texttt{0301} & \texttt{0098} & \texttt{1004} & \texttt{520a} & \texttt{0220} & \texttt{4440} & \texttt{0110} & \texttt{022f} & \texttt{00d0} & \texttt{cc41} & \texttt{fc08} & \texttt{dddd} & \texttt{2030} & \texttt{4274} & \texttt{0070} \\
17 & \texttt{9a08} & \texttt{3000} & \texttt{84d0} & \texttt{0850} & \texttt{1213} & \texttt{4664} & \texttt{c02c} & \texttt{8880} & \texttt{ee86} & \texttt{2f92} & \texttt{fc0c} & \texttt{dd0d} & \texttt{0004} & \texttt{0100} & \texttt{7d05} \\
18 & \texttt{0a08} & \texttt{3020} & \texttt{c0d4} & \texttt{075f} & \texttt{0200} & \texttt{0111} & \texttt{c00c} & \texttt{8080} & \texttt{ee0e} & \texttt{9c55} & \texttt{1706} & \texttt{55cc} & \texttt{0240} & \texttt{4444} & \texttt{0f00} \\
19 & \texttt{0808} & \texttt{b820} & \texttt{c064} & \texttt{0d00} & \texttt{0213} & \texttt{4004} & \texttt{853d} & \texttt{9b91} & \texttt{9e61} & \texttt{1ca1} & \texttt{cc0c} & \texttt{2e0d} & \texttt{a008} & \texttt{2202} & \texttt{b0c8} \\
20 & \texttt{0020} & \texttt{58c0} & \texttt{a002} & \texttt{f8a0} & \texttt{92b9} & \texttt{0888} & \texttt{95c3} & \texttt{0994} & \texttt{0d0d} & \texttt{cc72} & \texttt{fcb3} & \texttt{9000} & \texttt{c008} & \texttt{8088} & \texttt{a0d8} \\
21 & \texttt{00a8} & \texttt{5040} & \texttt{ab02} & \texttt{340a} & \texttt{0bb0} & \texttt{0808} & \texttt{0ccc} & \texttt{9d90} & \texttt{9909} & \texttt{dd00} & \texttt{1271} & \texttt{ee7d} & \texttt{7530} & \texttt{4284} & \texttt{0800} \\
22 & \texttt{c008} & \texttt{5400} & \texttt{0ba8} & \texttt{000d} & \texttt{0300} & \texttt{1001} & \texttt{0cca} & \texttt{4d90} & \texttt{9d0d} & \texttt{9499} & \texttt{5606} & \texttt{11cd} & \texttt{4000} & \texttt{8188} & \texttt{7008} \\
23 & \texttt{c058} & \texttt{0400} & \texttt{0320} & \texttt{9000} & \texttt{68b3} & \texttt{46a8} & \texttt{c06c} & \texttt{8190} & \texttt{6e0e} & \texttt{3300} & \texttt{3073} & \texttt{9090} & \texttt{c080} & \texttt{8288} & \texttt{20d0} \\
24 & \texttt{4828} & \texttt{5820} & \texttt{8020} & \texttt{5008} & \texttt{3033} & \texttt{8998} & \texttt{e22c} & \texttt{8d80} & \texttt{9e09} & \texttt{ec52} & \texttt{0cbc} & \texttt{3033} & \texttt{2060} & \texttt{4244} & \texttt{0870} \\
25 & \texttt{0400} & \texttt{9a02} & \texttt{0064} & \texttt{07a0} & \texttt{0219} & \texttt{4602} & \texttt{0111} & \texttt{9b96} & \texttt{0090} & \texttt{d09d} & \texttt{1606} & \texttt{ffcc} & \texttt{0040} & \texttt{4144} & \texttt{0d02} \\
26 & \texttt{0088} & \texttt{d048} & \texttt{a602} & \texttt{0700} & \texttt{021f} & \texttt{4357} & \texttt{9569} & \texttt{0998} & \texttt{6000} & \texttt{2222} & \texttt{fc9f} & \texttt{ae3d} & \texttt{a60e} & \texttt{0080} & \texttt{3840} \\
27 & \texttt{0098} & \texttt{9008} & \texttt{7602} & \texttt{0050} & \texttt{121e} & \texttt{4557} & \texttt{95c2} & \texttt{9994} & \texttt{9990} & \texttt{9c99} & \texttt{ac06} & \texttt{10dd} & \texttt{0540} & \texttt{4d88} & \texttt{0d00} \\
28 & \texttt{6a08} & \texttt{0020} & \texttt{8090} & \texttt{0009} & \texttt{030e} & \texttt{4657} & \texttt{9009} & \texttt{2020} & \texttt{9e3d} & \texttt{cc50} & \texttt{1cbd} & \texttt{a033} & \texttt{0c04} & \texttt{0888} & \texttt{6d04} \\
29 & \texttt{c0a8} & \texttt{5000} & \texttt{8b20} & \texttt{0006} & \texttt{0d00} & \texttt{0100} & \texttt{84c2} & \texttt{c994} & \texttt{0600} & \texttt{0050} & \texttt{1c71} & \texttt{4edd} & \texttt{0cae} & \texttt{4000} & \texttt{2940} \\
30 & \texttt{0008} & \texttt{1000} & \texttt{7bdf} & \texttt{9400} & \texttt{08b3} & \texttt{4c08} & \texttt{0cc2} & \texttt{ddd0} & \texttt{994d} & \texttt{2c92} & \texttt{0c0c} & \texttt{c000} & \texttt{4800} & \texttt{8888} & \texttt{f000} \\
31 & \texttt{0c08} & \texttt{9800} & \texttt{7064} & \texttt{0060} & \texttt{6269} & \texttt{0200} & \texttt{9099} & \texttt{b990} & \texttt{92fd} & \texttt{9900} & \texttt{1253} & \texttt{0099} & \texttt{0002} & \texttt{0010} & \texttt{0b73} \\
32 & \texttt{1110} & \texttt{000e} & \texttt{0400} & \texttt{70a0} & \texttt{9219} & \texttt{2aa8} & \texttt{0660} & \texttt{fd20} & \texttt{9e0d} & \texttt{9099} & \texttt{0606} & \texttt{00cc} & \texttt{0032} & \texttt{4276} & \texttt{0b72} \\
33 & \texttt{30a8} & \texttt{0040} & \texttt{8900} & \texttt{5800} & \texttt{3213} & \texttt{4cc8} & \texttt{0aaa} & \texttt{fd90} & \texttt{920d} & \texttt{0030} & \texttt{cc7c} & \texttt{3030} & \texttt{0062} & \texttt{4044} & \texttt{0a72} \\
34 & \texttt{8880} & \texttt{e000} & \texttt{8420} & \texttt{000a} & \texttt{0de0} & \texttt{4c58} & \texttt{955a} & \texttt{909d} & \texttt{9000} & \texttt{d0dd} & \texttt{6606} & \texttt{eecd} & \texttt{0008} & \texttt{1000} & \texttt{b0d9} \\
35 & \texttt{0c68} & \texttt{0800} & \texttt{3020} & \texttt{7028} & \texttt{9299} & \texttt{2220} & \texttt{953c} & \texttt{9091} & \texttt{0e0e} & \texttt{cc9c} & \texttt{1c06} & \texttt{eedd} & \texttt{0c40} & \texttt{4888} & \texttt{2d00} \\
36 & \texttt{4440} & \texttt{0e00} & \texttt{0020} & \texttt{9ea0} & \texttt{02b9} & \texttt{4400} & \texttt{95c9} & \texttt{0990} & \texttt{6d0d} & \texttt{9999} & \texttt{fc06} & \texttt{00dd} & \texttt{0604} & \texttt{4404} & \texttt{7c04} \\
37 & \texttt{2220} & \texttt{00e0} & \texttt{8000} & \texttt{00a0} & \texttt{6219} & \texttt{4ca8} & \texttt{95cc} & \texttt{9990} & \texttt{99f6} & \texttt{af11} & \texttt{3003} & \texttt{851d} & \texttt{0200} & \texttt{4414} & \texttt{0b04} \\
38 & \texttt{0002} & \texttt{0010} & \texttt{1009} & \texttt{9040} & \texttt{b8b3} & \texttt{8aa8} & \texttt{0550} & \texttt{0220} & \texttt{5e3d} & \texttt{2092} & \texttt{0cac} & \texttt{f033} & \texttt{1000} & \texttt{b28b} & \texttt{0008} \\
39 & \texttt{0c98} & \texttt{9000} & \texttt{7420} & \texttt{1048} & \texttt{b0bb} & \texttt{8888} & \texttt{955b} & \texttt{000d} & \texttt{00dd} & \texttt{dd40} & \texttt{1242} & \texttt{aa39} & \texttt{2080} & \texttt{2222} & \texttt{00f0} \\
40 & \texttt{4000} & \texttt{5620} & \texttt{00a8} & \texttt{0759} & \texttt{020f} & \texttt{4757} & \texttt{0ee0} & \texttt{fdd0} & \texttt{924d} & \texttt{2292} & \texttt{fcac} & \texttt{ee3d} & \texttt{00a2} & \texttt{0222} & \texttt{0b62} \\
41 & \texttt{0010} & \texttt{940c} & \texttt{0602} & \texttt{00d0} & \texttt{1219} & \texttt{2002} & \texttt{8578} & \texttt{0228} & \texttt{5eed} & \texttt{ec62} & \texttt{0070} & \texttt{65f6} & \texttt{02a0} & \texttt{4222} & \texttt{0b40} \\
42 & \texttt{0398} & \texttt{0008} & \texttt{5400} & \texttt{0058} & \texttt{1211} & \texttt{2331} & \texttt{2022} & \texttt{8aa0} & \texttt{5e8d} & \texttt{9c11} & \texttt{4703} & \texttt{9900} & \texttt{95d0} & \texttt{4288} & \texttt{2000} \\
43 & \texttt{1288} & \texttt{3048} & \texttt{8400} & \texttt{700a} & \texttt{0b80} & \texttt{1908} & \texttt{a66a} & \texttt{8d50} & \texttt{de0d} & \texttt{9c22} & \texttt{fc03} & \texttt{d0dd} & \texttt{0080} & \texttt{1222} & \texttt{00d2} \\
44 & \texttt{0200} & \texttt{30a8} & \texttt{c004} & \texttt{0600} & \texttt{02df} & \texttt{0400} & \texttt{e00e} & \texttt{8a80} & \texttt{9e81} & \texttt{4444} & \texttt{6506} & \texttt{55cd} & \texttt{0010} & \texttt{4277} & \texttt{0002} \\
45 & \texttt{8418} & \texttt{9402} & \texttt{0420} & \texttt{7000} & \texttt{6de6} & \texttt{b3a8} & \texttt{842c} & \texttt{9c91} & \texttt{9009} & \texttt{0040} & \texttt{1171} & \texttt{55c6} & \texttt{9008} & \texttt{b28a} & \texttt{b0d8} \\
46 & \texttt{9508} & \texttt{0002} & \texttt{0450} & \texttt{0040} & \texttt{656e} & \texttt{b9a8} & \texttt{952c} & \texttt{9991} & \texttt{0066} & \texttt{dc51} & \texttt{0707} & \texttt{cccc} & \texttt{0504} & \texttt{4d8c} & \texttt{7d04} \\
\bottomrule
\end{tabular}
\end{table}

\section{Matching, post-processing, pencils and DAG certificates}\label{app:checks}

Command lines, file names, hashes and the details of the runs and tests are in the README files of the archive (see Data and code availability).

\subsection{Matching of public and searched decompositions of rank 47}\label{app:search}

We matched the decompositions in the following sources with the five classes by explicit equivalences: the decomposition of Fawzi et al.~\cite{FawziEtAl2022}, the file \texttt{444-47-mod2.exp} of the repository~\cite{KauersMoosbauerFlipsRepo} of~\cite{KauersMoosbauer2023flip}, the two collections on the web site of Kauers~\cite{KauersSchemes444r47,KauersSchemes444x47}, the record of Zaru~\cite{Zaru2026}, and copies of AT47 and KM47 in later catalogues and artifacts. As lists of terms, AT47 and KM47 are the decompositions of~\cite{FawziEtAl2022} and~\cite{KauersMoosbauerFlipsRepo}. We analysed the collection~\cite{KauersSchemes444x47} as an archive of $99{,}101$ files from the same web site. Up to the order of their terms, these files contain only four distinct decompositions. Two of them lie in the class of AT47 and two in that of KM47. Of the 19 files of the collection~\cite{KauersSchemes444r47}, 13 lie in the class of KM47, five in that of AT47, and one file in that of C3. The second decomposition of rank 47 of Zaru~\cite{Zaru2026}, given there in the cyclic convention with the same encoding of matrices, lies in the class of C5. No decomposition in these sources is equivalent to C4.

Our flip-graph searches consisted of about $226{,}000$ descents of several kinds: plain descents from the standard algorithm, descents from decompositions glued from smaller formats, descents restricted to decompositions with a symmetry of order 2 or 3, and descents after adding 2, 3, 6 or 12 extra terms to a known decomposition. They produced about $8.8$ million decompositions of rank 47, counted with multiplicity except that the first $41{,}809$ descents kept only distinct ones, and no descent reached rank 46. The $712{,}634$ distinct decompositions from those first descents were all matched to their classes by explicit equivalences. Of the later decompositions, about $8.1$ million, a random sample of $4{,}083$ was matched in the same way. The invariant hash used for the rest is computed from the matrix ranks of the factors and of the sums of pairs of factors in each position, minimized over the six permutations of the positions, and $G$ preserves these data.

\subsection{Post-processing}\label{app:runs}

At depth 16, $20{,}866$ orbit representatives went to post-processing. At depth 18 there were $14{,}229{,}163$. Of these, $14{,}085{,}423$ were settled in the first stage of post-processing (Section~\ref{sec:cert}), $143{,}645$ in the second and $86$ in the third. Post-processing left nine orbit representatives (Section~\ref{sec:d18}).

\subsection{The pencils for the subset of C4}\label{app:pencils}

Besides our script for the bound (Section~\ref{sec:hardest}), an independent program enumerates all $2^{28}$ matrices $c$ in Gray-code order. For a pencil $e_0\otimes s_0+e_1\otimes s_1$ it uses the bound $\max\bigl(\rk[\,s_0\ s_1\,],\ \rk\bigl[\begin{smallmatrix}s_0\\ s_1\end{smallmatrix}\bigr]\bigr)$. The ranks of $s_0$, $s_1$ and $s_0+s_1$ never exceed this bound, because the column space of $[\,s_0\ s_1\,]$ contains their column spaces. Its minimum over all $2^{28}$ pencils is 4, attained by 25 matrices $c$, among them $c=0$, so the bound $\Rk(\Sigma_X)\ge18$ has no margin. Like the count 57 in Section~\ref{sec:hardest}, the count 25 refers to the choice of $b_0$ and $b_1$ made there.

\subsection{The DAG certificates}\label{app:dag}

In the files of $Y_1$, $Y_2$ and $Y_3$, a coarsening after the search put leaves at 13, 21 and 42 nodes of codimension 5 in place of the substitution labels recorded there by the search: 13 SAT leaves (leaves settled by a rank or lifting rule) for $Y_1$, 10 capacity and 11 SAT leaves for $Y_2$, and 24 capacity and 18 SAT leaves for $Y_3$. Every line of an unreachable node in these files is for a subspace of codimension 4 that contains one of these leaves. In the certificate for $Y_4$, all $1{,}678$ SAT leaves have codimension 4.

\begin{table}[ht]
\centering
\caption{The DAG certificates for $Y_1$, $Y_2$, $Y_3$ and $Y_4$. The abbreviations \textsf{SUB}, \textsf{CAP}, \textsf{OPT}, RANK and LIFT stand for substitution labels, capacity leaves, SAT leaves, the rank rule and the lifting rule. \textsf{OPT} leaves are counted by the rule that settles them in the check, and instances are counted over the \textsf{OPT} leaves of each certificate.}\label{tab:dag}
\small
\begin{tabular}{@{}lrrrr@{}}
\toprule
 & $Y_1$ & $Y_2$ & $Y_3$ & $Y_4$\\
\midrule
Position used as $A$, and $\dim A$ & third, 10 & first, 9 & first, 9 & first, 9\\
Nodes reachable from $0$ & 1{,}506{,}516 & 380{,}442 & 268{,}164 & 454{,}575\\
\textsf{SUB} nodes & 36{,}499 & 15{,}157 & 11{,}391 & 16{,}766\\
Flattening leaves & 1{,}409{,}094 & 328{,}848 & 226{,}085 & 408{,}074\\
\textsf{CAP} leaves & 57{,}630 & 34{,}772 & 28{,}377 & 28{,}057\\
\textsf{OPT} leaves & 3{,}293 & 1{,}665 & 2{,}311 & 1{,}678\\
\addlinespace
\textsf{OPT} leaves settled by RANK & 1{,}541 & 1{,}057 & 1{,}469 & 1{,}117\\
\quad by LIFT, through relaxations only & 0 & 4 & 11 & 1\\
\quad by LIFT, with full instances & 1{,}752 & 604 & 831 & 560\\
Instances of RANK leaves & 16{,}257 & 22{,}914 & 34{,}352 & 30{,}029\\
LIFT instances refuted through the relaxation & 145{,}805 & 66{,}461 & 99{,}404 & 73{,}956\\
LIFT instances refuted directly & 74{,}815 & 25{,}353 & 26{,}910 & 24{,}602\\
\bottomrule
\end{tabular}
\end{table}

\subsection{Certificate formats and their checks}\label{app:formats}

Here $X$, $k$ and the tests 1--3 are as in Section~\ref{sec:cert}. A certificate for $X$ is a tree written in pre-order, with leaves of six kinds. A \textsf{TRIV} leaf asserts a target of at most 0, and an \textsf{NZ} leaf a target of at most 1 for a nonzero tensor. The Koszul flattenings with $p=1,2,3$ (Section~\ref{sec:flat}) are labelled \textsf{KOS}, \textsf{YNG} and \textsf{YNG7}, where 7 is the dimension of $V$ for $p=3$. \textsf{FLAT}, \textsf{KOS}, \textsf{YNG} and \textsf{YNG7} leaves name a position and, except for \textsf{FLAT}, a projection $\pi$. The inner nodes of the tree are \textsf{SUB} nodes, which name a position and a pivot and have one child for each branch of~\eqref{eq:onestep}. A \textsf{SUB} node is valid only if the pivot slice of the current tensor, taken after peeling in the peeled format, is nonzero. A check recomputes the tensor at each node from the scheme, the index list of $X$ and the path from the root. At a leaf with target $k$ it requires the matrix rank to be at least $k$, $2k-1$, $6(k-1)+1$ or $20(k-1)+1$, respectively. For \textsf{FLAT} this is the flattening bound, and for the other three these are the conditions of~\eqref{eq:young}. For peeled substitution, the check first peels the list at every node and lowers the target by the number of peeled terms. A certificate for one of the fast tests~1--3 is a single leaf.

The DAG certificates (Section~\ref{sec:gsl}) have the following format. A certificate file lists the nodes, one per line. A line gives the reduced row echelon basis of $U$ in the coordinates of $A$, followed by the label: \textsf{SUB} with the form $f$ in the coordinates of $A/U$ that come from the non-pivot coordinates of the echelon basis, a flattening leaf with its position and projections as in Section~\ref{sec:cert}, \textsf{CAP}, or \textsf{OPT}. A node labelled \textsf{OPT} is a leaf that the checker settles by a RANK or a LIFT argument. The file contains no multisets and no proofs. The coordinates of $A$, $B$ and $C$ are the greedy reduced coordinates (Section~\ref{sec:cert}) of $\Sigma_Y$ for the order of Table~\ref{tab:open}.

From the decomposition C3, the term list of $Y$ and the certificate, a checker recomputes the following.
\begin{enumerate}[label=\textup{(C\arabic*)},nosep]
\item The tensor $T$ in reduced coordinates, with a check that its terms are distinct with nonzero factors and that $T$ is concise in the position used as $A$.
\item For each node reachable from $0$: the canonical form of the echelon basis, the children $U_p$ of a \textsf{SUB} node, which must be present in the file, the list $L_U$, its core and the tensor $X_U$. Lines of nodes that are not reachable from $0$ are parsed and checked for canonical form, but not evaluated.
\item The flattening ranks of the flattening leaves and the capacities of the \textsf{CAP} leaves.
\item For each \textsf{OPT} leaf: the admissible multisets, from its own implementation of the capacity bound, and the CNF formulas of all RANK and LIFT instances and relaxations. The leaf is valid if $\cp(X_U)\ge k-p_U-1$ and every RANK instance is unsatisfiable, or if every instance $\mathrm{Lift}(s,m)$ of Proposition~\ref{prop:lift} is unsatisfiable or has an unsatisfiable relaxation. For LIFT the checker takes $s_0=\max\bigl(\lb(0),\,p_U+\cp(X_U)\bigr)$, where $\lb(0)$ is the bound for $\Rk(T/U)$ itself (Section~\ref{sec:gsl-leaves}). No admissible multiset has size below $\cp(T/U)$, so this gives the same instances as $s_0=\max\bigl(\cp(T/U),\,p_U+\cp(X_U)\bigr)$.
\item The padding condition of Proposition~\ref{prop:lift} at every LIFT leaf.
\end{enumerate}
The checker we used is described in Section~\ref{sec:verif}.

\paragraph{Finding certificates.} We found the certificates with a memoized depth-first search over subspaces, with a fixed position as $A$. At a node without a flattening or capacity leaf, the search tries the children $U_p$. As soon as the children it cannot settle span $A/U$, the node fails. Otherwise every nonzero form $f$ that vanishes on them is a valid pivot, and the search takes one for which the fewest children are \textsf{SUB} or \textsf{OPT} nodes. The search stops at codimension 4. A node of codimension 4 without a flattening or capacity leaf becomes an \textsf{OPT} leaf, provided that its numbers of admissible multisets are small enough for the SAT stage. The files of $Y_1$, $Y_2$ and $Y_3$ were then coarsened at some nodes of codimension 5 (Appendix~\ref{app:dag}).

\end{document}