Evidence

../

The entry point checks the finite diagnostics of the lead. Run from the repository root:

uv run --no-sync python wiki/research/leads/complete_bipartite_size_ramsey/evidence/main.py

It needs networkx and numpy from the evidence group and takes under a minute. Arithmetic is exact: Python integers for counts and loads, and NumPy uint32 for colourings of graphs with at most 15 edges. It checks:

• the exact witness inventory, dimensions, binary alphabet, and vertex domain, including that the complete-host witness concerns $K_{17}$ and $K_{3,3}$;
• the capacities of Lemma 2 that the lead tabulates, from exact binomials;
• each stored colouring of a complete bipartite host, for $n=2$ the hosts $K_{3,6}$ and $K_{4,6}$ and for $n=3$ the hosts $K_{5,40}$, $K_{6,40}$, $K_{7,28}$, $K_{8,28}$, $K_{9,22}$, $K_{10,20}$, $K_{11,18}$, $K_{12,16}$, $K_{13,15}$ and $K_{14,14}$, twice: by the red and blue loads of every $n$-set of columns, and by the common red and blue columns of every $n$-set of rows;
• the counting inequality of Lemma 2 for $K_{3,7}$, $K_{4,7}$ and $K_{7,29}$;
• a colouring of every $K_{a,b}$ with $a\le b$ and $ab\le20$ ($n=2$) or $ab\le202$ ($n=3$), so that the cheapest complete bipartite Ramsey hosts have $21$ and $203$ edges;
• $b(2)=5$: a colouring of $K_{4,4}$, and the absence of five pairwise compatible rows of length $5$, which covers every colouring of $K_{5,5}$;
• the $313$ isomorphism classes of graphs with minimum degree at least $3$ and at most $14$ edges, each with a good colouring checked against every 4-cycle, and their completeness: in every cell of vertex and edge counts, the sum of $v!/|\mathrm{Aut}(G)|$ equals the number of labelled graphs, counted independently through degree sequences; and $K_6\to C_4$ over all $2^{15}$ colourings;
• the stored colouring of $K_{17}$, by common neighbourhoods and by every pair of disjoint $3$-sets;
• the $30$ affine hyperplanes of $\mathbb F_2^4$, generated by their defining linear equations: every translation permutes the family, every $4$-set has both loads at most $3$, and every four rows have fewer than four common points in either colour. The plane $\{0,1,2,3\}$ has both loads exactly $3$, refuting divisibility by $4$ for arbitrary translation-invariant families. The capacity at $(a,n)=(16,4)$ is $78$.

The colourings are in assets/witnesses.json. A SAT solver found them; nothing in them is trusted until the entry point checks it. The hyperplane construction is generated directly by the checker and proved in the lead. Negative controls reject a corrupted colouring, a nonbinary row, a missing or duplicated host witness, a smaller replacement for the stated $K_{17}$ target, and a missing host class.

The completeness count for $n=2$ is independent of the atlas and extension enumeration. For a prescribed labelled degree sequence, delete its first vertex and sum the counts of the residual sequences over every possible set of its neighbours. Negative degrees contribute zero, and the empty sequence contributes one. Sorting residual sequences merely relabels vertices, so it does not change their counts. Summing over sorted degree sequences with minimum degree $3$ and sum $2m$, weighted by the number of their distinct permutations, counts every labelled graph in the $(v,m)$ cell exactly once. The generated representatives are deduplicated by isomorphism; their orbit sizes sum to that independent count in every cell. Thus none is missing. The degree-removal argument in the lead reduces every possible host with at most $14$ edges to one of these cells or to the empty graph.

For the complete bipartite minima, symmetry permits $a\le b$. Below an edge threshold $q$, only $a\le\lfloor\sqrt q\rfloor$ need checking, and the witness for $b=\lfloor q/a\rfloor$ covers every smaller $b$ by deleting rows. When $a\le2n-2$, a column split with both colour classes smaller than $n$ can be repeated arbitrarily. These reductions explain the exhaustive scope even though the stored witness list is finite.

The entry point does not check the solver verdict that $K_{9,23}$ has no good colouring, the theorem $r(K_{3,3})=18$ behind $K_{18}$, or the propositions of the lead. The discovery script writes the SAT instance for a complete bipartite or complete host to the ignored output/ folder and, given --solve, runs kissat from the path and writes any colouring it finds there; its unsatisfiable verdicts are solver verdicts without a checked certificate. For example:

uv run --no-sync python wiki/research/leads/complete_bipartite_size_ramsey/evidence/produce.py kab 9 23 3 --solve 600

The encoding has one Boolean variable per edge, with true meaning red. Every candidate copy contributes two clauses excluding its all-red and all-blue assignments. In the bipartite case, auxiliary prefix-equality variables put the rows in nonincreasing lexicographic order. Permuting rows preserves avoidance, so this removes no feasible colouring class. Repeated rows remain allowed. In the complete-host case, the encoding uses every unordered pair of disjoint $n$-sets. The recorded $K_{9,23}$ verdict came from Kissat 4.0.4; this encoding and that solver's verdict do not replace a checked unsatisfiability certificate.