MerLean-example

55 Overview: Balanced Product Codes Formalization

This chapter provides the root module of the balanced product codes formalization. The file balanced_product_codes.lean contains only import declarations, assembling all definitions, lemmas, theorems, corollaries, and remarks from the submodules into a single coherent library. No new declarations are made at this level; all mathematical content is introduced in the imported files listed below.

The formalization is organized into the following components:

  1. Definitions (Def_1 through Def_30): Chain complexes and cohomology, classical codes, CSS codes, LDPC codes, subsystem CSS codes, cell complexes, cycle graphs, double complexes, total complexes, tensor product double complexes, fiber bundle double complexes, augmented complexes, graph expansion, Tanner code local systems, dual codes, binary entropy, Cheeger constants, edge boundary vertices, Cayley graphs, LPS expander graphs, balanced product vector spaces, balanced product chain complexes, quotient graph trivializations, invariant labelings, balanced product Tanner cycle codes, horizontal/vertical homology splittings, iota/pi maps, horizontal subsystem balanced product codes, and unipotent subgroups for LPS.

  2. Theorems and Corollaries (Thm_1 through Thm_15, Cor_1 through Cor_3): The Künneth formula, small double complex homology, fiber bundle homology, the projection-induces-isomorphism theorem, the Alon–Boppana bound, the Alon–Chung theorem, the Alon–Chung contrapositive, the Sipser–Spielman expander code distance bound, expander violated checks, expander bit degree bounds, the Gilbert–Varshamov-plus theorem, LPS Ramanujan graphs, encoding rate for circle codes, homological and cohomological distance bounds, subsystem code parameters, explicit families of quantum codes, and the distance-balanced family theorem.

  3. Lemmas (Lem_1 through Lem_4): Relative Cheeger inequalities, edge-to-vertex expansion, relative vertex-to-edge expansion, and the Künneth balanced product.

  4. Remarks (Rem_1 through Rem_3): Base field conventions, notation conventions, and the expanding matrix definition.