verify_compact_affine_redundancy.py

"""Finite checks for the row-parity construction and selected volume bounds.
No unrestricted lower-bound proof or machine implementation is checked.
"""
import json, math
from pathlib import Path

def qmask(u,v,n):
    return sum(((u>>i&1)*(v>>j&1)) << (i*n+j) for i in range(n) for j in range(n))

rows=[]
for n in range(2,7):
    worst=0; checked=0
    for u in range(1<<n):
        for v in range(1<<n):
            selected=[]
            k=v.bit_count()
            for i in range(n):
                if not(u>>i&1): continue
                if k<=1+n-k:
                    selected.extend(1<<(i*n+j) for j in range(n) if v>>j&1)
                else:
                    selected.append(((1<<n)-1)<<(i*n))
                    selected.extend(1<<(i*n+j) for j in range(n) if not(v>>j&1))
            actual=0
            for a in selected: actual ^= a
            assert actual==qmask(u,v,n)
            assert len(selected)==u.bit_count()*min(k,1+n-k)
            worst=max(worst,len(selected)); checked+=1
    assert worst==n*((n+1)//2)
    rows.append({'n':n,'all_queries_checked':checked,'maximum_probes':worst})
# Powers of two make h exact using integer arithmetic (no rounded logs).
volumes=[]
for ell in range(6,13):
    n=1<<ell; k=n*n//2; h=(2*n+ell-1)//ell
    c=math.comb(k,h)
    assert c>1<<n
    assert h*ell<=3*n
    volumes.append({'n':n,'k':k,'h':h,'binomial_bit_length':c.bit_length(),'required_bit_length_greater_than':n})
out={'status':'passed','scope':'Finite construction identities n=2..6 and volume inequalities at powers of two 64..4096; not an unrestricted or formal lower-bound proof','row_parity':rows,'volume_checks':volumes}
Path(__file__).with_name('compact-affine-redundancy-output.json').write_text(json.dumps(out,indent=2)+'\n')
print(json.dumps(out))