The bounded long-division step

Inserting one coefficient raises the stored degree by at most one. The single XOR cancellation removes its possible leading term, giving the unique monic remainder while restoring the fixed state width.

theorem Complexity.BitPolynomial.Internal.ofBits_cons (bit : Bool) (bits : List Bool) : ofBits (bit :: bits) = Polynomial.C ↑bit.toNat + Polynomial.X * ofBits bits

theorem Complexity.BitPolynomial.Internal.ofBits_replicate_false (n : ℕ) : ofBits (List.replicate n false) = 0

theorem Complexity.BitPolynomial.Internal.remainderStep_length (modulus : List Bool) (bit : Bool) (state : List Bool) : (remainderStep modulus bit state).length = significantLength modulus - 1

theorem Complexity.BitPolynomial.Internal.remainderStep_correct (modulus : List Bool) (bit : Bool) (state : List Bool) (hm : 0 < significantLength modulus) (hs : state.length = significantLength modulus - 1) : ofBits (remainderStep modulus bit state) = ofBits (bit :: state) %ₘ ofBits modulus