Division by binary monic polynomials

The divisor is represented by its lower coefficients p; the leading one is implicit. Horner long division keeps a fixed-width remainder and records each discarded leading coefficient in the quotient. Division by the constant one has a separate branch. No irreducibility or field structure is assumed.

theorem MIPRE.LowDegree.BinaryPolynomial.evalBits_shiftReduce_division {R : Type u_1} [CommRing R] [CharP R 2] (z : R) (p a : Cost.BitStr) (hlen : List.length a = List.length p) : evalBits z (shiftReduce p a) + (evalBits z p + z ^ List.length p) * ofBool (List.getLastD a false) = z * evalBits z a

The discarded bit records exactly the multiple of the monic modulus removed by one reduction step, without any assumption that the modulus vanishes.

@[reducible, inline]

abbrev MIPRE.LowDegree.BinaryPolynomial.DivisionState : Type

Modulus, quotient, and remainder for a Horner division step.

Equations

• MIPRE.LowDegree.BinaryPolynomial.DivisionState = (MIPRE.Cost.BitStr × MIPRE.Cost.BitStr × MIPRE.Cost.BitStr)

def MIPRE.LowDegree.BinaryPolynomial.divisionStep (s : DivisionState) (b : Bool) : DivisionState

One input coefficient is appended to the Horner computation.

Equations

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

theorem MIPRE.LowDegree.BinaryPolynomial.divisionStep_width (s : DivisionState) (b : Bool) : (divisionStep s b).1 = s.1 ∧ List.length (divisionStep s b).2.1 = List.length s.2.1 + 1 ∧ List.length (divisionStep s b).2.2 ≤ List.length s.2.2

Quotient width increases once per input coefficient; remainder width cannot grow.

theorem MIPRE.LowDegree.BinaryPolynomial.fold_divisionStep_width (l : Cost.BitStr) (s : DivisionState) : (List.foldl divisionStep s l).1 = s.1 ∧ List.length (List.foldl divisionStep s l).2.1 = List.length s.2.1 + List.length l ∧ List.length (List.foldl divisionStep s l).2.2 ≤ List.length s.2.2

The width invariant holds for arbitrary initial states, including malformed ones.

theorem MIPRE.LowDegree.BinaryPolynomial.divisionStep_length (p q r : Cost.BitStr) (b : Bool) (hr : List.length r = List.length p) : List.length (divisionStep (p, q, r) b).2.2 = List.length p

On well-formed states, a division step preserves the fixed remainder width.

def MIPRE.LowDegree.BinaryPolynomial.divisionFold (p a : Cost.BitStr) : DivisionState

Unnormalized Horner division result.

Equations

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

theorem MIPRE.LowDegree.BinaryPolynomial.divisionFold_width (p a : Cost.BitStr) : (divisionFold p a).1 = p ∧ List.length (divisionFold p a).2.1 = List.length a ∧ List.length (divisionFold p a).2.2 = List.length p

The right-fold state retains its modulus and its prescribed remainder width.

theorem MIPRE.LowDegree.BinaryPolynomial.evalBits_divisionStep {R : Type u_1} [CommRing R] [CharP R 2] (z : R) (p q r : Cost.BitStr) (b : Bool) (hp : p ≠ []) (hr : List.length r = List.length p) : (evalBits z p + z ^ List.length p) * evalBits z (divisionStep (p, q, r) b).2.1 + evalBits z (divisionStep (p, q, r) b).2.2 = ofBool b + z * ((evalBits z p + z ^ List.length p) * evalBits z q + evalBits z r)

The division-step invariant is an identity in any characteristic-two ring.

theorem MIPRE.LowDegree.BinaryPolynomial.evalBits_divisionFold {R : Type u_1} [CommRing R] [CharP R 2] (z : R) (p a : Cost.BitStr) (hp : p ≠ []) : (evalBits z p + z ^ List.length p) * evalBits z (divisionFold p a).2.1 + evalBits z (divisionFold p a).2.2 = evalBits z a

Horner long division reconstructs the dividend.

def MIPRE.LowDegree.BinaryPolynomial.divModBits (p a : Cost.BitStr) : Cost.BitStr × Cost.BitStr

Quotient and remainder by the monic polynomial polyOfBits (p ++ [true]). The degree-zero case divides by one; all outputs are normalized.

Equations

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

theorem MIPRE.LowDegree.BinaryPolynomial.divModBits_width (p a : Cost.BitStr) : List.length (divModBits p a).1 ≤ List.length a ∧ List.length (divModBits p a).2 ≤ List.length p

Output widths are bounded by the input and divisor widths.

theorem MIPRE.LowDegree.BinaryPolynomial.polyOfBits_divModBits (p a : Cost.BitStr) : polyOfBits (p ++ [true]) * polyOfBits (divModBits p a).1 + polyOfBits (divModBits p a).2 = polyOfBits a

Monic division is correct as a polynomial identity, including division by one.

theorem MIPRE.LowDegree.BinaryPolynomial.coeff_polyOfBits_eq_zero (a : Cost.BitStr) (i : ℕ) (hi : List.length a ≤ i) : (polyOfBits a).coeff i = 0

Coefficients past a representation's width vanish.

theorem MIPRE.LowDegree.BinaryPolynomial.degree_divModBits_remainder_lt (p a : Cost.BitStr) : (polyOfBits (divModBits p a).2).degree < ↑(List.length p)

The remainder has degree strictly smaller than the monic divisor.

noncomputable def MIPRE.LowDegree.BinaryPolynomial.headBitProg : Cost.PolyTimeFun Cost.BitStr Bool

Equations

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

noncomputable def MIPRE.LowDegree.BinaryPolynomial.lastBitProg : Cost.PolyTimeFun Cost.BitStr Bool

Equations

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

noncomputable def MIPRE.LowDegree.BinaryPolynomial.divisionStepProg : Cost.PolyTimeFun (DivisionState × Bool) DivisionState

Equations

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

theorem MIPRE.LowDegree.BinaryPolynomial.divisionStep_bounded : divisionStepProg.FoldBounded (12 * Polynomial.X + 12)

noncomputable def MIPRE.LowDegree.BinaryPolynomial.divisionFoldProg : Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr) DivisionState

Ambient Horner long division, with one iteration per dividend coefficient.

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryPolynomial.divisionFoldProg_apply (p a : Cost.BitStr) : divisionFoldProg.toFun (p, a) = divisionFold p a

noncomputable def MIPRE.LowDegree.BinaryPolynomial.isEmptyBitsProg : Cost.PolyTimeFun Cost.BitStr Bool

Equations

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

noncomputable def MIPRE.LowDegree.BinaryPolynomial.divModBitsProg : Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr) (Cost.BitStr × Cost.BitStr)

Uniform deterministic polynomial-time division by any binary monic polynomial.

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryPolynomial.divModBitsProg_apply (p a : Cost.BitStr) : divModBitsProg.toFun (p, a) = divModBits p a