"""Exact check (Gaussian rationals) of the leading rank-one coefficient on the two slices of A2-6,
SO_2-model X = {A symmetric, det A = 1} over k((t)), Cartan embedding = identity.

(a) slice of closure(O_1) at x_0 = I:  A = [[1 + a/t, b/t], [b/t, 1 - a/t]], b = +-i a.
    claim: det A = 1 and t*A mod t = a * v v^T with v = (1, +-i).
(b) slice of closure(O_2) at x_1 = diag(t, 1/t): A = h x_1,
    h = [[1 + c/t + c^2/t^2 + c^3/t^3, e/t], [e/t^3, 1 - c/t]], e = +-i c^2.
    claim: A symmetric, det A = 1, min val -2, and t^2*A mod t = c * v v^T with v = (c, +-i).
In both cases the double cover {w : w w^T = leading coefficient} restricted to the punctured branch
is {w = +-sqrt(param) v}, the Kummer cover of the branch coordinate.
"""
from fractions import Fraction as Fr
import random

class G:
    def __init__(s, re, im=0): s.re, s.im = Fr(re), Fr(im)
    def __add__(s, o): o = o if isinstance(o, G) else G(o); return G(s.re + o.re, s.im + o.im)
    __radd__ = __add__
    def __neg__(s): return G(-s.re, -s.im)
    def __sub__(s, o): return s + (-(o if isinstance(o, G) else G(o)))
    def __mul__(s, o):
        o = o if isinstance(o, G) else G(o)
        return G(s.re * o.re - s.im * o.im, s.re * o.im + s.im * o.re)
    __rmul__ = __mul__
    def __eq__(s, o): o = o if isinstance(o, G) else G(o); return s.re == o.re and s.im == o.im
    def iszero(s): return s.re == 0 and s.im == 0

I = G(0, 1)

def lp(d): return {k: v for k, v in d.items() if not v.iszero()}
def mul(a, b):
    c = {}
    for i, u in a.items():
        for j, v in b.items():
            c[i + j] = c.get(i + j, G(0)) + u * v
    return lp(c)
def add(a, b, s=1):
    c = dict(a)
    for k, v in b.items():
        c[k] = c.get(k, G(0)) + (v if s == 1 else -v)
    return lp(c)
def matmul(A, B):
    return [[add(mul(A[i][0], B[0][j]), mul(A[i][1], B[1][j])) for j in range(2)] for i in range(2)]
def det(A): return add(mul(A[0][0], A[1][1]), mul(A[0][1], A[1][0]), -1)
def coeff(p, k): return p.get(k, G(0))

def rnd(): return G(random.randint(-9, 9), random.randint(-9, 9))

ok = True
for _ in range(20):
    a = rnd()
    if a.iszero(): continue
    for sg in (1, -1):
        b = sg * I * a
        A = [[{0: G(1), -1: a}, {-1: b}], [{-1: b}, {0: G(1), -1: -a}]]
        d = det(A); ok &= (d == {0: G(1)})
        v = (G(1), sg * I)
        lead = [[coeff(A[i][j], -1) for j in range(2)] for i in range(2)]
        ok &= all(lead[i][j] == a * v[i] * v[j] for i in range(2) for j in range(2))
    c = rnd()
    if c.iszero(): continue
    for sg in (1, -1):
        e = sg * I * c * c
        h = [[{0: G(1), -1: c, -2: c * c, -3: c * c * c}, {-1: e}], [{-3: e}, {0: G(1), -1: -c}]]
        x1 = [[{1: G(1)}, {}], [{}, {-1: G(1)}]]
        A = matmul(h, x1)
        ok &= (A[0][1] == A[1][0])
        ok &= (det(A) == {0: G(1)})
        mv = min(min(A[i][j]) for i in range(2) for j in range(2) if A[i][j])
        ok &= (mv == -2)
        v = (c, sg * I)
        lead = [[coeff(A[i][j], -2) for j in range(2)] for i in range(2)]
        ok &= all(lead[i][j] == c * v[i] * v[j] for i in range(2) for j in range(2))
print("all slice identities hold:", ok)