"""ladder.py -- proofs of the 2p-ladder identities by exact polynomial identity testing:
all six identities are rational functions of p of bounded degree; exact verification at 29 odd
values (far above the degree) proves them for all odd p.
"""
import sys; sys.path.insert(0,'.')
from fractions import Fraction as F
from sectors import sigvals

def formula_vals(p):
    """formula-based values on (j,j+1), j=0..2p-1: v=sigma_p form, s2, w=sigma_2p form"""
    out=[]
    for j in range(2*p):
        v=F(2*(j%p)+1-p,2*p)
        sgn=(-1)**j
        s2=F(-sgn,4)
        w=F(2*j+1-2*p,4*p)+F(sgn,4*p)-v/2
        out.append((v,s2,w))
    return out

# sanity vs true sigma values at p=3,5,7
for p in [3,5,7]:
    sv=sigvals(2*p); ok=all(formula_vals(p)[j][2]==sv[j] for j in range(2*p))
    sp_=sigvals(p);  ok2=all(formula_vals(p)[j][0]==sp_[j%p] for j in range(2*p))
    print(f"p={p}: w-formula matches sigma_2p: {ok}, v matches sigma_p: {ok2}")

# identities as exact checks at MANY odd p (polynomial identity testing; degrees << #points)
odd_ps=list(range(3,60,2))   # 29 points, includes composite odd (formula family)
allok={1:True,2:True,3:True,4:True,5:True,6:True}
for p in odd_ps:
    vals=formula_vals(p); n=2*p
    av=lambda f: sum(f(v,s2,w) for v,s2,w in vals)/n
    A=av(lambda v,s2,w: s2*w**3)          # <s_2 s_2p^3>
    B=av(lambda v,s2,w: s2*v*v*w)         # <s_p^2 s_2 s_2p>
    mv2=av(lambda v,s2,w: v*v); mw2=av(lambda v,s2,w: w*w)
    cov=av(lambda v,s2,w: v*v*w*w)-mv2*mw2
    I3=av(lambda v,s2,w: v*w**3)          # <s_p s_2p^3>
    I4=av(lambda v,s2,w: s2*v*w*w)        # <s_2 s_p s_2p^2>
    allok[1]&= (4*A+3*B==0)
    allok[2]&= (cov==F(-(p*p-1),48*p**4))
    allok[3]&= (B==F(p*p-1,96*p**3))
    allok[4]&= (A==F(-(p*p-1),128*p**3))
    allok[5]&= (I3==0)
    allok[6]&= (I4==0)
print("ID1  4<s2 s2p^3>+3<s2 sp^2 s2p> = 0           :", allok[1])
print("ID2  Cov(sp^2,s2p^2) = -(p^2-1)/(48p^4)       :", allok[2])
print("ID3  <s2 sp^2 s2p> = (p^2-1)/(96p^3)          :", allok[3])
print("ID4  <s2 s2p^3> = -(p^2-1)/(128p^3)           :", allok[4])
print("ID5  <sp s2p^3> = 0                           :", allok[5])
print("ID6  <s2 sp s2p^2> = 0                        :", allok[6])
print(f"verified at {len(odd_ps)} odd values of p (3..59); rational-function degrees are far below 29")

# --- double-ladder orthogonality (Lemma lem:dladder): component identities ---
def AB(r):
    A={}; B={}
    for rho in range(r):
        v=F(2*rho+1-r,2*r)
        A[rho]=F(2*rho+1-2*r,4*r)+F(1,4)-v/2
        B[rho]=F(1,4*r)-F((-1)**rho,4)
    return A,B
dl_ok=True
for r in range(3,60,2):
    A,B=AB(r)
    vA=sum(F(2*rho+1-r,2*r)*A[rho] for rho in range(r))
    vB=sum(F(2*rho+1-r,2*r)*B[rho] for rho in range(r))
    dl_ok &= (vA==0 and vB==0)
for r in [3,5,7]:
    sv=sigvals(2*r); A,B=AB(r)
    dl_ok &= all(A[j%r]+(-1)**j*B[j%r]==sv[j] for j in range(2*r))
print("double-ladder components (vA=vB=0, A/B matches sigma_2r):", dl_ok)