Kernel-checked shard 8 of 8 for the exhaustive Sp₄(𝔽₂) detector.

theorem Connes.Sp4.kernelDetectorBlock28 (high : Fin 8) (middle low : Fin 16) : kernelDetectorCheck (BitVec.ofNat 16 (2048 * 28 + 256 * ↑high + 16 * ↑middle + ↑low)) = true

The detector succeeds on 16-bit matrix block 28 (with indices 0 through 31).

theorem Connes.Sp4.kernelDetectorBlock29 (high : Fin 8) (middle low : Fin 16) : kernelDetectorCheck (BitVec.ofNat 16 (2048 * 29 + 256 * ↑high + 16 * ↑middle + ↑low)) = true

The detector succeeds on 16-bit matrix block 29 (with indices 0 through 31).

theorem Connes.Sp4.kernelDetectorBlock30 (high : Fin 8) (middle low : Fin 16) : kernelDetectorCheck (BitVec.ofNat 16 (2048 * 30 + 256 * ↑high + 16 * ↑middle + ↑low)) = true

The detector succeeds on 16-bit matrix block 30 (with indices 0 through 31).

theorem Connes.Sp4.kernelDetectorBlock31 (high : Fin 8) (middle low : Fin 16) : kernelDetectorCheck (BitVec.ofNat 16 (2048 * 31 + 256 * ↑high + 16 * ↑middle + ↑low)) = true

The detector succeeds on 16-bit matrix block 31 (with indices 0 through 31).