basis-change-check.py

#!/usr/bin/env python3
"""Exact n=2 free-distance check, LSB-first row-major coordinates.
No external packages required. GL(4,2) enumeration is of dual query maps;
the realized storage map is the inverse transpose. Results are finite evidence.
"""
from itertools import permutations
from fractions import Fraction
import json

def lin(x, cols):
    out=0
    for i,col in enumerate(cols):
        if (x>>i)&1: out ^= col
    return out

def independent(cols):
    return len({lin(x,cols) for x in range(1<<len(cols))})==1<<len(cols)

def rank1(u,v):
    return sum((((u>>i)&1)*((v>>j)&1))<<(2*i+j) for i in range(2) for j in range(2))

queries=[rank1(u,v) for u in range(4) for v in range(4)]
rankone=sorted(set(queries)-{0})
codes={tuple([0])}
for a in range(1,16): codes.add(tuple(sorted([0,a])))
for a in range(1,16):
    for b in range(a+1,16): codes.add(tuple(sorted([0,a,b,a^b])))
codes=sorted(codes,key=lambda c:(len(c),c))
distances={c:[min((q^b).bit_count() for b in c) for q in range(16)] for c in codes}
identity=(1,2,4,8)
claimed_storage_rows=(1,2,4,9)
# w_i = dot(storage_rows[i],a). Because this storage map is involutory,
# its dual query map is M^T, whose columns are the rows of M.
claimed_dual_cols=claimed_storage_rows
claimed_code=(0,7,10,13)
claimed_q=[lin(q,claimed_dual_cols) for q in queries]
claimed_d=[distances[claimed_code][q] for q in claimed_q]
# Transposed shear: w=(a00+a11,a01,a10,a11). Its dual columns = rows.
corrected_storage_rows=(9,2,4,8)
corrected_dual_cols=corrected_storage_rows
corrected_q=[lin(q,corrected_dual_cols) for q in queries]
corrected_d=[distances[claimed_code][q] for q in corrected_q]

def optimize(qs):
    values=[(sum(distances[c][q] for q in qs),c) for c in codes]
    m=min(x[0] for x in values)
    return m,[list(c) for val,c in values if val==m]

sys_min,sys_codes=optimize(queries)
claimed_basis_min,claimed_basis_codes=optimize(claimed_q)
best=10**9
best_count=0
first=None
gl_count=0
for cols in permutations(range(1,16),4):
    if not independent(cols): continue
    gl_count+=1
    image=[lin(q,cols) for q in rankone]
    for c in codes:
        total=sum(distances[c][q] for q in image)
        if total<best:
            best=total; best_count=1; first={'dual_columns':list(cols),'code':list(c)}
        elif total==best: best_count+=1

result={
 'coordinate_order':['00','01','10','11'],
 'bit_order':'LSB first',
 'query_count':len(queries),
 'distinct_nonzero_rank_one_queries':rankone,
 'code_count':len(codes),
 'gl4_count':gl_count,
 'pair_count':gl_count*len(codes),
 'systematic_minimum':{'distance_sum':sys_min,'mean':str(Fraction(sys_min,16)),'codes':sys_codes},
 'all_bases_minimum':{'distance_sum':best,'mean':str(Fraction(best,16)),'achieving_pairs':best_count,'first':first},
 'claimed_witness':{'storage_rows':list(claimed_storage_rows),'dual_columns':list(claimed_dual_cols),'code':list(claimed_code),'query_table':[{'u':u,'v':v,'raw':queries[4*u+v],'dual':claimed_q[4*u+v],'distance':claimed_d[4*u+v]} for u in range(4) for v in range(4)],'distance_sum':sum(claimed_d),'mean':str(Fraction(sum(claimed_d),16))},
 'claimed_basis_reoptimized':{'distance_sum':claimed_basis_min,'mean':str(Fraction(claimed_basis_min,16)),'codes':claimed_basis_codes},
 'corrected_witness':{'storage_rows':list(corrected_storage_rows),'dual_columns':list(corrected_dual_cols),'code':list(claimed_code),'query_table':[{'u':u,'v':v,'raw':queries[4*u+v],'dual':corrected_q[4*u+v],'distance':corrected_d[4*u+v]} for u in range(4) for v in range(4)],'distance_sum':sum(corrected_d),'mean':str(Fraction(sum(corrected_d),16))}
}
assert gl_count==20160
assert len(codes)==51
assert sys_min==7
assert best==6
assert sum(claimed_d)==8
assert sum(corrected_d)==6
print(json.dumps(result,indent=2))