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

This module isolates an exhaustive Boolean-matrix certificate showing that the finite symplectic factor has no nontrivial normal abelian subgroup. The search is split into kernel-checked chunks and decoded back to Mathlib's symplectic-matrix carrier for the public theorem used in Zhou §6.

def Connes.Sp4.kernelDetectorCheck (x : BitVec 16) : Bool

Boolean certificate predicate used by the kernel-checked finite search.

Equations

• One or more equations did not get rendered due to their size.

theorem Connes.Sp4.no_nontrivial_normal_abelian_subgroup_of_kernelDetector (hcertificate : ∀ (x : BitVec 16), kernelDetectorCheck x = true) (N : Subgroup ↥Group) (hnormal : N.Normal) (hab : ∀ (x y : ↥N), x * y = y * x) : N = ⊥

A complete detector certificate implies that the finite symplectic factor has no nontrivial normal abelian subgroup.