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 Kim's building-up construction of binary self-dual codes is equivalent to Chinburg-Zhang's Hilbert symbol construction. Se…