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

TL;DR

This paper formalizes and extends the construction of self-dual codes using algebraic and geometric methods, introducing a q-ary version and providing explicit optimal codes with formal proof in Lean 4.

Contribution

It demonstrates the equivalence of Kim's and Chinburg-Zhang's constructions, introduces a q-ary extension, and constructs new optimal self-dual codes with formal verification.

Findings

Equivalence of Kim's and Chinburg-Zhang's constructions established.

New efficient q-ary self-dual code construction methods introduced.

Explicit optimal self-dual codes over GF(5) and GF(13) constructed and formalized.

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.