verify-minimal-quotient.py

#!/usr/bin/env python3
"""Exact finite trace-kernel certificate and independent checks; standard library only."""
from pathlib import Path
from fractions import Fraction as F
import json

ROOT=Path(__file__).resolve().parent
checks=[]
def check(name,ok):
    assert ok,name
    checks.append(name)
zero=(0,0,0,0)
h=(1,1,-1,-1)
a=(1,0,0,-1)
def av(u,v): return tuple(x+y for x,y in zip(u,v))
def sv(n,u): return tuple(n*x for x in u)
def om(u,v): return sum(u[j+2]*v[j]-u[j]*v[j+2] for j in range(2))
def mon(u=zero,p=0,c=1): return {(u,F(p)):c}
def add(*ps):
    d={}
    for p in ps:
        for k,c in p.items(): d[k]=d.get(k,0)+c
    return {k:c for k,c in d.items() if c}
def neg(p): return {k:-c for k,c in p.items()}
def mul(p,q):
    d={}
    for (u,x),c in p.items():
        for (v,y),b in q.items():
            k=(av(u,v),x+y+F(om(u,v),2))
            d[k]=d.get(k,0)+c*b
    return {k:c for k,c in d.items() if c}
def sc(p,n,c=1): return mul(mon(p=n,c=c),p)
def norm(p):
    out={}
    for (u,x),c in p.items():
        e=u[1]; k=av(u,sv(-e,h))
        out=add(out,mon(k,x-F(om(sv(e,h),k),2),c))
    return out
def same(p,q): return norm(add(p,neg(q)))=={}
one=mon()
f0=add(mon((-2,0,0,0)),mon((0,0,2,0)),neg(one))
f1=add(mon((0,-2,0,0)),mon((0,0,0,2)),neg(one))
S=add(mon(sv(2,a)),mon(sv(-2,a)))
v1=sc(add(mon((-2,0,0,2)),mon((0,-2,2,0)),mon((0,0,2,2))),-2,-1)
# Z'_j = -A^2 W(-2 e_zj -2 e_wj).
Zp=mon((-2,0,-2,0),2,-1); Zpi=mon((2,0,2,0),-2,-1)
Yp=mon((0,-2,0,-2),2,-1); Ypi=mon((0,2,0,2),-2,-1)
v2=add(sc(mul(Zpi,Ypi),-8),sc(add(mul(Zp,Ypi),mul(Zpi,Yp)),-4),
       sc(add(Zpi,Ypi),-4,-1),sc(add(Zpi,Ypi),-8,-1),mon(p=-8),one)
P=add(v2,sc(mul(add(S,one),v1),-2),sc(add(S,mon(c=2)),-4),neg(one))
left0=mon((0,0,2,4),-4)
left1=mon((0,0,2,2),-4)
left2=mul(mon(sv(2,a),-8),mon((0,0,0,2)))
G=add(mul(left0,f0),mul(left1,f1),mul(left2,f0))
check('GY candidate kernel identity:',same(P,G))


# Native PP source formulas transported by Z -> w1^2, Y -> w0^2,
# Z'' -> z1^2, Y'' -> z0^2 (the retained marking reversal).
pp1=sc(add(mon((-2,0,0,2)),mon((0,0,2,0))),1)
pp2=add(sc(add(mul(Zpi,Yp),mul(Zp,Ypi)),4),mul(Zpi,Ypi),
        sc(add(Zpi,Ypi),4,-1),neg(add(Zpi,Ypi)),mon(c=2))
# A negative ribbon twist on the 2-cable has eigenvalues A^-8 and 1
# on the 2nd Jones-Wenzl summand and the trivial summand, respectively.
pp2zero=add(sc(add(pp2,neg(one)),-8),one)
check('2-cable framing correction is exactly GY Eq100:',pp2zero==v2)
check('1-cable framing correction differs by a tetrahedron multiple:',
      add(sc(pp1,-3,-1),neg(v1))==mul(mon((0,0,2,0),-2),f1))

# All original relations use squared edge, hence no opposite-root sign
# specialization is needed for the derived finite relation itself.
def quotient(row,n):
    return add(*(mon(sv(j,row),c=1 if n>=0 else -1)
                 for j in (range(n) if n>=0 else range(n,0))))
U={}
for (u,x),c in add(P,neg(G)).items():
    e=u[1]; assert e%2==0
    k=av(u,sv(-e,h))
    U=add(U,mul(mon(p=x-F(om(sv(e,h),k),2),c=c),mul(quotient(sv(2,h),e//2),mon(k))))
E2=add(mon(sv(2,h)),neg(one))
check('full finite squared-edge identity:',P==add(G,mul(E2,U)))
delta=add(mon(p=2,c=-1),mon(p=-2,c=-1))
d2=mul(delta,delta)
pk=add(d2,sc(mul(add(d2,neg(one)),delta),-2),sc(d2,-4),neg(one))
check('filled bracket is A^-4:',pk==mon(p=-4))


# Use the published native PP expression directly, not the identified formula.
vnative=sc(pp1,-3,-1)
Pnative=add(pp2zero,sc(mul(add(S,one),vnative),-2),sc(add(S,mon(c=2)),-4),neg(one))
left3=sc(mul(add(S,one),mon((0,0,2,0))),-4)
L0=add(left0,left2); L1=add(left1,left3)
check('published native representatives satisfy finite certificate',
      Pnative==add(mul(L0,f0),mul(L1,f1),mul(E2,U)))
check('every certificate monomial is even',all(all(x%2==0 for x in u) for p in [L0,L1,U,E2,Pnative] for u,d in p))
check('meridian operator commutes with edge',om(a,h)==0)
# Independent oracle: ordered z0^r z1^s w0^t w1^u multiplication.
def pbw(p):
    return add(*(mon(u,x+F(u[0]*u[2]+u[1]*u[3],2),c) for (u,x),c in p.items()))
def pmul(p,q):
    return add(*(mon(av(u,v),x+y+u[2]*v[0]+u[3]*v[1],c*b)
        for (u,x),c in p.items() for (v,y),b in q.items()))
check('independent ordered-product oracle verifies native identity',
      pbw(Pnative)==add(pmul(pbw(L0),pbw(f0)),pmul(pbw(L1),pbw(f1)),pmul(pbw(E2),pbw(U))))
# Direct 2-strand TL calculation: e^2=delta e, crossing=A*1+A^-1*e.
def tlmul(x,y):
    return (mul(x[0],y[0]),add(mul(x[0],y[1]),mul(x[1],y[0]),mul(delta,mul(x[1],y[1]))))
cross=(mon(p=1),mon(p=-1))
fulltwist=tlmul(cross,cross)
fulltwist=tuple(sc(x,6) for x in fulltwist) # two individual ribbon twists
check('two-cable twist has A^8 on the through summand',fulltwist[0]==mon(p=8))
check('two-cable twist has 1 on the trivial summand',add(fulltwist[0],mul(delta,fulltwist[1]))==one)
check('closed two-cable framing identity',add(mul(fulltwist[0],d2),mul(fulltwist[1],delta))==add(sc(add(d2,neg(one)),8),one))
# One parity character gives the obstruction without listing sectors.
w=(0,0,1,-1)
def eta(u):return (u[1]+u[2])%2
check('unused parity is zero on edge and meridian, one on witness',eta(h)==eta(a)==0 and eta(w)==1)
check('witness insertion preserves the edge relation',om(w,h)==0)
check('actual basis images have even unused parity',all(eta(u)==0 for p in [one,vnative,pp2zero,mon(a),mon(sv(-1,a))] for u,d in p))
check('translated witness evaluates to the unit before averaging',mul(mon(sv(-1,w)),mon(w))==one)
# Exact q^(1/2) coefficients of the single detecting series. The proven
# outer tail is 8*k^2+4*abs(k) in A-degree; this truncation is only a control.
TMAX=12
def seed(m,e,cut):
    out={}; n=max(-e,0)
    while True:
        shift=n*(n+1)-(2*n+e)*m
        if shift>cut and n>=m:break
        if shift<=cut:
            bound=cut-shift; den=[0]*(bound+1); den[0]=1
            for length in [n,n+e]:
                for j in range(1,length+1):
                    for d in range(2*j,bound+1):den[d]+=den[d-2*j]
            for d,c in enumerate(den):
                if c:out[d+shift]=out.get(d+shift,0)+(-1)**n*c
        n+=1
    return {d:c for d,c in out.items() if c}
series={}
K=0
while 4*(K+1)**2+2*(K+1)<=TMAX:K+=1
for k in range(-K,K+1):
    s=seed(-k,-k,TMAX+2)
    check('minimum degree of squared summand k='+str(k),2*min(s)==4*k*k+2*abs(k))
    for x,c in s.items():
        for y,d in s.items():
            if x+y<=TMAX:series[x+y]=series.get(x+y,0)+c*d
series={d:c for d,c in series.items() if c}
check('detector unit constant is one',series.get(0)==1 and min(series)==0)
def enc(p):return [{'root':list(u),'A_degree':str(x),'coefficient':c} for (u,x),c in sorted(p.items())]
certificate={'ring':'Q(i,A^(1/2))','identity':'P_native=L0*f0+L1*f1+(W(2h)-1)*U',
 'h':h,'a':a,'P_native':enc(Pnative),'L0':enc(L0),'L1':enc(L1),'U':enc(U),
 'f0':enc(f0),'f1':enc(f1),'E2':enc(E2),'filled_bracket':enc(pk)}
(ROOT/'kernel-certificate.json').write_text(json.dumps(certificate,indent=2)+'\n')
result={'status':'passed','checks':checks,'count':len(checks),
 'F_unit_in_q_half_powers':{str(d):c for d,c in sorted(series.items())},
 'cutoff_q_half_degree':TMAX,'outer_tail_q_half_degree':4*(K+1)**2+2*(K+1),
 'scope':'Finite native identity, correct module sides, cable framing, parity and a certified coefficient control. Published geometric trace formulas and the named-action theorem are proof dependencies.'}
(ROOT/'exact-results.json').write_text(json.dumps(result,indent=2)+'\n')
print(json.dumps(result,indent=2))