Formalizing building-up constructions of self-dual codes through isotropic lines in Lean

Formalizing building-up constructions of self-dual codes through isotropic lines in Lean Source: arxiv Isotropic lines govern a $q$-ary analogue of the Chinburg-Zhang reduction mechanism for $q \equiv 1 \pmod 4$. The construction identifies a universal rank-$r$ boxed normal form for specific coordinate pairings, yielding optimal self-dual codes such as $[12,6,6]$ over $\mathbb{F}_{13}$ and $[20,10,8]$ over $\mathbb{F}_{13}$.