"""
Ramsey FINAL v2 - type-separated, certificate-checked re-execution.
For each multiplier-invariant space:
  A) every candidate tested: local K_s count (#K_s through vertex 0)
  B) candidates with count>0 -> 'clique-rejected'; track MIN (compare to claim)
  C) candidates with count=0 -> must contain independent t-set (alpha>=t);
     searcher must return an explicit certificate, which we edge-scan verify.
  Verdict: paper's 'no (s,t)-free candidate' holds iff C never fails.
  Also: min over (B) == claimed best_violations?
"""
import json, re, os, sys, time, random
sys.setrecursionlimit(100000)

BODIES = r"C:\Users\jack\rc_corpus\bodies"
FULL = lambda n: (1 << n) - 1
def rot(x,k,n): return x if k==0 else ((x<<k)|(x>>(n-k))) & FULL(n)
def popcount(x): return bin(x).count("1")

def class_orbits(n,a):
    cls={}
    for r in range(1,n//2+1): cls[r]=r; cls[n-r]=r
    seen=set(); orbs=[]
    for r in range(1,n//2+1):
        if r in seen: continue
        o=set(); x=r
        while True:
            c=cls[x]
            if c in o: break
            o.add(c); x=(a*x)%n
        orbs.append(o); seen|=o
    return orbs

def adj_from_m0(m0,n): return [rot(m0,v,n) for v in range(n)]

def local_Ks_count(adj,m0,s):
    """#K_s through vertex 0 = #K_{s-1} in N(0)."""
    N=m0
    if s==3:
        cnt=0
        for u in bits_iter(N):
            cnt+=popcount(adj[u]&N&((1<<u)-1))
        return cnt
    elif s==4:
        cnt=0
        for u in bits_iter(N):
            nu=adj[u]&N&((1<<u)-1)
            for w in bits_iter(nu):
                cnt+=popcount(adj[w]&nu&((1<<w)-1))
        return cnt
    raise ValueError

def bits_iter(x):
    while x:
        b=x&-x; yield b.bit_length()-1; x^=b

def find_iset_exact(adj,n,t,budget_s=60):
    """Return ('yes',cert)|('no',None)|('timeout',None). Cert=edge-scannable list."""
    comp=[0]*n; full=FULL(n); t0=time.time()
    for v in range(n): comp[v]=full&~adj[v]&~(1<<v)
    class TO(Exception): pass
    def color_sort(P):
        order=[];bounds=[];U=P;c=0
        while U:
            c+=1;avail=U
            while avail:
                b=avail&-avail;v=b.bit_length()-1
                order.append(v);bounds.append(c)
                U^=b;avail&=~b;avail&=~comp[v]
        return order,bounds
    def expand(C,P):
        if time.time()-t0>budget_s: raise TO()
        if len(C)>=t: return list(C)
        order,bounds=color_sort(P)
        for i in range(len(order)-1,-1,-1):
            if len(C)+bounds[i]<t: return None
            v=order[i]
            C.append(v)
            r=expand(C,P&comp[v])
            if r: return r
            C.pop(); P&=~(1<<v)
        return None
    try:
        r=expand([],full)
        return ("yes",r) if r else ("no",None)
    except TO:
        return ("timeout",None)

def cert_valid_is(adj,cert,t):
    if len(cert)<t: return False
    for i,u in enumerate(cert):
        for w in cert[i+1:]:
            if adj[u]>>w & 1: return False
    return True

def brute_alpha_small(adj,n):
    import itertools
    for k in range(n,0,-1):
        for sub in itertools.combinations(range(n),k):
            if all(not(adj[a]>>b&1) for a,b in itertools.combinations(sub,2)):
                return k
    return 0

# ---- validate searcher at operating point on small ground truths ----
rng=random.Random(11); val_ok=0; val_n=0; certs_ok=0
for _ in range(40):
    n=rng.choice([12,13,14,15,16])
    S=set(rng.sample(range(1,n//2+1), rng.randint(2,5)))
    m0=0
    for c in S: m0|=(1<<c)|(1<<((n-c)%n))
    adj=adj_from_m0(m0,n)
    truth=brute_alpha_small(adj,n)
    q=min(truth+1,n)
    st,cert=find_iset_exact(adj,n,q,budget_s=30)
    val_n+=1
    if st=="no": val_ok+=1
    if st=="yes" and cert_valid_is(adj,cert,q): certs_ok+=1
print(f"searcher validation: nonexistence correct {val_ok}/{val_n}; yes-certificates valid {certs_ok}/{val_n}")

# ---- process the four exhaustion papers ----
PAPERS=["rcs_ppr_nfq9eydk3r1db32nzht1","rcs_ppr_zcre71rgb0sxv8gn2nt9",
        "rcs_ppr_9k1hv0ms2mrvpstwjpdq","rcs_ppr_brc4gatdk02xe4978cjz"]
out={}
for pid in PAPERS:
    p=json.load(open(os.path.join(BODIES,pid+".json"),encoding="utf-8"))
    rec=json.loads(re.search(r"```json\r?\n(\{.*?\})\r?\n```",p["body"],re.S).group(1))
    n=rec["n"]; s_cell,t_cell=rec["cell"]
    print("="*74); print(pid,"cell",rec["cell"],"n=",n,flush=True)
    out[pid]={"cell":rec["cell"],"n":n,"spaces":[]}
    for sp in rec["spaces"]:
        a=int(re.search(r"x\s*->\s*(\d+)x",sp["invariant_under"]).group(1))
        orbs=class_orbits(n,a); k=len(orbs)
        orb_masks=[sum((1<<c)|(1<<((n-c)%n)) for c in o) for o in orbs]
        t0=time.time()
        min_clique=None; argmin=None
        zero_clique=0; alpha_certified=0; free=[]; timeouts=0; cert_fail=0
        spot_checked=0
        for mask in range(1,1<<k):
            m0=sum(orb_masks[i] for i in bits_iter(mask))
            adj=adj_from_m0(m0,n)
            lv=local_Ks_count(adj,m0,s_cell)
            if lv>0:
                if min_clique is None or lv<min_clique:
                    min_clique=lv; argmin=m0
            else:
                zero_clique+=1
                st,cert=find_iset_exact(adj,n,t_cell,budget_s=120)
                if st=="timeout": timeouts+=1
                elif st=="yes":
                    alpha_certified+=1
                    if spot_checked<5:
                        spot_checked+=1
                        if not cert_valid_is(adj,cert,t_cell): cert_fail+=1
                else:
                    free.append(bin(m0))
        res={"mult":a,"orbits":len(orbs),"orbits_match":len(orbs)==sp["orbits"],
             "cands":2**k-1,"cands_match":(2**k-1)==sp["total_candidates"],
             "zero_local_clique_candidates":zero_clique,
             "alpha_certified":alpha_certified,"timeouts":timeouts,
             "free_candidates":len(free),
             "certificate_failures":cert_fail,
             "min_clique_reject":min_clique,
             "claimed_best":sp["best_violations"],
             "min_matches_claim":min_clique==sp["best_violations"],
             "exhaustion_holds":len(free)==0 and timeouts==0,
             "seconds":round(time.time()-t0,1)}
        out[pid]["spaces"].append(res)
        print(json.dumps(res,indent=1),flush=True)

json.dump(out,open(r"C:\Users\jack\rc_audit\ramsey_final2.json","w"),indent=1)
print("saved ramsey_final2.json")