#!/usr/bin/env python3
"""Finite Weyl-algebra certificate over a formal central involution ring.

No sign assignments, triangulations, or slopes are enumerated. Central masks
are monomials in k[e,z]/(e^2-1,z^2-1), not evaluations of e and z.
Only Python's standard library is required.
"""
from fractions import Fraction as F
from pathlib import Path
import json

ROOT = Path(__file__).resolve().parent
checks = []
zero = (0, 0, 0, 0)
h = (-1, -1, 1, 1)
s = (-1, 0, 0, 1)
v = (-4, 0, 4, 0)

def check(name, value):
    assert value, name
    checks.append(name)

def addv(u, v): return tuple(a+b for a, b in zip(u, v))
def scale(n, u): return tuple(n*a for a in u)
def omega(u, v): return sum(u[j+2]*v[j]-u[j]*v[j+2] for j in range(2))
def ga(a, b): return a[0]+b[0], a[1]+b[1]
def gm(a, b): return a[0]*b[0]-a[1]*b[1], a[0]*b[1]+a[1]*b[0]
def ipow(n): return ((1,0),(0,1),(-1,0),(0,-1))[n % 4]
def mon(u=zero, power=0, c=(1,0), mask=0): return {(u,F(power),mask):c}
def plus(*ps):
    out = {}
    for p in ps:
        for k,c in p.items(): out[k] = ga(out.get(k,(0,0)),c)
    return {k:c for k,c in out.items() if c != (0,0)}
def neg(p): return {k:(-c[0],-c[1]) for k,c in p.items()}
def times(p,q):
    out = {}
    for (u,a,mask),c in p.items():
        for (v,b,nask),d in q.items():
            k = (addv(u,v),a+b+F(omega(u,v),2),mask ^ nask)
            out[k] = ga(out.get(k,(0,0)),gm(c,d))
    return {k:c for k,c in out.items() if c != (0,0)}

one = mon()
f1 = plus(mon((-2,0,0,0)),mon((0,0,2,0)),neg(one))
f2 = plus(mon((0,-2,0,0)),mon((0,0,0,2)),neg(one))
vac = plus(one,neg(mon(v)))
E2 = plus(mon(scale(2,h)),neg(one))
M2 = plus(mon(scale(2,s)),neg(mon(power=4)))
eps,zet = mon(mask=1),mon(mask=2)
E = plus(mon(h),neg(eps))
M = plus(mon(s),mon(power=2,mask=2))
check('central involutions are formal coefficients',times(eps,eps)==one and times(zet,zet)==one and eps!=one and zet!=one)
check('moment rows commute',omega(h,s)==0)
check('squared edge is a correct-sided consequence',times(E,plus(mon(h),eps))==E2)
check('squared meridian is a correct-sided consequence',times(M,plus(mon(s),neg(mon(power=2,mask=2))))==M2)

# Eight left tetrahedron multiples, inherited as an algebraic starting point.
terms=[(1,1,1,4,1),(2,2,0,4,-1),(1,1,0,4,-1),
       (1,0,2,4,1),(2,1,1,4,-1),(2,0,1,4,1),
       (1,0,1,0,-1),(2,1,0,0,1)]
G={}
lefts=[]
for j,r,t,a,c in terms:
    left=mon((0,0,2*r+2,2*t-2),a,(c,0))
    lefts.append((j,left))
    G=plus(G,times(left,f1 if j==1 else f2))

def normalize_even(p):
    out={}
    for (u,a,mask),c in p.items():
        z1,z2,w1,w2=u
        assert z1%2==0 and z2%2==0
        e,n=-z2,-z1+z2
        k=(0,0,w1+z2,w2+z1)
        lam=addv(scale(e,h),scale(n,s))
        assert addv(lam,k)==u and e%2==n%2==0
        # Both central involutions appear to even powers and disappear here.
        out=plus(out,mon(k,a-F(omega(lam,k),2)+2*n,c,mask))
    return out
check('the squared moment normal form gives the required vacuum',normalize_even(vac)==plus(one,neg(mon((0,0,4,-4)))))
check('eight tetrahedron multiples normalize to the vacuum',normalize_even(G)==normalize_even(vac))

def power_quotient(row,n,power):
    """Exact (W(row)^n-A^(power*n))/(W(row)-A^power)."""
    js=range(n) if n>=0 else range(n,0)
    sign=1 if n>=0 else -1
    return plus(*(mon(scale(j,row),power*(n-1-j),(sign,0)) for j in js))

# Factor the residual using squared moments only, not any specialized sign.
U,V={},{}
residual=plus(vac,neg(G))
for (u,a,mask),c in residual.items():
    z1,z2,w1,w2=u
    e,n=-z2,-z1+z2
    assert e%2==n%2==0
    k=(0,0,w1+z2,w2+z1)
    lam=addv(scale(e,h),scale(n,s))
    pref=mon(power=a-F(omega(lam,k),2),c=c,mask=mask)
    U=plus(U,times(times(times(pref,power_quotient(scale(2,h),e//2,0)),mon(scale(n,s))),mon(k)))
    V=plus(V,times(times(pref,power_quotient(scale(2,s),n//2,4)),mon(k)))
check('finite identity uses squared moments before any sign specialization',vac==plus(G,times(E2,U),times(M2,V)))
Ufull=times(plus(mon(h),eps),U)
Vfull=times(plus(mon(s),neg(mon(power=2,mask=2))),V)
check('full central-ring identity with original generator sides',vac==plus(G,times(E,Ufull),times(M,Vfull)))
check('right multipliers genuinely retain central variables',any(k[2] for k in Ufull) and any(k[2] for k in Vfull))

def cyclic(p):
    out={}
    for (u,a,mask),c in p.items():
        n=sum(u[2:])
        Cu=(-u[2],-u[3],u[0]-u[2],u[1]-u[3])
        out=plus(out,mon(Cu,a+n,gm(ipow(n),c),mask))
    return out
def inverse(p): return cyclic(cyclic(p))
check('inverse cyclic transport retains the complete formal identity',inverse(vac)==plus(inverse(G),times(inverse(E),inverse(Ufull)),times(inverse(M),inverse(Vfull))))
check('native meridian and edge retain their central characters',
      inverse(E)==plus(mon((2,2,1,1),-2,c=(-1,0)),neg(eps)) and
      inverse(M)==plus(mon((1,1,1,0),-1,c=(0,-1)),mon(power=2,mask=2)))

def exchange(p):
    return {((u[1],u[0],u[3],u[2]),a,m):c for (u,a,m),c in p.items()}
reverseM2=plus(mon(scale(-2,s)),neg(mon(power=4)))
check('reversed meridian squared relation transports modulo the squared edge',
      exchange(M2)==plus(times(reverseM2,mon(scale(2,h))),times(E2,mon(power=4))))
reverseVac=plus(one,neg(mon(scale(-1,v))))
check('reversed longitude square transports modulo the squared edge',
      plus(reverseVac,neg(exchange(vac)))==times(E2,times(plus(mon(scale(2,h)),one),mon(scale(-1,v)))))
reverseG=exchange(G)
reverseU=plus(exchange(U),times(mon(power=4),exchange(V)),times(plus(mon(scale(2,h)),one),mon(scale(-1,v))))
reverseV=times(mon(scale(2,h)),exchange(V))
check('full reversed-meridian squared identity',reverseVac==plus(reverseG,times(E2,reverseU),times(reverseM2,reverseV)))
reverseM=plus(mon(scale(-1,s)),mon(power=2,mask=2))
check('full reversed-meridian central-ring identity',reverseVac==plus(reverseG,times(E,times(plus(mon(h),eps),reverseU)),times(reverseM,times(plus(mon(scale(-1,s)),neg(mon(power=2,mask=2))),reverseV))))

# A second product oracle uses ordered z^a w^b monomials, not Weyl products.
def pbw(p):
    out={}
    for (u,a,m),c in p.items():
        out=plus(out,mon(u,a+F(u[0]*u[2]+u[1]*u[3],2),c,m))
    return out
def pbw_times(p,q):
    out={}
    for (u,a,m),c in p.items():
        for (v,b,n),d in q.items():
            out=plus(out,mon(addv(u,v),a+b+u[2]*v[0]+u[3]*v[1],gm(c,d),m^n))
    return out
Gpbw=plus(*(pbw_times(pbw(left),pbw(f1 if j==1 else f2)) for j,left in lefts))
check('ordered-monomial multiplication independently verifies the displayed identity',pbw(vac)==plus(Gpbw,pbw_times(pbw(E),pbw(Ufull)),pbw_times(pbw(M),pbw(Vfull))))

def encoded(p):
    return [{'root':list(u),'A_degree':str(a),'central_mask':m,'coefficient':list(c)} for (u,a,m),c in sorted(p.items())]
packet={'ring':'Q(i,A^(1/2))[epsilon,zeta]/(epsilon^2-1,zeta^2-1)',
        'identity':'1-W(v)=G+(W(2h)-1)U+(W(2s)-A^4)V',
        'h':h,'s':s,'v':v,'tetrahedron_left_multipliers':terms,
        'G':encoded(G),'U_squared':encoded(U),'V_squared':encoded(V),
        'U_central':encoded(Ufull),'V_central':encoded(Vfull),
        'reverse_U_squared':encoded(reverseU),'reverse_V_squared':encoded(reverseV)}
(ROOT/'central-certificate.json').write_text(json.dumps(packet,indent=2)+'\n')
result={'status':'passed','checks':checks,'count':len(checks),
        'scope':'Full central-vertex quotient, with no specialization of opposite-root involutions.',
        'limits':'Uses retained actual triangulation and named-action conventions. Does not prove the target zero or refute the existence of a nonzero quotient.'}
(ROOT/'exact-results.json').write_text(json.dumps(result,indent=2)+'\n')
print(json.dumps(result,indent=2))