# Directed strongly regular graphs with t = λ + 1: twin classes of closed neighbourhoods and the nonexistence of (66, 10, 5, 4, 1) and (91, 12, 6, 5, 1)

## 1. Problem and result

A directed strongly regular graph (DSRG) with parameters $(v, k, t, \lambda, \mu)$ is a loopless directed graph on $v$ vertices whose adjacency matrix $A$ satisfies

$$
AJ = JA = kJ, \qquad A^2 = tI + \lambda A + \mu (J - I - A),
$$

where $J$ is the all-ones matrix [1]. Every vertex has $k$ outgoing and $k$ incoming arcs, $t$ of them reciprocated, and the number of paths of length 2 from $x$ to $y \ne x$ is exactly $\lambda$ if the arc $x \to y$ is present and exactly $\mu$ if it is not. The heads of the arcs leaving a vertex $x$ are called its out-neighbours, and their set is denoted $\Gamma^+(x)$. The complement, the graph with matrix $J - I - A$, is also a DSRG, with parameters $(v, v - k - 1, v - 2k + t - 1, v - 2k + \mu - 2, v - 2k + \lambda)$ [1]; the complement of the complement is the original graph, so a graph with a given parameter set exists exactly when a graph with the complementary set exists, and parameter sets are treated in pairs. Throughout, $0 < t < k < v - 1$.

The table of Hobart and Brouwer [2] collects the feasible parameter sets with $v \le 110$, their constructions and their nonexistence results. The rStation problem `strongly_regular_graphs` [3] asks to resolve the open sets of this table. In the version of the table of 14 October 2026, 700 sets have $t = \lambda + 1$: 515 constructed, 46 marked as nonexistent and 139 open. Of them, 32 sets have $\mu = 1$, and seven of these 32 are open. The version of the table of 31 October 2026 adds results of the platform: there the sets $(40, 9, 6, 5, 1)$ and $(80, 19, 13, 12, 2)$ of Theorem 2, together with their complements, are marked as nonexistent by a condition from [5], and the set $(96, 11, 4, 3, 1)$ as constructed. The sets of Theorems 1 and 4 and the set $(96, 15, 10, 9, 1)$ are still open there. The numbers and statuses below follow the version of 14 October.

The paper studies the family $t = \lambda + 1$ through the matrix $B = A + I$. Its row $x$ is the closed out-neighbourhood $N^+[x] = \{x\} \cup \Gamma^+(x)$, and its column $y$ is the closed in-neighbourhood $N^-[y]$. Vertices $x \ne y$ with $N^+[x] = N^+[y]$ are called *row twins*, and those with $N^-[x] = N^-[y]$ *column twins*. The class $C_x$ is the vertex $x$ together with its row twins, and the class $D_x$ is the vertex together with its column twins; $a = |C_x|$ and $d = |D_x|$. We also put $K = k + 1$ and $q = \lambda + 2 - \mu$; $f$ is the multiplicity of the eigenvalue $q - 1$ of $A$ (Lemma 5).

**Theorem 1.** There is no directed strongly regular graph with parameters $(66, 10, 5, 4, 1)$ or $(91, 12, 6, 5, 1)$, and none with the complementary parameters $(66, 55, 50, 45, 50)$ or $(91, 78, 72, 66, 72)$.

**Theorem 2.** There is no directed strongly regular graph with parameters $(40, 9, 6, 5, 1)$, $(80, 19, 13, 12, 2)$ or $(96, 15, 10, 9, 1)$, and none with the complementary parameters $(40, 30, 27, 21, 27)$, $(80, 60, 54, 42, 54)$ or $(96, 80, 75, 65, 75)$.

**Theorem 3.** If a DSRG with $t = \lambda + 1$ and $\mu < \lambda + 2$ exists, then

$$
(\lambda + 2 - \mu)^2 \le \mu(v - k - 1). \tag{1}
$$

**Theorem 4.** There is no directed strongly regular graph with parameters $(28, 6, 3, 2, 1)$, and none with the complementary parameters $(28, 21, 18, 15, 18)$.

**Table 1.** The six closed pairs. The spectrum of $A$ is written as eigenvalues with their multiplicities.

| Set | Complement | Spectrum of $A$ | What fails | Where proved |
|---|---|---|---|---|
| $(66, 10, 5, 4, 1)$ | $(66, 55, 50, 45, 50)$ | $10^1, 4^{11}, (-1)^{54}$ | $k = 2\lambda + 2$, $\lambda = 4$: all classes are pairs, but $\lvert N^+[x]\rvert = 11$ | Theorem 15 |
| $(91, 12, 6, 5, 1)$ | $(91, 78, 72, 66, 72)$ | $12^1, 5^{13}, (-1)^{77}$ | $k = 2\lambda + 2$, $\lambda = 5$: all classes are pairs, but $\lvert N^+[x]\rvert = 13$ | Theorem 15 |
| $(40, 9, 6, 5, 1)$ | $(40, 30, 27, 21, 27)$ | $9^1, 5^{5}, (-1)^{34}$ | $q = 6 > \mu f = 5$ | Theorem 3 |
| $(80, 19, 13, 12, 2)$ | $(80, 60, 54, 42, 54)$ | $19^1, 11^{5}, (-1)^{74}$ | $q = 12 > \mu f = 10$ | Theorem 3 |
| $(96, 15, 10, 9, 1)$ | $(96, 80, 75, 65, 75)$ | $15^1, 9^{8}, (-1)^{87}$ | $q = 10 > \mu f = 8$ | Theorem 3 |
| $(28, 6, 3, 2, 1)$ | $(28, 21, 18, 15, 18)$ | $6^1, 2^{7}, (-1)^{20}$ | $k = 2\lambda + 2$, $\lambda = 2$: a vertex without a twin is excluded by the solver; without such a vertex all classes are pairs, but $\lvert N^+[x]\rvert = 7$ | Theorem 4, Section 6 |

**How the proof works.** When $t = \lambda + 1$, the equation for $A^2$ becomes $B^2 = qB + \mu J$ (Lemma 5). The entry $(x, y)$ of this equation is the number of vertices in $N^+[x] \cap N^-[y]$, and it depends only on whether $y$ lies in $N^+[x]$. The row class of a vertex $x$ lies inside $N^+[x] \cap N^-[x]$ and does not fill it, so it is small: $a \le \lambda + 1$ (Lemma 6). A vertex outside the class sees at most $\mu$ vertices of it, and double counting of pairs gives $a(\lambda + 2 - a) \le \mu(K - a)$ (Proposition 8). Every vertex outside the class has arcs to at least $q$ vertices outside $N^+[x]$, and every vertex outside $N^+[x]$ receives exactly $\mu$ arcs from $N^+[x]$. Counting these arcs gives the lower bound $a \ge K - \mu f$ (Proposition 9). Comparing two neighbourhoods that contain a common vertex of the class gives the upper bound $a \le K - q$ (Proposition 10). Together the two bounds require $q \le \mu f$, which is inequality (1).

When $\mu = 1$, the classes are much more rigid: two distinct vertices are never twins by row and by column at the same time, and $a + d \le \lambda + 3$ (Lemma 12). When $k = 2\lambda + 2$, the rank of $B$ is $k + 2$, exactly one more than the number of rows of $N^+[x]$. For a vertex without a row twin, the rows of $N^+[x]$ are independent, and outside $N^+[x]$ the rows of $B$ reduce to a single vector modulo their span. Hence such a vertex has a rigid structure: its second neighbourhood splits into blocks, and the sizes of the blocks agree only when $\lambda \le 2$ (Theorem 14). When $\lambda \ge 4$, the twin classes must be pairs, while $N^+[x]$ consists of an odd number $2\lambda + 3$ of vertices and cannot be split into pairs (Theorem 15).

The set $(28, 6, 3, 2, 1)$ also has $k = 2\lambda + 2$, but $\lambda = 2$, and Theorem 14 does not exclude a vertex without a twin. Theorem 4 splits the graphs into three cases (Section 6). A vertex without a row twin is excluded by a SAT solver: the formula that a graph with such a vertex would satisfy is unsatisfiable, and the proof of unsatisfiability is accepted by two checkers. A vertex without a column twin is a vertex without a row twin in the graph with matrix $A^\top$. If every vertex has twins, then a class of $\lambda + 1$ vertices is impossible, all classes are pairs, and $N^+[x]$ of $K = 7$ vertices again cannot be split into pairs (Lemma 16).

**Contributions.**

1. Theorem 3 and the bounds on classes for any $\mu$ (Section 4). Inequality (1) is invariant under blow-up by cliques, so every set it excludes excludes its whole line of blow-ups. In the table [2] it excludes six sets: the three open sets of Theorem 2 and three sets marked as nonexistent. None of them is constructed, and equality in (1) holds exactly for thirteen constructed sets $(8m, 4m - 1, 3m - 1, 3m - 2, m)$, $m = 1, \dots, 13$.
2. Theorem 14 on a vertex without a twin and Theorem 15 on the family $\mu = 1$, $t = \lambda + 1$, $k = 2\lambda + 2$, $\lambda \ge 4$ (Section 5). They close two open sets of the table, Theorem 1.
3. Theorem 4 and Lemma 16 (Section 6). Lemma 16 forbids a class of $\lambda + 1$ vertices in a graph where every vertex has twins and $K > 2(\lambda + 1)$; when $\lambda = 2$, all classes of such a graph are pairs. Hence Theorem 4 needs a solver search only for a vertex without a twin, and the solver proves the unsatisfiability of its formula in less than a second.
4. Sharpness (Section 7). The flag graph of a generalized quadrangle of order $(\sigma, \tau)$ is a known DSRG [23]; it turns into equalities the bound $a + d \le \lambda + 3$ and the double counting of Proposition 8. The quadrangle $W(2)$ gives a constructed DSRG $(45, 8, 4, 3, 1)$ with $k = 2\lambda + 2$ and $\lambda = 3$, so the threshold $\lambda \ge 4$ of Theorem 15 cannot be lowered.
5. A formalization in Lean 4 with the Mathlib library (Section 8). All five nonexistence results of Theorems 1 and 2 are proved together with the complements for any matrix, without hypotheses; inequality (1) is proved for any DSRG matrix with $t = \lambda + 1$ and $\mu < \lambda + 2$, and Lemma 16 for any DSRG matrix with $\mu = 1$ and $t = \lambda + 1$. Lean reduces Theorem 4 to one statement: a DSRG $(28, 6, 3, 2, 1)$ has no vertex without a row twin. That statement rests on a certificate of unsatisfiability, not on Lean. The remark on sharpness is not written in Lean either.

**What is taken from earlier work.** The spectrum of a DSRG, the multiplicity formulas and the decomposition of $\mathbb R^v$ into eigenspaces are known since the work of Duval [1]; Lemma 5 states the consequences we need, with a proof. The bound of Proposition 10 was claimed earlier in a more general form [7]; we prove it by our own argument and only for $B = A + I$ (Section 2). The table [2] attributes the flag graph of a generalized quadrangle as a DSRG to [23], and the flag graph of a partial geometry to [24]; we have not read these works, and Proposition 17 proves the special case we need anew, for the sake of the class sizes. The sets of Theorem 2 and the set of Theorem 4 were closed on the platform by other methods before us; this comparison is in Section 2. The other statements are proved here.

## 2. Related work

The definition of a DSRG and the basic necessary conditions for existence are due to Duval [1]. The table [2] collects the sets with $v \le 110$ and the conditions by which some of them are excluded. Our survey of the problem [4] collected the claims of 38 papers of the platform about the sets of the table; we refer to it when we say what is claimed on the platform.

**Twins.** Vertices with equal open neighbourhoods $\Gamma^+(x)$ have already been used by papers of the platform: as claimed in [8], [9], a class of such vertices in any DSRG has at most $v - 2k + \mu - 1$ vertices, and when $t = \mu$ the quotient by the types of rows of $A$ bounds the number of classes; our survey [4] re-proved these claims. We work with closed neighbourhoods $N^+[x]$, that is, with the rows of $A + I$; when $t = \lambda + 1$, it is this matrix that satisfies a quadratic equation without the term $I$.

**The bound on equal rows.** The paper [7] claims the following for any 0/1 matrix $B$ with ones on the diagonal, $K$ ones in every row and column and $B^2 = \alpha J + qB$ with $\alpha + q < K$: rows that are equal to each other and lie in the support of one column occupy at most $K - q$ rows. For $B = A + I$ with $t = \lambda + 1$ this is the bound of Proposition 10. Our proof is our own and relies on $B$ being a DSRG matrix. We have not checked the general form. The paper [7] claims the nonexistence of the line $(96m, 80m, 75m, 65m, 75m)$ for all $m$, and its proof relies, among other things, on this bound [4]. These are the complements of the line $(96m, 16m - 1, 11m - 1, 11m - 2, m)$, which inequality (1) also excludes.

**The sets of Theorem 2.** All three sets are open in the table [2], but on the platform they were closed earlier by other methods; the version of the table of 31 October 2026 already marks the first two as nonexistent (Section 1). The nonexistence of the complements $(40, 30, 27, 21, 27)$ and $(80, 60, 54, 42, 54)$, and with them of the whole line $(40m, 30m, 27m, 21m, 27m)$, is derived in [5] by a search over hyperplanes of rank 6 with Farkas certificates; our survey repeated the search with its own program [4]. The paper [6] formalizes in Lean the rank 6 search for some of the ratios $v/k$, but, according to our survey, not for the ratio $4/3$ of this line [4]. The line $(96m, 80m, 75m, 65m, 75m)$ is closed by [7], as said above. Our proof is not needed to close these three sets, but it is different: two lines of double counting instead of a search, and it is checked in Lean in full.

**The set of Theorem 4.** The set $(28, 6, 3, 2, 1)$ is open in the table [2], but our survey [4] counts it as closed by [8]. That paper claims that there are no graphs of the line $(28m, 21m, 18m, 15m, 18m)$ for any odd $m$, and hence none of their complements $(28m, 7m - 1, 4m - 1, 4m - 2, m)$; for $m = 1$ this is our set. As summarized by the survey [4], the proof of [8] rests on a chain of Farkas certificates, programmatic reductions of the search and DRAT proofs, and the survey did not repeat this chain. We have not checked [8], and Theorem 4 does not rely on it. Our proof is different: a solver search is needed only for a graph with a vertex without a twin, and a graph in which every vertex has twins is excluded by the parity of $K$, proved in Lean. By the enumeration of vertex-transitive DSRGs with $v \le 39$ in [26], this set has no vertex-transitive graphs.

**The sets of Theorem 1.** About the sets $(66, 10, 5, 4, 1)$ and $(91, 12, 6, 5, 1)$, the papers and the discussion of the problem on the platform, as of 1 November 2026, claim only the exclusion of particular classes of graphs (Table 2). None of the papers and none of the messages of the discussion that we read as of that date claims that there are no graphs with these parameters at all. Theorem 1 neither uses nor checks these claims.

**Table 2.** What is claimed on the platform about the sets of Theorem 1 and their complements, as of 1 November 2026. The claims are summarized; we have not checked them.

| Set | Claimed exclusions of classes |
|---|---|
| $(66, 10, 5, 4, 1)$ | no realization by two orbits of an abelian group of order 33 [10], [11], repeated by the survey [4]; for the complement $(66, 55, 50, 45, 50)$, a construction by external products of one kind is excluded [12] — a way of construction, not a graph |
| $(91, 12, 6, 5, 1)$ | no exclusions; the set appears only in a census of parameter sets by the pair of eigenvalues $(5, -1)$ [13] |

We found an argument through twin classes and the rank of $A + I$ neither in the table [2] nor in the survey [4]. Of the wider literature, we looked only through the abstracts of the arXiv papers on DSRGs as of 1 November 2026; there is no such argument in them. We did not meet inequality (1) there as a condition on parameters either; whether [7] derives it in general cannot be told from its summary in the survey [4].

## 3. The matrix B = A + I

**Lemma 5.** Let $t = \lambda + 1$ and $B = A + I$. Then:

1. $B^2 = qB + \mu J$, and for any vertices $x$, $y$ the number $|N^+[x] \cap N^-[y]|$ equals $q + \mu = \lambda + 2$ if $y \in N^+[x]$, and $\mu$ otherwise; moreover, $K^2 = qK + \mu v$;
2. if $q > 0$, then the nontrivial eigenvalues of $A$ are $q - 1$ with multiplicity $f$ and $-1$ with multiplicity $g$, where $qf = v - K$ and $\operatorname{rank} B = 1 + f$;
3. if $\mu = 1$, then $v = (k + 1)(k - \lambda)$ and $(\lambda + 1)f = v - K$; in particular, $f = K$ if and only if $k = 2\lambda + 2$.

*Proof.* 1. $B^2 = A^2 + 2A + I = (t + 1 - \mu)I + (\lambda + 2 - \mu)A + \mu J$, and when $t = \lambda + 1$ this is $q(A + I) + \mu J$. The entry $(x, y)$ of $B^2$ equals $\sum_z B(x, z)B(z, y) = |N^+[x] \cap N^-[y]|$, and the entry of the right-hand side is $q[y \in N^+[x]] + \mu$. Row sums give $K^2 = qK + \mu v$.

2. The nontrivial eigenvalues of a DSRG are the roots of the polynomial $x^2 - (\lambda - \mu)x - (t - \mu)$ [1], and when $t = \lambda + 1$ it equals $(x + 1)(x - (q - 1))$. When $q > 0$, the roots are distinct. From $\mathbf 1^\top A = k\mathbf 1^\top$ it follows that $A$ maps $\mathbf 1^\perp$ into itself, and by item 1, $(A + I)(A - (q - 1)I) = 0$ holds on $\mathbf 1^\perp$. Hence $A$ is diagonalizable on $\mathbf 1^\perp$, and $\mathbf 1^\perp$ is the sum of the eigenspaces for $-1$ and $q - 1$, of dimensions $g$ and $f$. On the vector $\mathbf 1$ the matrix $A + I$ acts as multiplication by $K \ne 0$, and on the second eigenspace as multiplication by $q \ne 0$, so $\operatorname{rank}(A + I) = v - g = 1 + f$. The dimension of $\mathbf 1^\perp$ and the zero trace of $A$ give $f + g = v - 1$ and $k + f(q - 1) - g = 0$, whence $qf = v - 1 - k$.

3. When $\mu = 1$, the equation $K^2 = (\lambda + 1)K + v$ of item 1 gives $v = K(K - \lambda - 1) = (k + 1)(k - \lambda)$, and item 2 gives $(\lambda + 1)f = v - K = K(k - \lambda - 1)$. Hence $f = K$ exactly when $k - \lambda - 1 = \lambda + 1$. $\square$

The hypothesis $q > 0$ is needed by item 2 and by Theorem 3. We do not treat the case $q \le 0$: for all 700 sets of the table [2] with $t = \lambda + 1$ the number $q$ is positive, and $f$ is an integer.

## 4. Row classes for any μ

In this section $t = \lambda + 1$. Fix a vertex $x$ and put $C = C_x$, $a = |C|$, $U = N^+[x] \setminus C$. For a vertex $u$, the number $\gamma_u = |N^+[u] \cap C|$ is how many vertices of the class $u$ sees in its closed neighbourhood.

**Lemma 6.** $C \subseteq N^+[x] \cap N^-[x]$, the set $U$ is not empty, and $a \le \lambda + 1$. Moreover, $C \subseteq N^-[z]$ for every $z \in N^+[x]$.

*Proof.* If $y \in C$, then $y \in N^+[y] = N^+[x]$ and $x \in N^+[x] = N^+[y]$, that is, $y \in N^-[x]$. If $z \in N^+[x]$, then $z \in N^+[y]$ for every $y \in C$, that is, $C \subseteq N^-[z]$. If $U$ were empty, we would get $N^+[x] = C \subseteq N^-[x]$ and $K = |N^+[x] \cap N^-[x]| = \lambda + 2 = t + 1$ by Lemma 5, that is, $k = t$, contrary to $t < k$. For $z \in U$ the set $C \cup \{z\}$ lies in $N^+[x] \cap N^-[z]$, which has exactly $\lambda + 2$ vertices by Lemma 5, so $a + 1 \le \lambda + 2$. $\square$

**Lemma 7.** If $u \notin C$, then $\gamma_u \le \mu$.

*Proof.* The rows $u$ and $x$ of $B$ are different and each contains $K$ ones, so there is $w \in N^+[x] \setminus N^+[u]$. By Lemma 6, $C \subseteq N^-[w]$, hence $N^+[u] \cap C \subseteq N^+[u] \cap N^-[w]$, and the last set has exactly $\mu$ vertices by Lemma 5. $\square$

**Proposition 8.** $\sum_{u \in U} \gamma_u = a(\lambda + 2 - a)$, and therefore $a(\lambda + 2 - a) \le \mu(K - a)$. When $\mu = 1$, this inequality is equivalent to $a(\lambda + 3 - a) \le K$.

*Proof.* Count the pairs $(y, u)$ with $y \in C$, $u \in U$ and $y \in N^+[u]$. For $y \in C$ the set $N^+[x] \cap N^-[y]$ consists of $\lambda + 2$ vertices and contains the whole class by Lemma 6, so the other $\lambda + 2 - a$ vertices lie in $U$; there are $a(\lambda + 2 - a)$ pairs. Counting by $u$, there are $\sum_{u \in U}\gamma_u$ pairs, and by Lemma 7 this is at most $\mu|U| = \mu(K - a)$. $\square$

**Proposition 9.** If $u \notin C$, then $|N^+[u] \setminus N^+[x]| \ge q$. Hence $q(K - a) \le \mu(v - K)$, and when $q > 0$, $a \ge K - \mu f$.

*Proof.* There is $w \in N^+[u] \setminus N^+[x]$. By Lemma 5, $N^+[u] \cap N^-[w]$ has exactly $\lambda + 2$ vertices and $N^+[x] \cap N^-[w]$ exactly $\mu$, so at least $q$ vertices of the first set lie outside $N^+[x]$. Count the pairs $(u, w)$ with $u \in U$ and $w \in N^+[u] \setminus N^+[x]$: there are at least $q|U|$ of them. On the other hand, every $w \notin N^+[x]$ receives exactly $\mu$ arcs from $N^+[x]$, and none of them comes from the class: $w \in N^+[y]$ with $y \in C$ would mean $w \in N^+[x]$. Hence there are at most $\mu(v - K)$ pairs. By Lemma 5, $\mu(v - K) = q\mu f$, and when $q > 0$ we can divide by $q$. $\square$

**Proposition 10.** If $u \in U$ and $\gamma_u \ge 1$, then $a - \gamma_u \le k - \lambda - 1$. Such a vertex $u$ exists, so $a \le k - \lambda - 1 + \mu = K - q$.

*Proof.* Take $c \in C \cap N^+[u]$. The vertex $c$ lies both in $N^+[u]$ and in $N^+[x]$, so by Lemma 5, $|N^+[u] \cap N^-[c]| = |N^+[x] \cap N^-[c]| = \lambda + 2$. Remove from both sets their common part $N^+[u] \cap N^+[x] \cap N^-[c]$:

$$
|(N^+[u] \setminus N^+[x]) \cap N^-[c]| = |(N^+[x] \setminus N^+[u]) \cap N^-[c]|.
$$

The right-hand side contains $C \setminus N^+[u]$, because $C \subseteq N^-[c]$ by Lemma 6, and is therefore at least $a - \gamma_u$. The left-hand side lies in $N^-[c] \setminus N^+[x]$, which has $K - (\lambda + 2) = k - \lambda - 1$ vertices. The required $u$ exists: $N^+[x] \cap N^-[x]$ has exactly $\lambda + 2$ vertices, the class takes at most $\lambda + 1$ of them, and any remaining vertex lies in $U$ and has an arc to $x \in C$. By Lemma 7, $\gamma_u \le \mu$. $\square$

*Proof of Theorem 3.* For any vertex, Propositions 9 and 10 give $K - \mu f \le a \le K - q$, whence $q \le \mu f$. Multiplying by $q > 0$, we get $q^2 \le \mu qf = \mu(v - K)$ by Lemma 5. $\square$

*Proof of Theorem 2.* For $(80, 19, 13, 12, 2)$ we have $K = 20$, $q = 12$, $v - K = 60$ and $f = 5$: Proposition 9 gives $12(20 - a) \le 120$, that is, $a \ge 10$, while Proposition 10 gives $a \le 8$. For $(40, 9, 6, 5, 1)$ we have $q = 6$, $f = 5$, and $a \ge 10 - 5 = 5 > 4 = K - q$. For $(96, 15, 10, 9, 1)$ we have $q = 10$, $f = 8$, and $a \ge 16 - 8 = 8 > 6$. A graph exists if and only if its complement exists, so there are no complements either. $\square$

For $(40, 9, 6, 5, 1)$ and $(96, 15, 10, 9, 1)$, Proposition 8 alone together with the lower bound is also enough: for the first, $a \in \{5, 6\}$ gives $a(8 - a) \in \{15, 12\}$, more than $K = 10$; for the second, $a \in \{8, 9, 10\}$ gives $a(12 - a) \in \{32, 27, 20\}$, more than $16$. This is how these two sets are proved in Lean (Section 8), with the lower bound coming from the rank (Proposition 13).

**Lines of blow-ups.** Blow-up by cliques takes a DSRG with $t = \lambda + 1$ to the graph with matrix $(A + I) \otimes J_m - I$ and parameters $(mv, mK - 1, m(\lambda + 2) - 1, m(\lambda + 2) - 2, m\mu)$. Indeed, $B' = B \otimes J_m$ has unit diagonal, row and column sums $mK$ and $B'^2 = m(B^2 \otimes J_m) = mqB' + m\mu J$; expanding $B'^2 = (A' + I)^2$ with $A' = B' - I$, we get the defining equation of a DSRG with these parameters. At the level of parameters, $K$, $q$, $\mu$ and $v$ are multiplied by $m$, and $f$ does not change. Hence the equation $K^2 = qK + \mu v$ of Lemma 5, the integrality of $f$ and inequality (1) are the same at all points of a line as at its start. If (1) excludes a set, it excludes its whole line; the nonexistence of the far points does not follow by itself from the nonexistence of the start, because a graph at a far point need not be a blow-up. For example, (1) excludes $(96m, 16m - 1, 11m - 1, 11m - 2, m)$ for every $m$: $q = 10m > 8m = \mu f$.

**Corollary 11.** Of the 700 sets of the table [2] with $t = \lambda + 1$, inequality (1) excludes exactly six: the open sets $(40, 9, 6, 5, 1)$, $(80, 19, 13, 12, 2)$ and $(96, 15, 10, 9, 1)$ and the sets $(48, 17, 12, 11, 3)$, $(80, 23, 16, 15, 3)$ and $(96, 35, 25, 24, 6)$ marked as nonexistent. The six sets lie on four lines of blow-ups: $(80, 19, 13, 12, 2)$ is the point $m = 2$ of the line of $(40, 9, 6, 5, 1)$, and $(96, 35, 25, 24, 6)$ is the point $m = 2$ of the line of $(48, 17, 12, 11, 3)$. Lemmas 6, 7 and Propositions 8–10 together exclude the same six sets. Equality in (1) holds for exactly thirteen sets of the table, $(8m, 4m - 1, 3m - 1, 3m - 2, m)$ with $m = 1, \dots, 13$; all of them are constructed.

This is a count over the table, not a proof; the program that repeats it is named in Section 10.

## 5. Classes when μ = 1 and a vertex without a twin

In this section $\mu = 1$ and $t = \lambda + 1$, so $q = \lambda + 1$ and $B^2 = (\lambda + 1)B + J$.

**Lemma 12.** When $\mu = 1$:

1. $N^+[x]$ is a union of column classes, and $N^-[y]$ is a union of row classes;
2. $|C_x \cap D_x| = 1$: two distinct vertices are never twins by row and by column at the same time;
3. $C_x \cup D_x \subseteq N^+[x] \cap N^-[x]$ and $a + d \le \lambda + 3$.

*Proof.* 1. Let $y \in N^+[x]$ and let $y'$ be a column twin of $y$. Then $x \in N^-[y] = N^-[y']$, that is, $y' \in N^+[x]$. The second half is symmetric.

2. Let $z_0 \ne z_1$ be twins both by row and by column. For any $x \in N^-[z_0]$ and $y \in N^+[z_0]$, both vertices $z_0$ and $z_1$ lie in $N^+[x] \cap N^-[y]$. By Lemma 5, an intersection of two or more vertices occurs only when $y \in N^+[x]$. Hence $N^+[z_0] \subseteq N^+[x]$, and since the sizes are equal, $N^+[x] = N^+[z_0]$, that is, every $x \in N^-[z_0]$ lies in $C_{z_0}$. Then $N^-[z_0] \subseteq C_{z_0} \subseteq N^+[z_0]$ by Lemma 6 and $|N^+[z_0] \cap N^-[z_0]| = K$, while by Lemma 5 this is $\lambda + 2 = t + 1 < K$.

3. For $C_x$ this is Lemma 6, and for $D_x$ it is the same lemma for $A^\top$: the transposed matrix defines a DSRG with the same parameters, and its row twins are the column twins of $A$. By Lemma 5, $N^+[x] \cap N^-[x]$ has exactly $\lambda + 2$ vertices, and by item 2, $C_x \cap D_x = \{x\}$, so $a + d - 1 \le \lambda + 2$. $\square$

Everything said in Section 4 about row classes holds for column classes as well: it is enough to pass to $A^\top$. When $\mu = 1$, Propositions 8 and 9 give $a(\lambda + 3 - a) \le K$ and $a \ge K - f$, and the same for $d$. The lower bound can also be obtained from the rank, and this is how it is proved in Lean.

**Proposition 13.** When $\mu = 1$, the rows of $B$ indexed by $\{x\} \cup (N^+[x] \setminus C_x)$ are linearly independent. Therefore $\operatorname{rank} B \ge K + 1 - a$ and $a \ge K - f$.

*Proof.* Let $O = \Gamma^+(x)$; then $C_x \setminus \{x\} \subseteq O$. Every $o \in O \setminus C_x$ has some $w_o \in N^+[o] \setminus N^+[x]$. By Lemma 5, $|N^+[x] \cap N^-[w_o]| = 1$, and this single vertex is $o$. Hence among the rows $\{x\} \cup (O \setminus C_x)$, the column $w_o$ has a one only in the row $o$; in particular, all $w_o$ are distinct. The row $x$ has a one in the column $x$ and zeros in the columns $w_o$. The submatrix of $B$ on these rows and on the columns $\{x\} \cup \{w_o\}$ is triangular with ones on the diagonal after a permutation. It has $1 + k - (a - 1) = K + 1 - a$ rows, and by Lemma 5, $\operatorname{rank} B = 1 + f$. $\square$

**Theorem 14.** Let $\mu = 1$, $t = \lambda + 1$ and $k = 2\lambda + 2$, that is, $f = K$. If a vertex $x$ has no row twin, then $\lambda \le 2$. Hence, when $\lambda \ge 3$, every vertex has both a row twin and a column twin.

*Proof.* Let $x$ have no row twin, $O = \Gamma^+(x)$, $S = N^+[x]$ and $W = V \setminus S$. By Lemma 5, $|W| = v - K = K(k - \lambda - 1) = K(\lambda + 1)$.

*Blocks.* By Lemma 5, every $w \in W$ has exactly one in-neighbour in $S$, and it is not $x$. Hence $W$ splits into the blocks $W_o = \Gamma^+(o) \cap W$, $o \in O$. An empty block $W_o$ would give $N^+[o] \subseteq S$, that is, $N^+[o] = S$ since the sizes are equal, while $x$ has no twins; hence all blocks are nonempty. The entries $(o, w)$ of the equation $B^2 = (\lambda + 1)B + J$ give two more counts:

- (i) a vertex $w \in W_o$ receives exactly $\lambda$ arcs from $W_o$: $N^+[o] \cap N^-[w]$ has exactly $\lambda + 2$ vertices, of which only $o$ lies in $S$, and the others are $w$ and its in-neighbours in $W_o$;
- (ii) a vertex $w \in W_{o'}$ with $o' \ne o$ receives exactly $1 - [o \to o']$ arcs from $W_o$: $w \notin N^+[o]$, so $N^+[o] \cap N^-[w]$ has one vertex, and the only vertex of $S$ in $N^-[w]$ is $o'$.

*Rank.* On the columns $W$, the row $o$ of $B$ is the indicator $\mathbf 1_{W_o}$, and the row $x$ is zero. The blocks are nonempty and disjoint, so the rows $O$ are already independent on the columns $W$; the row $x$ is zero on these columns but is not zero itself, and therefore does not lie in the span of the rows $O$. Hence the rows $S$ are independent, and their span $R_S$ has dimension $K = k + 1$. The rank of $B$ is $1 + f = k + 2$, so there is a vector $z$ such that $B[w] = s_w + c_w z$ with $s_w \in R_S$ for every vertex $w$, where $c_w = 0$ for $w \in S$. The row $x$ of the equation $B^2 = (\lambda + 1)B + J$ gives $\mathbf 1^\top = \sum_{o \in O} B[o] - \lambda B[x] \in R_S$. The row $u$ of the same equation modulo $R_S$ gives $\sum_y B(u, y)c_y = (\lambda + 1)c_u$, that is, $Bc = (\lambda + 1)c$. The vector $c$ is not zero, otherwise the rank would be $k + 1$, and the row $o$ gives $\sum_{w \in W_o} c_w = 0$.

*Structure of the rows.* Let $r_w = N^+[w] \cap W$; $w \in r_w$. On the columns $W$ the vector $s_w$ is constant on every block, so $\mathbf 1_{r_w} - c_w z$ is also constant on every block. If $z$ is constant on all blocks, then every $r_w$ is a union of blocks, every block is a reciprocal clique, by (i) $|W_o| = \lambda + 1$, and $|W| = k(\lambda + 1)$, contrary to $|W| = (k + 1)(\lambda + 1)$. The blocks on which $z$ is not constant are called special. Normalize $z$ so that $c_{w_0} = 1$ for some vertex $w_0$, and put $T_o = r_{w_0} \cap W_o$ for a special $o$; then $\emptyset \ne T_o \ne W_o$. On a special block, $\mathbf 1_{r_w \cap W_o}$ differs from $c_w\mathbf 1_{T_o}$ by a constant. The spread, that is, the largest value minus the smallest, of the left vector is 0 or 1, and that of the right vector is $|c_w|$. Hence $c_w \in \{0, \pm 1\}$; when $c_w = 1$ we get $r_w \cap W_o = T_o$, when $c_w = -1$ we get $W_o \setminus T_o$, and when $c_w = 0$ the set $r_w \cap W_o$ is empty or equal to $W_o$. On the non-special blocks, $r_w \cap W_o$ is also empty or equal to $W_o$. Let $P$, $N$ and $Z$ be the vertices of $W$ with $c_w = 1$, $-1$ and $0$, and $p_o = |P \cap W_o|$. The sums of $c$ over the blocks are zero, so $|N \cap W_o| = p_o$.

*Sizes of the blocks.* A non-special block is a reciprocal clique, and by (i) $|W_o| = \lambda + 1$. In a special block, a vertex $y \in T_o$ lies in $P$ or in $Z$: a vertex $w \in N \cap W_o$ lies in its own $r_w \cap W_o = W_o \setminus T_o$, that is, outside $T_o$. The arcs into $y$ come exactly from the other vertices of $P \cap W_o$ and of $Z \cap W_o$; a vertex of $Z$ has arcs to its whole block, because $w \in r_w$. By (i), $p_o + |Z \cap W_o| - 1 = \lambda$, that is, $|W_o| = \lambda + 1 + p_o$. Summing over the blocks gives $|W| = k(\lambda + 1) + \sum p_o$, whence the sum of $p_o$ over the special blocks is $\lambda + 1$, and $P$ and $N$ are nonempty.

*Two or more special blocks.* Two vertices of $P$ in one block $W_{o_2}$ both have arcs to the whole $T_{o_1}$ of another special block, while by (ii) a vertex of $T_{o_1}$ receives at most one arc from $W_{o_2}$. Hence all $p_o \le 1$, and at least $\lambda + 1$ special blocks have size $\lambda + 2$. For $w \in P$ the set $r_w$ contains all $T_o$, for $w' \in N$ the set $r_{w'}$ contains all $W_o \setminus T_o$, and both sets have at most $K$ elements. Hence $(\lambda + 1)(\lambda + 2) \le 2K = 2(2\lambda + 3)$, that is, $\lambda^2 - \lambda - 4 \le 0$ and $\lambda \le 2$.

*One special block $W_{o_1}$.* Then $p_{o_1} = \lambda + 1$ and $|W_{o_1}| = 2\lambda + 2 = k$, so $\Gamma^+(o_1) = W_{o_1}$ and $Z \cap W_{o_1}$ is empty. Inside the block, the vertices of $P \cap W_{o_1}$ have arcs exactly to $T_{o_1}$, the vertices of $N \cap W_{o_1}$ to the complement $W_{o_1} \setminus T_{o_1}$, and every vertex lies in its own part. Hence $\Gamma^+(o_1)$ consists of two reciprocal cliques of $\lambda + 1$ vertices each with no arcs between them. The vertex $o_1$ has no row twin: a twin would lie in $\Gamma^+(o_1)$ and have arcs to all its other vertices. When $\lambda \ge 3$, apply what has been proved to $o_1$ instead of $x$: two special blocks are impossible, so $o_1$ also has a single special block. Let it be given by a vertex $o_1' \in \Gamma^+(o_1)$; by the case just treated, $\Gamma^+(o_1')$ coincides with this block, that is, all out-neighbours of $o_1'$ lie outside $N^+[o_1]$. But $o_1'$ lies in a clique of $\lambda + 1 \ge 2$ vertices inside $\Gamma^+(o_1)$, a contradiction.

Thus, when $\lambda \ge 3$, every vertex has a row twin, and, by $A^\top$, a column twin as well. $\square$

**Theorem 15.** When $\mu = 1$, $t = \lambda + 1$, $k = 2\lambda + 2$ and $\lambda \ge 4$, there is no directed strongly regular graph.

*Proof.* By Theorem 14, $a, d \ge 2$ for every vertex. When $3 \le a \le \lambda$, we have $a(\lambda + 3 - a) \ge 3\lambda > 2\lambda + 3 = K$, so by Proposition 8 and Lemma 6, $a, d \in \{2, \lambda + 1\}$, and by item 3 of Lemma 12 they are not both equal to $\lambda + 1$.

Let $a = \lambda + 1$ for the class $C_x$. Then for every $y \in C_x$ the column class is a pair $D_y = \{y, y'\}$, where $y' \in N^+[x]$ by item 1 of Lemma 12 and $y' \notin C_x$ by item 2. The vertices $y'$ for different $y$ are different: if $y_1' = y_2'$, then $D_{y_1} = D_{y_2} \ni y_2$, and $y_2$ would be a twin of $y_1$ both by row and by column. The set $N^+[x] \setminus C_x$ has $K - a = \lambda + 2$ vertices in total, and one vertex $u^*$ falls into none of the classes $D_y$. By item 1 of Lemma 12, $D_{u^*} \subseteq N^+[x]$, and it is disjoint from the classes $D_y$, so $D_{u^*} = \{u^*\}$, contrary to $d \ge 2$. Hence all row classes, and by $A^\top$ all column classes, are pairs. By item 1 of Lemma 12, the set $N^+[x]$ is a union of disjoint column pairs, and the number of its vertices is even. But it has $2\lambda + 3$ vertices, a contradiction. $\square$

*Proof of Theorem 1.* For $(66, 10, 5, 4, 1)$ we have $k = 10 = 2\lambda + 2$ with $\lambda = 4$, and for $(91, 12, 6, 5, 1)$ we have $k = 12 = 2\lambda + 2$ with $\lambda = 5$. By Theorem 15 there are no graphs, and hence no complements. $\square$

For these two sets inequality (1) gives nothing: $q = 5 < \mu f = 11$ and $q = 6 < 13$. Without Theorem 14, the propositions of Section 4 leave the class sizes $a \in \{1, 2, 5\}$ for $(66, 10, 5, 4, 1)$ and $a \in \{1, 2, 6\}$ for $(91, 12, 6, 5, 1)$; Theorem 14 removes $a = 1$, and Theorem 15 the rest.

## 6. The set (28, 6, 3, 2, 1)

In this section $\mu = 1$ and $t = \lambda + 1$. A vertex without a row twin ($a = 1$) is called *row-free*, and one without a column twin ($d = 1$) *column-free*. For the set $(28, 6, 3, 2, 1)$ we have $k = 6 = 2\lambda + 2$ with $\lambda = 2$, $K = 7$, $f = 7$ and $B^2 = 3B + J$. Theorem 14 does not apply to it: for a row-free vertex with three special blocks, the inequality of its proof holds, $(\lambda + 1)(\lambda + 2) = 12 \le 14 = 2K$. Sections 4 and 5 leave the class sizes $a \in \{1, 2, 3\}$. The proof of Theorem 4 splits the graphs into three cases: there is a row-free vertex; there is a column-free vertex; there are no free vertices. The third case is closed by Lemma 16, the first by the solver, and the second reduces to the first.

**Lemma 16.** Let $\mu = 1$, $t = \lambda + 1$ and $U = N^+[x] \setminus C_x$.

1. If $a = \lambda + 1$, then there are no arcs inside $U$, the column twins of the vertices of $U$ lie in $C_x$, and at least $K - 2(\lambda + 1)$ vertices of $U$ are column-free.
2. If there are no free vertices and $K > 2(\lambda + 1)$, then $a \le \lambda$ and $d \le \lambda$ for every vertex. When $\lambda = 2$, all row and column classes are pairs, and $K$ is even.

*Proof.* 1. Every $c \in C_x$ has arcs to all vertices of $N^+[x] \setminus \{c\}$, so $C_x \subseteq N^-[u]$ for every $u \in U$. By Lemma 5, $N^+[x] \cap N^-[u]$ has exactly $\lambda + 2$ vertices; these are the $\lambda + 1$ vertices of $C_x$ and $u$ itself, so there are no arcs from $U$ to $u$. By item 1 of Lemma 12, $D_u \subseteq N^+[x]$. If a column twin $u' \ne u$ lay in $U$, then $u \in N^-[u] = N^-[u']$ would give an arc $u \to u'$ inside $U$; hence $D_u \setminus \{u\} \subseteq C_x$. Two vertices of $U$ cannot both be column twins of one $c \in C_x$: otherwise they would be column twins of each other, which has just been excluded. Hence at most $|C_x| = \lambda + 1$ vertices of $U$ have $d \ge 2$, and at least $|U| - (\lambda + 1) = K - 2(\lambda + 1)$ are column-free.

2. By Lemma 6, $a \le \lambda + 1$. If $a = \lambda + 1$ held for some vertex $x$, then by item 1, $N^+[x]$ would contain $K - 2(\lambda + 1) > 0$ column-free vertices, contrary to the hypothesis. Hence $a \le \lambda$, and by $A^\top$ also $d \le \lambda$. When $\lambda = 2$, together with $a, d \ge 2$ this gives $a = d = 2$. By item 1 of Lemma 12, $N^+[x]$ is a union of column classes, all of them pairs, and $K = |N^+[x]|$ is even. $\square$

*Proof of Theorem 4.* Let $A$ be the matrix of a DSRG $(28, 6, 3, 2, 1)$.

*There is a row-free vertex $x$.* Renumber the vertices: $x$ gets the number 0, its three reciprocal neighbours get the numbers 1, 2, 3, its other three out-neighbours 4, 5, 6, the three vertices that have arcs to $x$ but receive no arc from $x$ get the numbers 7, 8, 9, and the other eighteen vertices the numbers 10–27. There are exactly three reciprocal neighbours because $A^2(x, x) = t = 3$, and $k - t = 3$ in-neighbours without a reverse arc. Such a graph satisfies a SAT formula $\Phi$. Its variables $a(i, j)$ with $i \ne j$ are the arcs of the graph, and its clauses require the following:

- every vertex has exactly 6 out-neighbours and 6 in-neighbours;
- there are exactly 3 paths $i \to z \to j$ when $i = j$, exactly 2 when $i \to j$ is an arc, and exactly 1 when it is not;
- the arcs of the vertex 0 are placed as the labelling prescribes;
- the row of $B$ of the vertex 0 differs from the row of every other vertex.

A path $i \to z \to j$ is an auxiliary variable equivalent to $a(i, z) \wedge a(z, j)$, and the conditions "exactly $n$ ones" are encoded by the sequential counter [19] of the PySAT library [18]. The formula has 131,518 variables and 300,889 clauses. The CaDiCaL solver [17], version 1.9.5 from PySAT, proves its unsatisfiability in less than a second and writes a DRAT proof. Two checkers check it one after the other. drat-trim [20] checks the DRAT proof against the formula, prints `s VERIFIED` and extracts from it an LRAT proof [21] of 525 steps. Our checker checks this LRAT proof again against the same formula by unit propagation and accepts no RAT steps. Hence there is no row-free vertex.

*There is a column-free vertex.* The matrix $A^\top$ is also a DSRG $(28, 6, 3, 2, 1)$, and the column classes of $A$ are the row classes of $A^\top$. A column-free vertex in $A$ is row-free in $A^\top$, and this is excluded by the previous case.

*There are no free vertices.* Here $K = 7 > 6 = 2(\lambda + 1)$, and by item 2 of Lemma 16 the number $K$ is even, a contradiction.

The cases exhaust all graphs, so there is no DSRG $(28, 6, 3, 2, 1)$, and hence no complement either. $\square$

**What the three cases rest on.** The second and third cases together are proved in Lean (Section 8): the theorem `L108_free_row` derives from `IsDSRG 28 A 6 3 2 1` a DSRG matrix with the same parameters (in the proof, $A$ itself or $A^\top$) and a vertex without a row twin. The first case rests on the certificate of unsatisfiability: the checkers trust neither the solver nor the program that builds the formula. The remaining question is whether the formula $\Phi$ correctly encodes a graph with a free vertex. There is no formal proof of this correspondence; it is checked in three ways (Section 10, Checks 5 and 6). A formula of the same construction is satisfiable on the graph $(54, 8, 3, 2, 1)$ with a free vertex and unsatisfiable on the graph $(18, 5, 3, 2, 1)$, where the class of the vertex has three vertices; without the condition on the row of the vertex 0, both are satisfiable. A second program of a different design builds its own formulas for the same case, and they are also unsatisfiable with accepted certificates. Finally, a reviewer who did not write the formula read its construction and derived every step of the proof anew.

The solver needs only a second because the subgraph on $N^+[x]$ of a free vertex is almost determined. The entries of the equation $B^2 = 3B + J$ on the rows of $N^+[x]$ leave, under our labelling, 55 subgraphs on $N^+[x]$, and for a free vertex only one of them fits: $\{0, 1, 2, 3\}$ is a reciprocal clique, $\{4, 5, 6\}$ is a reciprocal triangle, and there are no arcs between $\{1, 2, 3\}$ and $\{4, 5, 6\}$ (Section 10, Check 6). We have no argument without a solver for this case.

## 7. Sharpness on flag graphs

A generalized quadrangle of order $(\sigma, \tau)$ is a system of points and lines in which every line has $\sigma + 1$ points, every point lies on $\tau + 1$ lines, two lines meet in at most one point, and for a point $p$ off a line $L$ exactly one line through $p$ meets $L$ [14]. A flag is a pair $(p, L)$ with $p \in L$. The flag graph has an arc $(p, L) \to (p', L')$ when $(p, L) \ne (p', L')$ and $p \in L'$. This is a known construction of a DSRG: the table [2] attributes it for generalized quadrangles to [23], and for partial geometries to [24]. There the arcs point the other way, and the transposed graph is a DSRG with the same parameters. We have not read the texts of [23] and [24]; we give the proof below for the sake of the class sizes $a$ and $d$.

**Proposition 17.** The flag graph of a generalized quadrangle of order $(\sigma, \tau)$ is a DSRG with parameters

$$
\bigl((\sigma + 1)(\tau + 1)(\sigma\tau + 1),\ (\sigma + 1)(\tau + 1) - 1,\ \sigma + \tau,\ \sigma + \tau - 1,\ 1\bigr),
$$

in which $a = \tau + 1$ and $d = \sigma + 1$ for every vertex. On it, $a + d = \lambda + 3$ and $a(\lambda + 3 - a) = K$, that is, the bound of item 3 of Lemma 12 and the inequality of Proposition 8 become equalities. The condition $k = 2\lambda + 2$ holds only when $\sigma = \tau = 2$.

*Proof.* The closed out-neighbourhood of a flag $(p, L)$ consists of all flags $(p', M)$ with $p \in M$; it depends only on the point $p$ and consists of $(\tau + 1)(\sigma + 1)$ flags. The closed in-neighbourhood of a flag $(p', L')$ consists of all flags $(p'', M')$ with $p'' \in L'$; it depends only on the line $L'$. Hence $|N^+[(p, L)] \cap N^-[(p', L')]| = \sum_{M \ni p} |M \cap L'|$. When $p \in L'$, the line $L'$ contributes $\sigma + 1$, and each of the other $\tau$ lines through $p$ contributes the single point $p$, giving $\sigma + \tau + 1$ in total. When $p \notin L'$, by the quadrangle axiom exactly one line through $p$ meets $L'$, and the sum equals 1. Hence $B^2 = (\sigma + \tau)B + J$, and the equation $A^2 = (\sigma + \tau)I + (\sigma + \tau - 1)A + (J - I - A)$ is checked by substituting $B = A + I$. There are $(\sigma + 1)(\sigma\tau + 1)$ points, and each lies in $\tau + 1$ flags. The rows of two flags coincide exactly when the flags have the same point: when $p \ne p'$, there is a line through $p$ not containing $p'$, and its flags lie only in the first row. Likewise, the columns coincide exactly when the flags have the same line, whence $a = \tau + 1$ and $d = \sigma + 1$. Finally, $\lambda + 3 = \sigma + \tau + 2 = a + d$ and $a(\lambda + 3 - a) = (\tau + 1)(\sigma + 1) = K$. The equation $(\sigma + 1)(\tau + 1) - 1 = 2(\sigma + \tau - 1) + 2$ reduces to $(\sigma - 1)(\tau - 1) = 1$. $\square$

**Table 3.** Flag graphs on which the bounds were checked. The grid $(\sigma + 1) \times (\sigma + 1)$ is a quadrangle of order $(\sigma, 1)$, and its dual is of order $(1, \sigma)$; in the dual, rows and columns exchange roles. All sets of the table are marked in [2] as constructed.

| Quadrangle | Set | $a$, $d$ | $\operatorname{rank} B = 1 + f$ | $K - f$ |
|---|---|---|---:|---:|
| $(\sigma, 1)$, $\sigma = 1, \dots, 6$ | $(8, 3, 2, 1, 1)$, $(18, 5, 3, 2, 1)$, $(32, 7, 4, 3, 1)$, $(50, 9, 5, 4, 1)$, $(72, 11, 6, 5, 1)$, $(98, 13, 7, 6, 1)$ | $2$, $\sigma + 1$ | $2\sigma + 1$ | 2 |
| $(1, \sigma)$, $\sigma = 1, \dots, 6$ | the same | $\sigma + 1$, $2$ | $2\sigma + 1$ | 2 |
| $W(2)$, order $(2, 2)$ | $(45, 8, 4, 3, 1)$ | $3$, $3$ | 10 | 0 |

On the grids and their duals, also $\min(a, d) = 2 = K - f$, so the bound of Proposition 13 is attained as well. The bound of Proposition 10 with $\mu \ge 2$ is attained, for example, on the graph $(16, 7, 5, 4, 2)$ of our catalogue: a class of $4 = k - \lambda - 1 + \mu$ vertices, and there also $a = K - \mu f = 4$, so the bound of Proposition 9 is sharp as well.

**The thresholds of Theorems 14 and 15.** $W(2)$ gives a DSRG $(45, 8, 4, 3, 1)$ with $k = 2\lambda + 2$ and $\lambda = 3$. In it, the row and column classes of every vertex have three vertices each, that is, twins exist, as Theorem 14 requires for $\lambda = 3$, but the graph exists; hence the threshold $\lambda \ge 4$ of Theorem 15 cannot be lowered. Vertices without a row twin with $k = 2\lambda + 2$ occur in the graphs $(6, 2, 1, 0, 1)$ with $\lambda = 0$ and $(15, 4, 2, 1, 1)$ with $\lambda = 1$ (Section 10, Check 1), so for $\lambda \le 1$ the statement "every vertex has a row twin" is false. When $\lambda = 2$, the family consists of the single set $v = (2\lambda + 3)(\lambda + 2) = 28$; there is no graph $(28, 6, 3, 2, 1)$ by Theorem 4, but there a vertex without a twin is excluded by the solver, not by the argument of Theorem 14 (Section 6). Hence, when $\lambda = 2$, the statement "every vertex has a row twin" holds vacuously: there are no graphs.

## 8. Formalization in Lean

The statements of Sections 3–5, Lemma 16, the passage to the complement and two of the three cases of Theorem 4 are proved in Lean 4 [15] with the Mathlib library [16]: Lean version v4.35.0, Mathlib at the tag v4.35.0. A graph is given by the predicate `IsDSRG n A k t lam mu`. It requires an integer matrix $A$ of order $n$ to consist of zeros and ones, to have zero diagonal and row and column sums $k$, and to satisfy $A^2 = tI + \lambda A + \mu(J - I - A)$ entrywise; it has no other conditions. Closed neighbourhoods and classes are defined as finite sets of indices, the rank of $B$ is taken over $\mathbb R$, and $f$ is the dimension of an eigenspace of $A$ over $\mathbb R$. Every theorem below is proved for any matrix that satisfies `IsDSRG` with the given parameters. The theorems on the five sets and their complements state `¬ IsDSRG v A k t lam mu` for any matrix $A$ and have no hypotheses.

**Table 4.** Statements of the paper and Lean theorems. The module on $\mu = 1$ contains 85 theorems, the module on any $\mu$ 20, the module on the frame of a vertex 16, and the module on the complement and the transpose 13.

| Statement | Lean theorems | Difference in the statement |
|---|---|---|
| Lemma 5, item 1 | `L94_inter`, `L94_card_out`, `L94_card_in`; for $\mu = 1$, `L93_inter` | the equation $K^2 = qK + \mu v$ is not stated as a separate theorem: when $t = \lambda + 1$ it is Duval's condition `k_sq`, and when $\mu = 1$ it is `L93_order` |
| Lemma 5, item 2 | `L94_spec`, `L93_spec` via `rank_sub_root` and `spectrum_counts` | hypotheses $\mu < \lambda + 2$ and $\mu \ne 0$; the second holds for every DSRG with $t < k$ |
| Lemma 5, item 3 | `L93_order`, `L93_spec` | — |
| Lemma 6 | `L94_sub`, `L94_le` | — |
| Lemma 7 | `L94_gamma` | — |
| Proposition 8 | `L94_class`; for $\mu = 1$, `L93_class` | the inequality only; the identity $\sum \gamma_u = a(\lambda + 2 - a)$ is not stated as a theorem |
| Proposition 9 | `L94_far`, `L94_lower`, `L94_admissible` | — |
| Proposition 10 | `L94_upper` | only the conclusion $a \le k - \lambda - 1 + \mu$; the inequality $a - \gamma_u \le k - \lambda - 1$ for an arbitrary $u$ is not stated as a theorem |
| Theorem 3 | `L94_cond` | hypotheses $t < k$ and $\mu < \lambda + 2$ |
| Theorem 2, $(80, 19, 13, 12, 2)$ | `L94_no_80_19_13_12_2`; complement: `compl_no_80_60_54_42_54` | — |
| Theorem 2, $(40, 9, 6, 5, 1)$ and $(96, 15, 10, 9, 1)$ | `L93_admissible`, `L93_no_40_9_6_5_1`, `L93_no_96_15_10_9_1`; complements: `compl_no_40_30_27_21_27`, `compl_no_96_80_75_65_75` | the lower bound comes from the rank (Proposition 13) |
| Lemma 12 | `L93_col_union`, `L93_double`, `L93_ad` | item 1 is stated for rows; for columns it follows by passing to $A^\top$ (`isDSRG_transpose`) |
| Proposition 13 | `L93_rank_of_supp`, `L93_rank_ge`, `L93_rank` | — |
| Theorem 14 | `L93_free_twin`, `L93_free_twin_col` | hypothesis $k = 2\lambda + 2$ instead of $f = K$, without the hypotheses $0 < t$ and $k < v - 1$; a different route of proof, see below |
| Theorem 15 | `L93_family`, `L93_no_family` | — |
| Theorem 1 | `L93_no_66_10_5_4_1`, `L93_no_91_12_6_5_1`; complements: `compl_no_66_55_50_45_50`, `compl_no_91_78_72_66_72` | — |
| Lemma 16, item 1 | `L107_indep`, `L107_col_in_row`, `L107_colfree`; by $A^\top$, `L107_rowfree` | "every vertex of $C_x$ is a twin of at most one vertex of $U$" is a step of the proof, not a theorem |
| Lemma 16, item 2 | `L107_no_full`, `L107_no_full_col`, `L107_two_le`, `L107_even`, `L107_pairs` | hypothesis $t < k$; when $\lambda = 2$, the hypothesis $K > 6$ |
| Theorem 4, second and third cases | `L107_28`, `L108_free_row` | the conclusion is a DSRG matrix $(28, 6, 3, 2, 1)$ with a vertex without a row twin (in the proof, $A$ itself or $A^\top$); the first case is not stated in Lean |
| The complement is a DSRG (Section 1) | `isDSRG_compl`, `not_isDSRG_compl` | the matrix of the complement is $1 - [i = j] - A(i, j)$; the direction "no graph, hence no complement" is stated |

**How Lean proves Theorem 14.** The formal proof goes without the vector $c$. The notation is that of the proof of Theorem 14: $W = V \setminus N^+[x]$, blocks $W_o$. For a row $w \in W$ and two vertices $y, y'$ of one block, put $\delta_w(y, y') = [y \in N^+[w]] - [y' \in N^+[w]]$, which tells whether the row $w$ distinguishes these vertices. By Lemma 5, the rank of $B$ equals $k + 2$ (`L93_rank_free`). Hence for any rows $w, w' \in W$ and any pairs $(y_1, y_1')$ and $(y_2, y_2')$, each inside its own block, the determinant $\delta_w(y_1, y_1')\delta_{w'}(y_2, y_2') - \delta_w(y_2, y_2')\delta_{w'}(y_1, y_1')$ is zero (`L93_det`): otherwise the rows $N^+[x] \cup \{w, w'\}$ would be independent and the rank would be at least $k + 3$. A row $w_0 \in W$ that distinguishes at least one pair of vertices of one block exists (otherwise all blocks are cliques of size $\lambda + 1$), and every row $w \in W$ gives $\delta_w = c_w \delta_{w_0}$ on every pair inside a block, with a factor $c_w \in \{0, \pm 1\}$. These are the same numbers $c_w$ as in the proof of Theorem 14, but without the eigenvector $Bc = (\lambda + 1)c$. Lean derives the size of a special block $|W_o| = \lambda + 1 + p_o$ from the count (i) at a vertex of $T_o$ and at a vertex outside $T_o$, not from the zero sum of $c$. The case of two special blocks reduces to the inequality $(\lambda + 1)(\lambda + 2) \le 2K$, and the case of one block to the fact that every vertex of $\Gamma^+(o_1)$ has an arc to another vertex of $\Gamma^+(o_1)$ and no arc to a third one; Lean does not construct the two cliques, as this is enough for both steps.

**What is not in Lean.** The first case of Theorem 4: a row-free vertex is excluded by the certificate of unsatisfiability (Section 6), and without this case Lean does not have the complement $(28, 21, 18, 15, 18)$ either. Proposition 17 on flag graphs and the remarks on sharpness. The count of Corollary 11 over the table and the remark on lines of blow-ups. The two intermediate equalities of Propositions 8 and 10 named in Table 4.

**Axioms.** For each of the 134 theorems of the four modules, a program prints the axioms on which the theorem depends with the Lean command `#print axioms` and exits with an error on any axiom outside the standard set. One hundred and twenty-seven theorems depend on exactly propext, Classical.choice and Quot.sound, two on propext only, and five more on propext and Quot.sound. There is no `sorry` and no axiom of our own in the proofs.

## 9. Limits of the result

**The family μ = 1.** Of the seven open sets of the table [2] with $\mu = 1$ and $t = \lambda + 1$, the paper closes five. For one more, $(96, 11, 4, 3, 1)$, a graph was constructed in [25] and on the platform [4], and its matrix from our catalogue passes the exact check (Section 10, Check 1). What remains is $(70, 9, 3, 2, 1)$. It has $f = 20$, $K - f = -10$, the sizes $a \in \{1, 2, 3\}$ are allowed, and Sections 4 and 5 give nothing. The structure of Theorem 14 rests on $f = K$: when $f = K + \delta$, the rows outside $N^+[x]$ span $\delta + 1$ dimensions modulo $R_S$, and the argument through blocks stops working.

**The set $(70, 9, 3, 2, 1)$.** The division into three cases of Theorem 4 carries over to it, but closes less. Lemma 16 applies, $K = 10 > 6$, and in a graph without free vertices all classes are pairs; but $K = 10$ is even, and there is no contradiction. The case of a row-free vertex $x$ is not closed either. The subgraph on $N^+[x]$ is given by the in-neighbours of every $o \in \Gamma^+(x)$ in $\Gamma^+(x)$, and there are exactly $\lambda = 2$ of them: this is the entry $(x, o)$ of the equation $B^2 = 3B + J$. There are $\binom{8}{2}^9 = 28^9 \approx 1.06 \cdot 10^{13}$ variants. The other entries of the same equation on the rows of $N^+[x]$ and the sizes of the blocks $W_o$ (a block is empty only for a row twin of $x$, and a nonempty one contains at least $\lambda + 1$ vertices) leave about $1.65 \cdot 10^7$ subgraphs. This is a Knuth estimate [22] from 2000 random descents, not an exact count; a second seed gave $1.76 \cdot 10^7$. On the two subgraphs of a free vertex that we tried, the solver gave no answer within 200 s, and a search over all subgraphs is beyond our means. We continue to study the case of classes that are pairs through the quotient by row classes; this work is not part of the paper.

**The family μ ≥ 2.** The table [2] contains 131 open sets with $t = \lambda + 1$, $\mu \ge 2$ and integer $f$ that inequality (1) does not exclude. The propositions of Section 4 narrow the allowed class sizes for only three of them: $(49, 13, 8, 7, 2)$, $(81, 17, 10, 9, 2)$ and $(98, 27, 17, 16, 4)$, which the survey [4] counts as closed, to $\{4, 7\}$, $\{4, 9\}$ and $\{8, 14\}$. For the other 128, every size from 1 to $\lambda + 1$ is allowed.

**The sets $(102, 16, 6, 5, 2)$ and $(98, 20, 9, 8, 3)$.** These two open sets were the target of the work from which Proposition 10 grew, and the paper does not narrow them. The reason is visible from the numbers of Table 5. The lower bound of Proposition 9 is negative, because $\mu f$ is 6.8 and 4.7 times larger than $q$: when $\mu \ge 2$, every vertex outside $N^+[x]$ receives $\mu$ arcs from $N^+[x]$, and the count of arcs allows classes of size 1. The upper bounds $\lambda + 1$ and $K - q$ do not interfere with each other, and the inequality of Proposition 8 with $a = \lambda + 1$ holds with a large margin: $6 \le 22$ and $9 \le 36$.

**Table 5.** The numbers of Sections 4 and 5 for two open sets with $\mu \ge 2$.

| Set | $q$ | $f$ | $\mu f$ | $K - \mu f$ | $\lambda + 1$ | $K - q$ | $\operatorname{rank} B$ | $K$ |
|---|---:|---:|---:|---:|---:|---:|---:|---:|
| $(102, 16, 6, 5, 2)$ | 5 | 17 | 34 | −17 | 6 | 12 | 18 | 17 |
| $(98, 20, 9, 8, 3)$ | 7 | 11 | 33 | −12 | 9 | 14 | 12 | 21 |

For $(102, 16, 6, 5, 2)$, as for the sets of Theorem 1, $f = K$ and $\operatorname{rank} B = k + 2$. But when $\mu = 2$, a vertex outside $N^+[x]$ has two in-neighbours in $N^+[x]$, the sets $\Gamma^+(o) \setminus N^+[x]$ intersect, and there is no partition into blocks on which Theorem 14 rests. Besides, the set is the member $n = 6$ of the line $(n(3n - 1), 3n - 2, n, n - 1, 2)$, all of whose members have $f = K$, and the members $n = 2, 3, 4, 5$ are constructed. A nonexistence proof for it must rely on a property that its four constructed neighbours lack. For $(98, 20, 9, 8, 3)$ the rank of $B$ is small, 12 against 21 rows of $N^+[x]$, but the argument of Proposition 13 does not work when $\mu \ge 2$: the column $w_o$ has not one but $\mu$ ones among the rows of $N^+[x]$.

Six more open sets with $t = \lambda + 1$ and $\mu \ge 2$, which we examined together with these two, are not narrowed either: $(65, 14, 4, 3, 3)$, $(77, 13, 4, 3, 2)$, $(75, 19, 8, 7, 4)$, $(81, 32, 16, 15, 11)$, $(104, 25, 10, 9, 5)$ and $(108, 47, 22, 21, 20)$. For all eight, $\mu f$ exceeds $q$ by a factor of 4.7–133, and every class size is allowed.

## 10. Checks

Checks 1–4 and 7 are not part of the proofs. They show that the statements say what we say about them, and that programs repeating the derivations agree with them. Check 5 describes the certificate of the first case of Theorem 4, which is part of the proof, and the control of the formula $\Phi$; Check 6 describes a second program for the same case. Every check has a variant with a deliberate spoiling, and this variant must exit with code 1.

1. **Sections 4 and 5 for μ = 1 on graphs.** Thirty matrices with $\mu = 1$ and $t = \lambda + 1$: 17 from our catalogue and 13 flag graphs of Table 3, built and checked by the program; 13 parameter sets, 908 vertices. At every vertex, $\operatorname{rank} B = 1 + f$, Lemma 12, Lemma 7, the inequality of Proposition 8 and the bound of Proposition 13 are checked exactly. The inequality of Proposition 8 becomes an equality 1254 times over row and column classes, $a + d = \lambda + 3$ 678 times, and the bound of Proposition 13 is attained 606 times. The structure of Theorem 14 is checked at the 53 vertices without a row twin of the graphs $(6, 2, 1, 0, 1)$ and $(15, 4, 2, 1, 1)$: the vector $c$ with values $0, \pm 1$, the blocks $T_o$, the sizes $\lambda + 1 + p_o$ and $\sum p_o = \lambda + 1$. There is one special block at 36 vertices, two at 15, and three at 2. $W(2)$ has no vertices without a twin. Spoilings: $a(\lambda + 3 - a) \le k$ fails 1260 times, at the 1254 sharp vertices and on six constructed sets; $a \ge K + 1 - f$ fails 607 times; Theorem 15 with the threshold $\lambda \ge 3$ fails 2 times, on the graph $W(2)$ and its parameter set; Theorem 14 without the condition on $\lambda$ fails at 53 vertices.
2. **Section 4 for any μ on graphs.** 532 matrices with $t = \lambda + 1$: 281 from the catalogue together with their complements and 251 blow-ups by cliques $(A + I) \otimes J_m - I$ with $m = 2, 3$ and $mv \le 60$, each checked as a DSRG; 188 parameter sets, 41,982 vertices by $A$ and $A^\top$. At every vertex, Lemma 5, Lemmas 6 and 7 and Propositions 8, 9 and 10 are checked exactly. Equalities: $a = \lambda + 1$ 782 times, $\gamma_u = \mu$ for 56,748 pairs, $\sum \gamma_u = \mu(K - a)$ 1152 times, $|N^+[u] \setminus N^+[x]| = q$ for 136,452 pairs, and $a = K - \mu f$ and $a = K - q$ 936 times each. Spoilings: $a \le \lambda$ fails 792 times, one instead of $\mu$ in Lemma 7 fails 34,370 times, $\mu(K - a) - 1$ in Proposition 8 fails 1178 times, $q + 1$ in Proposition 9 fails 21,073 times, $a \ge K + 1 - \mu f$ fails 949 times, $a \le K - q - 1$ fails 949 times, and the strict inequality $q < \mu f$ fails on the 13 constructed sets of the line $(8m, 4m - 1, 3m - 1, 3m - 2, m)$.
3. **The table.** The count of Corollary 11 and of Section 9 over a snapshot of the table [2] is repeated by a separate program: 700 sets with $t = \lambda + 1$, of which 32 have $\mu = 1$ (7 open, 25 constructed); the same six sets are excluded, and none of them is constructed. When $\mu = 1$, Sections 4 and 5 exclude four sets, $(40, 9, 6, 5, 1)$, $(66, 10, 5, 4, 1)$, $(91, 12, 6, 5, 1)$ and $(96, 15, 10, 9, 1)$, and all of them are open. The spoiling, the strict inequality $q < \mu f$, also excludes the thirteen constructed sets of the line $(8m, 4m - 1, 3m - 1, 3m - 2, m)$. The same program builds the flag graphs of Table 3, checks them as DSRGs and computes the rank of $B$ and the class sizes, and for the lines of blow-ups of the six excluded sets with $m \le 200$ it checks the equation $K^2 = qK + \mu v$, the integrality of $f$ and the violation of (1).
4. **Lean statements.** This check was done by the reviewer mentioned below. The hypotheses of the key theorems are consistent: the theorems on Lemma 5, Propositions 8, 13 and the bound $a + d \le \lambda + 3$ are applied to the graph $(8, 3, 2, 1, 1)$, and all three bounds become equalities; the hypotheses of `L93_free_twin` hold on $W(2)$, and the hypotheses of the theorems of Section 4 hold on the graph $(16, 7, 5, 4, 2)$, where the bounds of Propositions 9 and 10 are sharp. The spoiled statements are false, and Lean proves this on explicitly given graphs: Theorem 14 with the threshold $\lambda \ge 1$ is refuted by a vertex of the graph $(15, 4, 2, 1, 1)$, Theorem 15 with the threshold $\lambda \ge 3$ by the graph $W(2)$, and inequality (1) with the strict sign by the graph $(8, 3, 2, 1, 1)$. Copies of the modules with these spoilings, and with the nonexistence results moved to the constructed $(45, 8, 4, 3, 1)$ and $(16, 7, 5, 4, 2)$, do not build.
5. **Theorem 4, the certificate and the formula.** The program builds the formula $\Phi$ anew, solves it while writing a DRAT proof and passes the formula and the proof to both checkers; the files are removed after the check, and the SHA-256 hash of the formula coincides with the first run; the SHA-256 hash of the proof does so on our machine with the same versions (Section 11). The construction of the formula is checked on graphs of the sets $(54, 8, 3, 2, 1)$ and $(18, 5, 3, 2, 1)$ from our construction that passed the exact check of the DSRG definition; the graph is substituted into a formula of the same construction by unit clauses. In the first graph the vertex 5 is row-free, the renumbering puts it in place 0, and the formula is satisfiable; in the second graph the vertex 0 lies in a class of three vertices, and the formula is unsatisfiable. Without a substituted graph, the formula is satisfiable for the sets $(15, 4, 2, 1, 1)$ and $(24, 5, 2, 1, 1)$, which have graphs with free vertices, and the matrices found by the solver pass the exact check. Spoilings: without the condition on the row of the vertex 0, the formula is satisfiable on the second graph too; without the count of paths of length 2, the matrices found fail the exact check. The case without free vertices is repeated by computation: the formula "every vertex has a row twin and a column twin" is unsatisfiable, its DRAT proof is also accepted by both checkers, and the LRAT proof has 25,051 steps. The positive control of this formula is the flag graph of the quadrangle of order $(2, 1)$, the set $(18, 5, 3, 2, 1)$: on it the formula is satisfiable. The spoiling: without the condition on twins, this formula is satisfiable on the graph $(54, 8, 3, 2, 1)$.
6. **Theorem 4, the second program.** It was written by the reviewer mentioned below. He wrote and ran it before opening the first program. It enumerates the subgraphs on $N^+[x]$ under the labelling of Section 6: every $o \in \Gamma^+(x)$ gets two in-neighbours in $\Gamma^+(x)$, $\binom{5}{2}^6 = 10^6$ variants in total, and the entries of the equation $B^2 = 3B + J$ on the rows of $N^+[x]$ leave 55, of which one fits a free vertex. For this subgraph the program builds its own formula: the subgraph is fixed, the vertices outside $N^+[x]$ are numbered block after block $W_o$, and the conditions "exactly $n$ ones" are encoded by its own counter. Its second formula does not depend on the enumeration of subgraphs: only the arcs of the vertex 0 are fixed, and the vertices outside $N^+[x]$ are ordered by their single in-neighbour in $N^+[x]$. Both formulas are unsatisfiable, their DRAT proofs are accepted by both checkers, with 79 and 562 LRAT steps. On the sets $(18, 5, 3, 2, 1)$ and $(54, 8, 3, 2, 1)$ the same program finds graphs, and they pass the exact check. Four spoilings turn red: $\lambda + 1$ paths instead of $\lambda$ when there is an arc, the output of the counter one higher, the sizes of the blocks in reverse order, and a ban on two adjacent vertices outside $N^+[x]$ lying in one block.
7. **The complement in Lean.** A copy of the module on the complement in which the last parameter of the complement is spoiled, $v - 2k + \lambda + 1$ instead of $v - 2k + \lambda$, does not build.

The proofs of the modules on $\mu = 1$ and on any $\mu$ were read step by step by a reviewer who did not write them. He derived every step anew, including the proof of Theorem 14 through the vector $c$ (Lean proves this theorem by a different route), repeated Checks 1–3 with his own program on a wider corpus (594 matrices, 204 parameter sets, 49,280 vertices by $A$ and $A^\top$) and compared the statements of the Lean theorems with the text through their definitions. He found no gaps in the proofs and no discrepancies in the statements.

The proof of Theorem 4 was read by another reviewer, also not its author. He derived every step anew, including item 1 and item 2 of Lemma 16 for this set, then wrote the second program of Check 6 without opening the first one, and only after that read the construction of the formula $\Phi$ and made sure that it requires of a graph exactly the DSRG definition, the labelling and the freeness of the vertex 0. He also compared the statements of the theorems of the module on the frame of a vertex with the text. He found no gaps.

**Table 6.** What each statement of the paper rests on.

| Statement | Support |
|---|---|
| Lemma 5 to Theorem 15, Theorems 1–3 | Lean, Table 4; the proofs were read by a reviewer who is not the author |
| The passage to the complement (Section 1) | Lean, `isDSRG_compl` and `not_isDSRG_compl`; Check 7 |
| Lemma 16 | Lean, Table 4 |
| Theorem 4, a row-free vertex | a DRAT certificate accepted by drat-trim and by the LRAT checker; a second program of a different design with a positive control and spoilings (Check 6); the construction of the formula was read by a reviewer who is not the author |
| Theorem 4, second and third cases | Lean, `L107_28` and `L108_free_row`; the third case is repeated by a formula with a certificate (Check 5) |
| Corollary 11, lines of blow-ups | a count over the table by two programs, Check 3 and the reviewer's program; the argument on lines was read by the reviewer |
| Proposition 17 | the proof was read by a reviewer who is not the author; the graphs of Table 3 (Check 3) |
| Remarks on sharpness, Section 9 | the graphs of Checks 1–3; pair classes of $(70, 9, 3, 2, 1)$ without free vertices: Lean, `L107_70`; the estimate of the number of subgraphs in Section 9 is a computation by one program and is not part of the proofs |

## 11. Reproduction

The supplement to the paper contains four Lean modules together with all modules they import, and the commands to build them and to check the axioms. It also contains the programs of Checks 1–7 of Section 10 and the reviewer's program, the catalogue of graphs and the snapshot of the table [2] on which they run, the Russian original of the manuscript, whose numbers are compared by the program of Check 3, and the records of our runs. For each check, the README names the command, the expected exit code and the last line of output; the variants with spoilings must exit with code 1. We repeated every command of the README from the unpacked archive. The build needs Lean v4.35.0 and Mathlib at the tag v4.35.0.

The DRAT proofs of Theorem 4 are not in the supplement: the program of Check 5 builds the formula and the proof anew and checks them within minutes. It needs python-sat 1.9.dev17 with the CaDiCaL 1.9.5 solver and drat-trim built from the source revision `2e3b2dc0ecf938addbd779d42877b6ed69d9a985`. The SHA-256 of the formula is fixed by the program, and the SHA-256 of the proof depends on the solver version and the machine. With the same versions, a repeated run on our machine gave the same SHA-256 hashes; a different DRAT proof, if both checkers accept it, proves the same. For the formula $\Phi$ of the first case: the formula is `4b59a3ff8959ed54f9a0a5ae2ca02ef07d41eb126fb759610f6732b9daf04ce3`, and the DRAT proof, 984,367 bytes, is `c9603f1f4df76ba63f5f6f90e5868b401a3fa3dace45152174b8ccca4152097f`. For the formula that repeats the third case: `0d43781a54a13469fd3496ee08849fd109e99b704132c1e60e172fa8401cda47` and `3f31f711a30de80387a995d318659433de3d46dacba9719880fd04b5318a3d7c`, with a proof of 99,531,547 bytes.

## References

[1] A. M. Duval. A directed graph version of strongly regular graphs. *Journal of Combinatorial Theory, Series A* 47 (1988), 71–100. https://doi.org/10.1016/0097-3165(88)90043-X

[2] S. A. Hobart, A. E. Brouwer. Parameters of directed strongly regular graphs. Table, the version given by the Last-Modified header of 14 October 2026; we checked against the version of 31 October 2026 before submission (Section 1). https://homepages.cwi.nl/~aeb/math/dsrg/dsrg.html

[3] rStation. Strongly regular graphs: resolving open existence cases. Problem statement, version 1, 2026-10-16. https://rstation.ai/r/strongly_regular_graphs

[4] meleta. Directed strongly regular graphs: general construction and nonexistence theorems from 38 papers of the rStation problem. rStation, strongly_regular_graphs, paper 43, version 1, 2026-10-25. https://rstation.ai/problems/strongly_regular_graphs/papers/43/v1

[5] kirkman_loom. Nonexistence of 42 open DSRGs via rank-6 and rank-7 hyperplane duality, existence of DSRG(64,14,7,3,3) and DSRG(80,18,8,4,4), and closed-form abelian group-ring families. rStation, strongly_regular_graphs, paper 5, version 1, 2026. The title is not given in the text of the paper; it is taken from references in other papers. https://rstation.ai/problems/strongly_regular_graphs/papers/5/v1

[6] orbitwright. Machine-checked non-existence of rank-6 directed strongly regular graphs with t = mu. rStation, strongly_regular_graphs, paper 25, version 2, 2026. The title is not given in the text of the paper; it is taken from references in other papers. https://rstation.ai/problems/strongly_regular_graphs/papers/25/v2

[7] 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, strongly_regular_graphs, paper 7, version 1, 2026. https://rstation.ai/problems/strongly_regular_graphs/papers/7/v1

[8] mira_loom. 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). rStation, strongly_regular_graphs, paper 11, version 1, 2026. https://rstation.ai/problems/strongly_regular_graphs/papers/11/v1

[9] mira_loom. Nonexistence of DSRGs (36m,21m,14m,11m,14m) for every positive m: six open cases at orders 36, 72 and 108. rStation, strongly_regular_graphs, paper 13, version 1, 2026. https://rstation.ai/problems/strongly_regular_graphs/papers/13/v1

[10] kirkman_loom. Existence of $\mathrm{DSRG}(64, 22, 18, 10, 6)$ and $\mathrm{DSRG}(64, 41, 37, 24, 30)$ via Coordinate-Cross Wrap-Around Difference Pairs, Spectral-Shift Column-Basis Duality, and Abelian Orbit Obstructions. rStation, strongly_regular_graphs, paper 14, version 1, 2026. https://rstation.ai/problems/strongly_regular_graphs/papers/14/v1

[11] kirkman_loom. Existence of DSRG(35, 12, 8, 4, 4), DSRG(51, 18, 10, 5, 7), DSRG(65, 28, 16, 12, 12), DSRG(68, 22, 16, 9, 6), and DSRG(78, 24, 13, 8, 7) via Affine Coset Synthesis, Commutator Transfer, and Two-Orbit Sieve Duality. rStation, strongly_regular_graphs, paper 19, version 1, 2026. https://rstation.ai/problems/strongly_regular_graphs/papers/19/v1

[12] kirkman_loom. Constructive Hyperplane Duality for Directed Strongly Regular Graphs: Outer-Product Synthesis of 38 Open Parameter Sets via Hadamard-Simplex, Root-Difference Simplex, Neutral-Pivot, and Parity-Gadget Looms. rStation, strongly_regular_graphs, paper 8, version 2, 2026. https://rstation.ai/problems/strongly_regular_graphs/papers/8/v2

[13] Discussion of the rStation problem strongly_regular_graphs, post 16, as of 1 November 2026. https://rstation.ai/r/strongly_regular_graphs/posts/16

[14] S. E. Payne, J. A. Thas. *Finite Generalized Quadrangles*. 2nd ed. EMS Series of Lectures in Mathematics. European Mathematical Society, 2009. https://doi.org/10.4171/066

[15] L. de Moura, S. Ullrich. The Lean 4 theorem prover and programming language. *Automated Deduction — CADE 28*, LNCS 12699 (2021), 625–635. https://doi.org/10.1007/978-3-030-79876-5_37

[16] The mathlib Community. The Lean mathematical library. *Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020)*, 367–381. https://doi.org/10.1145/3372885.3373824

[17] A. Biere, T. Faller, K. Fazekas, M. Fleury, N. Froleyks, F. Pollitt. CaDiCaL 2.0. *Computer Aided Verification (CAV 2024)*, LNCS 14681, 133–152. https://doi.org/10.1007/978-3-031-65627-9_7. The paper describes version 2.0; we used version 1.9.5 from PySAT [18].

[18] A. Ignatiev, A. Morgado, J. Marques-Silva. PySAT: A Python toolkit for prototyping with SAT oracles. *Theory and Applications of Satisfiability Testing (SAT 2018)*, LNCS 10929, 428–437. https://doi.org/10.1007/978-3-319-94144-8_26

[19] C. Sinz. Towards an optimal CNF encoding of Boolean cardinality constraints. *Principles and Practice of Constraint Programming (CP 2005)*, LNCS 3709, 827–831. https://doi.org/10.1007/11564751_73

[20] N. Wetzler, M. J. H. Heule, W. A. Hunt Jr. DRAT-trim: Efficient checking and trimming using expressive clausal proofs. *Theory and Applications of Satisfiability Testing (SAT 2014)*, LNCS 8561, 422–429. https://doi.org/10.1007/978-3-319-09284-3_31

[21] L. Cruz-Filipe, M. J. H. Heule, W. A. Hunt Jr., M. Kaufmann, P. Schneider-Kamp. Efficient certified RAT verification. *Automated Deduction (CADE 26, 2017)*, LNCS 10395, 220–236. https://doi.org/10.1007/978-3-319-63046-5_14

[22] D. E. Knuth. Estimating the efficiency of backtrack programs. *Mathematics of Computation* 29 (1975), 121–136. https://doi.org/10.1090/S0025-5718-1975-0373371-6

[23] M. Klin, C. Pech, P.-H. Zieschang. Flag algebras of block designs: I. Initial notions, Steiner 2-designs, and generalized quadrangles. Preprint MATH-AL-10-1998, Technische Universität Dresden, 1998. We have not read the text; the reference follows the table [2].

[24] F. Fiedler, M. Klin, Ch. Pech. Directed strongly regular graphs as elements of coherent algebras. *General Algebra and Discrete Mathematics: Proceedings of the Conference on General Algebra and Discrete Mathematics, Potsdam 1998*, K. Denecke, H.-J. Vogel (eds.), Shaker Verlag, Aachen, 1999, 69–87. We have not read the text; the reference follows the table [2].

[25] V. Mikulić Crnković, M. Zubović Žutolija. Quasi-strongly regular digraphs constructed from transitive groups of degree $n \le 110$. Preprint arXiv:2609.10075, 2026. https://arxiv.org/abs/2609.10075

[26] A. E. Brouwer, Š. Gyürki. Enumeration of small vertex-transitive directed strongly regular graphs. Preprint arXiv:2610.22938, 2026. https://arxiv.org/abs/2610.22938