verify_short_dependencies.py

"""Exact n=2 counterexample only. Not verification of the asymptotic proof."""
import itertools
import json

# P columns: first row entries/parity, second row entries/parity.
columns = [1, 2, 3, 4, 8, 12]
def syndrome(a):
    q = 0
    for j, col in enumerate(columns):
        if (a >> j) & 1:
            q ^= col
    return q
fibers = {q: [a for a in range(64) if syndrome(a) == q] for q in range(16)}
def query(u, v):
    return (v if u & 1 else 0) ^ ((v << 2) if u & 2 else 0)
def lift(u, v, basis):
    a = 0
    for i in range(2):
        for j in range(2):
            if ((u >> i) & 1) and ((v >> j) & 1):
                a ^= basis[2*i+j]
    return a
costs = [min(a.bit_count() for a in fibers[query(u,v)])
         for u in range(4) for v in range(4)]
counts = {}
for basis in itertools.product(*(fibers[1 << j] for j in range(4))):
    vals = [lift(u,v,basis) for u in range(4) for v in range(4)]
    assert all(syndrome(lift(u,v,basis)) == query(u,v)
               for u in range(4) for v in range(4))
    worst = max(a.bit_count() for a in vals)
    counts[worst] = counts.get(worst, 0) + 1
fixed_slice = []
for a,b in itertools.product(fibers[query(3,1)], fibers[query(3,2)]):
    fixed_slice.append(max(a.bit_count(),b.bit_count(),(a^b).bit_count()))
assert max(costs) == 2
assert min(counts) == 3
assert sum(counts.values()) == 256
assert min(fixed_slice) == 3
kernel = fibers[0]
assert min(a.bit_count() for a in kernel if a) == 3
# Single-row minimum leaders have a weight-three additivity defect.
assert syndrome(1 ^ 2 ^ 4) == 0 and (1 ^ 2 ^ 4).bit_count() == 3
print(json.dumps({"scope": "Exhaustive n=2 row-parity counterexample only; no formal or asymptotic verification",
 "storage_bits":6, "patterns_examined":64, "kernel":kernel,
 "kernel_minimum_distance":3, "optimal_arbitrary_selector_cost":max(costs),
 "bilinear_selector_count":256, "bilinear_worst_cost_distribution":counts,
 "optimal_bilinear_selector_cost":min(counts),
 "optimal_fixed_u_11_linear_selector_cost":min(fixed_slice)}, indent=2))