\documentclass[11pt]{article}
\usepackage[T1]{fontenc}
\usepackage[margin=1in]{geometry}
\usepackage{amsmath,amssymb,amsthm,mathtools,booktabs,microtype,xcolor}
\usepackage{xurl}
\usepackage[colorlinks=true,allcolors=blue!50!black]{hyperref}
\setlength{\emergencystretch}{2em}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}\newtheorem{definition}[theorem]{Definition}
\theoremstyle{remark}\newtheorem{remark}[theorem]{Remark}
\newcommand{\F}{\mathbb F}
\DeclareMathOperator{\im}{im}\DeclareMathOperator{\rank}{rank}
\newcommand{\lean}[1]{{\small\path{#1}}}
\title{A Product Formula for Partition-Restricted\\Boundary Hypermatrix Counts}
\author{Yuran Xiu\\IIIS, Tsinghua University\\
\texttt{xiuyr23@mails.tsinghua.edu.cn}}
\hypersetup{pdfauthor={Yuran Xiu}}
\date{14 October 2026}
\begin{document}
\maketitle
\begin{abstract}
We prove the Koprowski--Lewis product conjecture for nondegenerate
$2\times(k+1)\times k$ hypermatrices over finite fields with two
partition-shaped layers of prescribed zeros. The result holds for every
positive $k$, every finite field, and every admissible pair of partitions.
After fixing the first slice, nondegeneracy is equivalent to simplicity
of a partial linear map. Applying the simple-extension theorem of
Arora, Ram, and Venkateswarlu inside the successive allowed row spaces
gives the product directly. We include an elementary proof of that
extension theorem and justify the equivalence with the defining
projective critical locus of the hyperdeterminant. The complete counting
statement and its semantic equivalences have been checked in Lean.
\end{abstract}

\section{The counting formula}
Let $\F$ be a finite field with $q$ elements and let $k\geq1$.
For $r\geq1$, put $[r]_q=1+q+\cdots+q^{r-1}$.
Let $\lambda=(\lambda_1,\ldots,\lambda_k)$ and
$\mu=(\mu_1,\ldots,\mu_k)$ be weakly decreasing sequences of
nonnegative integers satisfying
\begin{equation}\label{eq:admissible}
 \mu_j\leq\lambda_j\leq k+1-j,\qquad
 \mu_j\leq k-j\qquad(1\leq j\leq k).
\end{equation}
Consider ordered pairs of $(k+1)\times k$ matrices $(A,B)$ over $\F$
such that the last $\lambda_j$ entries of column $j$ of $A$ and the
last $\mu_j$ entries of column $j$ of $B$ vanish.

Write $K$ for an algebraic closure of $\F$. Call $(A,B)$
\emph{pencil-nondegenerate} if
\begin{equation}\label{eq:pencil}
 \rank_K(sA+tB)=k
       \quad\text{for every }(s,t)\in K^2\setminus\{(0,0)\}.
\end{equation}
The field $K$ is essential: checking only $\F$-rational directions is
not the condition in this paper. Section~\ref{sec:critical} proves that
\eqref{eq:pencil} is exactly hyperdeterminantal nondegeneracy in this
boundary format.

\begin{theorem}\label{thm:product}
The number of nondegenerate pairs $(A,B)$ with these zero restrictions is
\begin{equation}\label{eq:product}
 q^{k^2}(q-1)^{2k}
 \prod_{j=1}^k[k+2-j-\lambda_j]_q
 \prod_{j=1}^k[k+1-j-\mu_j]_q.
\end{equation}
\end{theorem}

This is Conjecture~3.1 of Koprowski and Lewis~\cite{KL}. Their work
proves several special cases and expresses the general count, after
normalization, as a polynomial with nonnegative coefficients whose
value at $q=1$ counts hyperrook placements. A public manuscript of
Zeng~\cite{Zeng} treats all partition restrictions for $k=3$ by a
finite polynomial census. Theorem~\ref{thm:product} covers arbitrary
$k$ without a census of shapes.

The linear-algebraic ingredient is already known: Lemma~2.10 of
Arora, Ram, and Venkateswarlu~\cite{ARV} counts simple extensions of a
partial linear map by one domain dimension. Our contribution is its
application with both nested zero restrictions retained, together with
the resulting full hypermatrix formula. For completeness,
Section~\ref{sec:extension} supplies an elementary induction proof of
the extension count; the count itself is not claimed as a new theorem.

\section{Simple partial maps and pencils}\label{sec:simple}
\begin{definition}
For a subspace $D\subseteq V$, a linear map $f:D\to V$ is
\emph{simple} if the only subspace $L\subseteq D$ for which
$f(L)\subseteq L$ is $L=0$.
\end{definition}
This definition excludes every nonzero invariant subspace, not just
invariant lines over the base field. It is unchanged if one replaces
$V$ by any subspace containing both $D$ and $f(D)$. Restricting a simple
map to a smaller domain preserves simplicity.

\begin{lemma}\label{lem:basechange}
Simplicity of a finite-dimensional partial map is preserved and
reflected by extension of the base field.
\end{lemma}
\begin{proof}
Let $\dim D=k$, and define
\[
 D_0=D,\qquad D_{i+1}=\{u\in D:f(u)\in D_i\}.
\]
This is a descending sequence. If $D_{i+1}=D_i$, the common subspace
is invariant and all subsequent terms are the same. Each invariant
subspace is contained in every $D_i$. Consequently $f$ is simple if
and only if $D_k=0$: otherwise some step among the first $k$ fails to
decrease dimension and gives a nonzero invariant subspace.

Each $D_{i+1}$ is obtained from $D_i$ by a preimage and an intersection
of subspaces defined by linear equations. Row reduction of those
equations over the base field remains valid over any extension field.
Thus scalar extension gives precisely the corresponding sequence and
preserves every dimension. In particular it preserves and reflects
$D_k=0$.
\end{proof}

\begin{proposition}\label{prop:pencil-simple}
Regard $A,B$ as maps $U\to V$, where $\dim U=k$ and $\dim V=k+1$.
Condition~\eqref{eq:pencil} holds if and only if $A$ is injective and
the map $f:\im A\to V$ determined by $f(Ax)=Bx$ is simple.
\end{proposition}
\begin{proof}
Condition~\eqref{eq:pencil} includes $(s,t)=(1,0)$, hence forces $A$
to be injective. Assume this and extend scalars to $K$. A nonzero
vector $x$ in the kernel of $sA+tB$ must have $t\ne0$. Its image
$u=Ax\ne0$ satisfies $f(u)=-(s/t)u$, giving an invariant line.
Conversely, on any nonzero invariant subspace the restriction of $f$
is an endomorphism over an algebraically closed field. It has an
eigenvector $u=Ax\ne0$, which supplies a singular pencil direction.
Lemma~\ref{lem:basechange} identifies simplicity over $K$ with
simplicity over $\F$.
\end{proof}

\section{Counting one-dimensional extensions}\label{sec:extension}
\begin{lemma}[Simple-extension count, cf.\ {\cite[Lemma 2.10]{ARV}}]
\label{lem:extension}
Let $U\subset U'\subseteq V$ have dimensions $r,r+1,m$, respectively,
over $\F$, and let $f:U\to V$ be simple. The number of simple maps
$g:U'\to V$ extending $f$ is $q^m-q^{r+1}$.
\end{lemma}
\begin{proof}
Fix $v\in U'\setminus U$. An extension $g_w$ is uniquely specified
by $g_w(v)=w\in V$. We prove by strong induction on $r$ that exactly
$q^{r+1}$ values of $w$ give a nonzero invariant subspace. We allow
$U'=V$ in the induction; then the asserted number of simple extensions
is zero.

Let $\pi:V\to V/U'$ be the quotient map, and put
\[
 H=\{u\in U:f(u)\in U'\},\qquad h=\dim H,\qquad
 C=\pi\circ f.
\]
Rank--nullity gives $\dim\im C=r-h$. If $\pi(w)\notin\im C$,
the equation $C(u)+\alpha\pi(w)=0$ forces $\alpha=0$.
Any invariant subspace of $g_w$ lies in
$\ker(\pi\circ g_w)$, so is then contained in $U$. Simplicity of
$f$ forces that subspace to be zero. These values of $w$ are all good.

For each $c\in\im C$, choose $u_c\in U$ with $C(u_c)=c$.
The values of $w$ with $\pi(w)=c$ are uniquely
$w=f(u_c)+y$, where $y\in U'$. Set $v_c=v-u_c$. Directly,
\begin{equation}\label{eq:kernel}
 K_c:=\ker(\pi\circ g_w)=H\oplus\F v_c,
 \qquad g_w(v_c)=y.
\end{equation}
Indeed, $C(u)+\alpha c=0$ is equivalent to
$u+\alpha u_c\in H$, and
$u+\alpha v=(u+\alpha u_c)+\alpha(v-u_c)$.
The subspace $K_c$ has dimension $h+1$ and is independent of $y$.

Every invariant subspace of $g_w$ is contained in $K_c$; conversely,
an invariant subspace for $g_w|_{K_c}:K_c\to U'$ is invariant for
$g_w$. The map $f|_H:H\to U'$ is simple. If $h<r$, induction applied
to $H\subset K_c\subseteq U'$ therefore shows that exactly
$q^{h+1}$ of the choices $y$ are bad. There are $q^{r-h}$ values of
$c$, giving $q^{r-h}q^{h+1}=q^{r+1}$ bad extensions in total.

If $h=r$, then $H=U$ and $\im C=0$. In the only relevant fibre
$c=0$, choose $u_0=0$. Now $K_0=U'$, and all $q^{r+1}$ choices
$y\in U'$ give endomorphisms of the nonzero space $U'$. They are
all bad. This also proves the base case $r=0$ without an induction
call. Subtracting the bad count from the $q^m$ extensions proves the
lemma.
\end{proof}

\section{Keeping the two nested restrictions}\label{sec:count}
Write $n=k+1$, $a_j=n-\lambda_j$, and $b_j=n-\mu_j$. In $V=\F^n$,
let $F_d$ be the span of the first $d$ standard basis vectors. The
hypotheses give
\begin{equation}\label{eq:flags}
 a_1\leq\cdots\leq a_k,\quad b_1\leq\cdots\leq b_k,
 \quad j\leq a_j\leq b_j,\quad j+1\leq b_j.
\end{equation}
The column restrictions are exactly $A_j\in F_{a_j}$ and
$B_j\in F_{b_j}$.

First count the injective matrices $A$. If columns $1,\ldots,j-1$
are independent, their span lies in $F_{a_j}$ and has $q^{j-1}$
elements. Hence
\begin{equation}\label{eq:Acount}
 \#\{\text{allowed injective }A\}
   =\prod_{j=1}^k(q^{a_j}-q^{j-1}).
\end{equation}
Fix one such $A$, and put $D_j=\langle A_1,\ldots,A_j\rangle$,
with $D_0=0$.

We choose the columns of $B$ in order, retaining exactly the prefixes
for which $f_{j-1}:D_{j-1}\to V$, $f_{j-1}(A_i)=B_i$, is simple.
At step $j$, take the ambient space to be $F_{b_j}$. This is legitimate:
\eqref{eq:flags} gives $D_j\subseteq F_{b_j}$, and monotonicity of
the $b_i$ gives $f_{j-1}(D_{j-1})\subseteq F_{b_j}$. Simplicity
does not change when this smaller ambient space is used.

Lemma~\ref{lem:extension}, applied to
$D_{j-1}\subset D_j\subseteq F_{b_j}$, gives
$q^{b_j}-q^j$ simple extensions. Each one is specified uniquely by
its value $B_j=f_j(A_j)$, so it is precisely an allowed choice of
the new column. Every retained prefix has the same number of
continuations. All prefixes of a simple final map are simple, so none
of the desired pairs is discarded. Proposition~\ref{prop:pencil-simple}
identifies the final retained maps with the desired nondegenerate
pencils. Consequently, for every fixed allowed injective $A$,
\begin{equation}\label{eq:Bcount}
 \#\{\text{allowed nondegenerate }B\mid A\}
       =\prod_{j=1}^k(q^{b_j}-q^j).
\end{equation}

Multiplying \eqref{eq:Acount} and \eqref{eq:Bcount} counts actual
ordered matrices; no change-of-basis quotient or stabilizer division
occurs. Finally,
$q^d-q^e=q^e(q-1)[d-e]_q$ for $d>e$, and
$\sum_{j=1}^k((j-1)+j)=k^2$. This proves
Theorem~\ref{thm:product} for pencil-nondegeneracy.

\section{Hyperdeterminantal nondegeneracy}\label{sec:critical}
The boundary-format hyperdeterminant used in~\cite{KL} vanishes on
the projective critical locus of the multilinear form
\begin{equation}\label{eq:form}
 F(s,t,x,y)=y^{\mathsf T}(sA+tB)x
   =\sum_{i=1}^{k+1}\sum_{j=1}^k(A_{ij}s+B_{ij}t)x_jy_i.
\end{equation}
Here $(s,t)$, $x$, and $y$ must each be nonzero. The vanishing of
all first partial derivatives is equivalent to
\begin{equation}\label{eq:critical}
 Cx=0,\qquad y^{\mathsf T}C=0,\qquad
 y^{\mathsf T}Ax=y^{\mathsf T}Bx=0,
 \quad C=sA+tB.
\end{equation}
The value of $F$ then vanishes as well.

\begin{proposition}\label{prop:critical}
Over an algebraic closure, a nonzero critical triple for
\eqref{eq:form} exists if and only if some nonzero pencil direction
has rank less than $k$.
\end{proposition}
\begin{proof}
A critical triple gives a nonzero kernel vector $x$ of $C$, so one
implication is immediate. Conversely suppose $Cx=0$ with $x\ne0$.
If $t\ne0$, set $v=Ax$; if $t=0$, set $v=Bx$ (then $s\ne0$
and $Ax=0$). Consider
\[
 d:K^k\times K\longrightarrow K^{k+1},\qquad
 d(u,c)=Cu+cv.
\]
It is a map between spaces of equal dimension and has the nonzero
kernel vector $(x,0)$. Its image is therefore proper, and some
nonzero linear functional $y^{\mathsf T}$ annihilates that image.
Thus $y^{\mathsf T}C=0$ and $y^{\mathsf T}v=0$. If $t\ne0$,
$sAx+tBx=0$ also implies $y^{\mathsf T}Bx=0$; if $t=0$, the
remaining equation follows from $Ax=0$. All of \eqref{eq:critical}
hold.
\end{proof}
This argument is valid in every characteristic. It proves equality of
the relevant zero loci, which is exactly what the nonzero count needs;
no normalization of a defining hyperdeterminant polynomial is required.
It completes the source interpretation of Theorem~\ref{thm:product}.

\section{Specializations and formal verification}
For $\lambda=\mu=0$, formula~\eqref{eq:product} becomes the
unrestricted boundary-format count
\[
 q^{k^2}(q-1)^{2k}[k+1]_q!\,[k]_q!,
 \qquad [r]_q!=\prod_{i=1}^r[i]_q.
\]
At the other extreme, $\lambda_j=k+1-j$ and $\mu_j=k-j$ make
every $q$-integer factor equal to 1. The proof treats these cases and
all intermediate shapes uniformly.

In the accompanying project \lean{boundary-hypermatrix-count}, the
declarations \lean{Boundary.full_pencil_target} and
\lean{Boundary.full_source_target} establish the full product for,
respectively, the algebraic-closure pencil condition and the literal
multilinear-polynomial critical-point condition. The extension theorem
is proved in the project, rather than assumed as an axiom. The
formalization implements scalar-extension invariance by an equivalent
square trajectory matrix: the map
$(x_0,\ldots,x_k)\mapsto(Bx_i-Ax_{i+1})_{i=0}^{k-1}$ is injective
exactly when $A$ is injective and its partial map is simple, and
nonvanishing of its determinant is unchanged by field embeddings.
Formal partial differentiation supplies every equation in
\eqref{eq:critical}.

The 22-module build uses Lean 4.27.0 and mathlib revision
\lean{a3a10db0e9d66acbebf76c5e6a135066525ac900}; all
dependency revisions are in \lean{lake-manifest.json}. Run
\texttt{\small python3 scripts/verify.py --packages /path/to/packages} with
those dependencies provisioned. Saved successful logs and the statement
audit are identified in \lean{verification/result.json}. The final
transitive axiom lists contain only \lean{propext},
\lean{Classical.choice}, and \lean{Quot.sound}. No proof placeholder,
new mathematical axiom, or native computation is used. The pinned
compiler and library proof objects are trusted. This verification
concerns the mathematical statements; it does not certify the prose
or establish bibliographic priority.

\begin{thebibliography}{9}
\bibitem{KL}
B. Koprowski and J. B. Lewis,
\emph{Enumeration of nondegenerate $2\times(k+1)\times k$ hypermatrices},
arXiv:2602.22129v1 (2026).
\url{https://arxiv.org/abs/2602.22129v1}.
\bibitem{ARV}
A. Arora, S. Ram, and A. Venkateswarlu,
\emph{Unimodular polynomial matrices over finite fields},
J. Algebraic Combin. \textbf{53} (2021), 1299--1312.
\url{https://doi.org/10.1007/s10801-020-00963-2}.
\bibitem{Zeng}
X. Zeng, \emph{All partition-restricted counts of nondegenerate
$2\times4\times3$ hypermatrices}, public manuscript,
\href{https://github.com/ArtificialZeng/AI-Has-Taste/blob/main/reproducible_source_code/BigWIN2/BW2-N01-P12/source/manuscript/main.tex}{AI-Has-Taste repository},
accessed 14 October 2026.
\end{thebibliography}
\end{document}