"""Exact audit certificates for FMS Theorem 1 / Theorem 4.7 (1),(4). Finite arithmetic verifies 26 ranks. Uniform arguments are in headline-audit.md; these finite runs alone are not proofs of the infinite families. """ from pathlib import Path import json import sympy as s from sympy.matrices.normalforms import smith_normal_form from sympy.polys.domains import ZZ from sympy.liealgebras.cartan_type import CartanType ROOT=Path(__file__).resolve().parent x=s.Symbol('x') def companion(poly): poly=s.Poly(poly,x);n=poly.degree();eye=s.eye(n) a=s.Matrix.hstack(eye[:,1:],s.Matrix([-poly.nth(j) for j in range(n)])) assert a.charpoly(x).as_expr()==poly.as_expr() return a def factors(matrix): sn=smith_normal_form(matrix,domain=ZZ) return [int(abs(sn[i,i])) for i in range(matrix.rows) if abs(sn[i,i])!=1] def a_root(n): return s.Matrix(n,n,lambda i,j:2 if i==j else -1 if abs(i-j)==1 else 0) def d_root(n): g=2*s.eye(n) for i in range(n-3):g[i,i+1]=g[i+1,i]=-1 for j in [n-2,n-1]:g[n-3,j]=g[j,n-3]=-1 assert g.det()==4 return g def exceptional_lattices(): """Odd-rank non-2-elementary Nikulin candidates; include one extra 2-elementary case appearing in FMS, so exclusions never rely on omitting that candidate. A1+E6 is retained from the primary classification (FMS prints A1+E8). """ u=s.Matrix([[0,1],[1,0]]) a=lambda n:a_root(n) d=lambda n:d_root(n) e8=CartanType('E8').cartan_matrix();e6=CartanType('E6').cartan_matrix() assert e8.det()==1 and e6.det()==3 positive=[('A3',a(3)),('A1+A2',s.diag(a(1),a(2))), ('A1+2A2',s.diag(a(1),a(2),a(2))), ('2A1+A3',s.diag(a(1),a(1),a(3))), ('A2+A3',s.diag(a(2),a(3))),('A1+A4',s.diag(a(1),a(4))), ('A5',a(5)),('D5',d(5)),('A7',a(7)), ('A3+D4',s.diag(a(3),d(4))),('A2+D5',s.diag(a(2),d(5))), ('D7',d(7)),('A1+E6',s.diag(a(1),e6)), ('A1+E8 (extra 2-elementary candidate)',s.diag(a(1),e8)), ('A3+E8',s.diag(a(3),e8))] result=[('U+'+name,s.diag(u,k)) for name,k in positive] result += [('U(4)+3A1',s.diag(4*u,a(1),a(1),a(1))), ('<-6>+2A2',s.diag(-6,a(2),a(2)))] result += [(f'<-{2**k}>+D4',s.diag(-(2**k),d(4))) for k in [2,3,4]] return [{'name':name,'rank':g.rows,'determinant':int(g.det()),'smith_factors':factors(g)} for name,g in result] def gram(family,n): row=[-2,-3]+([-4]*(n-2) if family==1 else [-4]*(n-4)+[-5,-6]) return s.Matrix(n,n,lambda i,j:row[abs(i-j)]) def check_case(family,n,exceptions): if family==1: p=s.Poly(s.div(x**(n+1)-1,x+1,x)[0],x) q=s.Poly((x+1)*s.div(x**n-1,x-1,x)[0],x) order=n+1 else: p=s.Poly((x+1)*(x**(n-1)+1),x) q=s.Poly((x-1)**2*(x**(n-2)-1),x) order=2*n-2 assert s.gcd(p,q).degree()==0 a,b=companion(p),companion(q);eye=s.eye(n) c=a.inv()*b assert c*c==eye and (c-eye).rank()==1 u=(c-eye)[:,-1] assert u[-1]==-2 and c-eye==u*eye[-1,:] t=a if family==1 else -a assert t**order==eye and a**order==eye orbit_vectors=[u];b_vectors=[u] for j in range(1,n): orbit_vectors.append(t*orbit_vectors[-1]);b_vectors.append(b*b_vectors[-1]) o=s.Matrix.hstack(*orbit_vectors);ob=s.Matrix.hstack(*b_vectors) assert o.det()!=0 oi=o.inv() transition=oi*ob assert all(z.q==1 for z in transition) and abs(transition.det())==1 k=gram(family,n) assert list(k[0,:])==[v[-1] for v in orbit_vectors] tb=oi*t*o;cb=oi*c*o assert tb.T*k*tb==cb.T*k*cb==k assert all(z.q==1 for z in tb) and all(z.q==1 for z in cb) assert cb==eye+eye[:,0]*k[0,:] assert all(k[j,j+1]==-3 for j in range(n-1)) if family==1: assert k.det()==-n*(n+1) assert factors(k)==[n*(n+1)] # Positive A_n form followed by a rank-one negative update. positive=2*eye+s.Matrix(n,n,lambda i,j:1 if abs(i-j)==1 else 0) assert k==positive-4*s.ones(n) assert all(positive[:j,:j].det()==j+1 for j in range(1,n+1)) isotropic=s.Matrix([-1,0,-1,1]+[0]*(n-4)) else: assert k.det()==-64 and factors(k)==[2,2,16] # E0 is a Gram matrix of a full-rank signed-cycle root basis. N=n-1;ein=s.eye(N) r=s.Matrix.hstack(ein[:,0]-ein[:,-1], *[ein[:,j-1]+ein[:,j] for j in range(1,N)]) assert abs(r.det())==2 yy=s.zeros(N,n);yy[0,0]=1;yy[0,n-1]=-1 for j in range(1,N):yy[j,j]=1 assert k==yy.T*r.T*r*yy-4*s.ones(n) # This dual vector has order 8, excluding every 2-elementary lattice. v=eye[:,0]+eye[:,-1] assert k*v==-8*s.ones(n,1) and (v.T*k*v)[0]==-16 isotropic=s.Matrix([-1,0,-1,1]+[0]*(n-4)) if n>=7 else s.Matrix([-1,0,-2,0,1]) assert (isotropic.T*k*isotropic)[0]==0 same=[v['name'] for v in exceptions if v['rank']==n and v['smith_factors']==factors(k)] if family==2 and n==5:assert same==['<-16>+D4'] else:assert not same return {'family':family,'n':n,'chosen_orbit_operator':'A' if family==1 else '-A', 'finite_generator_order_bound':order,'orbit_determinant':str(o.det()), 'original_B_orbit_lattice_transition_determinant':str(transition.det()), 'gram_first_row':[int(v) for v in k[0,:]],'determinant':int(k.det()), 'smith_factors':factors(k),'inertia_positive_negative_zero':[n-1,1,0], 'isotropic_vector':list(map(int,isotropic)), 'matching_exception_smith_factors':same, 'reflection_quotient_status':'finite: explicit isometry' if same else 'infinite conditional on cited Nikulin classification'} if __name__=='__main__': exceptions=exceptional_lattices() cases=[] for family in [1,2]: for n in range(5,30,2): cases.append(check_case(family,n,exceptions)) print(f'family {family}, n={n}: exact checks passed',flush=True) k=gram(2,5) m=s.Matrix([[-5,-1,-1,1,1],[8,1,2,-2,-1],[0,0,0,1,-1], [0,0,0,0,1],[3,1,0,-1,-1]]) dstar=s.Matrix([[2,-1,-1,-1],[-1,2,0,0],[-1,0,2,0],[-1,0,0,2]]) target=s.diag(-16,dstar) assert m.det()==-1 and m.T*k*m==target result={'arithmetic':'exact integers and rationals','finite_cases':cases, 'classification_candidates':exceptions, 'n5_family2_isometry':{'gram':[[int(v) for v in row] for row in k.tolist()], 'basis_change':[[int(v) for v in row] for row in m.tolist()], 'basis_change_determinant':-1, 'transformed_gram':[[int(v) for v in row] for row in target.tolist()], 'target':'<-16> orthogonal_sum D4', 'implication':'The lattice is reflective by Nikulin 1979 Theorem 4. ' 'The infinite-reflection-quotient certificate fails; ' 'thinness of this hypergeometric subgroup remains unresolved.'}, 'uniform_scope':'Uniform arguments are supplied in headline-audit.md; ' 'the finite cases alone do not prove all n.'} (ROOT/'exact-headline-results.json').write_text(json.dumps(result,indent=2)+'\n') print('All 26 cases and the integral D4 isometry verified.',flush=True)