Correct carryless multiplication of binary polynomials

BitPolynomial.ofBits interprets a bit list as coefficients over ZMod 2, constant coefficient first. ofBits_mulBits proves that the concrete parity convolution computes polynomial multiplication for every pair of lists, including empty lists and lists with high zero padding.

The result has length equal to the sum of the input lengths. For nonempty operands its last coefficient is therefore zero. No normalization or irreducibility assumption is needed. The uniform polynomial-time certificate is in Complexitylib.Classes.P.BitPolynomial.

theorem Complexity.BitPolynomial.ofBits_coeff (bits : List Bool) (k : ℕ) : (ofBits bits).coeff k = ↑(bits[k]?.getD false).toNat

A represented polynomial's coefficient is the corresponding bit, or zero past the list.

theorem Complexity.BitPolynomial.mulBits_length (a b : List Bool) : (mulBits a b).length = a.length + b.length

Carryless multiplication retains exactly the sum of the two input lengths.

theorem Complexity.BitPolynomial.ofBits_mulBits (a b : List Bool) : ofBits (mulBits a b) = ofBits a * ofBits b

The concrete bit-list product denotes the product over the two-element field.

theorem Complexity.BitPolynomial.mulEval_pair (a b : List Bool) : mulEval (pair a b) = mulBits a b

On a paired input, the evaluator returns the carryless product of its two operands.