verify_repair_space_obstruction.py

"""Finite RM restrictions/flat checks; not a proof of asymptotic access bounds."""
import json
from itertools import combinations
from math import comb
from fractions import Fraction

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

def rows_rm(m, k):
    return [sum(1 << x for x in range(1 << m) if x & mask == mask)
            for mask in range(1 << m) if mask.bit_count() <= k]

# Small independent instance, not m=10k used in the asymptotic family.
m, k = 4, 2
length = 1 << m
rows = rows_rm(m, k)
code = [0]
for row in rows:
    code += [x ^ row for x in code]
assert len(set(code)) == 1 << sum(comb(m, i) for i in range(k+1))
assert min(x.bit_count() for x in code if x) == 1 << (m-k)

# Enumerate affine codimension-two flats by independent normal vectors.
flats = set()
for a, b in combinations(range(1, length), 2):
    for c in range(2):
        for e in range(2):
            flat = sum(1 << x for x in range(length)
                       if (a & x).bit_count() % 2 == c
                       and (b & x).bit_count() % 2 == e)
            flats.add(flat)
assert flats <= set(code)
assert all(x.bit_count() == 1 << (m-k) for x in flats)
p = Fraction((1 << (m-k))-1, length-1)
for x in range(length):
    through = [f for f in flats if f >> x & 1]
    for y in range(length):
        if y != x:
            assert Fraction(sum(f >> y & 1 for f in through), len(through)) == p

small = proper = 0
threshold = Fraction(1 << (k+1), 1) / (1 + ((1 << (k+1))-1)*p)
for B in range(1, 1 << length):
    t = B.bit_count()
    r = rank([row & B for row in rows])
    if t < 1 << (k+1):
        assert r == t
        small += 1
    short = min((f & B).bit_count() for f in flats if f & B)
    assert short <= 1+(t-1)*p
    if r < t:
        assert t >= 1 << (k+1)
        assert Fraction(t, short) >= threshold
        proper += 1

dimensions = []
for j in range(1, 11):
    dim = sum(comb(10*j, i) for i in range(j+1))
    assert dim < 1 << (5*j)
    dimensions.append({"k": j, "dimension": dim, "advice_budget": 1 << (5*j)})

print(json.dumps({
    "scope": "Finite RM(2,4) restriction and affine-flat checks; no formal or asymptotic query verification.",
    "coordinates": length, "dimension": rank(rows), "codewords": len(code),
    "minimum_weight": min(x.bit_count() for x in code if x),
    "affine_flats": len(flats), "pair_probability": str(p),
    "nonempty_retained_sets": (1 << length)-1,
    "small_full_restrictions": small, "proper_restrictions": proper,
    "proper_block_aspect_lower_bound": str(threshold),
    "dimension_checks": dimensions,
    "not_checked": ["all containing codes or partitions by enumeration",
                    "adaptive algorithms", "unbounded theorem", "general correction lemma"]
}, indent=2))