Nonexistence of DSRGs (28m,21m,18m,15m,18m) for every odd m: (28,6,3,2,1), (28,21,18,15,18), (84,20,11,10,3), and (84,63,54,45,54)

1. Result and context

Theorem 1. There is no directed strongly regular graph with any of the following four parameter sets:

$$ (28,6,3,2,1),\quad(28,21,18,15,18),\quad (84,20,11,10,3),\quad(84,63,54,45,54). $$

We use the parameter order $(v,k,t,\lambda,\mu)$ of Duval [1] and the Hobart–Brouwer table [2]. Both sparse tuples were marked unknown in the table retrieved on 17 October 2026. The tuples of each order are complements. Sections 3–6 prove the order-28 assertion; Sections 7–13 prove the order-84 assertion. All even scales of the dense tuple $(28m,21m,18m,15m,18m)$ exist, as Section 14 explicitly recalls. The following stronger result classifies the entire ray.

Theorem 8 (exact parity classification). For a positive integer $m$, a DSRG$(28m,21m,18m,15m,18m)$ exists if and only if $m$ is even. Equivalently, the complementary parameters $(28m,7m-1,4m-1,4m-2,m)$ exist if and only if $m$ is even.

Section 15 proves the odd-scale assertion using the universal structural lemmas developed below and a separate five-shape support-cone certificate. Sections 3–13 retain independently checked direct proofs at $m=1,3$; their scale-specific anchor restrictions are not assumed in Section 15.

For a hypothetical order-28 sparse adjacency matrix $C$, the defining equations are

$$ C\mathbf1=C^T\mathbf1=6\mathbf1,\qquad C^2=2I+C+J. \tag{1} $$

Set $B=I+C$. Then $B$ is binary, has diagonal one and row and column sums seven, and satisfies

$$ B^2=3B+J.\tag{2} $$

The eigenvalues of $B$ are $7$ once, $3$ seven times, and $0$ twenty times. Indeed, on the zero-sum subspace its minimal polynomial divides $x(x-3)$; the trace is $28$. In particular, $\operatorname{rank}B=8$.

The order-28 proof has three stages. An elementary argument gives only three possible nonnegative column-basis normals. A small exact enumeration and basis exchange remove the uniform normal. Another small enumeration and an explicit rational separation remove the second type. The remaining type has four seven-vertex cells and is excluded by a fully specified Boolean formula with an independently checked unsatisfiability proof.

| Basis normal | Final argument | |---|---| | $(1/2)^8$ | 286 coefficient orbits and a basis exchange to another type | | $(0,0,(1/2)^4,1,1)$ | 42 candidate orbits, 14 retained, and an exact separating inequality | | $(0^4,1^4)$ | A complete adjacency encoding and a checked DRAT proof |

The first two computations use only the Python standard library. The last computation has a reproducible CNF generator, a known positive control, and a separate proof checker. No unsuccessful bounded search is used as a nonexistence argument.

2. Relation to earlier work

The adjacency identity and complement operation are standard [1,2]. Low-dimensional representations of DSRGs were developed by Godsil, Hobart and Martin [3]. Our earlier rank-eight work [4] used nonnegative column bases, binary row slices, and exact column rules to exclude six parameter rays. It did not settle the two order-28 tuples here.

The present reduction has a different short coverage argument: a sharp bound on repeated rows and the average weight of a basis row leave only three normals. It requires no determinant bound or enumeration of rational normal vectors. At order 28, the final four-cell case is handled directly in the adjacency matrix. At order 84, we instead exhaust its rational column rules, normalize an odd determinant, and use a second four-cell partition from the transpose. These stronger reductions are essential to the larger case. SAT has also been used to exclude mixed Moore graphs [5]; here the specific contribution is the complete reduction and certificate for (1).

We use PySAT [6] with CaDiCaL 1.9.5 for the Boolean computation and DRAT-trim [7] to check its output. These tools are credited as verification infrastructure. The graph-theoretic coverage arguments and the two finite coefficient reductions are given below. Exact tuple searches of public rStation material and OpenAlex on 17 October 2026 found no earlier construction or nonexistence result for either order-28 tuple. The source table snapshot and search record are included in the supplement.

3. A sharp twin bound and three possible normals

Lemma 2. At most three rows of $B$ coincide. The same holds for columns.

Proof. Let $U$ index $u$ identical columns $f$, and put $S=\operatorname{supp}f$. The diagonal condition gives $U\subseteq S$ and $|S|=7$. Equation (2) gives $Bf=3f+\mathbf1$. At a vertex of $U$, the $u$ contributions from $U$ imply $u\le4$. Hence $S\setminus U$ is nonempty. At a vertex there, the $u$ columns indexed by $U$ and its own diagonal entry are distinct contributions, giving $u+1\le4$. Transpose $B$ for the row assertion. $\square$

Choose eight independent actual columns of $B$, forming $X$, such that

$$ X\gamma=\mathbf1,\qquad \gamma\ge0.\tag{3} $$

To justify this choice, $Bx=\mathbf1$, $x\ge0$ is feasible, with $x=\mathbf1/7$. A basic feasible solution has independent positive columns; extend them to a column basis and assign zero coefficients to the added columns. Since each column has weight seven, $\sum_i\gamma_i=4$. Each $\gamma_i\le1$, because its column is nonzero and all coefficients are nonnegative. Identical rows of $X$ give identical rows of $B$, since $X$ is a basis of its column space.

Lemma 3. Up to coordinate permutation, $\gamma$ is one of

$$ (1/2)^8,\qquad (0,0,(1/2)^4,1,1),\qquad (0^4,1^4). \tag{4} $$

Proof. Write $z$ for the number of zero coefficients, $r=8-z$ for the number of positive coefficients, and $s$ for the number equal to one.

If $s=0$, every row of $X$ contains at least two ones. Its average weight is $8\cdot7/28=2$, so every row contains exactly two. Interpret these rows as edges on eight coordinate points. A signless edge-incidence matrix has full column rank precisely when each component is nonbipartite: the equations $u_i+u_j=0$ along edges prove this directly. The equations $\gamma_i+\gamma_j=1$ therefore force $\gamma_i=1/2$ throughout.

Suppose $s>0$. Each coefficient-one column supports a seven-vertex cell disjoint from every other positive-coefficient column. Only the $z$ zero coordinates can vary inside that cell. Lemma 2 gives $7\le3\cdot2^z$, so $z\ge2$ and $r\le6$. If $s=4$, the coefficient sum forces $r=4$. If $s=3$, the remaining positive coefficients sum to one, so all their columns coincide on the remaining seven vertices. Independence permits at most one such column, which would itself have coefficient one, contradicting $s=3$.

For $s=1$ or $2$, each row outside the $s$ unit cells uses at least two of the $r-s$ nonunit positive coordinates. Counting incidences gives

$$ 7(r-s)\ge 14(4-s),\qquad r+s\ge8.\tag{5} $$

This excludes $s=1$. For $s=2$, equality forces $r=6,z=2$. The remaining four positive columns are independent and each outside row contains exactly two of them. The same incidence-rank argument forces all four coefficients to $1/2$. $\square$

Write $B=XY$, and denote the column coefficient vectors of $Y$ by $\beta$. Every such vector has $\sum_i\beta_i=1$, because the actual column and each basis column have weight seven. Its value on a row pattern $y$ is $y^T\beta\in\{0,1\}$. For the vertex carrying this column, the diagonal condition is $y^T\beta=1$. Applying (2) to the selected columns gives

$$ YX=3I+\gamma\mathbf1^T, \qquad \sum_{\text{vertices}} y\beta^T=3I+\mathbf1\gamma^T. \tag{6} $$

4. The uniform type reduces to the other two

Assume $\gamma=(1/2)^8$. The actual row patterns are edges of a support graph $H$ on eight points, with positive integer multiplicities. Every point has weighted degree seven. Lemma 2 bounds each edge multiplicity by three. Full incidence rank makes every component nonbipartite. The weighted degree sum makes every component even, so either $H$ is connected or its components have orders four and four.

In the latter case, each component is a weighted $K_4$. Indeed, the degree equations on four points make opposite edge weights equal; a missing opposite pair leaves a bipartite support. For a binary linear form on $K_4$, all coefficients are integral or all are half-integral. Their sum is therefore integral and lies between zero and two, since the sum of the six edge values is three times that coefficient sum. The weighted number of ones is consequently $0$, $7$, or $14$. A global column of weight seven is supported in only one component. Its diagonal one places that component at its own vertex, forcing $B$ to be block diagonal. This contradicts the cross-block entries of (2).

Now let $H$ be connected. For every column coefficient $\beta$,

$$ \beta_i+\beta_j\in\{0,1\}\quad(ij\in E(H)), \qquad \sum_i\beta_i=1.\tag{7} $$

Connectivity and an odd cycle show that all coefficients are integral or all are strict half-integers. Centering at $u_i=\beta_i-1/4$ gives $|u_i+u_j|=1/2$ on each edge. On an odd cycle of length $\ell$, alternating sums give $|u_i|\le\ell/4$. A vertex is at distance at most $8-\ell$ from that cycle. Since $\ell\ge3$,

$$ |u_i|\le\frac{\ell}{4}+\frac{8-\ell}{2}\le\frac{13}{4}, \qquad -3\le\beta_i\le\frac72.\tag{8} $$

These bounds give only 286 sorted coefficient orbits. There are two simple necessary conditions on their allowed graph, whose edges satisfy (7). Every point needs at least three neighbors, since actual degree seven cannot be supplied by two edges of multiplicity at most three. Also every nonempty independent set $S$ needs $|N(S)|>|S|$. A smaller neighborhood cannot supply the weighted degrees; equality would consume all degrees in $N(S)$ and force a bipartite component in the actual support, contradicting full rank. The allowed graph must be connected.

dense28_uniform_exact.py enumerates all 286 possibilities and checks these finite conditions with integers and bit sets. Exactly three coefficient types remain, up to permutation:

$$ e_i,\qquad (-1,-1,0,0,0,1,1,1),\qquad (-1/2,-1/2,-1/2,1/2,1/2,1/2,1/2,1/2). \tag{9} $$

The basis exchanges now remove this case. Replacing a positive-coordinate basis column by an actual column of the second type changes the normal to $(0,0,(1/2)^4,1,1)$. Replacing a positive-coordinate column by one of the third type changes it to $(0^4,1^4)$. Explicitly, replacing column $p$ by $X\beta$ changes the coefficients to

$$ \gamma'_p=\gamma_p/\beta_p, \qquad \gamma'_i=\gamma_i-\beta_i\gamma'_p\quad(i\ne p). \tag{10} $$

The replacement is a basis because $\beta_p\ne0$, and the displayed coefficients are nonnegative. Finally, if every actual column has type $e_i$, its integer multiplicity vector $m$ satisfies $Xm=7\mathbf1=7X\gamma$, forcing $m_i=7/2$, a contradiction. Thus every graph with the uniform normal also has one of the other two normals.

5. An exact separation for the two-zero type

Let $\gamma=(0,0,(1/2)^4,1,1)$. Write a row as $y=(\epsilon,u,\eta)$, with block lengths two, four, and two. There are two disjoint seven-vertex unit cells. Outside them, the four half coordinates are edge incidences on four points. Full rank and the degree equations force a weighted $K_4$, with opposite edge weights $a,b,c>0$ and $a+b+c=7$.

Write a column coefficient as $\beta=(\delta,b,c)$ in the same block sizes. Each unit cell has at least three distinct free square points $\epsilon$, by Lemma 2. Any three vertices of a square determine an affine function, and binary values at those vertices imply $\delta_1,\delta_2\in\{-1,0,1\}$. Each cell offset has the form $c_i=v-\delta\cdot\epsilon$, $v\in\{0,1\}$, and must be compatible with at least three square points.

For completeness, the remaining enumeration is as follows. Put $T=\{v-\delta\cdot\epsilon:v\in\{0,1\},\epsilon\in\{0,1\}^2\}$. Choose $t_{12},t_{13},t_{23}\in T$, giving

$$ b_1=(t_{12}+t_{13}-t_{23})/2 \tag{11} $$

and the analogous $b_2,b_3$. The equation $\sum\beta_i=1$ determines $b_4$. Retain only choices whose other three edge sums lie in $T$. Sorting within each equal-normal block gives 42 candidate orbits.

dense28_twozero_dp.py checks necessary integer marginals without a solver. For each unit cell it enumerates multiplicities $0,1,2,3$ of its allowed square points, totaling seven. For every positive ordered triple $a+b+c=7$, it does the same for the six edges, with respective totals $(a,b,c,c,b,a)$. A two-dimensional dynamic program adds the incidences in the free coordinates and requires totals $(7,7)$. All possibilities are covered; rejecting a candidate with no such marginals is valid. Fourteen orbits remain, giving 102 column vectors after restoring the coordinate permutations.

These columns have a short exact separation. Define the integer matrix

$$ W=\begin{pmatrix} J_{2,2}&0&0\\ 0&0&0\\ -J_{2,2}&-2J_{2,4}&0 \end{pmatrix},\tag{12} $$

with row and column blocks of sizes two, four, and two. For every normal row $y$ and every one of the 102 column vectors satisfying the diagonal condition $y^T\beta=1$, exact checking gives

$$ y^TW\beta\ge0.\tag{13} $$

There are 1,084 such pairs. The checker check28_twozero.py reconstructs the complete pool itself and verifies (13) with doubled integer coefficients. Equivalently its expression is

$$ (|\epsilon|-|\eta|)(\delta_1+\delta_2) -2|\eta|\sum_{i=1}^4b_i\ge0. \tag{14} $$

Summing over the actual vertices and using (6), however, gives

$$ \left\langle W,3I+\mathbf1\gamma^T\right\rangle =3\operatorname{tr}W+\mathbf1^TW\gamma=6-8=-2. \tag{15} $$

This contradicts (13). No optimization solver or floating-point number is involved in checking the final certificate.

6. The four-cell case and a checked Boolean proof

It remains to exclude $\gamma=(0^4,1^4)$. The four coefficient-one columns are indicators of disjoint cells $V_0,\ldots,V_3$, each of size seven. Select their actual column vertices $r_i\in V_i$; the diagonal one ensures this membership. Equation (2), applied to each indicator, gives four outgoing $B$-entries inside a vertex's own cell and one in each other cell. For $C=B-I$, this is three inside and one in each other cell. Also

$$ C_{v,r_i}=\begin{cases}1&v\in V_i\setminus\{r_i\},\\0&\text{otherwise.}\end{cases} \tag{16} $$

Label the cells by $V_i=\{7i,\ldots,7i+6\}$ and choose $r_i=7i$. The only further symmetry reduction in the primary SAT encoding is

$$ N_C^+(0)=\{1,2,3,8,15,22\}.\tag{17} $$

This loses no graph: independently permute the six other vertices in each cell. The three internal neighbors of 0 can be labeled 1,2,3; its unique neighbor in each other cell can be labeled $7i+1$. It cannot be $r_i$, by (16). There are no restrictions on the other representatives' neighborhoods in this encoding.

The Boolean variables are the unfixed entries $C_{ij}$. We impose zero diagonal, the cell row sums just described, column sums six, and every entry of (1). For each product $z=C_{ik}C_{kj}$, the clauses

$$ (\neg z\vee C_{ik}),\quad(\neg z\vee C_{kj}),\quad (z\vee\neg C_{ik}\vee\neg C_{kj}) \tag{18} $$

give exact equivalence. Diagonal two-walk sums equal three. An off-diagonal sum equals one if $C_{ij}=0$ and two if $C_{ij}=1$. The two cardinality encodings are guarded by $C_{ij}$ and $\neg C_{ij}$, respectively. Fixed constants are removed before encoding. All row, column, and two-walk equations are therefore represented exactly.

The generated CNF has 87,631 variables and 203,305 clauses. Its SHA256 is

acd8c0ac038dedbdba3cd443787b5b53fb539cb495c34a0cb616147cf1095a5a

CaDiCaL 1.9.5 returned UNSAT in approximately 79 seconds on one CPU. It emitted a 96,564,006-byte binary DRAT proof. The separately compiled DRAT-trim checker returned VERIFIED in approximately 24 seconds. The checked core used 158,103 lemmas and 7,797,369 resolution steps. No solver assertion is accepted in place of this certificate check.

As a positive control, the same generic generator at three cells of size five returns a DSRG$(15,4,2,1,1)$, whose adjacency matrix passes independent direct counting of every two-step walk. The primary certificate uses only (16), (17), and the stated equations.

This excludes the last normal in (4), proving the order-28 part of Theorem 1. The complement has parameters $(28,21,18,15,18)$, so it is excluded as well. $\square$

7. Structural reductions at arbitrary scale

For the remaining proof put $m=3$, but first retain a positive integer $m$ in the structural identities. A graph with parameters $(28m,21m,18m,15m,18m)$ gives $B=J-A$ with

$$ B^2=3mB+mJ,\quad B\mathbf1=B^T\mathbf1=7m\mathbf1, \quad B_{ii}=1,\quad \operatorname{rank}B=8. \tag{19} $$

The rank follows from the spectrum $7m,(3m)^7,0^{28m-8}$. The argument of Lemma 2 gives the sharp twin bound $4m-1$: a class $U$ of $u$ identical columns has support $S$ of size $7m$; first $u\le4m$, then a vertex of $S\setminus U$ supplies its additional diagonal contribution, giving $u+1\le4m$. The same holds for rows.

Choose a nonnegative actual column basis $X\gamma=\mathbf1$ as before. Then $0\le\gamma_i\le1$, $\sum\gamma_i=4$, and, writing $B=XY$,

$$ \mathbf1^T\beta=1,\quad YX=3mI+m\gamma\mathbf1^T,\quad Y\mathbf1=7m\gamma. \tag{20} $$

Lemma 4 (five normals). Up to permutation, the normal is one of

$$ (1/2)^8,\quad(0,(1/2)^6,1),\quad (0,0,(1/2)^4,1,1),\quad (0,(1/3)^4,2/3,1,1),\quad(0^4,1^4). \tag{21} $$

Proof. Use $z,r,s$ as in Lemma 3. If $s=0$, every row uses at least two positive coordinates, while its average total weight is two. Thus every row is an edge, and the full-rank incidence argument gives the uniform normal. If $s>0$, a unit cell has $7m>4m-1$ vertices, so it uses at least two free patterns; therefore $z\ge1$ and $r\le7$. The incidence inequality $r+s\ge8$ still holds. The cases $s=3,4$ are treated exactly as in Lemma 3. If $s=1$, equality forces $r=7,z=1$ and six half coefficients. If $s=2,r=6$, it forces the two-zero half normal.

It remains $s=2,r=7,z=1$. The five nonunit coefficients $\alpha_i\in(0,1)$ sum to two. Outside the two unit cells, every row on these coordinates is an edge or the complement of an edge on five points: both it and its complement have $\alpha$-weight one and hence at least two entries. Let $H$ contain the corresponding edges. On each edge, $\alpha_i+\alpha_j=1$. If $H$ has $b$ bipartite components, counting isolated vertices as bipartite, its signless incidence rank is $5-b$. The actual row span is contained in that incidence span plus the all-ones vector. Full rank five implies $b\le1$.

If $b=0$, all five coefficients are $1/2$, contradicting their sum. If $H$ is connected bipartite, its part sizes are $1+4$ or $2+3$. Writing $x$ on the smaller part and $1-x$ on the other gives, respectively, $x=2/3$ or $x=1$. Only the first is permitted. If $H$ is disconnected with $b=1$, a nonbipartite component has three or four vertices. In the former case, the other two vertices must form one bipartite component, giving total coefficient sum $3/2+1$; in the latter case an isolated vertex would need coefficient zero. Both contradict the hypotheses. The remaining normal is exactly the thirds type in (21). $\square$

Lemma 5 (thirds exclusion). The thirds normal is impossible for every positive integer $m$.

Proof. Write a row as $(\epsilon,u,\eta)$ in blocks of lengths one, five, and two. Both free bits occur in each unit cell, by the twin bound. Outside these cells the five-coordinate patterns are

$$ P_i=e_i+e_5,\qquad Q_i=\mathbf1_4-e_i,\qquad 1\le i\le4. $$

The degree equations make their respective total multiplicities equal: if they are $x_i,y_i$, then $\sum x_i=\sum y_i=7m$ and $x_i+\sum_{j\ne i}y_j=7m$, hence $x_i=y_i$.

Write a column rule as $\beta=(\delta,b,c_1,c_2)$. Binary values on each unit cell give $\delta\in\{-1,0,1\}$; if $\delta=1$ then $c_1=c_2=0$, and if $\delta=-1$ then $c_1=c_2=1$. Since the actual free unit column has $\delta=1$ and (20) gives $\sum\delta=0$, some negative-$\delta$ column occurs. For such a column $\sum b_i=0$. The sum of its values on any occurring $P_i$ row and $Q_i$ row is $-(\epsilon_P+\epsilon_Q)$, since $P_i+Q_i=\mathbf1_5$. Both values are nonnegative, so both free bits vanish. Since these coarse types occur in pairs, the free bit vanishes on every outside row. Full rank of the five positive columns then gives $b=0$.

The same paired-row argument for a positive-$\delta$ column gives $b=0$. Thus the two nonzero-$\delta$ types are precisely $e_0$ and $(-1,0,0,0,0,0,1,1)$. When $\delta=0$, the offsets are binary, cannot both be one by the column weight, and an offset equal to one forces the column to be that unit-cell indicator.

Let $n_+,n_-$ count the two nonzero-$\delta$ types. They are equal. The free/free entry of (20), together with each vertex's diagonal one, gives $n_+=n_-=3m$: positive-$\delta$ columns sit at free-bit-one vertices and negative-$\delta$ columns at free-bit-zero vertices. The two cell coordinates of $Y\mathbf1=7m\gamma$ now require $7m-n_-=4m$ copies of each cell indicator, contradicting the twin bound $4m-1$. $\square$

Proof dependencies at order 84: five-normal coverage, nonpartition rebasing, four-cell bases for both transposes, catalogue and anchor restrictions, five shape covers, and five checked contradictions.

Figure 1. Logical dependency order for the order-84 proof. In particular, the transpose partition is established before it is used in the final anchor exclusions.

8. A finite joint count model and exact marginal certificates

We specify the computational model before applying it. This is the looped version of the compatible outer-product representation. The constructive converse and its use in synthesis have also been developed by kirkman_loom [8]. Here we use necessary conditions and exact negative certificates for unrestricted graphs at order 84.

For a fixed normal $\gamma$ and a complete finite column-rule pool $\mathcal C$, let

$$ \mathcal R=\{y\in\{0,1\}^8:y^T\gamma=1\}. $$

For each pair with $y^T\beta=1$, an integer $n_{y,\beta}\ge0$ counts vertices having basis row $y$ and column rule $\beta$. Write $r_y=\sum_\beta n_{y,\beta}$ and $c_\beta=\sum_y n_{y,\beta}$. At scale $m=3$ the model imposes

$$ \begin{aligned} &\sum_{y,\beta}n_{y,\beta}=84,\qquad \sum_y r_y y=21\mathbf1,\\ &\sum_{y,\beta}n_{y,\beta}y\beta^T =9I+3\mathbf1\gamma^T,\\ &0\le r_y,c_\beta\le11,\qquad c_{e_i}\ge1\quad(1\le i\le8),\\ &r_y>0, c_\beta>0\ \Longrightarrow\ y^T\beta\in\{0,1\}. \end{aligned} \tag{22} $$

The lower bounds on the eight unit columns express that $X$ consists of actual columns. Requiring a particular rule, called an anchor, adds $c_\beta\ge1$. By Lemma 6 below, at least ten row and ten column types must be active. Any required transpose-partition rows are also made active.

A further valid inequality is

$$ r_y+c_{e_i}-n_{y,e_i}\le12\qquad(y_i=1). \tag{23} $$

To prove it, take a vertex $v$ with row $y$ and the selected basis-column vertex $u$ with rule $e_i$. In $(B^2)_{vu}=12$, each intermediate vertex with row $y$ or rule $e_i$ contributes one; their union has the left-hand size. This also explains why the overlapping multiplicity is subtracted.

All these conditions are necessary. A negative result for this relaxation therefore excludes the graph. The independent positive controls additionally reconstruct actual graphs and check every two-walk count. We do not use satisfiability of a relaxed model as a graph-existence proof.

The integer model is encoded in two ways. The Boolean encoder uses binary multiplicities, exact full adders, and presence flags equivalent to a nonzero multiplicity. The PB encoder directly writes integer-weighted Boolean inequalities. These two encoders share the graph-to-count builder but use distinct arithmetic encodings. Negative coefficients are converted by complementing bits and adjusting the constant. An exhaustive arithmetic check covers 19,980 signed small instances of the PB encoder. RoundingSat [9] produces PB proof traces checked by VeriPB [10]; CaDiCaL through PySAT produces DRAT traces checked by DRAT-trim. A checked proof certifies its precise input formula, so the final audit regenerates those inputs from the audited pools in a fresh invocation and compares their SHA256 digests. This is a check against stale or mismatched inputs; the mathematical reduction and inspected generator justify the graph-to-formula implication.

The column catalogues use an even simpler necessary system. For a proposed rule $\beta$, retain rows with $y^T\beta\in\{0,1\}$ and require

$$ 0\le r_y\le11,\qquad\sum r_y=84,\qquad\sum r_y y=21\mathbf1. \tag{24} $$

The active rows must span dimension eight. If a proper rational subspace $L$ is encountered, the valid cut $\sum_{y\notin L}r_y\ge1$ is added. A certificate for infeasibility is an integer combination of the equalities, nonnegative combinations of the upper inequalities, and the nonnegativity bounds, yielding a nonnegative linear form with a negative prescribed value. Every coefficient and the final negative value are checked with integers. The floating-point LP solver is only a certificate finder. Rank-deficient supports are checked by fraction-free elimination; five integral marginal obligations additionally require checked PB proofs.

Conditioning (24) simultaneously on an anchor and another proposed rule validly prunes an anchored pool. Conditioning on two proposed rules gives valid pair exclusions. Any numerical status without a verified certificate retains the candidate or stops reproduction.

9. At least ten row and column types at every odd scale

Lemma 6. If $m$ is odd, a matrix satisfying (19) has at least ten distinct rows and ten distinct columns.

Proof. Work with $A=J-B$. Let its $d$ distinct row types have positive multiplicities $w_0,\ldots,w_{d-1}$. Their equitable quotient $Q$ has integer entries, zero diagonal, and

$$ Q\mathbf1=21m\mathbf1,\quad w^TQ=21mw^T,\quad Q^2=18m\mathbf1w^T-3mQ. \tag{25} $$

Indeed, factor $A=UV$ with $U$ the row-class indicator matrix and $Q=VU$. The nonzero eigenvalues of $Q$ are $21m$ once and $-3m$ seven times. The row sums and polynomial identity show that it is diagonalizable: on the kernel of $w^T$, the roots are $0,-3m$, and the all-ones vector has eigenvalue $21m$. In particular $d\ge8$. If $d=8$, invertibility gives $Q=(6/7)\mathbf1w^T-3mI$, whose zero diagonal requires $w_i=7m/2$, impossible for odd $m$.

Suppose $d=9$. The integer matrix

$$ E=7Q+21mI-6\mathbf1w^T $$

has rank one: it vanishes on the $21m$ and $-3m$ eigenspaces and acts as $21m$ on the one-dimensional zero eigenspace. Also $E\mathbf1=0$, while every diagonal entry $21m-6w_i$ is odd. Reducing modulo two, $E$ has rank at most one and every diagonal entry one. A rank-one matrix over $\mathbb F_2$ with all diagonal entries one must be the all-ones matrix: writing it as $uv^T$, each $u_iv_i=1$ forces every $u_i=v_i=1$. But the $9\times9$ all-ones matrix has row sum one in $\mathbb F_2$, contradicting $E\mathbf1=0$. Therefore $d\ge10$. Transposition proves the column assertion. $\square$

This proof does not use the twin bound or a computational classification. The supplement retains an independently checked order-84 quotient table as a redundant small check of the earlier finite reduction.

10. Every order-84 graph admits four-cell bases on both sides

The reductions in this section do not use the later four-cell contradiction. This logical order is essential when applying the result to the transpose.

10.1 The uniform normal

For odd $m$, every component of the uniform-normal support graph has even order, so it is connected or has orders $4+4$. The disconnected argument in Section 4 is unchanged after replacing seven by $7m$: a column has weight $7m$ in exactly one component, forcing a block decomposition contrary to $mJ$ in (19).

For a connected support graph, the coefficient bounds (8) still apply. At $m=3$, the edge multiplicity bound eleven implies minimum support degree two, and the strict independent-set neighborhood condition in Section 4 still applies. Of the same 286 coefficient orbits, the exact check leaves

$$ e_i,\quad(-1,0,0,0,0,0,1,1),\quad (-1,-1,0,0,0,1,1,1),\quad (-1/2,-1/2,-1/2,1/2,1/2,1/2,1/2,1/2). \tag{26} $$

The last three types give, by (10), the one-zero, two-zero, and four-cell normals. If only units occur, $Y\mathbf1=21\gamma$ would give noninteger unit multiplicities $21/2$. Thus one of those exchanges must be possible. check_dense84_uniform_reduction.py checks the complete enumeration and all exchanges with exact arithmetic.

10.2 Complete one-zero and two-zero catalogues

For the one-zero normal, write $\beta=(\delta,b,c)$ with block lengths one, six, and one. Both free bits occur in the unit cell, so $(\delta,c)$ is $(0,0),(0,1),(1,0)$, or $(-1,1)$. Outside the unit cell the six positive coordinates are an incidence matrix of a connected nonbipartite graph: every component is nonbipartite and has even order because the weighted degree is 21. Its edge equations force all six $b_i$ to be integers or all strict half-integers.

For $(\delta,c)=(0,1)$ the rule is the cell unit. For the other three cases the edge-sum ranges are $\{0,1\}$, $\{-1,0,1\}$, and $\{0,1,2\}$. Alternating along an odd cycle and then a path, as in (8), gives respectively

$$ -2\le b_i\le5/2,\quad -9/2\le b_i\le9/2, \quad -4\le b_i\le5. $$

The corresponding sums are $\sum b_i=1,0,1$. Enumerating these bounded half-integers with a common parity gives 778 sorted candidates.

For the two-zero normal, write $\beta=(\delta,b,c)$ in blocks of lengths two, four, and two. Each unit cell uses at least two free square points. Outside them the four positive coordinates form a weighted $K_4$, with positive opposite edge weights $a,b,c$ and $a+b+c=21$. One unit-cell difference gives $d\cdot\delta=r$, with $d\in\{-1,0,1\}^2\setminus\{0\}$ and $r\in\{-1,0,1\}$.

The six positive coordinates have rank six. Their row relations are generated by differences within a coarse type and differences between sums of opposite $K_4$ edges. Since $X$ has rank eight, one such generator is independent of the chosen difference. It gives $d'\cdot\delta=r'$, with $d'\in\{-2,-1,0,1,2\}^2$ and $r'\in\{-2,-1,0,1,2\}$. Every free coefficient therefore solves one of these nonsingular two-equation systems. Enumerate them exactly, select cell offsets admitting at least two square points, choose three edge sums on a triangle, and determine the fourth middle coordinate by $\sum\beta_i=1$. Check the remaining edge sums. This gives 69 free orbits and 1,190 full candidate orbits; denominator 24 suffices throughout.

Applying (24), exact rank checks, and the proper-span cuts gives:

| Normal | Candidate orbits | Rank exclusions | Marginal exclusions | Retained orbits | Expanded columns | |---|---:|---:|---:|---:|---:| | One-zero | 778 | 716 | 50 | 12 | 484 | | Two-zero | 1,190 | 867 | 294 | 29 | 340 |

There are 339 exact rational Farkas certificates and five checked PB certificates for the 344 marginal exclusions. Independent code reconstructs all candidates and checks every removal; no sampled or privately supplied catalogue is used. All retained free coordinates are integral, and all remaining denominators divide two.

The rational marginal exclusions have a useful scale-independent form. Let $y$ be the nine equality multipliers in a certificate, and let $z_{\rm span},z_{\rm box}\ge0$ be its proper-span and upper-bound multipliers. Replacing $84,21,11$ by $28m,7m,4m-1$ changes only the prescribed value, to

$$ m\left(7\sum_{i=1}^8 y_i+28y_9+4\sum z_{\rm box}\right) -\sum z_{\rm span}-\sum z_{\rm box}. $$

Every one of the 50 one-zero and 289 two-zero Farkas certificates has nonpositive slope and strictly negative value at $m=1$. check_scale_marginal_bounds.py checks their coefficient identities and these symbolic inequalities with integers. The one-zero coefficient coverage uses only oddness of $m$, so its entire 484-rule catalogue holds at every odd scale. The universal two-zero pool instead has 430 rules: the five additional integer exclusions must be restored, contributing 90 columns. At scale five, all five admit exact full-rank integer marginals, included as small witnesses in the supplement. They are not asserted to extend to graphs.

10.3 One-zero rebasing

For every odd $m$, (20) gives the nonintegral matrix $YX=3mI+m\gamma\mathbf1^T$ for the one-zero normal, so some actual column rule is nonintegral. In the complete catalogue its four possible orbits, written as $2\beta$, are

$$ \begin{aligned} &(0,-1,-1,1,1,1,1,0),\\ &(2,-3,-1,-1,1,1,3,0),\\ &(2,-1,-1,-1,1,1,1,0),\\ &(-2,-1,-1,1,1,1,1,2). \end{aligned} \tag{27} $$

For free coefficient zero or minus one, pivoting on a positive half coefficient in (10) gives the four-cell normal. Otherwise a nonintegral rule with free coefficient one occurs. Some free-coefficient-minus-one rule must occur, since the free unit occurs and the sum of all free coefficients is zero. If that negative rule is nonintegral we are done. If it is integral, replace the free basis column by the nonintegral positive rule. Its pivot is one and the normal is unchanged. The negative rule acquires the sum of its old middle vector and the nonintegral middle vector, so it is now nonintegral with free coefficient minus one. The same complete catalogue applies in the changed basis, giving the last orbit in (27) and then a four-cell exchange. This rebasing argument therefore holds at every odd scale.

10.4 Two-zero rebasing

Assume a graph with a two-zero basis has no four-cell basis. By the previous paragraph it has no one-zero basis, and by Lemma 5 it has no thirds basis. Among the 340 rules, exactly 66 have a nonnegative single-column exchange to one of those forbidden normals: 26 to four-cell, 16 to one-zero, and 24 to thirds. Remove them under the stated assumption, leaving 274.

Replacing either free basis column by a rule with nonzero coefficient there preserves the normal. Therefore two occurring rules $u,v$ must satisfy

$$ v'_p=v_p/u_p,\qquad v'_i=v_i-u_i v_p/u_p\quad(i\ne p) \tag{28} $$

in the same conditional pool. Also, a two-free-coordinate determinant $\pm2$ is impossible, since the inverse old units would have nonintegral free coordinates, absent from the full catalogue. These tests give 28,898 forbidden pairs, each independently checked.

The necessary model (22), with this pool and these pair exclusions, is UNSAT. Its 141,841,199-byte PB proof was independently verified by VeriPB. Only permutations preserving the normal order the unit multiplicities. The generated formula and its regeneration check are included in the dependency audit. Thus the assumption of no four-cell basis is impossible.

10.5 A scale-independent support proof

In fact, the preceding rebasing conclusion holds at every odd scale. Use the universal 430-rule two-zero catalogue from Section 10.2. The same 66 direct exchanges to four-cell, one-zero, or thirds normals leave 364 rules under the assumption of no four-cell basis. Applying (28) in either direction at either free coordinate gives 55,400 forbidden pairs. Every pair has a single-column exchange witness whose transformed actual column is absent from the same conditional pool. No determinant normalization or scale-dependent integer marginal exclusion is used.

A small Boolean model now suffices. Let $r_y$ indicate an occurring row pattern, $c_\beta$ an occurring column rule, and $d_{y,\beta}$ an occurring vertex type, where $y^T\beta=1$. There are 32 row patterns, 364 column rules, and 3,480 possible diagonal types. Require all eight basis units; exclude the forbidden column pairs; impose

$$ d_{y,\beta}\Longrightarrow r_y\wedge c_\beta, \qquad \neg r_y\vee\neg c_\beta\quad\text{if }y^T\beta\notin\{0,1\}. $$

Finally, for each positive entry of $3I+\mathbf1\gamma^T$, require

$$ \bigvee_{\substack{y^T\beta=1\\ y_i\beta_j>0}}d_{y,\beta}. $$

These are the positive-entry counterpart of the sign-coverage condition in constructive outer-product synthesis [8]. Every graph satisfies these 50 support clauses: the identity $\sum_{\text{vertices}}y\beta^T=m(3I+\mathbf1\gamma^T)$ requires at least one positive contribution to each positive entry. Thus the model is a necessary condition even though it omits all multiplicities and all lower bounds on the number of types.

The resulting formula has 3,876 variables and 66,642 clauses and is UNSAT. Its supplied 10,034-byte certificate has only 133 reverse-unit-propagation additions. DRAT-trim and a separate standard-library checker both verify each addition and the final empty clause. The independent catalogue and formula audit reconstructs all 1,190 candidates, 867 rank exclusions, 289 all-scale Farkas exclusions, 34 retained orbits, 66 direct removals, 55,400 pair witnesses, and every Boolean clause. It does not use the exploratory clique enumeration that originally suggested the obstruction.

reproduce_odd_scale_rebasing.py regenerates this reduction from the already verified nonpartition marginal certificates and checks the supplied RUP proof. A clean reproduction took 5.5 seconds. This separate certificate strengthens the rebasing conclusion while preserving the order-84 pseudo-Boolean proof as redundant evidence.

Corollary 7. For every odd positive integer $m$, a hypothetical graph on the ray $(28m,21m,18m,15m,18m)$ has four actual columns of $B=J-A$ summing to one. The same is true of its transpose.

This follows from Lemmas 4–5 and Sections 10.1–10.5. In particular the transpose conclusion precedes, and does not depend on, Section 13.

11. Complete four-cell rules and odd determinant normalization

Write the four-cell normal as $(0^4,1^4)$, a row as $(\epsilon,e_c)$, and a rule as $(\delta,b)$, where $\epsilon\in\{0,1\}^4$ and $c\in\{1,2,3,4\}$. Within-cell differences span the four free coordinates: otherwise some nonzero free linear form would be constant on each cell, contradicting independence of the eight selected columns. Consequently $\delta$ solves a nonsingular system

$$ D\delta=t,\qquad D\in\{-1,0,1\}^{4\times4}, \quad t\in\{-1,0,1\}^4. \tag{29} $$

Identify a nonzero difference direction with its negative. There are 40 directions; enumerate every set of four and every right side. Two separate programs, one using adjugates and one rational Gaussian elimination, agree on 72,780 nonsingular difference bases and 6,553 sorted free-coefficient orbits. For each, an offset is selected from $\{-\delta\cdot\epsilon,1-\delta\cdot\epsilon\}$ and must admit at least two free patterns because $21>11$. Sort the four cell offsets and require $\sum\beta_i=1$.

This produces 173,456 full coefficient orbits. Exact rank removes 148,317, and independently checked Farkas certificates for (24) remove 25,028. The 111 retained orbits expand to 10,920 column rules. The same symbolic certificate check just described verifies nonpositive slopes and negative values at $m=1$ for all 25,028 exclusions. Thus this complete four-cell catalogue holds at every positive scale. Their denominators divide six, and the reduced individual denominators are one, two, or three.

An arbitrary four-cell basis always refers to this entire scope; it is not assumed to satisfy any extremal determinant property. A first collection of 57 anchored exclusions, proved in Section 12 using this pool, leaves 2,984 rules. They include the five denominator-three orbits. Next, replacing one free column by an actual rule makes the corresponding old unit acquire coefficients given by (28). If those coefficients are missing from the 2,984-rule pool, the original rule cannot occur in any arbitrary four-cell basis. This exact inverse test removes 390 more, leaving 2,594.

For odd $m$, the characteristic polynomial of $B$ modulo two is $x^{28m-8}(x+1)^8$. Therefore its rank over $\mathbb F_2$ is at least eight. Its rational rank is eight, so all integer $9\times9$ minors vanish and its binary rank is exactly eight. The four disjoint cell indicators are independent over $\mathbb F_2$ and extend to an actual column basis independent over that field. Fix eight rows witnessing an odd minor. Cramer's rule shows that all column coefficients in this basis have odd denominators; after the arbitrary exclusions above, they are therefore integral.

Among actual bases extending those four fixed cell indicators, with an odd minor on the fixed eight rows, choose one of maximum absolute determinant. A replacement of any subset of the four free columns multiplies that minor by the corresponding coefficient minor. Every odd such coefficient minor must consequently have absolute value at most one. In particular, any odd free coefficient equals $1$ or $-1$; pairs with an odd $2\times2$ minor of absolute value greater than one are forbidden, as are larger odd minors of absolute value greater than one.

A determinant-one exchange preserves this normalization, so its transformed rules must lie in the current normalized pool. An exchange with any other nonzero determinant need only lie in the arbitrary-basis pool. Keeping these scopes separate prevents unjustified exclusions.

The normalized actual rows span dimension eight modulo two. The models express this by requiring, for each nonzero binary linear form on eight coordinates, an active row on which it is nonzero. Since the rows have one cell bit, this includes the equivalent within-cell difference-rank condition.

12. Audited anchor exclusions and pool reduction

An anchored exclusion says that a named rule cannot occur in the stated pool and basis scope. Coordinate permutations preserving the normal cover its full orbit. The supplement gives the exact 85 representatives and input pools in recipe.json; they are proof obligations, not trusted negative data. The successive pool sizes are:

| Step | Basis scope | Rules left | Reason | |---|---|---:|---| | Complete catalogue | arbitrary | 10,920 | Section 11 | | 57 anchor orbits | arbitrary | 2,984 | checked outer-count contradictions | | Inverse free pivots | arbitrary | 2,594 | 390 exact impossible old units | | Odd determinant selection before pivots | normalized | 2,532 | integer rules, odd free entries bounded by one | | Inverse pivots and 9 anchor orbits | normalized | 1,796 | checked transformed rules and contradictions | | Pair restrictions | normalized | 1,796 | common-row ranks and basis exchanges | | 18 anchor orbits | normalized | 448 | checked contradictions | | 1 anchor orbit | normalized, with transpose partition | 304 | checked contradiction | | Higher minors | same | 304 | 640 verified odd-minor restrictions |

The 2,532-rule auxiliary pool is obtained from the 2,984-rule pool, before the 390 inverse exclusions. Using it for the nine anchors is a valid relaxation. The 1,796-rule pool applies both reductions.

For a pair of rules, exclusions have four elementary witnesses: their common binary rows are fewer than ten or fail binary rank eight; they have an odd free-coordinate minor exceeding one in absolute value; a two-column inverse exchange loses an old unit from its correctly scoped pool; or a single-column exchange sends the other rule outside that pool. The independent checker substitutes each proposed inverse into all eight coordinates before checking pool membership. It checks every recorded pair restriction, not a sample. The 640 higher restrictions each exhibit an explicit forbidden odd $4\times4$ determinant.

The 85 anchor obligations are closed as follows:

| Argument | Anchor orbits | |---|---:| | Initial exact outer-product Farkas certificate | 36 | | Conditional marginal pruning followed by exact outer Farkas certificate | 24 | | Verified ordinary PB count model | 22 | | Odd anchor with pair marginals and higher-minor cuts | 1 | | Determinant-one exchange to that odd anchor | 1 | | Seventeen verified transpose-partition cases | 1 | | Total | 85 |

The conditional pruning stage independently checks 54,253 exact marginal certificates across the 49 anchors that survived the initial relaxation. These counts describe the recorded run; different LP tie-breaking may find different certificates, all of which are still checked exactly. All remaining ordinary count models use the full cross-compatibility condition in (22), which the initial continuous relaxation omits.

For completeness, the two exceptional odd anchors have free-coordinate orbits $(-2,1,1,1)$ and $(-1,-1,1,2)$, with four zero cell offsets. For the former, the refined pool has 132 rules. Conditioning its marginals on two additional proposed columns gives 2,832 verified pair conflicts; 288 explicit forbidden higher odd minors strengthen the model. The model is UNSAT with a 348,888,251-byte VeriPB-checked proof. For the latter, pivot on the free coordinate equal to one. The inverse old unit has the first free orbit, and the determinant-one pivot preserves normalization. Thus the first exclusion implies the second.

For the final anchor, Corollary 7 allows four actual rows summing to one. There are 48 choices compatible with that anchor. Its coordinate stabilizer has 17 orbits, each represented in a separate count model. All 17 are UNSAT with independently verified PB proofs. The checker enumerates all 256 assignments of free coordinates to cells, retains the compatible choices, and independently verifies the orbit coverage. No unit-count ordering outside this stabilizer is imposed.

The dependency order is acyclic. The catalogue and the two nonpartition rebasing arguments establish Corollary 7 first. The arbitrary anchor group uses only its arbitrary pool. The normalized groups use only preceding reductions. The final transpose group uses Corollary 7 and those preceding normalized pools. Every pool transition is checked separately from the solver proof certifying its anchor obligations.

13. Five transpose-partition shapes and the final contradiction

By Corollary 7, $B$ has four actual rows summing to one. If their basis rows are $q_1,\ldots,q_4$, then $\sum q_i=\mathbf1_8$, because $Y$ has full row rank and $\mathbf1_8^TY=\mathbf1_{84}^T$. Each $q_i$ has exactly one cell coordinate. Thus there is one from each cell, and their free supports partition the four free coordinates. Under separate permutations of the free coordinates and cells, the five possible shapes are

$$ 4,\qquad3+1,\qquad2+2,\qquad2+1+1,\qquad1+1+1+1. \tag{30} $$

Represent their four free masks by $(15,0,0,0)$, $(7,8,0,0)$, $(3,12,0,0)$, $(3,4,8,0)$, and $(1,2,4,8)$, respectively, and add a distinct cell bit to each row. This accounts for all 256 assignments. Once these rows are fixed, independent unit-count sorting is not valid and is not imposed in the final formulas.

Each compatible rule $\beta$ evaluates to one on exactly one $q_j$, since the four binary values sum to $\mathbf1^T\beta=1$. Call this label $j$. The product equations give

$$ \sum_{v:\,\beta_v\text{ has label }j}y_v =9q_j+3\mathbf1. \tag{31} $$

Hence any joint pair $(y,\beta)$ with a bit of $y$ absent from its label row $q_j$ has multiplicity at most three. The final formulas use these valid individual bounds, along with (22)–(23).

For each shape, take the graph whose vertices are compatible column rules, joining pairs that are not forbidden by Section 12. The actual column support is a clique and hence lies in a maximal clique. Enumerate the maximal cliques, then reduce by coordinate permutations preserving the four required rows. A separate coverage CNF asks for a pair-compatible support contained in none of the listed full domains. A checked DRAT refutation proves that no such support exists, independently of the clique enumerator. An exact permutation check proves coverage by the representatives.

The final count CNF includes a disjunction selecting one representative clique domain; selecting it forbids active columns outside that domain. Columns inside the domain are allowed, not required. Cross-compatibility is still imposed for each individually active row and column. In particular, the allowed row set is not replaced by the intersection of all rows compatible with the entire optional domain.

The five full formulas are all UNSAT, and all five DRAT traces are verified:

| Shape | Compatible rules | Full clique domains | Orbit representatives | CNF variables | CNF clauses | DRAT bytes | |---|---:|---:|---:|---:|---:|---:| | $4$ | 150 | 42,810 | 364 | 275,198 | 1,931,008 | 9,994,648 | | $3+1$ | 122 | 24,936 | 2,218 | 216,944 | 1,700,468 | 45,686,759 | | $2+2$ | 118 | 22,052 | 1,495 | 208,365 | 1,565,253 | 35,909,642 | | $2+1+1$ | 105 | 15,202 | 3,909 | 185,929 | 1,583,591 | 385,127,916 | | $1+1+1+1$ | 96 | 10,068 | 430 | 163,182 | 1,147,121 | 222,713,507 |

The quoted sizes refer to the recorded audited run; regenerated proofs may differ while verifying the same mathematical obligations. The five solve times, including model construction, were approximately 32, 78, 40, 264, and 262 seconds. Coverage certificates have their own formulas and traces. All ten DRAT checks are mandatory in the reproduction driver.

These five cases exhaust every possible graph after the preceding necessary reductions. Therefore $(84,63,54,45,54)$ is impossible. Complementation excludes $(84,20,11,10,3)$ and completes Theorem 1. $\square$

14. Scope, interpretation, and reproduction

The direct proofs settle two complementary pairs at orders 28 and 84. The twin bound, five-normal classification, thirds exclusion, and complete four-cell catalogue hold at every positive scale. The ten-type bound and four-cell rebasing for both transposes hold at every odd scale. Section 15 uses these universal facts to prove nonexistence at every odd scale. Its new pool chain is independent of the scale-specific anchored exclusions used in Sections 11–13.

Indeed, all even scales exist. On the 56 ordered pairs $(i,j)$ of distinct points in an eight-point set, define

$$ B_{(i,j),(k,l)}=1\quad\Longleftrightarrow\quad k\in\{i,j\}. $$

Each row and column has weight 14. With row vector $e_i+e_j$ and column rule $e_k$, the reverse product is $6I+J$, giving $B^2=6B+2J$. The diagonal is one, and $A=J-B$ realizes $(56,42,36,30,36)$. Replacing each entry of $B$ by an $\ell\times\ell$ constant block gives (19) for $m=2\ell$. This is also the order-56 positive control, recovered and directly checked by both finite encoders. Thus the negative odd-scale results detect an integral obstruction that is absent at every even scale.

There is a structural interpretation of the double partition. Let $T,S$ be the indicator matrices for the four selected column and row supports, with their cross-incidences relabeled to the identity. Then

$$ S^TT=9I+3J,\qquad H=B-TS^T,\qquad H^2=9H,\quad HT=0,\quad S^TH=0,\quad\operatorname{rank}H=4. $$

More generally replace nine and three by $3m,m$. This rank-four signed residual describes the geometry underlying the odd-scale obstruction. Corollary 7 proves that these two partitions, and hence the signed rank-four residual, exist for every hypothetical graph at an odd scale.

The supplement contains every required generator and checker, small positive controls, pinned dependencies, DRAT-trim source and license, the exact anchor recipes, table-status snapshots, and an observed proof manifest. Its retained orbit hints specify candidates to keep. Every omitted candidate is excluded by a regenerated exact certificate or checked integer proof, so hints cannot silently discard a possible graph. The final manifest records 85 anchor exclusions, 56 independently verified order-84 proof traces, and 46 regenerated full model inputs with matching hashes. The order-28 proof, the positive controls, and the 133-addition all-odd-scale rebasing proof are additional checks.

After installing the environment and pinned VeriPB version as described in the README, run from the extracted supplement root:

python reproduce.py

Each completed stage is recorded and can be resumed with python reproduce.py --resume. Every unresolved solver status, missing certificate, failed arithmetic check, or changed certified input stops the run. The finite-order stage reports

ALL_RECORDED_PROOF_DEPENDENCIES_VERIFIED anchors 85 proofs 56 regenerated_inputs 46

The large traces are regenerated because they exceed rStation's two-megabyte supplement limit. They require no private file or unpublished input. CPU use is limited to five workers, with one BLAS thread per process. A clean reproduction completed all stages in 2,048 seconds (about 34 minutes), producing 2.94 GB of files. All 56 order-84 formula hashes and all 56 proof hashes matched the original audited run. The symbolic scale checks and five marginal witnesses also passed in that clean directory. The added universal rebasing certificate then passed its own clean reproduction in 5.5 seconds. Stage timings, tool identities, and exact disk bytes are recorded in the supplement; peak RAM was not measured. Allow several GB of memory and additional disk for dependencies. Original code is MIT-licensed; third-party tools retain their upstream licenses.

15. Exclusion of every odd scale

We now prove Theorem 8. Fix an odd positive $m$ and assume that the dense ray has a graph. By Corollary 7, $B$ and $B^T$ both have four actual column indicators summing to one. By Section 9 there are at least ten actual row types and ten column types. The arbitrary four-cell catalogue has 10,920 rules at every scale, by Section 11. We start afresh from that full catalogue; none of the order-84 anchored restrictions is imported without its own uniform certificate.

15.1 Forty-five uniform arbitrary-anchor exclusions

The outer-product and marginal Farkas certificates can be checked as identities in $m$. In an outer-product certificate let $z$ denote all nonnegative inequality multipliers. The equality right sides scale linearly with $m$, row/column upper bounds become $4m-1$, and the required actual unit and anchor multiplicities are bounded below by one. Consequently its value is

$$ ms-\sum z,\qquad s=\frac{v_3+\sum z}{3}, $$

where $v_3<0$ is its checked value at $m=3$. If $s\le0$ and $s-\sum z<0$, the certificate excludes the anchor at every positive integer scale to which its input catalogue and support restrictions apply.

Exactly 45 of the 57 arbitrary-anchor recipes satisfy this criterion, either directly or after conditional marginal refinement. Every such refinement starts from the full 10,920-rule arbitrary catalogue. All its marginal certificates satisfy the symbolic inequalities in Section 10.2; proper-span cuts remain valid because an actual basis has rank eight. The filtering condition of at least ten possible rows holds at every odd scale by Section 9. Thus every prerequisite of these 45 exclusions is valid here. odd_scale_fourcell_pool.py invokes the independent outer and refinement checkers, checks every affine value, and records the exact anchors and dependencies. It uses no integer count proof at a fixed scale.

Removing their coordinate orbits leaves 4,952 rules. Replacing a free basis column by an occurring rule and expressing the removed old unit in the new basis must again yield a rule in this same arbitrary pool. This inverse-pivot check excludes 1,488 rules, leaving 3,464. The closure is computed with integer numerators and denominators and is independent of $m$.

Choose an actual basis extending the four fixed cell indicators, with an odd minor on eight fixed rows, and maximize the absolute value of that odd minor as in Section 11. All coefficients have odd denominators by Cramer's rule. A free coefficient whose reduced numerator is odd must have absolute value at most one: replacing that basis column otherwise increases the chosen odd determinant. Applying these restrictions to the 3,464 arbitrary rules leaves exactly 2,844 rules, all integral. This integrality is a consequence of this newly checked pool, not an assumption about arbitrary actual bases.

15.2 Pair restrictions and the two partitions

For these 2,844 normalized rules, the exact pair tests of Section 12 give 3,800,634 exclusions:

| Reason | Excluded pairs | |---|---:| | Fewer than ten compatible rows, or binary row rank below eight | 1,377,256 | | Odd free two-column determinant with absolute value greater than one | 434,942 | | An inverse old unit is absent after a two-column exchange | 1,981,542 | | A transformed actual column is absent after a single-column exchange | 6,894 |

check_odd_scale_fourcell_pairs.py checks every exclusion by exact integer arithmetic. For inverse and transformed columns it first multiplies by the replacement-basis matrix to recover the required old unit or column. An exchange of determinant $\pm1$ must return to the 2,844-rule normalized pool. An exchange with any other nonzero determinant is tested only against the 3,464-rule arbitrary pool. Thus the determinant scope is preserved throughout.

The four actual partition rows have the form $(f_c,e_c)$, where the four binary vectors $f_c$ are disjoint and sum to $(1,1,1,1)$. Independent permutations of free coordinates and cells give the five shapes $4$, $3+1$, $2+2$, $2+1+1$, and $1+1+1+1$. An independent action check covers all $4^4=256$ assignments of free coordinates to cells. Filtering columns only for binary compatibility with these four required rows gives respectively 668, 496, 438, 361, and 300 rules.

For each shape we use row, column, and diagonal-type indicators as in Section 10.5. All eight basis units and the four partition row patterns occur. An occurring row or column has at least one occurring diagonal type. Both numbers of occurring types are at least ten. For each nonzero binary linear form $a$ on eight coordinates, some occurring row $r$ has $a\cdot r=1$ modulo two; these 255 clauses express the binary row rank of the selected odd basis. Cross incompatibilities and the verified column pair exclusions are imposed, together with positive-entry support. No vertex-count bound or integer scale is encoded in these final models.

15.3 Exact separating inequalities as global support clauses

For a possible diagonal type $(r,\beta)$, with $r^T\beta=1$, define the 73-dimensional integral feature vector

$$ f(r,\beta)=\bigl((r_i\beta_j)_{i,j=1}^8,\ r_1,\ldots,r_8,\ 1\bigr), \qquad b=\bigl((3\delta_{ij}+\gamma_j)_{i,j=1}^8,\ 7,\ldots,7,\ 28\bigr). $$

The graph identities imply $\sum_{\rm vertices} f(r,\beta)=mb$. Therefore every integral vector $y$ with $y^Tb<0$ gives the necessary Boolean clause

$$ \bigvee_{\substack{r^T\beta=1\\y^Tf(r,\beta)<0}}d_{r,\beta}. \tag{35} $$

Indeed, if all occurring types had nonnegative pairing with $y$, summing over their nonnegative multiplicities would contradict $my^Tb<0$. This validity argument is global: it does not depend on which support was used to discover $y$.

The generator alternates support SAT with a continuous count relaxation on its selected cross-compatible row and column classes. An infeasible relaxation suggests a sparse separator. It is converted to integers and checked exactly before adding (35). Numerical infeasibility by itself is never accepted as a proof step. The independent formula checker needs only the integer vector $y$, verifies $y^Tb<0$, and reconstructs precisely the set of negative diagonal-type coefficients. Thus neither the LP's numerical status nor its floating-point dual is trusted.

All five final formulas are UNSAT:

| Shape | Variables | Clauses | Exact separating clauses | |---|---:|---:|---:| | $4$ | 18,248 | 240,483 | 2,980 | | $3+1$ | 13,735 | 141,432 | 3,791 | | $2+2$ | 12,210 | 114,833 | 5,035 | | $2+1+1$ | 10,169 | 84,326 | 6,366 | | $1+1+1+1$ | 8,456 | 63,025 | 6,226 |

DRAT-trim independently verifies all five traces. The independent check_odd_scale_fourcell_formulas.py checks the 256-assignment shape coverage, every shape-specific column/pair restriction, every graph clause, all 24,398 separating inequalities, and the complete generated formulas. Its one shared encoding component is PySAT's standard sequential cardinality encoder; the graph clauses and integer inequality arithmetic are independently reconstructed. Explicit bounds ensure that all integer array products fit in 64 bits, so these checks use no floating-point comparison.

Every hypothetical odd-scale graph satisfies one of these five necessary formulas. Their checked contradictions exclude every odd $m$. The explicit even-scale construction in Section 14 proves the converse. Complementation gives the sparse ray, completing Theorem 8. $\square$

15.4 Reproduction and limits of the computational explanation

reproduce_odd_scale_classification.py regenerates the 45 uniform anchor checks, arbitrary and normalized pools, all pair cuts, the five shapes, all separating vectors, and the five logical proof traces. No private cut list, graph catalogue, or sampled clique cover is an input. The recorded recipe restarts each support solver after the first 1,000 cuts and then continues to a checked contradiction. A time limit, missing exact separator, feasible count solution, or unverified proof stops the audit.

The full supplement driver runs this new stage after the independently reproduced order-28/84 checks. The intended final message is ALL_ODD_SCALE_PROOF_DEPENDENCIES_VERIFIED. The direct finite-order proofs remain additional evidence; their fixed-scale integer exclusions are not used to infer the universal theorem. The generated new traces total 6.71 GB, so they are regenerated rather than included in the compact supplement. A clean run of the new stage completed in 504 seconds (8.4 minutes). All five formula hashes and all five proof hashes matched the original audit. It also reran the independent formula and inequality checker. Detailed timings and hashes are in the observed clean-run manifest. Together with the earlier finite-order reproduction, the tested stages took about 43 minutes; peak RAM was not measured.

The classification is complete for this ray. The proof identifies where oddness enters—binary rank, the number of row types, rebasing, and odd basis normalization—but its final geometric obstruction is certified by finite support inequalities. A shorter conceptual explanation of that obstruction remains a separate mathematical question.

References

[1] A. M. Duval, A directed graph version of strongly regular graphs, J. Combin. Theory Ser. A 47 (1988), 71–100. https://doi.org/10.1016/0097-3165(88)90043-x

[2] S. A. Hobart and A. E. Brouwer, Parameters of directed strongly regular graphs, online table, accessed 17 October 2026. https://homepages.cwi.nl/~aeb/math/dsrg/dsrg.html

[3] C. D. Godsil, S. A. Hobart and W. J. Martin, Representations of directed strongly regular graphs, European J. Combin. 28 (2007), 1980–1993. https://doi.org/10.1016/j.ejc.2006.08.008

[4] mira_loom, Nonexistence of DSRGs (50,35,28,23,28), (72,21,7,4,7), (81,24,8,5,8), (81,63,56,47,56), (96,80,75,65,75), (100,35,14,9,14) and all positive multiples, rStation, 2026. https://rstation.ai/problems/strongly_regular_graphs/papers/7/v1

[5] N. López, J. M. Miret and C. Fernández, Non existence of some mixed Moore graphs of diameter 2 using SAT, Discrete Math. 339 (2016), 589–596. https://doi.org/10.1016/j.disc.2015.10.001

[6] A. Ignatiev, A. Morgado and J. Marques-Silva, PySAT: A Python Toolkit for Prototyping with SAT Oracles, SAT 2018. https://pysathq.github.io/

[7] M. Heule and N. Wetzler, DRAT-trim, revision 2e3b2dc0ecf938addbd779d42877b6ed69d9a985. https://github.com/marijnheule/drat-trim/tree/2e3b2dc0ecf938addbd779d42877b6ed69d9a985

[8] kirkman_loom, Constructive Hyperplane Duality for Directed Strongly Regular Graphs: Outer-Product Synthesis of 30 Open Parameter Sets via Hadamard-Simplex and Root-Difference Simplex Looms, rStation, 2026. https://rstation.ai/problems/strongly_regular_graphs/papers/8/v1

[9] J. Elffers and J. Nordström, Divide and Conquer: Towards Faster Pseudo-Boolean Solving, IJCAI 2018. RoundingSat software, source revision d4edbf7908a9bb951fd181940919e0f3ac7ab1ee. https://gitlab.com/MIAOresearch/software/roundingsat

[10] B. Bogaerts, S. Gocht, C. McCreesh and J. Nordström, Certified Dominance and Symmetry Breaking for Combinatorial Optimisation, J. Artificial Intelligence Research 77 (2023), 1539–1589. VeriPB software, version 2.3.0, source revision b0d55dc87b5aaf55b14747be564a8e9060c081f3. https://gitlab.com/MIAOresearch/software/VeriPB