verify_compact_affine.py

"""Finite corroboration only; unrestricted proofs are in the companion note."""
import itertools, json
from pathlib import Path

def parity(x): return x.bit_count() & 1
def rank(rows):
    basis = {}
    for x in rows:
        while x:
            k=x.bit_length()-1
            if k in basis: x ^= basis[k]
            else: basis[k]=x; break
    return len(basis)
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))
def build(n, data, right=False):
    clauses=[]; count=2*n
    def fresh():
        nonlocal count
        count+=1; return count
    def pin(a,b): clauses.append((a if b else -a,))
    def AND(a,b,t): clauses.extend([(-t,a),(-t,b),(t,-a,-b)])
    def XOR(a,b,t): clauses.extend([(a,b,-t),(-a,-b,-t),(a,-b,t),(-a,b,t)])
    def chain(xs,target=None):
        z=xs[0]
        for i,a in enumerate(xs[1:],1):
            t=target if i==len(xs)-1 and target else fresh()
            XOR(z,a,t); z=t
        return z
    if right:
        u,v=data
        for j in range(n): pin(j+1,v>>j&1)
        terms=[]
        for i in range(n):
            c=fresh(); pin(c,u>>i&1); z=fresh(); AND(c,n+i+1,z); terms.append(z)
        pin(chain(terms),1)
    else:
        for i in range(n):
            terms=[]
            for j in range(n):
                c=fresh(); pin(c,data>>(i*n+j)&1); z=fresh(); AND(c,j+1,z); terms.append(z)
            chain(terms,n+i+1)
    return count,clauses

def projection(n, pair):
    count,clauses=pair; good=set()
    for bits in range(1<<count):
        if all(any(bool(bits>>(abs(l)-1)&1)==(l>0) for l in c) for c in clauses):
            good.add(bits&((1<<(2*n))-1))
    return good

n=2
left={a:projection(n,build(n,a)) for a in range(16)}
right={(u,v):projection(n,build(n,(u,v),True)) for u in range(4) for v in range(4)}
for a in range(16):
    expected={x | sum(parity((a>>(i*n)&3)&x) << (n+i) for i in range(n)) for x in range(4)}
    assert left[a]==expected
    for u,v in right:
        assert bool(left[a]&right[u,v])==bool(parity(a&qmask(u,v,n)))
for u,v in right:
    assert right[u,v]=={v|(y<<n) for y in range(4) if parity(u&y)}
    # Remove only final parity-output pin: every matrix has an extension.
    count,cs=build(n,(u,v),True)
    unpinned=projection(n,(count,cs[:-1]))
    assert all(left[a]&unpinned for a in left)
counts=[]
for n in range(2,9):
    vf,cf=build(n,0); vg,cg=build(n,(0,0),True)
    assert (vf,len(cf),sum(map(len,cf)))==(3*n*n,8*n*n-4*n,20*n*n-12*n)
    assert (vg,len(cg),sum(map(len,cg)))==(5*n-1,9*n-3,21*n-11)
    counts.append({'n':n,'left_variables':vf,'left_clauses':len(cf),'right_variables':vg,'right_clauses':len(cg)})
qs=[qmask(u,v,2) for u in range(4) for v in range(4)]
checked=0; min_worst=4
for rows in itertools.product(range(16),repeat=4):
    if rank(rows)!=4: continue
    weights=[sum(parity(row&q) for row in rows) for q in qs]
    assert sum(weights)>=16
    for row in rows:
        r=rank([row&3,row>>2])
        assert sum(parity(row&q) for q in qs)==8-(8>>r)
    min_worst=min(min_worst,max(weights)); checked+=1
result={'status':'passed','scope':'Finite exhaustive checks, not formal or unrestricted proof','dimension_2':{'matrix_query_pairs':256,'invertible_coefficient_maps':checked,'minimum_worst_support':min_worst,'cnf_projection':'all boundary and private assignments','negative_control':'removing output pin makes every join satisfiable'},'formula_counts':counts,'randomness':'none'}
Path(__file__).with_name('compact-affine-output.json').write_text(json.dumps(result,indent=2)+'\n')
print(json.dumps(result))