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.

@[reducible, inline]

abbrev Connes.Sp4.BVMatrix : Type

A four-by-four Boolean matrix packed into sixteen bits.

Equations

• Connes.Sp4.BVMatrix = BitVec 16

@[reducible, inline]

abbrev Connes.Sp4.BMatrix : Type

A four-by-four matrix with Boolean entries.

Equations

• Connes.Sp4.BMatrix = (Fin 4 → Fin 4 → Bool)

def Connes.Sp4.bvEntry (x : BVMatrix) : BMatrix

Decode a packed matrix in row-major order.

Equations

• Connes.Sp4.bvEntry x i j = BitVec.getLsbD x (4 * ↑i + ↑j)

def Connes.Sp4.boolDot (a b : BMatrix) (i j : Fin 4) : Bool

The row-column dot product over the field with two elements.

Equations

• Connes.Sp4.boolDot a b i j = (a i 0 && b 0 j ^^ a i 1 && b 1 j ^^ a i 2 && b 2 j ^^ a i 3 && b 3 j)

def Connes.Sp4.boolMul (a b : BMatrix) : BMatrix

Multiply Boolean matrices over the field with two elements.

Equations

• Connes.Sp4.boolMul a b = Connes.Sp4.boolDot a b

def Connes.Sp4.boolTranspose (a : BMatrix) : BMatrix

Transpose a Boolean matrix.

Equations

• Connes.Sp4.boolTranspose a i j = a j i

def Connes.Sp4.boolMatrixEqB (a b : BMatrix) : Bool

Decide entrywise equality of Boolean matrices.

Equations

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

def Connes.Sp4.boolOne : BMatrix

The identity matrix in the Boolean representation.

Equations

• Connes.Sp4.boolOne = Connes.Sp4.bvEntry 33825#16

def Connes.Sp4.boolJ : BMatrix

The standard symplectic form in the Boolean representation.

Equations

• Connes.Sp4.boolJ = Connes.Sp4.bvEntry 8580#16

def Connes.Sp4.boolG1 : BMatrix

The first chosen symplectic generator in the Boolean representation.

Equations

• Connes.Sp4.boolG1 = Connes.Sp4.bvEntry 5083#16

def Connes.Sp4.boolG1Inv : BMatrix

The inverse of the first chosen symplectic generator.

Equations

• Connes.Sp4.boolG1Inv = Connes.Sp4.bvEntry 24520#16

def Connes.Sp4.boolG2 : BMatrix

The second chosen symplectic generator in the Boolean representation.

Equations

• Connes.Sp4.boolG2 = Connes.Sp4.bvEntry 8631#16

def Connes.Sp4.boolG2Inv : BMatrix

The inverse of the second chosen symplectic generator.

Equations

• Connes.Sp4.boolG2Inv = Connes.Sp4.bvEntry 60804#16

def Connes.Sp4.boolConj (g gi x : BMatrix) : BMatrix

Conjugate a Boolean matrix using a supplied matrix and its inverse.

Equations

• Connes.Sp4.boolConj g gi x = Connes.Sp4.boolMul (Connes.Sp4.boolMul g x) gi

def Connes.Sp4.boolCommutesB (a b : BMatrix) : Bool

Decide whether two Boolean matrices commute.

Equations

• Connes.Sp4.boolCommutesB a b = Connes.Sp4.boolMatrixEqB (Connes.Sp4.boolMul a b) (Connes.Sp4.boolMul b a)

def Connes.Sp4.boolPairing (a b : Fin 4 → Bool) : Bool

The standard alternating pairing of Boolean four-vectors.

Equations

• Connes.Sp4.boolPairing a b = (a 2 && b 0 ^^ a 3 && b 1 ^^ a 0 && b 2 ^^ a 1 && b 3)

def Connes.Sp4.boolSymplecticB (x : BMatrix) : Bool

Check preservation of the symplectic form using its six independent row pairings.

Equations

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

theorem Connes.Sp4.boolSymplecticB_eq (x : BMatrix) : boolSymplecticB x = boolMatrixEqB (boolMul (boolMul x boolJ) (boolTranspose x)) boolJ

The six-pairing test agrees with the full symplectic matrix equation.

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.