"""Verification of every finite computation used in the hand proof that
S_t (t != 0) has no pivotal deformations other than varying t.

All computations are exact, with t a formal variable (rational functions over Q),
in the model of S_t inside Deligne's category with the Harman-Snowden basis:
   trivalent vertex = Res(B_{123}),  P = id - t^{-1} (unit o counit).
Normalisation: loop = t-1, bigon = (t-2)/t, I - H = t^{-1}(id - e).

Cyclic labelling of the boundary of Hom(X^m, X^n): b_1..b_m (left to right),
then t_n..t_1 (right to left); these are positions 0..m+n-1.  rho = rotation by
one click: position i -> i+1.
"""
from ratfunc import RF
from st import St
from deligne import to_cyclic, from_cyclic, rotate, canon
from evalmap import sfp
from pmap import from_word
from relations import build_relations, W
from rewrite import find_matches

t = RF.gen()
S = St(t)
one, zero = RF(1), RF(0)
I1, c, tau, taus, cup, cap = S.P, S.c, S.tau, S.taus, S.cup, S.cap
idd = S.id(2)
e = cup * cap
I = taus * tau
H = rotate(I, 2, 2, 1)
ok_all = True


def check(name, cond):
    global ok_all
    ok_all &= bool(cond)
    print(("  [ok]  " if cond else "  [FAIL] ") + name)


def cyc(f):
    k = f.m + f.n
    res = {}
    for p_, v in f.d.items():
        res[to_cyclic(p_, f.m, f.n)] = v
    return [res.get(q, zero) for q in sfp(k)]


def elt(m, n, coeffs):
    f = S.C.mor(m, n, {})
    for part, x in coeffs.items():
        f = f + (S.id(n) * S.C.mor(m, n, {from_cyclic(canon(part), m, n): one}) * S.id(m)).scale(RF(x))
    return f


def eq(f, g):
    return cyc(f) == cyc(g)


def perm_action(k, perm):
    """matrix (dict of columns) of the permutation action on sf partitions of k points"""
    idx = {p: i for i, p in enumerate(sfp(k))}
    return [idx[canon([[perm[x] for x in b] for b in p])] for p in sfp(k)]


print("== 0. The model satisfies the defining relations of S_t ==")
check("loop = t-1", cyc(cap * cup) == [t - 1])
check("lollipop = 0", all(x == 0 for x in cyc(cap * taus)))
check("bigon = (t-2)/t", eq(tau * taus, I1.scale((t - 2) / t)))
check("I - H = (id - e)/t", eq(I - H, (idd - e).scale(one / t)))
check("crossing is rotation invariant", eq(rotate(c, 2, 2, 1), c))
check("R1: cap o c = cap", eq(cap * c, cap))
check("R1.5: tau o c = tau", eq(tau * c, tau))
check("R2: c o c = id", eq(c * c, idd))
Lam = (tau @ I1) * (I1 @ c) * (c @ I1)
Rho = c * (I1 @ tau)
check("R2.5: (tau x 1)(1 x c)(c x 1) = c(1 x tau)", eq(Lam, Rho))
c1, c2 = c @ I1, I1 @ c
check("R3: c1 c2 c1 = c2 c1 c2", eq(c1 * c2 * c1, c2 * c1 * c2))
check("c commutes with e, I; c e = e, c I = I", eq(c * e, e) and eq(e * c, e) and eq(c * I, I) and eq(I * c, I))

print("== 1. Rotation eigenspaces on the 4-box space ==")
perm4 = perm_action(4, {i: (i + 1) % 4 for i in range(4)})
# eigenvalue multiplicities of the permutation action of Z/4 on sf partitions of 4 points
import sympy as sp
M4 = sp.zeros(4, 4)
for i, j in enumerate(perm4):
    M4[j, i] = 1
ev = M4.eigenvals()
check(f"rho on S_t^4 has eigenvalues {{1:3, -1:1}} (got {ev})", ev == {1: 3, -1: 1})

print("== 2. Level 4: the gauge image is the kernel of psi ==")
phi = {((0, 1), (2, 3, 4)): 1, ((0, 1, 2), (3, 4)): -1, ((0, 1, 4), (2, 3)): -1,
       ((0, 2, 3), (1, 4)): 1, ((0, 3), (1, 2, 4)): -1, ((0, 3, 4), (1, 2)): 1}


def PHI(v):
    s = zero
    for q, x in zip(sfp(5), v):
        if q in phi:
            s = s + RF(phi[q]) * x
    return s


def psi(x):
    return PHI(cyc((tau @ I1) * (I1 @ c) * (x @ I1)))


check("psi(id)=0, psi(e)=1, psi(c)=-1, psi(I)=-1/t",
      psi(idd) == 0 and psi(e) == 1 and psi(c) == -1 and psi(I) == -one / t)
gauge = [c * (idd + e) + (idd + e) * c, c * (I + H) + (I + H) * c, c * c + c * c]
check("gauge directions c w + w c (w = id+e, I+H, c) lie in ker psi", all(psi(g) == 0 for g in gauge))
check("... and they are linearly independent (so ker psi = gauge image)",
      sp.Matrix([[sp.sympify(str(x.n)) / sp.sympify(str(x.d)) if True else 0 for x in cyc(g)] for g in gauge]).rank() == 3)
check("cap o e = (t-1) cap and tau o e = 0", eq(cap * e, cap.scale(t - 1)) and all(x == 0 for x in cyc(tau * e)))

print("== 3. Level 5 ==")
Q = cyc((tau @ I1) * (I1 @ c) * (e @ I1))
check("(tau x 1)(1 x c)(e x 1) = Res(B_{b1b2|b3t2t1})", {sfp(5)[i]: v for i, v in enumerate(Q) if v != 0} == {((0, 1), (2, 3, 4)): one})
sig = perm_action(5, {0: 1, 1: 0, 2: 2, 3: 3, 4: 4})
r3 = perm_action(5, {i: (i + 3) % 5 for i in range(5)})
# E o (c x 1) is the relabelling b1 <-> b2
okk = True
for i, q in enumerate(sfp(5)):
    v = [zero] * 11
    v[i] = one
    f = elt(3, 2, {q: 1})
    w = cyc(f * c1)
    okk &= (w[sig[i]] == 1 and sum(1 for x in w if x != 0) == 1)
check("E o (c x 1) acts on the partition basis by b1 <-> b2", okk)
# rho^3 acts by i -> i+3 (rotation of partitions)
okk = all(eq(rotate(elt(3, 2, {q: 1}), 3, 2, 3), elt(3, 2, {canon([[(x + 3) % 5 for x in b] for b in q]): 1})) for q in sfp(5))
check("rho^3 acts on the partition basis by i -> i+3", okk)
A = sp.zeros(11, 11)
for i in range(11):
    A[sig[i], i] += 1
    A[r3[i], i] += 1
phivec = sp.Matrix([[phi.get(q, 0) for q in sfp(5)]])
check("phi o (sigma + rho^3) = 0", (phivec * A).is_zero_matrix)
ker = A.nullspace()
k5 = {((0, 1), (2, 3, 4)): 1, ((0, 1, 2), (3, 4)): -1, ((0, 1, 4), (2, 3)): -1,
      ((0, 2), (1, 3, 4)): 1, ((0, 2, 4), (1, 3)): -1, ((0, 4), (1, 2, 3)): 1}
k5v = sp.Matrix([k5.get(q, 0) for q in sfp(5)])
check("ker(sigma + rho^3) = C k5", len(ker) == 1 and (A * k5v).is_zero_matrix)
K5 = elt(3, 2, k5)
capk5 = cyc(K5 * (cup @ I1))
vtx = cyc(taus)
check("k5 o (cup x 1) = t * (trivalent vertex)", capk5 == [t * x for x in vtx])

print("== 4. Level 6 ==")
rho6 = perm_action(6, {i: (i + 1) % 6 for i in range(6)})
R6 = sp.zeros(41, 41)
for i, j in enumerate(rho6):
    R6[j, i] = 1
Vm = (R6 + sp.eye(41)).nullspace()
check("dim of the (-1)-eigenspace of rho on S_t^6 is 5", len(Vm) == 5)
T = c1 * c2 * c1
check("rho(c1c2c1) = c2c1c2 and rho^2(c1c2c1) = c1c2c1 (in the model)", eq(rotate(T, 3, 3, 1), c2 * c1 * c2) and eq(rotate(T, 3, 3, 2), T))
L1 = perm_action(6, {0: 0, 1: 1, 2: 2, 3: 3, 4: 5, 5: 4})  # (c x 1) o E : swap t1,t2
L2 = perm_action(6, {0: 0, 1: 2, 2: 1, 3: 3, 4: 4, 5: 5})  # E o (1 x c) : swap b2,b3
okk = all(cyc(c1 * elt(3, 3, {q: 1})) == cyc(elt(3, 3, {sfp(6)[L1[i]]: 1})) and
          cyc(elt(3, 3, {q: 1}) * c2) == cyc(elt(3, 3, {sfp(6)[L2[i]]: 1})) for i, q in enumerate(sfp(6)))
check("(c x 1 x 1) o E and E o (1 x c) act by t1<->t2 and b2<->b3", okk)
Lm = sp.zeros(41, 41)
for i in range(41):
    Lm[L1[i], i] += 1
    Lm[L2[i], i] += 1
B = sp.Matrix.hstack(*Vm)
K = (Lm * B).nullspace()
m6 = {((0, 1), (2, 3), (4, 5)): 1, ((0, 1), (2, 4), (3, 5)): -1, ((0, 2), (1, 3), (4, 5)): -1, ((0, 2), (1, 5), (3, 4)): 1,
      ((0, 4), (1, 2), (3, 5)): 1, ((0, 4), (1, 5), (2, 3)): -1, ((0, 5), (1, 2), (3, 4)): -1, ((0, 5), (1, 3), (2, 4)): 1}
m6v = sp.Matrix([m6.get(q, 0) for q in sfp(6)])
check("V_- intersect ker(L) = C m6", len(K) == 1 and (Lm * m6v).is_zero_matrix and (R6 * m6v + m6v).is_zero_matrix)
M6 = elt(3, 3, m6)
mer = cyc(M6 * (taus @ I1))
check("m6 o (tau* x 1) != 0  (and is independent of t)", any(x != 0 for x in mer) and all(x.d == 1 and x.n.degree() <= 0 for x in mer))
print("     m6 o (tau* x 1) =", {sfp(5)[i]: x for i, x in enumerate(mer) if x != 0})

print("== 5. Planar isotopies (rotation-invariant tau and c) ==")
rels = build_relations(t)
R = {r["name"]: r for r in rels}
L25, P25 = R["R25"]["L"], R["R25"]["rhs"][0][1]
LR3 = R["R3"]["L"]


def same_up_to_rot(Mrot_of, target, r):
    return Mrot_of.rotated(r).code() == target.code()


check("c(1 x tau)(c x 1) = rho^3(Lambda) and rho^3(P) = (tau x 1)(1 x c)",
      same_up_to_rot(L25, W(3, [("X", 0), ("T", 1), ("X", 0)]), 3) and same_up_to_rot(P25, W(3, [("X", 1), ("T", 0)]), 3))
check("c2c1c2 = rho(c1c2c1) and rho^2(c1c2c1) = c1c2c1",
      same_up_to_rot(LR3, W(3, [("X", 1), ("X", 0), ("X", 1)]), 1) and same_up_to_rot(LR3, LR3, 2))
check("(c x 1)(1 x c)(tau* x 1) = rho(Lambda) and rho(P) = (1 x tau*) c",
      same_up_to_rot(L25, W(2, [("Ts", 0), ("X", 1), ("X", 0)]), 1) and same_up_to_rot(P25, W(2, [("X", 0), ("Ts", 1)]), 1))
check("c o tau* is a rotation of tau o c (R1.5)",
      any(same_up_to_rot(R["R15"]["L"], W(1, [("Ts", 0), ("X", 0)]), r) for r in range(3)))
A3 = W(1, [("cup", 0), ("X", 0), ("X", 1), ("T", 0)])
B3 = W(1, [("cup", 0), ("T", 1), ("X", 0)])
check("Lambda o (cup x 1) contains a curl; P o (cup x 1) is a twisted vertex",
      len(find_matches(A3, R["R1"]["L"])) == 1 and len(find_matches(B3, R["R15"]["L"])) == 1)
print("== 6. All forms of naturality are rotations of R2, R2.5 (so C' is symmetric) ==")
def rot_pair(Lm, Rm, A_, B_):
    """exists k with rho^k(Lm) = A_ and rho^k(Rm) = B_ (as planar maps)"""
    return any(Lm.rotated(k).code() == A_.code() and Rm.rotated(k).code() == B_.code() for k in range(Lm.k))
versions = {
  "c(1 x tau) = (tau x 1)(1 x c)(c x 1)":      (W(3, [("X",0),("X",1),("T",0)]), W(3, [("T",1),("X",0)])),
  "c(tau x 1) = (1 x tau)(c x 1)(1 x c)":      (W(3, [("X",1),("X",0),("T",1)]), W(3, [("T",0),("X",0)])),
  "(tau* x 1)c = (1 x c)(c x 1)(1 x tau*)":   (W(2, [("Ts",1),("X",0),("X",1)]), W(2, [("X",0),("Ts",0)])),
  "(1 x tau*)c = (c x 1)(1 x c)(tau* x 1)":   (W(2, [("Ts",0),("X",1),("X",0)]), W(2, [("X",0),("Ts",1)])),
}
for name, (lhs, rhs) in versions.items():
    check("R2.5 form " + name, rot_pair(L25, P25, lhs, rhs))
L2m, P2m = R["R2"]["L"], R["R2"]["rhs"][0][1]
check("naturality wrt cap: (cap x 1)(1 x c)(c x 1) = 1 x cap is a rotated R2",
      rot_pair(L2m, P2m, W(3, [("X",0),("X",1),("cap",0)]), W(3, [("cap",1)])))
check("naturality wrt cup: (c x 1)(1 x c)(cup x 1) = 1 x cup ... is a rotated R2",
      rot_pair(L2m, P2m, W(1, [("cup",0),("X",1),("X",0)]), W(1, [("cup",1)])))
print()
print("ALL CHECKS PASSED" if ok_all else "SOME CHECK FAILED")