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, 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 qequiv1pmod4, we develop a q-ary analogue of this reduction-and-extension mechanism. The identity c2=-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 F5, optimal self-dual [8,4,5] and [10,5,6] codes over mathbb F13, and a self-dual [12,6,6] code over mathbb F13. We also give an exact repeated boxed realization of self-dual [18,9,8] and [20,10,10] codes over mathbb F13, 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.