"""Independent SymPy verification of the exported Sage certificate. Does not import Sage, chamber.py, or the previous audit's implementation. Uses exact rational matrices; recomputes vertices directly from intersections. """ from pathlib import Path from itertools import combinations, product import json import sympy as s ROOT=Path(__file__).resolve().parent def mat(a): return s.Matrix([[s.Rational(z) for z in row] for row in a]) def col(a): return s.Matrix([s.Rational(z) for z in a]) def inner(a,b): return (a.T*Q*b)[0] def integer_matrix(a): return all(z.q==1 for z in a) def finite_d4_orbit(start, reflections): found={tuple(start)}; queue=[start] for v in queue: for g in reflections: w=g*v if tuple(w) not in found: found.add(tuple(w));queue.append(w) return found def main(): global Q data=json.loads((ROOT/'certificate.json').read_text()) Q=mat(data['form_Q']);I=s.eye(5) assert Q==s.diag(-16,1,1,1,1) X=mat(data['lattice_basis_X']);G=mat(data['gram_in_integral_basis']) assert X.T*Q*X==G and abs(X.det())==2 and G.det()==-64 records=data['walls'];roots=[col(r['root']) for r in records] R=[mat(r['reflection_matrix']) for r in records] assert len(roots)==8 for r,g in zip(roots,R): assert inner(r,r)==2 and all(z.q==1 for z in r) and sum(r[1:])%2==0 assert g==I-r*r.T*Q and g*g==I and g.T*Q*g==Q assert integer_matrix(X.inv()*g*X) and abs(g.det())==1 gram=s.Matrix([[inner(a,b) for b in roots] for a in roots]) assert gram==mat(data['wall_gram']) pair_counts={0:0,-1:0,-3:0} for i,j in combinations(range(8),2): value=gram[i,j];pair_counts[value]+=1 if value in [0,-1]: order=2 if value==0 else 3 assert (R[i]*R[j])**order==I if order==3:assert R[i]*R[j]!=I else: z=s.Symbol('z') assert (R[i]*R[j]).charpoly(z).as_expr().expand()==((z-1)**3*(z*z-7*z+1)).expand() assert pair_counts=={0:12,-1:12,-3:4} # Known finite D4 root system: one root's orbit is all 24 roots. zero={tuple([0]+list(v)) for v in product(range(-1,2),repeat=4) if sum(z*z for z in v)==2} assert finite_d4_orbit(roots[0],R[:4])==zero assert zero=={tuple(col(v)) for v in data['all_height_zero_roots']} one={tuple([1]+list(v)) for v in product(range(-4,5),repeat=4) if sum(z*z for z in v)==18} assert len(one)==312 and all(sum(v[1:])%2==0 for v in one) assert one=={tuple(col(v)) for v in data['all_height_one_roots']} assert set().union(*(finite_d4_orbit(r,R[:4]) for r in roots[4:]))==one # Direct H-to-V conversion, independent of Sage's polyhedron backend. vertices=set() for ids in combinations(range(8),4): A=s.Matrix([list(roots[i][1:]) for i in ids]);b=s.Matrix([16*roots[i][0] for i in ids]) if not A.det():continue v=A.inv()*b if all(inner(s.Matrix([1]+list(v)),r)<=0 for r in roots):vertices.add(tuple(v)) assert vertices=={tuple(col(v['point'])) for v in data['vertices']} and len(vertices)==16 assert all(sum(z*z for z in v)<=16 for v in vertices) assert sum(sum(z*z for z in v)==16 for v in vertices)==6 # Four D4 inequalities imply a>=b>=c>=|d|; root 7 bounds a<=4. assert roots[7]==s.Matrix([1,4,1,1,0]) interior=s.Matrix([1,s.Rational(4,10),s.Rational(3,10),s.Rational(2,10),s.Rational(1,10)]) assert all(inner(interior,r)<0 for r in roots) for i in range(8): on_face=[s.Matrix(v) for v in vertices if inner(s.Matrix([1]+list(v)),roots[i])==0] assert s.Matrix.hstack(*[v-on_face[0] for v in on_face[1:]]).rank()==3 # Negative control: omitting wall 7 admits an ultraideal point. incomplete=s.Matrix([1,s.Rational(16,3),0,0,0]) assert all(inner(incomplete,r)<=0 for r in roots[:7]) assert inner(incomplete,incomplete)>0 and inner(incomplete,roots[7])>0 for rec in data['vertices']: ids=rec['active_walls'];sub=gram.extract(ids,ids) for size in range(1,5): assert all(sub.extract(js,js).det()>=0 for js in combinations(range(4),size)) if rec['type']=='ideal': assert sub.rank()==3 null=sub.nullspace()[0] assert all(z>0 for z in null) or all(z<0 for z in null) else:assert sub.det()>0 # All finite symmetries act on the actual lattice, including triality maps # that can have half-integral entries in Euclidean ambient coordinates. perms=set();by_perm={} for rec in data['chamber_symmetries']: g=mat(rec['matrix']);p=tuple(rec['permutation']) assert g.T*Q*g==Q and g[0,0]>0 and abs(g.det())==1 assert integer_matrix(X.inv()*g*X) assert all(g*roots[i]==roots[p[i]] for i in range(8)) perms.add(p);by_perm[p]=g assert len(perms)==48 assert all(tuple(p[q[i]] for i in range(8)) in perms for p in perms for q in perms) # Exhaust all 8! permutations to check there are no omitted Gram symmetries. from itertools import permutations all_aut={p for p in permutations(range(8)) if all(gram[p[i],p[j]]==gram[i,j] for i,j in combinations(range(8),2))} assert all_aut==perms symgens=[by_perm[tuple(p)] for p in data['ambient_presentation']['symmetry_generator_permutations']] for i,j,order in [(0,1,4),(1,2,3),(0,2,2)]: assert (symgens[i]*symgens[j])**order==I # Rebuild original companion pair independently and compare conjugations. def companion(coeffs): m=s.zeros(5) for i in range(4):m[i+1,i]=1 m[:,4]=s.Matrix([-v for v in coeffs]) return m A=companion([1,1,0,0,1]);B=companion([-1,2,-1,1,-2]);C=A.inv()*B J=mat(data['companion_to_euclidean_coordinates_J']) O=mat(data['companion_to_orbit_basis_O']);M=mat(data['preceding_orbit_isometry_M']) assert J==X*M.inv()*O.inv() u=(C-I)[:,4] assert O==s.Matrix.hstack(*[(-A)**i*u for i in range(5)]) for name,original in [('A',A),('B',B),('C',C)]: rec=data['original_generators'][name];g=mat(rec['matrix']) assert g==J*original*J.inv() rebuilt=I for i in rec['reflection_word']:rebuilt=rebuilt*R[i] finite=I for i in rec['symmetry_word_abc']:finite=finite*symgens[i] assert finite==mat(rec['chamber_symmetry_matrix']) assert int(rec['central_sign'])*rebuilt*finite==g result={'status':'all independent exact checks passed','arithmetic':'SymPy ZZ/QQ', 'wall_count':8,'finite_vertices':10,'ideal_vertices':6, 'height_zero_roots':24,'height_one_roots':312,'chamber_symmetries':48, 'dihedral_pairs':{'order_2':12,'order_3':12,'infinite':4}, 'negative_control':'omitted wall admits spacelike point (1,16/3,0,0,0)', 'known_case':'D4 finite simple-root reflection orbit reproduces all 24 roots', 'limitations':'Classical Coxeter fundamental-domain theorem and the written infinite-height reduction proof remain mathematical inputs; no Lean certification or subgroup index.'} (ROOT/'independent-verification.json').write_text(json.dumps(result,indent=2)+'\n') print(json.dumps(result,indent=2)) if __name__=='__main__':main()