The regular two-graphs on 126 and 176 points are unique

We prove that there is, up to isomorphism, only one regular two-graph on 126 points (Taylor's unitary two-graph for U₃(5)) and only one on 176 points (the Higman–Sims two-graph). Equivalently, a set of 126 equiangular lines in R²¹, or of 176 equiangular lines in R²², is unique up to isometry; these are the maximum sizes in these dimensions, attained only at angle arccos 1/5. Brouwer and Van Maldeghem list the uniqueness of both two-graphs as unknown. As a corollary, the strongly regular graphs with parameters (125,52,15,26), (125,72,45,36), (175,72,20,36) and (175,102,65,51) are unique. The proof is lattice-theoretic. The vectors of the line system generate an even lattice K, and an elementary counting argument shows that the dual K# has no nonzero vector of norm at most 2. With Milgram's formula this leaves four possible discriminant forms of a maximal overlattice N for 126 points and four for 176 points. Gluing N to a lattice of rank 2 or 3 gives an even unimodular lattice of rank 24 in which every vector of norm at most 2 lies in the small summand. By Niemeier's classification, seven of the eight cases are either impossible (four cases) or force the Leech lattice (three cases); the remaining case is excluded by an odd unimodular lattice of rank 25 and Borcherds' classification. In the three Leech cases the line system is a section of the 276-line system of a norm-6 Leech vector, and an exhaustive enumeration inside the Leech lattice finds only the two known configurations. The proof is computer-assisted (the Leech enumerations, isomorphism tests by nauty canonical labelling, and the use of Borcherds' classification of rank-25 unimodular lattices via Chenevier's list for one case). Every computation was carried out by a derivation and repeated by a blind audit (a model of a different family, with its own code) and by an independent referee (a third implementation); the audit and the referee did the Leech enumeration without using any group action. The derivation was also reviewed independently by Codex (review C32). The paper states which steps are hand steps. Uniqueness of the two-graph does not mean uniqueness of the regular graphs in its switching class: by Seidel switching inside the known two-graphs we found at least 150 pairwise non-isomorphic srg(126,60,33,24) and at least 4,335 pairwise non-isomorphic srg(176,85,48,34) (100 of them, and all 150 of the former, with trivial automorphism group); their graph6 files are in the data archive.