verify_quotient_correction.py

"""Finite certificate checks only; not a proof of the general query bounds."""
from itertools import permutations, combinations
from fractions import Fraction
import json

out=[]
for r in range(1,5):
    words=range(1,1<<r)
    enc={x:sum((((x&a).bit_count()&1)<<i) for i,a in enumerate(words)) for x in range(1<<r)}
    delta=1<<(r-1)
    assert all(enc[x].bit_count()==delta for x in words)
    totals={x:0 for x in words}; count=0
    for basis in permutations(words,r):
        representations={0:0}
        for i,a in enumerate(basis):
            additions={x^a:c|(1<<i) for x,c in representations.items()}
            if any(x in representations for x in additions): break
            representations.update(additions)
        else:
            count+=1
            for x in words: totals[x]+=representations[x].bit_count()
    target=Fraction(r*(1<<(r-1)),(1<<r)-1)
    assert all(Fraction(v,count)==target for v in totals.values())
    out.append({'r':r,'length':(1<<r)-1,'nonzero_weight':delta,'ordered_bases':count,'mean_coefficient_weight_every_nonzero_word':str(target)})

m=4; d=4*m*m
edges=list(combinations(range(m),2))
columns=[sum(1<<i for i in edges[k%len(edges)]) for k in range(d)]
rows=[sum(((a>>i)&1)<<j for j,a in enumerate(columns)) for i in range(m)]
cost_ratio=[]
for x in range(1<<m):
    z=0
    for i,row in enumerate(rows):
        if x>>i&1:z^=row
    total=0
    for ref in range(m):
        reconstructed=0;cost=0
        for i,row in enumerate(rows):
            if ((x>>i)^(x>>ref))&1:
                reconstructed^=row;cost+=row.bit_count()
        assert reconstructed==z
        total+=cost
    if z:cost_ratio.append(Fraction(total,m*z.bit_count()))
assert max(cost_ratio)<=Fraction(9,2)
print(json.dumps({'scope':'All ordered bases for simplex dimensions 1 through 4; all 16 messages and four reference choices for one repeated K4 incidence matrix. No query-bound, asymptotic or proof-assistant verification.', 'simplex':out,'duplicated_graph':{'m':m,'d':d,'max_expected_cost_ratio':str(max(cost_ratio)),'theorem_certificate_bound':'9/2'}},indent=2))