Kernel-checked Sp₄(𝔽₂) normal-subgroup certificate

The 65,536 Boolean matrices are checked in independent shards so Lake can compile the certificate in parallel. The public theorem is unchanged.

theorem Connes.Sp4.no_nontrivial_normal_abelian_subgroup (N : Subgroup ↥Group) (hnormal : N.Normal) (hab : ∀ (x y : ↥N), x * y = y * x) : N = ⊥

The finite symplectic factor has no nontrivial normal abelian subgroup. This strengthens the elementary-abelian case used in Zhou §6.