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

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

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

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

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

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

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

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

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