Documentation

MIPRE.Foundations.LowDegree.BinaryOddPrimeProgram

The explicit odd-prime-power construction program #

source
noncomputable def MIPRE.LowDegree.BinaryPolynomial.oddExtensionBits (q r : Cost.Unary) :
Cost.BitStr

The full binary modulus for Shoup's flat auxiliary extension.

Equations
Instances For
    source
    noncomputable def MIPRE.LowDegree.BinaryPolynomial.oddExtensionLowerBits (q r : Cost.Unary) :
    Cost.BitStr

    The lower coefficients used by quotient arithmetic.

    Equations
    Instances For
      source
      noncomputable def MIPRE.LowDegree.BinaryPolynomial.oddTraceBits (q r : Cost.Unary) :
      Cost.BitStr

      The trace generator in the explicitly represented flat extension.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def MIPRE.LowDegree.BinaryPolynomial.oddPrimePowerBits (q r : Cost.Unary) :
        Cost.BitStr

        Print the descended orbit polynomial of the trace generator.

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

          One total polynomial-time program takes unary prime and requested prime-power degree.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem MIPRE.LowDegree.BinaryPolynomial.oddPrimePowerBitsProg_apply (q r : Cost.Unary) :
            oddPrimePowerBitsProg.toFun (q, r) = oddPrimePowerBits q r
            source
            theorem MIPRE.LowDegree.BinaryPolynomial.polyOfBits_oddExtensionBits (q r : ℕ) (hr : 0 < r) :
            polyOfBits (oddExtensionBits (Cost.unary q) (Cost.unary r)) = (polyOfBits (nonresidueLiftBitsProg.toFun (Cost.unary q))).comp (Polynomial.X ^ r)

            The flat printed modulus has the exact Kummer composition semantics.

            source
            theorem MIPRE.LowDegree.BinaryPolynomial.oddExtensionBits_correct (q e : ℕ) (hq : Nat.Prime q) (hq2 : q ≠ 2) :
            have a := oddExtensionBits (Cost.unary q) (Cost.unary (q ^ e)); List.getLastD a false = true ∧ (polyOfBits a).Monic ∧ Irreducible (polyOfBits a) ∧ (polyOfBits a).natDegree = (polyOfBits (cyclotomicSeedBits (Cost.unary q))).natDegree * q ^ e

            Every requested odd-prime-power flat modulus is a canonical irreducible polynomial.

            source
            theorem MIPRE.LowDegree.BinaryPolynomial.oddExtensionLowerBits_spec (q e : ℕ) (hq : Nat.Prime q) (hq2 : q ≠ 2) :
            have a := oddExtensionBits (Cost.unary q) (Cost.unary (q ^ e)); have p := oddExtensionLowerBits (Cost.unary q) (Cost.unary (q ^ e)); List.length p = (polyOfBits a).natDegree ∧ polyOfBits a = polyOfBits (p ++ [true]) ∧ p ≠ []

            Every lower extension representation has the correct modulus width and equation.

            source
            theorem MIPRE.LowDegree.BinaryPolynomial.oddTraceBits_width (q r : Cost.Unary) :
            List.length (oddTraceBits q r) = List.length (oddExtensionLowerBits q r)

            The trace vector has exactly the flat extension width.

            source
            theorem MIPRE.LowDegree.BinaryPolynomial.evalBits_oddTraceBits_of_root {R : Type u_1} [CommRing R] [CharP R 2] (z : R) (q e : ℕ) (hq : Nat.Prime q) (hq2 : q ≠ 2) (hz : z ^ List.length (oddExtensionLowerBits (Cost.unary q) (Cost.unary (q ^ e))) = evalBits z (oddExtensionLowerBits (Cost.unary q) (Cost.unary (q ^ e)))) :
            evalBits z (oddTraceBits (Cost.unary q) (Cost.unary (q ^ e))) = ∑ i ∈ Finset.range (polyOfBits (cyclotomicSeedBits (Cost.unary q))).natDegree, z ^ 2 ^ (q ^ e * i)

            Interpreting the printed trace vector gives Shoup's precise Frobenius-stride sum.