Correct padded binary-polynomial addition

The concrete coefficientwise XOR represents addition over ZMod 2 for all input lists, including empty operands and high zero padding. Its exact length is the larger operand length. A uniform polynomial-time certificate is supplied by Complexitylib.Classes.P.BitPolynomial.Addition.

theorem Complexity.BitPolynomial.addBits_length (a b : List Bool) : (addBits a b).length = max a.length b.length

Addition retains the larger operand width, including high zero padding.

theorem Complexity.BitPolynomial.ofBits_addBits (a b : List Bool) : ofBits (addBits a b) = ofBits a + ofBits b

Padded coefficientwise XOR denotes polynomial addition.

theorem Complexity.BitPolynomial.addEval_pair (a b : List Bool) : addEval (pair a b) = addBits a b

The paired evaluator reads exactly its two operands.