Correct transposition of binary coefficient matrices

The output has the exact rectangular width. Position col*rows+row reads input position row*cols+col, with false for missing entries. Two transposes recover the requested rectangle, truncating excess bits and adding high false padding if needed. Exact-sized inputs therefore roundtrip unchanged.

All statements include zero dimensions and arbitrary input padding. The uniform machine certificate is in Complexitylib.Classes.P.BitPolynomial.Transpose.

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

Transposition always writes the exact requested rectangular width.

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

A matrix with no rows has empty output.

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

A matrix with no columns has empty output.

theorem Complexity.BitPolynomial.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

Each in-range output bit reads its transposed source index.

theorem Complexity.BitPolynomial.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

Matrix coordinates transpose directly, including missing input entries.

theorem Complexity.BitPolynomial.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))

Two transposes recover the requested rectangle with truncation and false padding.

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

Transposition is inverted by swapping dimensions when the input has exact width.

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

The paired evaluator reads its matrix and both runtime unary dimensions.

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

The output width is bounded by the square of the encoded input length.