"""Deep rigorous verification of one open box (from <part>.final.json 'still').
Recursive guillotine subdivision; each node is closed by one of the rigorous certificates of verify4
(exact Farkas emptiness with cutting planes, upper face, pair bound, leaf bound), otherwise split
with the search's gradient-score rule (u = sqrt(1-c) midpoints for equal-bound pairs near 1).
A cutting-plane loop that finds no point is never taken as emptiness. All terminal boxes are
recorded and checked to tile the root box. Usage: python deepfix.py par_j1_p2 INDEX [MAXNODES]"""
import sys, json, time, numpy as np
import verify4
from cover import check
verify4.init()
from flint import arb
import k4, bbC, gradx, dualK
from k4 import PAIRS
part=sys.argv[1]; idx=int(sys.argv[2]); MAXN=int(sys.argv[3]) if len(sys.argv)>3 else 300000
fin=json.load(open(part+".final.json")); V=fin["V"]; j=fin["j"]; pat=list(bbC.PATS[j])
root=[s["box"] for s in fin["still"] if s["index"]==idx][0]
jj=j; A_sym=bbC.symA(jj); eq=[[pat[p]==pat[q] for q in range(4)] for p in range(4)]
rsa=[{"34":k4.R34A,"44":k4.R44A}[x] for x in pat]; rs=np.array([{"34":k4.r34,"44":k4.r44}[x] for x in pat])
def split_choice(lo,hi):
    sq=[eq[p][q] and hi[m]>0.98 for m,(p,q) in enumerate(PAIRS)]
    try: g=gradx.grad_best(rsa,list(lo),list(hi),refine=False)
    except Exception: g=[None]*6
    score=[]
    for m,(p,q) in enumerate(PAIRS):
        w=hi[m]-lo[m]
        if sq[m]:
            K=float(dualK.sqrt_K(rsa,p,q,lo[m]).upper()); uw=np.sqrt(max(1-lo[m],0))-np.sqrt(max(1-hi[m],0)); score.append(2*K*uw+1e-15)
        elif g[m] is not None and g[m].is_finite(): score.append((abs(float(g[m].mid()))+float(g[m].rad()))*w)
        else: score.append(float(verify4.Lglob_arb(rsa,p,q,lo[m],hi[m]).upper())*w if True else w)
    m=int(np.argmax(score))
    if sq[m]:
        um=(np.sqrt(max(1-lo[m],0))+np.sqrt(max(1-hi[m],0)))/2; mid=1-um*um
        if not (lo[m]<mid<hi[m]): mid=(lo[m]+hi[m])/2
    else: mid=(lo[m]+hi[m])/2
    return m,mid
t0=time.time(); stack=[(list(root["lo"]),list(root["hi"]),list(root.get("cuts",[])),0)]
terminal=[]; counts=dict(empty=0,face=0,slab=0,leaf=0,tiny=0); worst=-1.0; n=0; open_boxes=[]
while stack:
    lo,hi,cuts,dep=stack.pop(); n+=1
    A,b=verify4.system(jj,cuts)
    kind=None
    if verify4.farkas_empty(lo,hi,A,b): kind="empty"
    else:
        xin,vecs=verify4.find_psd_cuts(np.array(lo),np.array(hi),cuts,A_sym,iters=60)
        cuts2=(list(cuts)+[v for v in vecs if v not in cuts])[-8:]
        if xin is None:
            Ax,bx=verify4.system(jj,vecs)
            if verify4.farkas_empty(lo,hi,Ax,bx): kind="empty"
        if kind is None and verify4.upper_face(lo,hi,A,b) is not None: kind="face"
        if kind is None:
            sv=verify4.slab_ok(pat,V,lo,hi)
            if sv is not None: kind="slab"; worst=max(worst,sv)
        if kind is None:
            for rf in (False,True):
                st,val=verify4.leaf_ok(pat,V,lo,hi,cuts2,None,refine=rf)
                if st=="ok": kind="leaf"; worst=max(worst,val); break
        cuts=cuts2
    if kind is not None:
        counts[kind]+=1; terminal.append((tuple(lo),tuple(hi))); continue
    if n>=MAXN or max(h-l for l,h in zip(lo,hi))<1e-9:
        counts["tiny"]+=1; open_boxes.append(dict(lo=lo,hi=hi)); terminal.append((tuple(lo),tuple(hi))); continue
    m,mid=split_choice(lo,hi)
    h1=list(hi); h1[m]=mid; l2=list(lo); l2[m]=mid
    stack.append((lo,h1,cuts,dep+1)); stack.append((l2,hi,cuts,dep+1))
    if n%2000==0: print(f"  {n} nodes {counts} stack {len(stack)} {time.time()-t0:.0f}s",flush=True)
ok,info=check(terminal,list(root["lo"]),list(root["hi"]))
res=dict(part=part,index=idx,V=V,nodes=n,counts=counts,max_ub=worst,cover="OK" if ok else str(info),open=open_boxes,seconds=round(time.time()-t0))
json.dump(res,open(f"deepfix_{part}_{idx}.json","w"),default=str)
print("RESULT",part,idx,"nodes",n,counts,"max_ub",worst,"cover",res["cover"],"open",len(open_boxes),f"{time.time()-t0:.0f}s",flush=True)