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

Abstract

The purpose of this paper is two-fold. First, we show that, after a specified form isometry, the two-coordinate reduction in the binary Hilbert-symbol realization of Chinburg and Zhang is inverse to Kim's building-up construction, up to permutation equivalence. Second, for $q\equiv1\pmod4$, we develop a $q$-ary analogue of this reduction-and-extension mechanism. The identity $c^2=-1$ yields the isotropic line governing the split construction. For every fixed ordered pairing of the coordinates, we obtain a universal rank-$r$ boxed normal form, where $r$ is the dimension of the intersection with the product of these isotropic lines. Applications include optimal self-dual $[6,3,4]$ and $[8,4,4]$ codes over $\mathbb F_{5}$, optimal self-dual $[8,4,5]$ and $[10,5,6]$ codes over $\mathbb F_{13}$, and a self-dual $[12,6,6]$ code over $\mathbb F_{13}$. We also give an exact repeated boxed realization of self-dual $[18,9,8]$ and $[20,10,10]$ codes over $\mathbb F_{13}$, in which the split-boxed parent and its building-up child occur in one complete generator matrix. The algebraic core is formalized in Lean 4.