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

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

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

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

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

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

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

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

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