def SymmetricBilinearForms.standardFormF2 (a b : ℕ) : Matrix (Fin (a + 2 * b)) (Fin (a + 2 * b)) (ZMod 2)

The standard normal form (matrix presentation) of Proposition 30.6. The Gram matrix of the block-diagonal form on (ZMod 2)^{a+2b} consisting of a copies of the rank-one form [1] followed by b copies of the hyperbolic plane ⎡⎣0 1 / 1 0⎤⎦. Indices 0,…,a-1 form the diagonal block; indices a, a+1, a+2, a+3, … form pairs (a+2k, a+2k+1) each giving a hyperbolic plane. This is the matrix appearing on the right-hand side of the classification theorem below.

theorem SymmetricBilinearForms.nondegenerate_symm_bilinearForm_F2_classification {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] [Module.Finite (ZMod 2) V] (B : LinearMap.BilinForm (ZMod 2) V) (hB_symm : B.IsSymm) (hB_nondeg : B.Nondegenerate) : ∃ (a : ℕ) (b : ℕ) (e : V ≃ₗ[ZMod 2] (Fin a → ZMod 2) × (Fin b → Fin 2 → ZMod 2)), (LinearMap.BilinForm.congr e) B = BilinFormZMod2.standardF2Form a b

Proposition 30.6 (Classification of nondegenerate symmetric bilinear forms over F₂). Every nondegenerate symmetric bilinear form B on a finite-dimensional vector space V over F₂ = ZMod 2 is isometric to a standard block-diagonal form: there exist natural numbers a, b and a linear isomorphism e : V ≃ₗ (F₂)^a × (F₂²)^b carrying B to standardF2Form a b, the orthogonal direct sum of a copies of the rank-one form ⟨1⟩ with b copies of the hyperbolic plane. This is the mod-2 analogue of the classical real / complex classification of symmetric bilinear forms and underlies the Wu–formula description of the intersection form on a closed 4-manifold's middle cohomology with F₂ coefficients.