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

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

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

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

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

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

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

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

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