Documentation

MIPRE.Foundations.LowDegree.BinaryArtinSchreierProg

Effective substitution by the Artin–Schreier polynomial #

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

One Horner step for substitution by X² + X. Both XOR inputs have equal width.

Equations
Instances For
    source
    @[simp]
    theorem MIPRE.LowDegree.BinaryPolynomial.artinSchreierStep_length (a : Cost.BitStr) (b : Bool) :
    List.length (artinSchreierStep a b) = List.length a + 2
    source
    theorem MIPRE.LowDegree.BinaryPolynomial.evalBits_artinSchreierStep {R : Type u_1} [CommRing R] [CharP R 2] (z : R) (a : Cost.BitStr) (b : Bool) :
    evalBits z (artinSchreierStep a b) = ofBool b + (z ^ 2 + z) * evalBits z a

    The Horner step has its stated semantics in every characteristic-two ring.

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

    Substitute X² + X, then remove redundant trailing zero coefficients.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem MIPRE.LowDegree.BinaryPolynomial.evalBits_substituteArtinSchreierBits {R : Type u_1} [CommRing R] [CharP R 2] (z : R) (a : Cost.BitStr) :
      evalBits z (substituteArtinSchreierBits a) = evalBits (z ^ 2 + z) a
      source
      theorem MIPRE.LowDegree.BinaryPolynomial.polyOfBits_substituteArtinSchreierBits (a : Cost.BitStr) :
      polyOfBits (substituteArtinSchreierBits a) = (polyOfBits a).comp (Polynomial.X ^ 2 + Polynomial.X)

      The executable substitution agrees with polynomial composition.

      source
      theorem MIPRE.LowDegree.BinaryPolynomial.fold_artinSchreierStep_length (l a : Cost.BitStr) :
      List.length (List.foldl artinSchreierStep a l) = List.length a + 2 * List.length l
      source
      noncomputable def MIPRE.LowDegree.BinaryPolynomial.artinSchreierStepProg :
      Cost.PolyTimeFun (Cost.BitStr × Bool) Cost.BitStr
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem MIPRE.LowDegree.BinaryPolynomial.artinSchreierStep_bounded :
        artinSchreierStepProg.FoldBounded (12 * Polynomial.X + 1)
        source
        noncomputable def MIPRE.LowDegree.BinaryPolynomial.substituteArtinSchreierBitsProg :
        Cost.PolyTimeFun Cost.BitStr Cost.BitStr

        A single ambient polynomial-time program for X² + X substitution.

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