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

arXiv: https://arxiv.org/abs/2604.08485 · HTML: https://mlsanity.com/paper/2604.08485/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 0 of its 36 references that are in the map.
- First posted on arXiv 9 Apr 2026.

## Built on by (most cited first, 1 of 1)

- [A machine-checked proof of the Dong-Yang classification of optimal (n,4) binary codes for BSCs](https://mlsanity.com/paper/2609.10579/) (2026)

## Abstract (arXiv)

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.