Documentation

MIPRE.Foundations.LowDegree.BinaryExactDivision

Total polynomial quotient on binary coefficient lists #

source
def MIPRE.LowDegree.BinaryPolynomial.quotientBits (a b : Cost.BitStr) :
Cost.BitStr

Polynomial quotient on arbitrary coefficient lists. A zero divisor returns zero; for a nonzero divisor its canonical leading one is passed implicitly to monic division.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem MIPRE.LowDegree.BinaryPolynomial.polyOfBits_quotientBits (a b : Cost.BitStr) :
    polyOfBits (quotientBits a b) = polyOfBits a / polyOfBits b

    The total quotient program agrees with Mathlib polynomial division.

    source
    theorem MIPRE.LowDegree.BinaryPolynomial.polyOfBits_quotientBits_mul (a b : Cost.BitStr) (hb : polyOfBits b ≠ 0) (hdiv : polyOfBits b ∣ polyOfBits a) :
    polyOfBits b * polyOfBits (quotientBits a b) = polyOfBits a

    Exact divisibility reconstructs the dividend, with no search or field enumeration.

    source
    theorem MIPRE.LowDegree.BinaryPolynomial.quotientBits_width (a b : Cost.BitStr) :
    List.length (quotientBits a b) ≤ List.length a

    Quotient width never exceeds dividend width, even for malformed inputs.

    source
    noncomputable def MIPRE.LowDegree.BinaryPolynomial.isEmptyDivProg :
    Cost.PolyTimeFun Cost.BitStr Bool
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def MIPRE.LowDegree.BinaryPolynomial.quotientBitsProg :
      Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr) Cost.BitStr

      One uniform ambient program for polynomial quotient, hence for exact division.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem MIPRE.LowDegree.BinaryPolynomial.quotientBitsProg_apply (a b : Cost.BitStr) :
        quotientBitsProg.toFun (a, b) = quotientBits a b