verify_rank_deletion.py

"""Exhaustive small bilinear approximation checks; not the RM conjecture."""
from itertools import product
from fractions import Fraction
import json

def rank(rows):
    basis={}
    for x in rows:
        while x:
            p=x.bit_length()-1
            if p in basis: x ^= basis[p]
            else:
                basis[p]=x
                break
    return len(basis)

def span(rows):
    out={0}
    for x in rows: out |= {y^x for y in tuple(out)}
    return out

# Coefficient rows are 2x2 binary matrices, encoded in four bits.
weights=[]
for a in range(16):
    t=rank([a&3,a>>2])
    weights.append(Fraction(1-(Fraction(1,2)**t),2))
forms=list(product(range(16),repeat=3))
low=[q for q in forms if rank(q)<=1]
for g in forms:
    deletion=min(mask.bit_count() for mask in range(8)
                 if rank([g[i] for i in range(3) if not(mask>>i&1)])<=1)
    best=min(sum(weights[g[i]^q[i]] for i in range(3)) for q in low)
    assert Fraction(deletion,4)<=best<=Fraction(deletion,2)
    columns=[sum(((g[i]>>j)&1)<<i for i in range(3)) for j in range(4)]
    W=span(columns); rho=rank(columns)
    if rho<=1: ghw=0
    else:
        # Independently enumerate all subspaces generated by rho-1 words of W.
        support=[]
        for basis in product(W,repeat=rho-1):
            if rank(basis)==rho-1:
                union=0
                for w in basis: union |=w
                support.append(union.bit_count())
        ghw=min(support)
    assert deletion==ghw

# Same full image, same U=span(e_0), distinct rank-one pushforward distances.
g1=[1,2,4,8]
g2=[1,9,6,11]
assert rank(g1)==rank(g2)==4
means=[sum(weights[x] for x in g[1:]) for g in (g1,g2)]
assert means==[Fraction(3,4),Fraction(9,8)]
print(json.dumps({
 'scope':'All 4096 maps F2^2 x F2^2 -> F2^3, rank budget one; exact enumeration of 106 candidate approximants. Not a test of the uniform Reed-Muller conjecture.',
 'maps':len(forms),'rank_one_or_zero_approximants':len(low),
 'approximation_sandwich':'passed','generalized_weight_identification':'passed',
 'same_image_different_distribution':{'coefficient_rows':[g1,g2], 'advice':'span of first output unit vector','mean_distances':list(map(str,means))},
 'not_verified':['arbitrary dimensions','universal rank-controlled repair','RM-family deletion inequality','new query lower bound']
},indent=2))