\begin{thebibliography}{99}

\bibitem{CKM16}
H.~Cohn, A.~Kumar and G.~Minton,
\emph{Optimal simplices and codes in projective spaces},
Geom. Topol. \textbf{20} (2016), no.~3, 1289--1357,
\href{https://doi.org/10.2140/gt.2016.20.1289}{doi:10.2140/gt.2016.20.1289};
\href{https://arxiv.org/abs/1308.3188v4}{arXiv:1308.3188v4}.
Section, theorem and equation numbers agree in both versions; page numbers cited here are those of arXiv v4.

\bibitem{Hoggar84}
S.~G.~Hoggar,
\emph{Parameters of $t$-designs in $\mathbb{F}P^{d-1}$},
European J. Combin. \textbf{5} (1984), no.~1, 29--36,
\href{https://doi.org/10.1016/S0195-6698(84)80015-3}{doi:10.1016/S0195-6698(84)80015-3}.

\bibitem{CK07}
H.~Cohn and A.~Kumar,
\emph{Universally optimal distribution of points on spheres},
J. Amer. Math. Soc. \textbf{20} (2007), no.~1, 99--148,
\href{https://doi.org/10.1090/S0894-0347-06-00546-7}{doi:10.1090/S0894-0347-06-00546-7}.

\bibitem{Baez02}
J.~C.~Baez,
\emph{The octonions},
Bull. Amer. Math. Soc. (N.S.) \textbf{39} (2002), no.~2, 145--205,
\href{https://doi.org/10.1090/S0273-0979-01-00934-X}{doi:10.1090/S0273-0979-01-00934-X};
\href{https://arxiv.org/abs/math/0105155v4}{arXiv:math/0105155v4}.

\bibitem{CJKT11}
H.~Cohn, Y.~Jiao, A.~Kumar and S.~Torquato,
\emph{Rigidity of spherical codes},
Geom. Topol. \textbf{15} (2011), no.~4, 2235--2273,
\href{https://doi.org/10.2140/gt.2011.15.2235}{doi:10.2140/gt.2011.15.2235};
\href{https://arxiv.org/abs/1102.5060v2}{arXiv:1102.5060v2}.

\bibitem{TZ08}
W.~Tadej and K.~\.Zyczkowski,
\emph{Defect of a unitary matrix},
Linear Algebra Appl. \textbf{429} (2008), no.~2--3, 447--481,
\href{https://doi.org/10.1016/j.laa.2008.02.036}{doi:10.1016/j.laa.2008.02.036};
\href{https://arxiv.org/abs/math/0702510v2}{arXiv:math/0702510v2}.

\bibitem{BSB13}
N.~Barros e S\'a and I.~Bengtsson,
\emph{Families of complex Hadamard matrices},
Linear Algebra Appl. \textbf{438} (2013), no.~7, 2929--2957,
\href{https://doi.org/10.1016/j.laa.2012.10.029}{doi:10.1016/j.laa.2012.10.029};
\href{https://arxiv.org/abs/1202.1181v2}{arXiv:1202.1181v2}.
Page numbers cited refer to the arXiv version.

\bibitem{CW96}
R.~Connelly and W.~Whiteley,
\emph{Second-order rigidity and prestress stability for tensegrity frameworks},
SIAM J. Discrete Math. \textbf{9} (1996), no.~3, 453--491,
\href{https://doi.org/10.1137/S0895480192229236}{doi:10.1137/S0895480192229236}.

\bibitem{Lojasiewicz59}
S.~\L{}ojasiewicz,
\emph{Sur le probl\`eme de la division},
Studia Math. \textbf{18} (1959), no.~1, 87--136,
\href{https://doi.org/10.4064/sm-18-1-87-136}{doi:10.4064/sm-18-1-87-136}.

\bibitem{AAA91}
E.~R.~Avakov, A.~A.~Agrachev and A.~V.~Arutyunov,
\emph{The level set of a smooth mapping in a neighborhood of a singular point, and zeros of a quadratic mapping},
Mat. Sb. \textbf{182} (1991), no.~8, 1091--1104 (Russian);
English transl., Math. USSR-Sb. \textbf{73} (1992), no.~2, 455--466,
\href{https://doi.org/10.1070/SM1992v073n02ABEH002555}{doi:10.1070/SM1992v073n02ABEH002555}.

\bibitem{IS01}
A.~F.~Izmailov and M.~V.~Solodov,
\emph{Error bounds for $2$-regular mappings with Lipschitzian derivatives and their applications},
Math. Program. \textbf{89} (2001), no.~3, 413--435,
\href{https://doi.org/10.1007/PL00011406}{doi:10.1007/PL00011406}.

\bibitem{VW00}
K.~G.~H.~Vollbrecht and R.~F.~Werner,
\emph{Why two qubits are special},
J. Math. Phys. \textbf{41} (2000), no.~10, 6772--6782,
\href{https://doi.org/10.1063/1.1286032}{doi:10.1063/1.1286032};
\href{https://arxiv.org/abs/quant-ph/9910064v1}{arXiv:quant-ph/9910064v1}.

\bibitem{Hoggar83}
S.~G.~Hoggar,
\emph{Parameters of association schemes},
Ars Combin. \textbf{16-B} (1983), 325--339.

\bibitem{BBRV02}
S.~Bandyopadhyay, P.~O.~Boykin, V.~Roychowdhury and F.~Vatan,
\emph{A new proof for the existence of mutually unbiased bases},
Algorithmica \textbf{34} (2002), no.~4, 512--528,
\href{https://doi.org/10.1007/s00453-002-0980-7}{doi:10.1007/s00453-002-0980-7};
\href{https://arxiv.org/abs/quant-ph/0103162v3}{arXiv:quant-ph/0103162v3}.


\bibitem{Yokota09}
I.~Yokota,
\emph{Exceptional Lie groups},
\href{https://arxiv.org/abs/0902.0431v1}{arXiv:0902.0431v1}, 2009.

\bibitem{Knill96}
E.~Knill,
\emph{Group representations, error bases and quantum codes},
Los Alamos National Laboratory report, 1996,
\href{https://doi.org/10.2172/378680}{doi:10.2172/378680};
\href{https://arxiv.org/abs/quant-ph/9608049v1}{arXiv:quant-ph/9608049v1}.

\bibitem{SPGP26}
E.~Svegborn, J.~Pauwels, N.~Gisin and A.~Pozas-Kerstjens,
\emph{Uncountably many inequivalent maximally entangled measurements for two qutrits},
\href{https://arxiv.org/abs/2607.16396v1}{arXiv:2607.16396v1}, 2026.

\bibitem{dMU21}
L.~de~Moura and S.~Ullrich,
\emph{The Lean~4 theorem prover and programming language},
in: Automated Deduction -- CADE~28, Lecture Notes in Comput. Sci. \textbf{12699},
Springer, Cham, 2021, 625--635,
\href{https://doi.org/10.1007/978-3-030-79876-5_37}{doi:10.1007/978-3-030-79876-5\_37}.

\bibitem{Mathlib20}
The mathlib Community,
\emph{The Lean mathematical library},
in: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs
and Proofs (CPP~'20), ACM, New York, 2020, 367--381,
\href{https://doi.org/10.1145/3372885.3373824}{doi:10.1145/3372885.3373824}.

\bibitem{Palomar}
Palomar registry of machine-checked Lean formalizations,
\url{https://palomar-registry.org/about}, entry
\href{https://palomar-registry.org/entry?id=PALOMAR-2026-10-29-000034&version=1}{\texttt{PALOMAR-2026-10-29-000034}, version~1}.

\bibitem{McCrimmon04}
K.~McCrimmon,
\emph{A Taste of Jordan Algebras},
Universitext, Springer, New York, 2004,
\href{https://doi.org/10.1007/b97489}{doi:10.1007/b97489}.

\bibitem{TZ06}
W.~Tadej and K.~\.Zyczkowski,
\emph{A concise guide to complex Hadamard matrices},
Open Syst. Inf. Dyn. \textbf{13} (2006), no.~2, 133--177,
\href{https://doi.org/10.1007/s11080-006-8220-2}{doi:10.1007/s11080-006-8220-2};
\href{https://arxiv.org/abs/quant-ph/0512154v2}{arXiv:quant-ph/0512154v2}.

\end{thebibliography}