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

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

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

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

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

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

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

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

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