The fixed-width binary quotient codec

Every quotient element has exactly one representation of length 2 * 3^s. Decoding is polynomial interpretation followed by the quotient map; encoding uses Mathlib's unique monic remainder. Arbitrary input lists may include padding or higher powers, while the encoding always has canonical width.

The representation proof uses AdjoinRoot.modByMonicHom and its inverse law: https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/AdjoinRoot.html. This semantic equivalence is separate from any encoded evaluator or FP claim.

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

Encoding retains exactly the modulus degree in coefficient bits.

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

The encoded polynomial is exactly the unique monic remainder.

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

Encoding and decoding recover every semantic quotient element.

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

Every list of the canonical width is recovered exactly, including high zeros.

noncomputable def Algebraic.Cutwidth.Extractor.BinaryFieldCodec.equiv (s : ℕ) : AdjoinRoot (binaryModulus s) ≃ Bits s

Quotient elements correspond exactly to coefficient lists of the modulus degree.

Equations

• One or more equations did not get rendered due to their size.

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

Bitwise polynomial addition decodes to quotient addition.

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

Carryless polynomial multiplication decodes to quotient multiplication.

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

Reducing by any bit representation of the modulus preserves the quotient class.

theorem Algebraic.Cutwidth.Extractor.BinaryFieldCodec.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

The bounded modular-squaring algorithm decodes to the corresponding power in the quotient, for every supplied representation of the binary modulus.