Translating binary polynomials in a supplied polynomial quotient

def MIPRE.LowDegree.BinaryQuotient.translateBits (p a : Cost.BitStr) : Cost.BitStr → List Cost.BitStr

Horner translation by the represented element a.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.LowDegree.BinaryQuotient.translateBits p a [] = []

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.length_translateBits (p a g : Cost.BitStr) : (translateBits p a g).length = List.length g

theorem MIPRE.LowDegree.BinaryQuotient.translateBits_width_le (p a g c : Cost.BitStr) : c ∈ translateBits p a g → List.length c ≤ List.length p

Translation bounds coefficient width on every raw input, irrespective of the root width.

theorem MIPRE.LowDegree.BinaryQuotient.translateBits_width (p a g : Cost.BitStr) (ha : List.length a = List.length p) (c : Cost.BitStr) : c ∈ translateBits p a g → List.length c = List.length p

Correct-width translation preserves the quotient coefficient width.

theorem MIPRE.LowDegree.BinaryQuotient.coeffPolynomial_translateBits {R : Type u_1} [CommRing R] [CharP R 2] [Algebra (ZMod 2) R] (z : R) (p a g : Cost.BitStr) (hp : p ≠ []) (hz : z ^ List.length p = BinaryPolynomial.evalBits z p) (ha : List.length a = List.length p) : coeffPolynomial z (translateBits p a g) = (Polynomial.map (algebraMap (ZMod 2) R) (polyOfBits g)).comp (Polynomial.X + Polynomial.C (BinaryPolynomial.evalBits z a))

The translation program substitutes X+a in the input binary polynomial.

@[reducible, inline]

abbrev MIPRE.LowDegree.BinaryQuotient.TranslateState : Type

Equations

• MIPRE.LowDegree.BinaryQuotient.TranslateState = (MIPRE.Cost.BitStr × MIPRE.Cost.BitStr × List MIPRE.Cost.BitStr)

def MIPRE.LowDegree.BinaryQuotient.translateStep (s : TranslateState) (b : Bool) : TranslateState

Equations

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

theorem MIPRE.LowDegree.BinaryQuotient.fold_translateStep_shape (pre p a : Cost.BitStr) (cs : List Cost.BitStr) : (List.foldl translateStep (p, a, cs) pre).1 = p ∧ (List.foldl translateStep (p, a, cs) pre).2.1 = a ∧ (List.foldl translateStep (p, a, cs) pre).2.2.length = cs.length + List.length pre

theorem MIPRE.LowDegree.BinaryQuotient.fold_translateStep_width (pre p a : Cost.BitStr) (cs : List Cost.BitStr) (N : ℕ) (hp : List.length p ≤ N) (hc : ∀ c ∈ cs, List.length c ≤ N) (c : Cost.BitStr) : c ∈ (List.foldl translateStep (p, a, cs) pre).2.2 → List.length c ≤ N

theorem MIPRE.LowDegree.BinaryQuotient.fold_translateStep_eq (bs p a : Cost.BitStr) (cs : List Cost.BitStr) : List.foldl translateStep (p, a, cs) bs = (p, a, List.foldl (fun (acc : List Cost.BitStr) (b : Bool) => linearMulCarry p a (if b = true then BinaryPolynomial.oneBits p else BinaryPolynomial.zeroBits p) acc) cs bs)

noncomputable def MIPRE.LowDegree.BinaryQuotient.translateStepProg : Cost.PolyTimeFun (TranslateState × Bool) TranslateState

Equations

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

theorem MIPRE.LowDegree.BinaryQuotient.translateStep_bounded : translateStepProg.FoldBounded (20 * Polynomial.X ^ 2 + 20 * Polynomial.X + 20)

noncomputable def MIPRE.LowDegree.BinaryQuotient.translateBitsProg : Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr × Cost.BitStr) (List Cost.BitStr)

One globally polynomial-time binary polynomial translation program.

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.translateBitsProg_apply (p a g : Cost.BitStr) : translateBitsProg.toFun (p, a, g) = translateBits p a g