Canonical binary polynomial degrees and monic division

theorem MIPRE.LowDegree.BinaryPolynomial.degree_polyOfBits_lt_length (a : Cost.BitStr) : (polyOfBits a).degree < ↑(List.length a)

The polynomial represented by a coefficient list has degree below its width.

theorem MIPRE.LowDegree.BinaryPolynomial.polyOfBits_append_true (p : Cost.BitStr) : polyOfBits (p ++ [true]) = polyOfBits p + Polynomial.X ^ List.length p

Appending a leading one makes the represented monic modulus explicit.

theorem MIPRE.LowDegree.BinaryPolynomial.monic_polyOfBits_append_true (p : Cost.BitStr) : (polyOfBits (p ++ [true])).Monic

Every lower-coefficient vector specifies a monic polynomial.

theorem MIPRE.LowDegree.BinaryPolynomial.natDegree_polyOfBits_append_true (p : Cost.BitStr) : (polyOfBits (p ++ [true])).natDegree = List.length p

The degree of a supplied monic modulus is exactly its lower-coefficient width.

theorem MIPRE.LowDegree.BinaryPolynomial.dropLast_append_true (a : Cost.BitStr) (h : List.getLastD a false = true) : List.dropLast a ++ [true] = a

A list with a true leading bit decomposes into its lower coefficients and that bit.

theorem MIPRE.LowDegree.BinaryPolynomial.monic_polyOfBits_of_getLast (a : Cost.BitStr) (h : List.getLastD a false = true) : (polyOfBits a).Monic

A coefficient list with leading bit one represents a monic polynomial.

theorem MIPRE.LowDegree.BinaryPolynomial.natDegree_add_one_of_getLast (a : Cost.BitStr) (h : List.getLastD a false = true) : (polyOfBits a).natDegree + 1 = List.length a

For a nonzero canonical representation, width is degree plus one.

theorem MIPRE.LowDegree.BinaryPolynomial.normalizeBits_eq_nil_iff (a : Cost.BitStr) : normalizeBits a = [] ↔ polyOfBits a = 0

Normalizing produces the empty list exactly when the polynomial is zero.

theorem MIPRE.LowDegree.BinaryPolynomial.length_normalizeBits (a : Cost.BitStr) (ha : polyOfBits a ≠ 0) : List.length (normalizeBits a) = (polyOfBits a).natDegree + 1

A normalized nonzero input has degree plus one coefficients.

theorem MIPRE.LowDegree.BinaryPolynomial.monic_polyOfBits (a : Cost.BitStr) (ha : polyOfBits a ≠ 0) : (polyOfBits a).Monic

Over the binary field, every nonzero polynomial represented by bits is monic.

theorem MIPRE.LowDegree.BinaryPolynomial.divModBits_eq_div_modByMonic (p a : Cost.BitStr) : (polyOfBits (divModBits p a).1, polyOfBits (divModBits p a).2) = (polyOfBits a /ₘ polyOfBits (p ++ [true]), polyOfBits a %ₘ polyOfBits (p ++ [true]))

The executable division agrees with Mathlib's monic quotient and remainder.