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

Jae-Hyun Baek, Jon-Lark Kim

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 Z…