Padded addition of binary coefficient lists

Addition XORs coefficients at equal indices, reading false beyond either operand. The output length is the larger input length, so missing high coefficients are padded with zeros. Both operands are runtime inputs.

def Complexity.BitPolynomial.addBits (a b : List Bool) : List Bool

Coefficientwise XOR, padding the shorter operand with high zero coefficients.

Equations

• Complexity.BitPolynomial.addBits a b = List.map (fun (i : ℕ) => a[i]?.getD false ^^ b[i]?.getD false) (List.range (max a.length b.length))

def Complexity.BitPolynomial.addEval (z : List Bool) : List Bool

Add two coefficient lists supplied through the standard pairing codec.

Equations

• Complexity.BitPolynomial.addEval z = Complexity.BitPolynomial.addBits (Complexity.pairFst z) (Complexity.pairSnd z)