Coordinates for arbitrary monic binary polynomial quotients

The basis and coefficient representation require only monicity. In particular, the modulus need not be irreducible or squarefree. The abstract coordinate maps are used in proofs; the executable addition and multiplication are the existing uniform coefficient-list programs.

def MIPRE.LowDegree.BinaryQuotient.coeffBit (z : ZMod 2) : Bool

Equations

• MIPRE.LowDegree.BinaryQuotient.coeffBit z = decide (z = 1)

theorem MIPRE.LowDegree.BinaryQuotient.ofBool_coeffBit (z : ZMod 2) : ofBool (coeffBit z) = z

theorem MIPRE.LowDegree.BinaryQuotient.coeffBit_ofBool (b : Bool) : coeffBit (ofBool b) = b

noncomputable def MIPRE.LowDegree.BinaryQuotient.coordinateEquiv (f : Polynomial (ZMod 2)) (hf : f.Monic) : AdjoinRoot f ≃ₗ[ZMod 2] Fin f.natDegree → ZMod 2

The monic quotient's specified power-basis coordinate equivalence.

Equations

• MIPRE.LowDegree.BinaryQuotient.coordinateEquiv f hf = (AdjoinRoot.powerBasisAux' hf).equivFun

noncomputable def MIPRE.LowDegree.BinaryQuotient.toBits (f : Polynomial (ZMod 2)) (hf : f.Monic) (x : AdjoinRoot f) : Cost.BitStr

Canonical bits of a quotient element in the monic power basis.

Equations

• MIPRE.LowDegree.BinaryQuotient.toBits f hf x = List.ofFn fun (i : Fin f.natDegree) => MIPRE.LowDegree.BinaryQuotient.coeffBit (((AdjoinRoot.powerBasisAux' hf).repr x) i)

noncomputable def MIPRE.LowDegree.BinaryQuotient.ofBits (f : Polynomial (ZMod 2)) (hf : f.Monic) (l : Cost.BitStr) : AdjoinRoot f

Decode the first natDegree f coefficients; omitted coefficients are zero.

Equations

• MIPRE.LowDegree.BinaryQuotient.ofBits f hf l = ∑ i : Fin f.natDegree, MIPRE.LowDegree.ofBool (List.getD l (↑i) false) • (AdjoinRoot.powerBasisAux' hf) i

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.length_toBits (f : Polynomial (ZMod 2)) (hf : f.Monic) (x : AdjoinRoot f) : List.length (toBits f hf x) = f.natDegree

The canonical encoding has precisely the quotient dimension.

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.ofBits_toBits (f : Polynomial (ZMod 2)) (hf : f.Monic) (x : AdjoinRoot f) : ofBits f hf (toBits f hf x) = x

Decoding a quotient element's canonical bits recovers the element.

theorem MIPRE.LowDegree.BinaryQuotient.toBits_ofBits (f : Polynomial (ZMod 2)) (hf : f.Monic) (l : Cost.BitStr) (hlen : List.length l = f.natDegree) : toBits f hf (ofBits f hf l) = l

Every correctly sized list is already the canonical quotient encoding.

theorem MIPRE.LowDegree.BinaryQuotient.ofBits_eq_evalBits (f : Polynomial (ZMod 2)) (hf : f.Monic) (l : Cost.BitStr) (hlen : List.length l = f.natDegree) : ofBits f hf l = BinaryPolynomial.evalBits (AdjoinRoot.root f) l

Correct-width decoding equals evaluation at the quotient's canonical root.

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.evalBits_toBits (f : Polynomial (ZMod 2)) (hf : f.Monic) (x : AdjoinRoot f) : BinaryPolynomial.evalBits (AdjoinRoot.root f) (toBits f hf x) = x

Canonical coefficient bits evaluate to the quotient element they encode.

theorem MIPRE.LowDegree.BinaryQuotient.evalBits_eq_iff (f : Polynomial (ZMod 2)) (hf : f.Monic) (a b : Cost.BitStr) (ha : List.length a = f.natDegree) (hb : List.length b = f.natDegree) : BinaryPolynomial.evalBits (AdjoinRoot.root f) a = BinaryPolynomial.evalBits (AdjoinRoot.root f) b ↔ a = b

Equality in any monic quotient is faithful on fixed-width coefficient lists.

theorem MIPRE.LowDegree.BinaryQuotient.root_eq (f : Polynomial (ZMod 2)) (p : Cost.BitStr) (hpoly : f = polyOfBits (p ++ [true])) : AdjoinRoot.root f ^ List.length p = BinaryPolynomial.evalBits (AdjoinRoot.root f) p

The quotient root satisfies the lower-coefficient reduction equation.

theorem MIPRE.LowDegree.BinaryQuotient.ofBits_xor (f : Polynomial (ZMod 2)) (hf : f.Monic) (a b : Cost.BitStr) (ha : List.length a = f.natDegree) (hb : List.length b = f.natDegree) : ofBits f hf (BinaryPolynomial.xorBitsProg.toFun (a, b)) = ofBits f hf a + ofBits f hf b

The fixed XOR program implements addition for any monic quotient.

theorem MIPRE.LowDegree.BinaryQuotient.ofBits_mulReduce (f : Polynomial (ZMod 2)) (hf : f.Monic) (p a b : Cost.BitStr) (hp : List.length p = f.natDegree) (hpoly : f = polyOfBits (p ++ [true])) (ha : List.length a = f.natDegree) (hb : List.length b = f.natDegree) : ofBits f hf (BinaryPolynomial.mulReduceProg.toFun (p, a, b)) = ofBits f hf a * ofBits f hf b

Uniform modular multiplication works before irreducibility is known.