verify_linear_storage_limits.py

"""Finite checks only: product encoders and sparse random-test identity."""
from fractions import Fraction
from itertools import product
from pathlib import Path
import json

def rank(rows):
    b={}
    for x in rows:
        while x:
            k=x.bit_length()-1
            if k in b: x^=b[k]
            else: b[k]=x; break
    return len(b)
def apply(rows,c):
    x=0
    for i,row in enumerate(rows):
        if c>>i&1: x^=row
    return x
checks=[]
for n in [2,3]:
    total=0; best=n*(n+1)
    for rows in product(range(1<<n),repeat=n+1):
        if rank(rows)!=n: continue
        fibers={v:[] for v in range(1<<n)}
        for c in range(1<<(n+1)): fibers[apply(rows,c)].append(c)
        assert all(len(x)==2 for x in fibers.values())
        ker=next(c for c in fibers[0] if c)
        h=ker.bit_count()
        worst=max(min(c.bit_count() for c in cs) for cs in fibers.values())
        assert worst==n+1-(h+1)//2
        best=min(best,n*worst);total+=1
    assert best==n*((n+1)//2)
    checks.append({'n':n,'all_full_rank_Q_checked':total,'minimum_product_worst_cost':best})
prob_checks=0
for S in range(2,7):
    dist={0:Fraction(1)}
    for t in range(1,5):
        nxt={}
        for mask,p in dist.items():
            nxt[mask]=nxt.get(mask,0)+p/2
            for j in range(S):
                x=mask^(1<<j);nxt[x]=nxt.get(x,0)+p/(2*S)
        dist=nxt
        for z in range(1,1<<S):
            observed=sum(p for x,p in dist.items() if (x&z).bit_count()%2)
            expected=(1-(1-Fraction(z.bit_count(),S))**t)/2
            assert observed==expected
            prob_checks+=1
out={'status':'passed','scope':'Exhaustive one-factor product fiber costs n=2,3 and exact rational sparse-test probabilities S=2..6,t=1..4. Not a formal or asymptotic proof; no random large-code witness constructed.','product_checks':checks,'probability_checks':prob_checks}
Path(__file__).with_name('linear-storage-limits-output.json').write_text(json.dumps(out,indent=2)+'\n')
print(json.dumps(out))