Soundness of the transposed legal-row pair masks

theorem Erdos97Octagon.RawIncidence.pairRowIndexMasks_bit (centre : Vertex) (pairIndex : Fin 64) (rowIndex : Fin 35) : bitSetB ((pairRowIndexMasks.getD ↑centre #[]).getD (↑pairIndex) 0) ↑rowIndex = bitSetB (searchRowChoiceAt centre rowIndex).pairMask ↑pairIndex

The transposed pair table records exactly which row choices contain each pair bit.