Uniform polynomial-time coefficient packing by transposition

One evaluator handles runtime binary matrices with two runtime unary dimensions. Missing input entries are false; excess entries are ignored. Zero dimensions and malformed paired inputs follow the total list and projection conventions. Both the encoded evaluator and the rule for computed dimensions and matrices are registered for polynomial-time composition.

theorem Complexity.BitPolynomial.transposeEval_mem_FP : transposeEval ∈ FP

Matrix transposition with runtime unary dimensions is uniformly polynomial-time.

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

Polynomial-time unary dimensions and a computed matrix may be supplied directly.