verify-move-defect.py

"""Exact rational controls for the local move defect; no external packages.

The generic proof is in the accompanying note. Rational evaluations are
regression controls, not a substitute for that proof or global topology.
Run: python3 verify-move-defect.py
"""
from fractions import Fraction as F
from itertools import product
import json

C = [(-1,-1,0,0,0,1), (0,0,0,1,-1,-1),
     (0,1,0,0,-1,-1), (-1,-1,0,1,0,0)]
h = (1,0,1,0,1,0)
def omega(u,v):
    return sum(u[2*t+1]*v[2*t]-u[2*t]*v[2*t+1] for t in range(3))
def add(a,b): return tuple(x+y for x,y in zip(a,b))
def basis(t): return tuple(int(i==t) for i in range(3))
def poch(q,n):
    out=F(1)
    for j in range(1,n+1): out*=1-q**j
    return out
def ell(q,s,a,b):
    d=tuple(-x-y for x,y in zip(s,b))
    if min(d)<0: return F(0)
    den=F(1)
    for n in d: den*=poch(q,n)
    return q**sum(x*y for x,y in zip(s,a))/den
def nf(q,a,b):
    n=-1-sum(b)
    if n<0: return {}
    out={}
    for d1 in range(n+1):
        for d2 in range(n-d1+1):
            d=(d1,d2,n-d1-d2); beta=add(b,d)
            out[beta]=ell(q,tuple(-x for x in beta),a,b)
    return out
def scaled(v,c): return {k:x*c for k,x in v.items() if x*c}
def lin(*vs):
    out={}
    for v in vs:
        for k,x in v.items(): out[k]=out.get(k,F(0))+x
    return {k:x for k,x in out.items() if x}
def action(j,b):
    a=C[j][::2]; d=C[j][1::2]
    return add(b,d),1-sum(x*y for x,y in zip(a,add(b,d)))
def rootell(A,s,u):
    # Ordered z_1^r_1 w_1^t_1 ...; primitive edge P=z_1 z_2 z_3.
    eps=u[0]%2
    if any(u[2*t]%2!=eps or u[2*t+1]%2 for t in range(3)): return F(0)
    a=tuple((u[2*t]-eps)//2 for t in range(3))
    b=tuple(u[2*t+1]//2 for t in range(3))
    return (-A**2)**eps*ell(A**4,s,a,b)

# Sparse Laurent polynomials in q and the ordered noncommuting generators.
def term(a=(0,0,0),b=(0,0,0),k=0,c=1): return {(tuple(a),tuple(b),k):c}
def mul(p,r):
    out={}
    for (a,b,k),x in p.items():
        for (c,d,l),y in r.items():
            key=(add(a,c),add(b,d),k+l+sum(i*j for i,j in zip(b,c)))
            out[key]=out.get(key,0)+x*y
    return {k:v for k,v in out.items() if v}

def main():
    counts={}
    def check(name,condition):
        assert condition,name
        counts[name]=counts.get(name,0)+1
    expected=((0,-1,0,0),(1,0,0,0),(0,0,0,-1),(0,0,1,0))
    check('symplectic_columns',tuple(tuple(omega(x,y) for y in C) for x in C)==expected)
    check('new_edge_centralizes_image',all(omega(h,c)==0 for c in C))
    zero=(0,0,0)
    fs=[lin(term(tuple(-x for x in basis(t))),term(b=basis(t)),term(c=-1)) for t in range(3)]
    # Formula (4), with literal left tetrahedron and right edge multiples.
    lhs=lin(term((1,0,0),(1,0,-1),c=-1),term((0,0,-1),(0,1,-1),k=1,c=-1),term(c=-1))
    edge=lin(term((1,1,1)),term(k=1,c=-1))
    rhs=lin(mul(term((1,0,0),(0,0,-1),c=-1),fs[0]),
            mul(term((0,0,-1),(0,0,-1),k=1,c=-1),fs[1]),
            mul(term(b=(0,0,-1),c=-1),fs[2]),
            scaled(mul(edge,term((0,-1,-1),(0,0,-1))),-1))
    check('generic_correct_sided_move_certificate',lhs==rhs)
    # Explicit integral inverse on ker(sum of local w exponents).
    for ax,bx,ay,by,av in product(range(-1,2),repeat=5):
        v=(ax,bx,ay,by,av,-bx-by)
        coeff=(ay-by-bx-av,ax-bx-av,ay+bx-ax,by-ax+bx+av,ay)
        rebuilt=tuple(sum(k*c[i] for k,c in zip(coeff,C+[h])) for i in range(6))
        check('unsaturated_lattice_inverse',rebuilt==v)
    for q in map(F,[2,F(2,3),F(3,2)]):
        for a in product(range(-1,2),repeat=3):
            for b in product(range(-1,2),repeat=3):
                v=nf(q,a,b)
                check('squared_edge_side',nf(q,add(a,(1,1,1)),b)==scaled(v,q))
                for t in range(3):
                    am=list(a);am[t]-=1
                    check('tetrahedron_side',not lin(scaled(nf(q,am,b),q**(-b[t])),nf(q,a,add(b,basis(t))),scaled(v,-1)))
        for b1,b2 in product(range(-2,3),repeat=2):
            b=(b1,b2,-1-b1-b2)
            check('resonant_basis',nf(q,(0,0,0),b)=={b:F(1)})
            for i,j in product(range(4),repeat=2):
                bj,ej=action(j,b); bij,ei=action(i,bj)
                bi,ei0=action(i,b); bji,ej0=action(j,bi)
                check('symbolic_q_commutation',bij==bji and ei+ej-ei0-ej0==expected[i][j])
    for A in [F(2),F(3,2)]:
        for s1,s2 in product(range(-1,2),repeat=2):
            s=(s1,s2,1-s1-s2)
            for u in product(range(-1,2),repeat=6):
                val=rootell(A,s,u)
                check('primitive_edge_side',rootell(A,s,add(u,h))==-A**2*val)
                for t in range(3):
                    um=list(u);um[2*t]-=2
                    up=list(u);up[2*t+1]+=2
                    check('root_tetrahedron_side',A**(-2*u[2*t+1])*rootell(A,s,um)+rootell(A,s,up)-val==0)
    result={'status':'passed','checks':counts,
      'exact_local_result':'cokernel basis beta in Z^3 with sum(beta)=-1',
      'explicit_witness':'ell_(1,0,0)(W_1^-1)=1; vanishes on move image',
      'limitations':['Local algebra only; no outer-edge descent asserted.',
                    'No generic native index identification with ell_s.',
                    'Finite rational checks are not a formal-language proof.']}
    print(json.dumps(result,indent=2))
if __name__=='__main__': main()