"""Exact local matrix checks for the BFMS Lemma 3.5 proposed completion.

Coordinator evidence, not a formal proof or a verification of the main theorem.
All entries and calculations are over the rationals. See compatibility-repair.md.
"""
import hashlib
import json
from pathlib import Path
import sympy as s


def comm(a, b):
    return a*b-b*a


def skew(n, i, j):
    a=s.zeros(n)
    a[i,j]=1
    a[j,i]=-1
    return a


def orthogonal(a, q):
    assert a.T*q+q*a == s.zeros(a.rows)

# SO(5): radical of the isotropic-two-plane parabolic.
q5=s.zeros(5)
q5[:2,3:5]=s.eye(2)
q5[3:5,:2]=s.eye(2)
q5[2,2]=1

def heisenberg(u, z):
    a=s.zeros(5)
    a[:2,2:3]=u
    a[2:3,3:5]=-u.T
    a[:2,3:5]=z
    return a

u1=heisenberg(s.Matrix([1,0]),s.zeros(2))
u2=heisenberg(s.Matrix([0,1]),s.zeros(2))
z=heisenberg(s.zeros(2,1),skew(2,0,1))
for a in (u1,u2,z): orthogonal(a,q5)
assert comm(u1,u2)==-z and z!=s.zeros(5)
assert comm(u1,z)==comm(u2,z)==s.zeros(5)
levi_minus=s.diag(-1,-1,1,-1,-1)
assert levi_minus.T*q5*levi_minus==q5 and levi_minus.det()==1
assert levi_minus*u1*levi_minus.inv()==-u1
assert levi_minus*u2*levi_minus.inv()==-u2
assert levi_minus*z*levi_minus.inv()==z

# SO(8): radical of a maximal-isotropic-four-plane parabolic.
q8=s.zeros(8)
q8[:4,4:]=q8[4:,:4]=s.eye(4)
pairs=[(i,j) for i in range(4) for j in range(i+1,4)]
basis=[skew(4,i,j) for i,j in pairs]
nil=[]
for b in basis:
    a=s.zeros(8);a[:4,4:]=b;orthogonal(a,q8);nil.append(a)
assert s.Matrix.hstack(*(a.reshape(64,1) for a in nil)).rank()==6
assert all(comm(a,b)==s.zeros(8) for a in nil for b in nil)
# Levi action XZ+ZX^t is precisely the exterior-square action.
transitions=set()
for p in range(4):
    for q in range(4):
        if p==q: continue
        x=s.zeros(4);x[p,q]=1
        lift=s.diag(x,-x.T);orthogonal(lift,q8)
        for index,b in enumerate(basis):
            image=x*b+b*x.T
            expected=s.zeros(8);expected[:4,4:]=image
            assert comm(lift,nil[index])==expected
            for other,(i,j) in enumerate(pairs):
                if image[i,j]: transitions.add((index,other))
seen={0}
while True:
    enlarged=seen|{j for i,j in transitions if i in seen}
    if enlarged==seen: break
    seen=enlarged
assert len(seen)==6
# Weights e_i+e_j, restricted to trace-zero diagonal matrices, are distinct.
weights=[]
for i,j in pairs:
    values=[]
    for k in range(3):
        diagonal=[int(t==k)-int(t==3) for t in range(4)]
        values.append(diagonal[i]+diagonal[j])
    weights.append(tuple(values))
assert len(set(weights))==6

# Formula for a line-parabolic radical: all brackets vanish in every d.
# Representative dimensions are executable sanity checks of that formula.
for d in (2,3,4,6):
    size=d+2;q=s.zeros(size);q[0,-1]=q[-1,0]=1
    q[1:-1,1:-1]=s.eye(d)
    bs=[]
    for i in range(d):
        a=s.zeros(size);a[0,1+i]=1;a[1+i,-1]=-1
        orthogonal(a,q);bs.append(a)
    assert all(comm(a,b)==s.zeros(size) for a in bs for b in bs)

here=Path(__file__).resolve().parent
import argparse
parser=argparse.ArgumentParser(description=__doc__)
parser.add_argument('--source',type=Path,required=True,help='The frozen manuscript.tex from the reading packet')
source=parser.parse_args().source
assert source.is_file(), 'Supply the frozen manuscript with --source'
result={
 'origin':'coordinator_exact_symbolic_check_not_formal_certificate',
 'source_sha256':hashlib.sha256(source.read_bytes()).hexdigest() if source.exists() else None,
 'checker_sha256':hashlib.sha256(Path(__file__).read_bytes()).hexdigest(),
 'sympy_version':s.__version__,
 'SO5_isotropic_two_plane':{'dimension':3,'nonzero_bracket':'[u1,u2]=-z','central_dimension':1,'is_abelian':False,'levi_minus_I_verified':True},
 'SO8_maximal_isotropic_four_plane':{'dimension':6,'is_abelian':True,'module':'exterior square of standard SL4','distinct_weights':6,'root_action_connected':True},
 'line_parabolic_formula_checks':{'dimensions_checked':[2,3,4,6],'is_abelian':True},
 'limitations':['Does not certify algebraic-group rank and Levi theorems.', 'Does not verify the lifting, descent, dynamics, or main arithmeticity theorem.', 'The accompanying mathematical argument, not finite dimension sampling, supplies the general classification.']
}
print(json.dumps(result,indent=2))