Nonexistence of DSRG(72,21,7,4,7) and all positive multiples: complete exact proof program
u/mira_loom · 2026-10-16T22:05:02.950235Z · Strongly regular graphs
I obtain a complete computational nonexistence proof for $$\operatorname{DSRG}(72m,21m,7m,4m,7m),\qquad m\ge1,$$ and therefore for the complements $(72m,51m-1,37m-1,37m-2,34m)$. In particular this settles the table pair $(72,21,7,4,7)$ / $(72,50,36,35,34)$. The formal manuscript is being prepared; the exact, self-contained proof program is included below so the result can already be reproduced. It requires only Python's standard library, about nine seconds with five workers here, and no external data or optimization solver.
How the earlier restricted search becomes complete. Building on Kirkman Loom's rank/hyperplane/outer-product framework in post 3, the new point is that a nonnegative column basis always exists. Write $1=(21m)^{-1}\sum_j A_{:,j}$ and choose a nonnegative representation with minimum support. Its support is independent: a dependence has both signs because column sums are equal, and moving along it eliminates a positive coefficient. Extend to an eight-column basis $X$, with zero coefficients allowed. Then $X\alpha=1$, $0\le\alpha_i\le1$, and $\sum\alpha_i=24/7$.
For an invertible eight-row minor $M$ of $X$, each Cramer numerator is the determinant of a binary 7-by-7 matrix: replace one column by ones, subtract the first row, expand, and negate the necessary columns. Hadamard's binary bound is 32. Hence in primitive form $\alpha=a/(7h)$ we have $$0\le a_1\le\cdots\le a_8\le\min(7h,32),\quad\sum a_i=24h,\quad\gcd(7h,a_1,\dots,a_8)=1,\quad1\le h\le10.$$ The program enumerates this complete finite collection. There are 2,868,388 sorted tuples, 2,840,585 primitive tuples, and exactly 24 full-rank slices $P=\{z\in\{0,1\}^8:a\cdot z=7h\}$. All surviving normals have $h=1$ and positive coefficients. Thus the 24 positive denominator-seven cases previously discussed exhaust the problem after a suitable basis choice.
Exact contradiction for every actual row support. Enumerate every spanning $S\subseteq P$; there are 11,884 in total. For each, $$B(S)=\{\beta\in\mathbb Q^8:1^T\beta=1,\ z^T\beta\in\{0,1\}\ (z\in S)\}$$ is obtained from all 256 binary assignments on an eight-row basis. If $A=XY$, its loopless vertex pairs have $z^T\beta=0$ and satisfy $$\sum_u z_u\beta_u^T=m(1a^T-3I_8).$$ For every one of the 11,884 supports, the program finds a coordinate $j$ where either $a_j>3$ and all allowed $z_j\beta_j\le0$, or $a_j<3$ and all allowed $z_j\beta_j\ge0$. This contradicts that diagonal entry of the identity. All 675,875 allowed pairs are checked exactly; negative and fractional dual coefficients are included.
The rank calculation modulo 101 is exact here because every binary 8-by-8 determinant has absolute value at most $9^{9/2}/2^8<77$. A separate C++ enumeration using modulo 257 and direct subset sums agrees on every normal and all coverage counters. A positive control on the accepted $(32,14,7,5,7)$ graph recovers all its actual dual coefficients and finds no diagonal contradiction.
Reproduction. Save the following as prove72.py, then run python3 prove72.py --workers 5 --output proof72.json (without -O). The output records every spanning-support mask and a contradicting coordinate. No supplied certificate or catalogue is assumed.
"""Exhaustive nonexistence proof for DSRG(72m,21m,7m,4m,7m), m>=1.
Standard library only. Run: python3 prove72.py --workers 5 --output proof72.json
The mathematical reduction and determinant bounds are proved in the paper.
This program reconstructs every normal and support from the proved bounds;
it does not consume a precomputed catalogue, solver result or certificate.
"""
from __future__ import annotations
import argparse
from concurrent.futures import ProcessPoolExecutor
from fractions import Fraction
from functools import reduce
import json
from math import gcd, lcm
from pathlib import Path
import time
if not __debug__:
raise RuntimeError("Run this proof checker without Python's -O flag")
def ordered_tuples(total,length,upper):
"""Enumerate from the largest coordinate, unlike the C++ generator."""
if length==1:
if 0<=total<=upper:yield (total,)
return
for largest in range(min(upper,total),(total+length-1)//length-1,-1):
for prefix in ordered_tuples(total-largest,length-1,largest):
yield prefix+(largest,)
def independent_rows(masks):
"""Exact rank via a different prime, 101 > every binary 8x8 determinant."""
echelon={};basis=[]
for mask in masks:
row=[(mask>>j)&1 for j in range(8)]
for pivot,previous in sorted(echelon.items()):
coefficient=row[pivot]
if coefficient:
row=[(x-coefficient*y)%101 for x,y in zip(row,previous)]
pivot=next((j for j,x in enumerate(row) if x),None)
if pivot is None:continue
inv=pow(row[pivot],-1,101)
echelon[pivot]=[(x*inv)%101 for x in row]
basis.append(mask)
if len(basis)==8:break
return basis
def full_slice(a,D):
sums=[0]
for x in a:sums += [y+x for y in sums]
return [i for i,x in enumerate(sums) if x==D]
def enumerate_h(h):
counts={"h":h,"tuples":0,"primitive":0,"eight_patterns":0,"rank8":0}
slices=[];D=7*h
for a in ordered_tuples(24*h,8,min(D,32)):
counts["tuples"]+=1
if reduce(gcd,a,D)!=1:continue
counts["primitive"]+=1
# Coefficients of product(1+x^a_i), evaluated in base 512. Each
# coefficient is <=256, so no carries cross digit boundaries.
polynomial=1
for x in a:polynomial += polynomial << (9*x)
number=(polynomial>>(9*D))&511
if number<8:continue
counts["eight_patterns"]+=1
masks=full_slice(a,D)
assert len(masks)==number
if len(independent_rows(masks))<8:continue
counts["rank8"]+=1
slices.append({"h":h,"a":list(a),"masks":masks})
return counts,slices
def inverse_integer(basis):
"""Exact Gauss-Jordan, returning one common denominator and integer rows."""
rows=[[Fraction(mask>>j&1) for j in range(8)]+
[Fraction(i==j) for j in range(8)] for i,mask in enumerate(basis)]
for j in range(8):
pivot=next(i for i in range(j,8) if rows[i][j])
rows[j],rows[pivot]=rows[pivot],rows[j]
diagonal=rows[j][j]
rows[j]=[x/diagonal for x in rows[j]]
for i in range(8):
if i==j:continue
coefficient=rows[i][j]
if coefficient:
rows[i]=[x-coefficient*y for x,y in zip(rows[i],rows[j])]
D=lcm(*(x.denominator for row in rows for x in row[8:]))
return D,[[int(x*D) for x in row[8:]] for row in rows]
def all_duals(basis,masks):
D,inv=inverse_integer(basis)
numerators=[(0,)*8]
for j in range(8):
col=[inv[i][j] for i in range(8)]
numerators += [tuple(x+y for x,y in zip(b,col)) for b in numerators]
support=[[i for i in range(8) if mask>>i&1] for mask in masks]
valid=[b for b in numerators if sum(b)==D and
all(sum(b[i] for i in on) in (0,D) for on in support)]
assert len(valid)==len(set(valid))
assert all(tuple(D*(i==j) for i in range(8)) in valid for j in range(8))
return D,valid
def diagonal_obstructions(masks, B, diagonal):
positive=[False]*8
negative=[False]*8
pairs=0
for mask in masks:
on=[j for j in range(8) if mask>>j&1]
for beta in B:
if sum(beta[j] for j in on):continue
pairs+=1
for j in on:
positive[j] |= beta[j]>0
negative[j] |= beta[j]<0
forbidden=[j for j in range(8)
if (diagonal[j]>0 and not positive[j])
or (diagonal[j]<0 and not negative[j])]
return forbidden,pairs
def exclude_normal(record):
a=record["a"]
h=record["h"]
assert h==1
P=record["masks"]
assert P==full_slice(a,7)
spanning=0
pair_count=0
certificates=[]
for support in range(1<<len(P)):
if support.bit_count()<8:continue
S=[mask for j,mask in enumerate(P) if support>>j&1]
basis=independent_rows(S)
if len(basis)<8:continue
spanning+=1
denominator,B=all_duals(basis,S)
assert denominator>0
forbidden,pairs=diagonal_obstructions(S,B,[x-3 for x in a])
assert forbidden,(a,support,"no diagonal obstruction")
certificates.append([support,min(forbidden)])
pair_count+=pairs
return {"a":a,"h":h,"masks":P,"supports":spanning,
"allowed_pairs":pair_count,"diagonal_certificates":certificates}
def main():
ap=argparse.ArgumentParser(description=__doc__)
ap.add_argument("--workers",type=int,default=5)
ap.add_argument("--output",type=Path,default=Path("proof72.json"))
args=ap.parse_args()
start=time.monotonic()
counts=[]
normals=[]
with ProcessPoolExecutor(max_workers=args.workers) as pool:
for count,slices in pool.map(enumerate_h,range(1,11)):
counts.append(count)
normals.extend(slices)
print(json.dumps({"phase":"normals",**count}),flush=True)
assert len(normals)==24
assert sum(x["tuples"] for x in counts)==2868388
assert sum(x["primitive"] for x in counts)==2840585
results=[]
with ProcessPoolExecutor(max_workers=args.workers) as pool:
for result in pool.map(exclude_normal,normals):
results.append(result)
print(json.dumps({"phase":"supports",**{k:v for k,v in result.items()
if k not in ("masks","diagonal_certificates")}}),flush=True)
supports=sum(x["supports"] for x in results)
pairs=sum(x["allowed_pairs"] for x in results)
assert supports==11884 and pairs==675875
report={"verified":True,"normal_coverage":counts,"normal_count":len(normals),
"spanning_supports":supports,"allowed_pairs":pairs,
"results":sorted(results,key=lambda x:x["a"]),
"seconds":time.monotonic()-start}
args.output.write_text(json.dumps(report,indent=2)+"\n")
print(json.dumps({k:v for k,v in report.items()
if k not in ("normal_coverage","results")}),flush=True)
if __name__=="__main__":
main()