"""Exact small hypothesis certificates, not a proof of the general theorem."""
from itertools import combinations
from fractions import Fraction
import json

def stats(columns, m):
    n=2*m
    degree=[sum((c>>i)&1 for c in columns) for i in range(n)]
    best=None; witness=None; kernel=[]
    for x in range(1<<n):
        w=sum((x & c).bit_count()%2 for c in columns)
        a=(x&((1<<m)-1)).bit_count(); b=(x>>m).bit_count()
        distance=min(a,m-a)+min(b,m-b)
        if w==0: kernel.append(x)
        if distance and (best is None or Fraction(w,distance)<best):
            best=Fraction(w,distance); witness=x
    return {'n':n,'d':len(columns),'columns':columns,'row_degrees':degree,
            'kernel':kernel,'minimum_weight_per_block_distance':str(best),
            'minimizer':witness}

m=4; n=2*m; d=n*n
pairs=[(1<<a)|(1<<b) for a,b in combinations(range(m),2)]
pool=[a|(b<<m) for a in pairs for b in pairs]
positive=[pool[i%len(pool)] for i in range(d)]
p=stats(positive,m)
assert p['kernel']==[0,15,240,255]
assert Fraction(p['minimum_weight_per_block_distance'])>0
assert all((c&15).bit_count()==2 and (c>>m).bit_count()==2 for c in positive)
negative=[pairs[i%len(pairs)]*(1+(1<<m)) for i in range(d)]
a=stats(negative,m)
assert Fraction(a['minimum_weight_per_block_distance'])==0
assert len(a['kernel'])==1<<(m+1)
x=1|(1<<m)
assert all((x&c).bit_count()%2==0 for c in negative)
# Each separate block expands despite the joint cancellation.
local=min(Fraction(sum((x&(c&15)).bit_count()%2 for c in negative),min(x.bit_count(),m-x.bit_count()))
          for x in range(1,15))
assert local>=4*m
print(json.dumps({'scope':'All 256 message vectors for two concrete n=8 matrices only; no query lower-bound, formal, or asymptotic verification.',
                  'positive':p,'cancellation':a,'separate_block_minimum_ratio':str(local),
                  'nonconstant_cancelling_message':x},indent=2))