verify-signed-angle.py

"""Exact controls, not a formal proof of the general signed-angle theorem.

Run: python3 verify-signed-angle.py
Uses only the Python standard library. Stdout is the reproducible JSON result.
"""
import json
import sys

# Laurent polynomials in t=A^2, represented exactly by exponent->integer.
def pmul(p,q):
    out={}
    for a,x in p.items():
        for b,y in q.items():
            out[a+b]=out.get(a+b,0)+x*y
    return {a:x for a,x in out.items() if x}

def padd(p,q):
    out=dict(p)
    for a,x in q.items():out[a]=out.get(a,0)+x
    return {a:x for a,x in out.items() if x}

def shift(frac,power):
    p,q=frac
    return ({a+power:x for a,x in p.items()},q)

def add(f,g):
    p,q=f; r,u=g
    return (padd(pmul(p,u),pmul(r,q)),pmul(q,u))

def neg(f):return ({a:-x for a,x in f[0].items()},f[1])

def F(a,b):
    if b >= 0:
        return ({},{0:1})
    den={0:1}
    for j in range(1,-b):den=pmul(den,{0:1,2*j:-1})
    return ({a*(2+b):1},den)

tetra=[]; moment=[]
for a in range(-3,4):
    for b in range(-5,4):
        tetra.append(not add(add(shift(F(a-1,b),-b),shift(F(a,b+1),-a)),neg(F(a,b)))[0])
        moment.append(not add(shift(F(a+1,b),-b),neg(shift(F(a,b),2)))[0])
assert all(tetra) and all(moment)
assert F(0,0)==({},{0:1}) and F(0,-1)==({0:1},{0:1})

def inv_poch(n,cut):
    p=[1]+[0]*cut
    for j in range(1,n+1):
        for k in range(j,cut+1):
            p[k]+=p[k-j]
    return p

def mul(a,b,cut):
    return [sum(a[j]*b[k-j] for j in range(k+1)) for k in range(cut+1)]

def double_sum(b,cut):
    # Used only for b=0,-1. The minimum exponent is
    # j(j-1)/2-b*j+k. Hence j>cut+2 or k>cut cannot contribute.
    assert b in (0,-1)
    p=[0]*(cut+1)
    for j in range(cut+3):
        base=j*(j-1)//2-b*j
        if base>cut:
            continue
        for k in range(cut-base+1):
            shift=base+k
            z=mul(inv_poch(j,cut-shift),inv_poch(k,cut-shift),cut-shift)
            for d,c in enumerate(z):
                p[d+shift]+=(-1)**j*c
    return p

cut=12
unit=double_sum(0,cut); other=double_sum(-1,cut)
assert unit==[0]*(cut+1)
assert other==[1]+[0]*cut

for u in range(8):
    for v in range(8):
        x=(u,v,v)
        delta=x[0]*x[1]+x[1]*x[2]+x[2]*x[0]
        assert delta==v*v+2*u*v
        assert delta+2*u-v==v*(v-1)+2*u*(v+1)
Omega=[[0,1,-1],[-1,0,1],[1,-1,0]]
assert all((int(i!=j)-Omega[i][j])>=0 for i in range(3) for j in range(3))

print(json.dumps({
 'status':'passed',
 'scope':'abstract one-block exact control; not an actual triangulation or independent audit',
 'python_version':sys.version.split()[0],
 'tetrahedron_recurrence_checks':len(tetra),
 'moment_recurrence_checks':len(moment),
 'q_degree_cutoff':cut,
 'unit_coefficients':unit,
 'w_inverse_square_coefficients':other,
 'cone':'x2=x3>=0, x1>=0',
 'theta':[2,-1,0],
 'null_ray_order':'theta dot (u,0,0)=2u>0',
 'general_theorem':'written argument, not inferred from these finite tests'
},indent=2))