Polynomial-time binary matrix transposition

Both runtime dimensions are unary lengths. Their product bounds the output, and division and remainder compute each transposed index in polynomial time. A bounded bitwise map reads the corresponding input bit, with false past its end.

theorem Complexity.BitPolynomial.Internal.transposeEval_mem_FP : transposeEval ∈ FP

theorem Complexity.BitPolynomial.Internal.transposeBits_mem_FP {rows cols : List Bool → ℕ} {bits : List Bool → List Bool} (hrows : UnaryFn rows) (hcols : UnaryFn cols) (hbits : bits ∈ FP) : (fun (z : List Bool) => transposeBits (rows z) (cols z) (bits z)) ∈ FP