§6 — no connected three-term weight-6 BB code with $n\le360$, $k\ge20$ has distance $\ge13$

Universally quantified data. Natural numbers $l,m$ with $l\ne0$, $m\ne0$; polynomials $A,B\subseteq G=\mathbb Z_l\times\mathbb Z_m$ (finite sets of monomials $x^iy^j$); a natural number $k$.

Unfolded definitions used below. For $l,m\ge 1$ write $G=\mathbb Z_l\times\mathbb Z_m$; an element $(i,j)\in G$ stands for the monomial $x^iy^j$, and a "polynomial" is a finite subset $P\subseteq G$ (its support, coefficients in $\mathbb F_2$). The circulant $M_P$ is the $G\times G$ matrix over $\mathbb F_2$ with $(M_P)_{g,h}=1$ iff $h-g\in P$ and $0$ otherwise. The qubit set is $Q=G\sqcup G$ (a left block $L$ and a right block $R$, $|Q|=2lm$). The check matrices (rows indexed by $G$, columns by $Q$) are

with the first block on $L$ and the second on $R$. A vector $v\in\mathbb F_2^{Q}$ is a nontrivial Z-logical if $H_Xv=0$ and $v\notin\operatorname{row}(H_Z)$ (the $\mathbb F_2$-span of the rows of $H_Z$); it is a nontrivial X-logical if $H_Zv=0$ and $v\notin\operatorname{row}(H_X)$. The weight $|v|$ is the number of nonzero coordinates of $v$.

Hypotheses.

1. $2lm\le 360$ (at most $360$ qubits, i.e. $lm\le180$; includes the degenerate shapes $l=1$ or $m=1$).
2. $|A|=3$ and $|B|=3$: each polynomial has exactly three distinct monomials (any monomials whatsoever, including $1$, and $A=B$ is allowed).
3. The Tanner graph is connected: on vertices $Q\sqcup C_X\sqcup C_Z$ (qubits, X-checks and Z-checks, each check set a copy of $G$), qubit $q$ is joined to X-check $c$ iff $(H_X)_{c,q}=1$ and to Z-check $c$ iff $(H_Z)_{c,q}=1$, with no other edges; this single graph must be connected.
4. $\operatorname{rank}_{\mathbb F_2}H_X+\operatorname{rank}_{\mathbb F_2}H_Z+k=2lm$ (so $k$ is the number of logical qubits), and $k\ge 20$.

Conclusion. There exists $v\in\mathbb F_2^{Q}$ that is a nontrivial X-logical or a nontrivial Z-logical, with $|v|\le 12$.

Equivalently, under these hypotheses $\min(d_X,d_Z)\le 12$, where $d_X,d_Z$ are the minimum weights of nontrivial X- and Z-logicals. It does not assert that both $d_X\le12$ and $d_Z\le12$, does not assert anything about codes with $k<20$, with more than $360$ qubits, with $|A|$ or $|B|\ne3$, or with disconnected Tanner graph, and asserts an upper bound $\le 12$ only (not that the distance equals $12$). The conclusion's existential also guarantees nontrivial logicals exist, which is consistent with $k\ge20>0$. The hypotheses are not obviously contradictory, so the statement is not evidently vacuous; it is a claim about every pair $(A,B)$ in a finite search space.