Uniform polynomial-time binary-polynomial addition

The registered evaluator XORs two runtime coefficient lists with high zero padding. Later polynomial programs can compose this certificate directly.

theorem Complexity.BitPolynomial.addEval_mem_FP : addEval ∈ FP

Padded addition of two runtime coefficient lists is uniformly polynomial-time.