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

The purpose of this paper is two-fold. First we show that Kim’s building-up construction of binary self-dual codes is equivalent to Chinburg-Zhang’s Hilbert symbol construction. Second we introduce a $q$-ary version of Chinburg-Zhang’s construction in order to construct $q$-ary self-dual codes efficiently. For the latter, we study self-dual codes over split finite fields ${\text{F}}_q$ with $q\equiv 1(\mathrm{m}\mathrm{o}\mathrm{d}4)$ through three complementary viewpoints: the building-up construction, the binary arithmetic reduction of Chinburg–Zhang, and the hyperbolic geometry of the Euclidean plane. The condition that $-1$ be a square is the common algebraic input linking these viewpoints: in the binary case it underlies the Lagrangian reduction picture, while in the split $q$-ary case it produces the isotropic line governing the correction terms in the extension formulas. As an application of our efficient form of generator matrices, we construct optimal self-dual codes from the split boxed construction, including self-dual $[6,3,4]$ and $[8,4,4]$ codes over $\text{GF}5$, MDS self-dual $[8,4,5]$ and $[10,5,6]$ codes over $\text{GF}13$, and a self-dual $[12,6,6]$ code over $\text{GF}13$. These structural statements are accompanied by a Lean~4 formalization of the algebraic core.