TFPT scientific source excerpt
Original repository path: verification/v634_st31_structure.py
Original file SHA-256: 5ff53ed031ca03103187ac22edf723aabce88bee3df1085c52486ecb0044d37c
Inclusive original lines: 280-346
Line numbers below refer to the original source.
This bounded excerpt is source evidence; it is not a new proof/checker run.
Conversation metadata and personal execution details are omitted where indicated.

000280 | # ============================== S2: G = FULL unitary stabilizer (exact)
000281 | section("S2: exact count of ALL unitary maps preserving the root set")
000282 | 
000283 | 
000284 | def gmul(u, v):
000285 |     return (u[0] * v[0] - u[1] * v[1], u[0] * v[1] + u[1] * v[0])
000286 | 
000287 | 
000288 | def gdet4(M):
000289 |     tot = (0, 0)
000290 |     for perm in itertools.permutations(range(4)):
000291 |         sgn = 1
000292 |         for a in range(4):
000293 |             for b in range(a + 1, 4):
000294 |                 if perm[a] > perm[b]:
000295 |                     sgn = -sgn
000296 |         term = (sgn, 0)
000297 |         for r in range(4):
000298 |             term = gmul(term, M[r][perm[r]])
000299 |         tot = (tot[0] + term[0], tot[1] + term[1])
000300 |     return tot
000301 | 
000302 | 
000303 | random.seed(0)
000304 | basis = None
000305 | for _ in range(50000):
000306 |     cand = random.sample(range(60), 4)
000307 |     M4 = [[(int(HG[a, b, 0]), int(HG[a, b, 1])) for b in cand] for a in cand]
000308 |     if gdet4(M4) == (1, 0):
000309 |         basis = [line_reps[a] for a in cand]
000310 |         break
000311 | check("S2.1 hermitian-unimodular Z[i]-basis among the line reps: %s"
000312 |       % (basis,), basis is not None)
000313 | 
000314 | t = time.time()
000315 | val_index = []
000316 | for i in range(N240):
000317 |     re4, im4 = herm4_rowvec(i)
000318 |     d = {}
000319 |     for j in range(N240):
000320 |         d.setdefault((int(re4[j]) // 4, int(im4[j]) // 4), set()).add(j)
000321 |     val_index.append(d)
000322 | 
000323 | 
000324 | def hval(i, j):
000325 |     return (int(RD[i] @ RD[j]) // 4, int(RD[i] @ JRD[j]) // 4)
000326 | 
000327 | 
000328 | b1, b2, b3, b4 = basis
000329 | g12, g13, g14 = hval(b1, b2), hval(b1, b3), hval(b1, b4)
000330 | g23, g24, g34 = hval(b2, b3), hval(b2, b4), hval(b3, b4)
000331 | count = 0
000332 | for r1 in range(N240):
000333 |     for r2 in val_index[r1].get(g12, ()):
000334 |         c3 = val_index[r1].get(g13, set()) & val_index[r2].get(g23, set())
000335 |         for r3 in c3:
000336 |             c4 = (val_index[r1].get(g14, set())
000337 |                   & val_index[r2].get(g24, set())
000338 |                   & val_index[r3].get(g34, set()))
000339 |             count += len(c4)
000340 | check("S2.2 EXACT count of unitary root-set automorphisms = %d (%.1f s): "
000341 |       "every Gram-matching image of a unimodular basis extends to a "
000342 |       "unitary automorphism of the Z[i]-E8 lattice, and those preserve "
000343 |       "{v : H(v,v) = 2} = the 240 roots" % (count, time.time() - t),
000344 |       count == 46080)
000345 | check("S2.3 => G (generated by the 60 reflections) IS the full unitary "
000346 |       "stabilizer of the mu4-quotient structure", count == len(Gset))