The canonical binary quotient codec round trips

Coefficients of the monic remainder lie in the two-element field, so the zero/one bit conversion is exact. The remainder's strict degree bound makes the fixed coefficient list complete.

theorem Algebraic.Cutwidth.Extractor.BinaryFieldCodec.Internal.length_encode (s : ℕ) (x : AdjoinRoot (binaryModulus s)) : (encode s x).length = 2 * 3 ^ s

theorem Algebraic.Cutwidth.Extractor.BinaryFieldCodec.Internal.ofBits_encode (s : ℕ) (x : AdjoinRoot (binaryModulus s)) : Complexity.BitPolynomial.ofBits (encode s x) = (AdjoinRoot.modByMonicHom ⋯) x

theorem Algebraic.Cutwidth.Extractor.BinaryFieldCodec.Internal.decode_encode (s : ℕ) (x : AdjoinRoot (binaryModulus s)) : decode s (encode s x) = x

theorem Algebraic.Cutwidth.Extractor.BinaryFieldCodec.Internal.encode_decode (s : ℕ) (bits : List Bool) (length : bits.length = 2 * 3 ^ s) : encode s (decode s bits) = bits

theorem Algebraic.Cutwidth.Extractor.BinaryFieldCodec.Internal.decode_addBits (s : ℕ) (a b : List Bool) : decode s (Complexity.BitPolynomial.addBits a b) = decode s a + decode s b

theorem Algebraic.Cutwidth.Extractor.BinaryFieldCodec.Internal.decode_mulBits (s : ℕ) (a b : List Bool) : decode s (Complexity.BitPolynomial.mulBits a b) = decode s a * decode s b

theorem Algebraic.Cutwidth.Extractor.BinaryFieldCodec.Internal.decode_remainderBits (s : ℕ) (a modulus : List Bool) (represents : Complexity.BitPolynomial.ofBits modulus = binaryModulus s) : decode s (Complexity.BitPolynomial.remainderBits a modulus) = decode s a

theorem Algebraic.Cutwidth.Extractor.BinaryFieldCodec.Internal.decode_frobeniusBits (s : ℕ) (a modulus count : List Bool) (represents : Complexity.BitPolynomial.ofBits modulus = binaryModulus s) : decode s (Complexity.BitPolynomial.frobeniusBits a modulus count) = decode s a ^ 2 ^ count.length