# Root-set bookkeeping in the section on even orthogonal descent in characteristic two (type B_m), checked for a range of m, r, n.
from itertools import product
def pos_roots(m):
    R=[]
    for i in range(m):
        v=[0]*m; v[i]=1; R.append(tuple(v))                    # e_i
        for j in range(i+1,m):
            a=[0]*m; a[i]=1; a[j]=-1; R.append(tuple(a))       # e_i-e_j
            b=[0]*m; b[i]=1; b[j]=1;  R.append(tuple(b))       # e_i+e_j
    return set(R)
def all_roots(m):
    P=pos_roots(m); return P|{tuple(-x for x in r) for r in P}
def e(m,*idx):
    v=[0]*m
    for s,i in idx: v[i-1]+=s
    return tuple(v)
def closed(S,m):
    A=all_roots(m)
    for a in S:
        for b in S:
            c=tuple(x+y for x,y in zip(a,b))
            if c in A and c not in S: return (a,b,c)
    return True
# ---------- Lemma on row iteration (label fl:lem:char2-row-iteration), step 5 ----------
def chain(m,r):          # roots of U_{chain,r}; r=m-1 means U_last^0
    S=pos_roots(m)-{e(m,(1,m))}
    if r<m-1: S-= {e(m,(1,i),(-1,m)) for i in range(r+1,m)}
    return S
def lam(m,r):            # roots carrying lambda_r
    if r==m-1: return {e(m,(1,i),(-1,i+1)) for i in range(1,m)}
    L={e(m,(1,i),(-1,i+1)) for i in range(1,r)}|{e(m,(1,r),(-1,m))}
    L|={e(m,(1,i),(-1,i+1)) for i in range(r+1,m-1)}|{e(m,(1,m-1),(1,m))}
    return L
def w(m,r,v):            # w_r: e_i->e_i (i<r), e_i->e_{i+1} (r<=i<=m-2), e_{m-1}->-e_m, e_m->e_r
    out=[0]*m
    for i in range(1,m+1):
        c=v[i-1]
        if c==0: continue
        if i<r: out[i-1]+=c
        elif i<=m-2: out[i]+=c
        elif i==m-1: out[m-1]-=c
        else: out[r-1]+=c
    return tuple(out)
ok=True
for m in range(3,10):
    for r in range(2,m):
        Nr=pos_roots(m)-{e(m,(1,m)),e(m,(1,r)),e(m,(1,r),(1,m))}-{e(m,(1,r),(-1,j)) for j in range(r+1,m)}
        img={w(m,r,v) for v in chain(m,r-1)}
        target=Nr|{e(m,(-1,m))}
        c1 = img==target
        c2 = {w(m,r,v) for v in lam(m,r-1)}==lam(m,r)
        c3 = w(m,r,e(m,(1,m-1)))==e(m,(-1,m))
        # row group U_{row,r}=N_r Z_r X_r
        row=pos_roots(m)-{e(m,(1,m))}-{e(m,(1,r),(-1,j)) for j in range(r+1,m)}
        c4 = row==Nr|{e(m,(1,r)),e(m,(1,r),(1,m))}
        c5 = closed(Nr|{e(m,(1,r))},m)==True and closed(chain(m,r-1),m)==True and closed(row,m)==True
        if not (c1 and c2 and c3 and c4 and c5): ok=False; print('FAIL',m,r,c1,c2,c3,c4,c5)
print('row-iteration lemma, step 5: group equality, character roots, row group, closure, 3<=m<=9 :',ok)
# ---------- Proposition on the direct generic descent (label fl:prop:char2-direct-generic), steps 1-3 ----------
ok=True; details=[]
for n in range(2,8):
    m=2*n
    A=lambda i: i            # A_i=e_i, i<n
    Bj=lambda j: n-1+j       # B_j=e_{n-1+j}, j<=n
    start=pos_roots(m)-{e(m,(1,m))}-{e(m,(1,n-1),(-1,Bj(j))) for j in range(1,n+1) if Bj(j)<m}
    # NB: U_{row,n-1} removes e_{n-1}-e_j for n-1<j<m, i.e. A_{n-1}-B_j for j<=n (B_n=e_{m-1})
    S=set(start)
    for i in range(n-2,0,-1):
        for j in range(1,i+2):
            X=e(m,(1,A(i)),(-1,Bj(j))); Yr=e(m,(1,Bj(j)),(-1,A(i+1)))
            if X not in S: ok=False; details.append(('X missing',n,i,j))
            S.discard(X)
            c=closed(S,m)
            if c!=True: ok=False; details.append(('not closed after removing X',n,i,j,c))
            S.add(Yr)
            c=closed(S,m)
            if c!=True: ok=False; details.append(('not closed after adding Y',n,i,j,c))
    wt=[0]*m
    for i in range(1,n): wt[A(i)-1]=2*(n-i)
    wt[Bj(1)-1]=2*n
    for i in range(1,n): wt[Bj(i+1)-1]=2*(n-i)
    wt[m-1]=0
    weight=lambda v: sum(a*b for a,b in zip(v,wt))
    Upos={v for v in all_roots(m) if weight(v)>0}
    delta=e(m,(1,Bj(1)),(-1,A(1)))
    if S!=Upos-{delta}: ok=False; details.append(('step 3 mismatch',n,sorted(S-Upos),sorted(Upos-S)))
    if min(weight(v) for v in Upos)<2: ok=False; details.append(('weight <2',n))
    # cross roots as stated in step 2
    cross_f={e(m,(1,A(i)),(-1,Bj(j))) for i in range(1,n) for j in range(1,n+1) if j>i+1}
    cross_r={e(m,(1,Bj(j)),(-1,A(i))) for i in range(2,n) for j in range(1,i+1)}
    allcross={v for v in S if sorted(abs(x) for x in v)[-2:]==[1,1] and sum(v)==0 and
              ((max(k for k,x in enumerate(v) if x)>=n-1) != (min(k for k,x in enumerate(v) if x)>=n-1)) and v[m-1]==0}
    if allcross!=cross_f|cross_r: ok=False; details.append(('cross roots',n,sorted(allcross^(cross_f|cross_r))))
print('direct generic descent, steps 1-3: exchanges, closure, kernel of delta in U_{>0}, 2<=n<=7 :',ok)
for d in details[:12]: print('   ',d)