# Checks the identities of Step 3 in the proof of Proposition 22.5
# (nonvanishing of the odd orthogonal descent): the vectors v_i, w_i
# form a hyperbolic basis for t in {0,-1}, and P_t^{-1} f_t P_t = f_SW.
import sympy as sp
t=sp.symbols('t')
def run(n):
    m=2*n; r=n-1; N=2*m
    e=lambda i:i-1; f=lambda i:m+i-1          # basis indices (1-based input)
    def E(a,b):
        M=sp.zeros(N,N); M[a,b]=1; return M   # sends basis vector b to a
    Em=lambda i,j: E(e(i),e(j))-E(f(j),f(i))  # E_{e_i-e_j}
    Ep=lambda i,j: E(e(i),f(j))-E(e(j),f(i))  # E_{e_i+e_j}
    Fm=lambda i,j: Em(i,j).T; Fp=lambda i,j: Ep(i,j).T
    ff=sp.zeros(N,N)
    for i in range(1,r): ff+=Fm(i,i+1)
    ff+= -Fm(r,m)+Fp(r,m)
    for j in range(n,m-1): ff+=Fm(j,j+1)
    ff+=Fp(m-1,m)
    ft=ff+t*Em(1,n)
    def vec(d):
        v=sp.zeros(N,1)
        for k,c in d.items(): v[k]+=c
        return v
    V={};W={}
    V[1]=vec({e(n):1}); W[1]=vec({f(n):1})
    for k in range(2,n+1):
        V[k]=vec({e(k-1):t,e(n+k-1):1}); W[k]=vec({f(k-1):2*t+1,f(n+k-1):t+1})
    V[n+1]=vec({e(m):-t,f(m):t+1}); W[n+1]=vec({e(m):t+1,f(m):-t})
    for h in range(0,n-1):
        s=(-1)**h
        V[n+2+h]=vec({f(r-h):s*(2*t+1),f(m-1-h):s*t}); W[n+2+h]=vec({e(r-h):s*(t+1),e(m-1-h):-s})
    P=sp.Matrix.hstack(*[V[i] for i in range(1,m+1)],*[W[i] for i in range(1,m+1)])
    J=sp.zeros(N,N)
    for i in range(1,m+1): J[e(i),f(i)]=1; J[f(i),e(i)]=1
    Q=lambda v: sum(v[e(i)]*v[f(i)] for i in range(1,m+1))
    fsw=sp.zeros(N,N)
    for i in range(1,m): fsw+=Fm(i,i+1)
    res={}
    for t0 in (0,-1):
        P0=P.subs(t,t0); ok_iso=(P0.T*J*P0==J) and all(Q(P0[:,c])==0 for c in range(N))
        ok_conj=(ft.subs(t,t0)*P0==P0*fsw)
        # Dickson/determinant: dimension of span(v_i) intersected with span(e_i)
        A=sp.Matrix.hstack(*[V[i].subs(t,t0) for i in range(1,m+1)])
        dim_int=m-A[m:,:].rank()
        res[t0]=(ok_iso,ok_conj,int(dim_int),P0.det())
    power=sp.simplify((ft**m)-((-1)**(n-1))*2*t*(t+1)*E(f(n),e(n)))
    return res, power==sp.zeros(N,N)
for n in (2,3,4,5):
    print(n, run(n))