Formalizing building-up constructions of self-dual codes through isotropic lines in Lean
Jae-Hyun Baek, Jon-Lark Kim
cs.IT
Apr 9, 2026 · v1
TL;DR
A Lean 4 formalization of the algebraic core of the self-dual-code constructions.
Abstract
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 \(\F_q\) with \(q \equiv 1 \pmod{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 \(\GF{5}\), MDS self-dual \([8,4,5]\) and \([10,5,6]\) codes over \(\GF{13}\), and a self-dual \([12,6,6]\) code over \(\GF{13}\). These structural statements are accompanied by a Lean~4 formalization of the algebraic core.
Problem
Kim's building-up construction and Chinburg-Zhang's Hilbert symbol construction produce binary self-dual codes, but their relationship is unclear. Additionally, no q-ary generalization of Chinburg-Zhang's method exists for efficient construction of self-dual codes over split finite fields.
Approach
The authors show that Kim's building-up construction is equivalent to Chinburg-Zhang's Hilbert symbol construction for binary self-dual codes. They introduce a q-ary version of Chinburg-Zhang's construction for self-dual codes over F_q with q congruent to 1 mod 4, studying these codes through three viewpoints: building-up construction, binary arithmetic of F_q, and isotropic lines in symplectic geometry. Parts of the theory are formalized in Lean.
Results
The equivalence between Kim's and Chinburg-Zhang's constructions is established. The new q-ary construction provides an efficient method for building self-dual codes over split finite fields, with formal verification in Lean supporting the correctness of the geometric approach via isotropic lines.
