Formalizing building-up constructions of self-dual codes through isotropic lines in Lean
Jae-Hyun Baek, Jon-Lark Kim
cs.IT
Apr 9, 2026 · v2
cs.CL
TL;DR
The algebraic core of the reduction and building-up constructions for self-dual codes via isotropic lines is formalized in Lean 4.
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.
Problem
Kim's building-up construction of self-dual codes and the two-coordinate reduction in Chinburg and Zhang's binary Hilbert-symbol realization lacked a precise inverse relationship. A q-ary analogue of this reduction and extension mechanism had not been developed.
Approach
After a specified form isometry, the binary two-coordinate reduction is shown to invert Kim's building-up construction up to permutation equivalence. For q ≡ 1 (mod 4), an element c with c^2 = -1 defines the isotropic line governing a split construction. For each fixed ordered pairing of coordinates this yields a universal rank-r boxed normal form, where r is the dimension of the intersection with the product of isotropic lines. The algebraic core is formalized in Lean 4.
Results
Applications include optimal self-dual [6,3,4] and [8,4,4] codes over F_5, optimal [8,4,5] and [10,5,6] codes and a [12,6,6] code over F_13. Exact repeated boxed realizations are given for [18,9,8] and [20,10,10] self-dual codes over F_13.