Index arithmetic for binary matrix transposition

The transposed source index stays inside the requested rectangle, and swapping dimensions reverses the index map. Consequently two transposes retain precisely the rectangle, adding false entries when the input is short.

theorem Complexity.BitPolynomial.Internal.transposeBits_length (rows cols : ℕ) (bits : List Bool) : (transposeBits rows cols bits).length = rows * cols

theorem Complexity.BitPolynomial.Internal.transposeBits_zero_rows (cols : ℕ) (bits : List Bool) : transposeBits 0 cols bits = []

theorem Complexity.BitPolynomial.Internal.transposeBits_zero_cols (rows : ℕ) (bits : List Bool) : transposeBits rows 0 bits = []

theorem Complexity.BitPolynomial.Internal.transposeBits_getD (rows cols : ℕ) (bits : List Bool) (k : ℕ) (bound : k < rows * cols) : (transposeBits rows cols bits)[k]?.getD false = bits[k % rows * cols + k / rows]?.getD false

theorem Complexity.BitPolynomial.Internal.transposeBits_getD_coord (rows cols : ℕ) (bits : List Bool) (row col : ℕ) (rowBound : row < rows) (colBound : col < cols) : (transposeBits rows cols bits)[col * rows + row]?.getD false = bits[row * cols + col]?.getD false

theorem Complexity.BitPolynomial.Internal.transposeBits_transposeBits (rows cols : ℕ) (bits : List Bool) : transposeBits cols rows (transposeBits rows cols bits) = List.map (fun (k : ℕ) => bits[k]?.getD false) (List.range (rows * cols))

theorem Complexity.BitPolynomial.Internal.transposeBits_transposeBits_of_length (rows cols : ℕ) (bits : List Bool) (size : bits.length = rows * cols) : transposeBits cols rows (transposeBits rows cols bits) = bits

theorem Complexity.BitPolynomial.Internal.transposeEval_pair (bits rowsWord colsWord : List Bool) : transposeEval (pair (pair bits rowsWord) colsWord) = transposeBits rowsWord.length colsWord.length bits

theorem Complexity.BitPolynomial.Internal.transposeEval_length_le (z : List Bool) : (transposeEval z).length ≤ z.length * z.length