verify_covering_composition.py

"""Finite evidence only; no asymptotic theorem or general code synthesis certified."""
import json
from math import isqrt
from pathlib import Path

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

def rm_words(k):
    L = 1 << k
    rows = [(1 << L)-1]
    rows += [sum(((x >> j) & 1) << x for x in range(L)) for j in range(k)]
    words = [0]
    for row in rows: words += [w ^ row for w in words]
    return rows, words

rm_checks = []
for k in [1, 2, 3, 4]:
    L = 1 << k
    rows, words = rm_words(k)
    worst = max(min((f ^ c).bit_count() for c in words) for f in range(1 << L))
    ceilroot = isqrt(L) + (isqrt(L)**2 < L)
    bound = (L-ceilroot)//2
    assert worst <= bound
    rm_checks.append(dict(k=k, length=L, all_words=1 << L, radius=worst, bound=bound))

greedy = []
for S, dim, R in [(8, 5, 3), (10, 6, 3)]:
    universe = set(range(1 << S))
    ball = {x for x in universe if x.bit_count() <= R}
    assert (len(ball) << dim) >= S * (1 << S)
    code = {0}; U = universe-ball; sizes = [len(U)]
    for _ in range(dim):
        if not U: break
        counts = [sum((x ^ g) in U for x in U) for g in universe]
        assert sum(counts) == len(U)**2
        g = min(range(1 << S), key=lambda i: counts[i])
        nxt = {x for x in U if (x ^ g) in U}
        assert len(nxt)*(1 << S) <= len(U)**2
        code |= {x ^ g for x in code}
        U = nxt; sizes.append(len(U))
    assert not U
    assert max(min((x ^ c).bit_count() for c in code) for x in universe) <= R
    greedy.append(dict(S=S, dimension_budget=dim, R=R, uncovered_sizes=sizes))

# Complete n=8 construction, with a public quotient and right inverse.
n = 8; S = n*n+n; d = n*n
block_rows, block_words = rm_words(6)
K = block_rows + [((1 << 8)-1) << 64]
assert len(basis(K)) == n
kb = basis(K)
pi = []
for j in range(S):
    if j in kb: continue
    z = 1 << j
    for p in sorted(kb):
        if (kb[p] & z).bit_count() % 2: z ^= 1 << p
    pi.append(z)
assert len(pi) == d and len(basis(pi)) == d
assert all((x & y).bit_count() % 2 == 0 for x in pi for y in K)
columns = [sum(((row >> j) & 1) << i for i, row in enumerate(pi)) for j in range(S)]
cb = {}
for j, q in enumerate(columns):
    lift = 1 << j
    while q:
        p = q.bit_length()-1
        if p in cb: q ^= cb[p][0]; lift ^= cb[p][1]
        else: cb[p] = (q, lift); break
def lift(q):
    a = 0
    while q:
        p = q.bit_length()-1
        q ^= cb[p][0]; a ^= cb[p][1]
    return a
def project(a):
    return sum(((row & a).bit_count() % 2) << i for i, row in enumerate(pi))
max_cost = 0; count = 0
for u in range(1 << n):
    for v in range(1 << n):
        q = sum(v << (n*i) for i in range(n) if (u >> i) & 1)
        a = lift(q)
        low = a & ((1 << 64)-1)
        c = min(block_words, key=lambda x: (low ^ x).bit_count())
        a ^= c
        if (a >> 64).bit_count() > 4: a ^= K[-1]
        assert project(a) == q
        assert a.bit_count() <= 32
        max_cost = max(max_cost, a.bit_count()); count += 1

sizes = []
for n in [16, 32, 64, 128, 256]:
    S = n*n+n
    # Stronger rational sufficient condition 2^n p >= S.
    term = 1; volume = 0
    for R in range(S+1):
        volume += term
        if (volume << n) >= S*(1 << S): break
        term = term*(S-R)//(R+1)
    assert (volume << n) >= S*(1 << S)
    assert ((volume-term) << n) < S*(1 << S)
    e = S.bit_length()-1; B = (n-1)//(e+1)
    L = 1 << ((S//B).bit_length()-1); r = S-B*L
    k = L.bit_length()-1
    assert B*(k+1)+(r>0) <= n
    ceilroot = isqrt(L)+(isqrt(L)**2 < L)
    explicit = B*((L-ceilroot)//2)+r//2
    if n >= 64: assert explicit < n*n/2
    sizes.append(dict(n=n,S=S,cohen_integer_sufficient_R=R,RM_bound=explicit,
                      product_optimum=n*((n+1)//2),B=B,L=L,tail=r))

out = dict(status="passed",scope="Finite evidence: exhaustive RM words for k=1..4; two full greedy-cover examples; n=8 quotient/decoder checked for all 65536 pairs u,v; exact integer covering conditions at n=16,32,64,128,256. No formal or asymptotic verification; no large Cohen witness synthesized.",
           RM_checks=rm_checks,greedy_examples=greedy,
           constructed_encoding=dict(n=8,S=72,query_pairs=count,max_observed_cost=max_cost,proved_bound=32),
           parameter_checks=sizes)
Path(__file__).with_name("covering-composition-output.json").write_text(json.dumps(out,indent=2)+"\n")
print(json.dumps(out))