Research
Formalizing building-up constructions of self-dual codes through isotropic lines in Lean
arXiv:2604.08485v1 Announce Type: cross 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 H
arXiv:2604.08485v1 Announce Type: cross 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.
Related
Source: arXiv cs.CL | 2026-04-10