verify_internal_repair.py

"""Finite syndrome identities and one repair; no universal stability verification."""
from fractions import Fraction
import json

def syndrome(x, s):
    p, a = x.bit_count() % 2, 0
    for j in range(1 << s):
        if x >> j & 1:
            a ^= j
    return p, a

def error(p, a):
    return (1 << a) ^ ((1-p) << 0)

results = []
for s in range(3, 9):
    M = 1 << s
    for p in range(2):
        for a in range(M):
            assert syndrome(error(p, a), s) == (p, a)
    mean_error = Fraction(sum(error(p,a).bit_count()
                              for p in range(2) for a in range(M)), 2*M)
    assert mean_error == Fraction(3,2)-Fraction(1,M)
    total = 0
    for a in range(M):
        for b in range(M):
            defect = error(0,a)^error(0,b)^error(0,a^b)
            expected = 4 if a and b and a != b else 0
            assert defect.bit_count() == expected
            # Exhaust the parity components, which must cancel.
            for p in range(2):
                for q in range(2):
                    assert error(p,a)^error(q,b)^error(p^q,a^b) == defect
            total += defect.bit_count()
    mean_defect = Fraction(total, M*M)
    assert mean_defect == 4*(1-Fraction(1,M))*(1-Fraction(2,M))
    k = s-2
    lower_ratio = (Fraction(k,4)+Fraction(1,2*M))/(mean_defect/2)
    assert lower_ratio >= Fraction(k,8)
    results.append({"s":s, "syndromes":2*M, "ordered_syndrome_pairs":4*M*M,
                    "mean_rounding_weight":str(mean_error),
                    "mean_one_variable_defect":str(mean_defect),
                    "proved_ratio_lower_expression":str(lower_ratio)})

# Exhaust actual input vectors only for C=RM(1,3), an 8-bit code.
s = 3
M = 1 << s
def section(p,a):
    # Use independent check columns at 0, e_1, ..., e_s.
    word = (p ^ (a.bit_count()%2)) << 0
    for j in range(s):
        if a >> j & 1:
            word ^= 1 << (1 << j)
    assert syndrome(word,s) == (p,a)
    return word

total_distance = 0
for x in range(1 << M):
    p,a = syndrome(x,s)
    Fx = x ^ error(p,a)
    Lx = x ^ section(p,a)
    assert syndrome(Fx,s) == (0,0)
    assert syndrome(Lx,s) == (0,0)
    total_distance += (Fx^Lx).bit_count()
actual = Fraction(total_distance,1 << M)/2  # multiply by uniform v_1
k=s-2
assert Fraction(k,4)+Fraction(1,2*M) <= actual
assert actual <= Fraction(k+6,4)-Fraction(1,2*M)

print(json.dumps({
    "scope":"Finite syndrome calculations; not an exhaustive search over bilinear repairs, and not a formal or asymptotic proof.",
    "syndrome_checks":results,
    "small_actual_input_case":{"s":s,"input_vectors":1<<M,
       "mean_bilinear_repair_error_per_copy":str(actual),
       "repair":"One explicit linear syndrome section, not an asserted optimum."},
    "not_checked":["all full Reed-Muller repairs","unused-input/evaluation-slice argument",
                   "full-rank query realizability","unbounded k inequality","query algorithms"]
},indent=2))