Documentation

MIPRE.Foundations.LowDegree.BinaryPrimePowerDispatch

Uniform dispatch and prime-power polynomial decomposition #

source
theorem MIPRE.LowDegree.BinaryPolynomial.polyOfBits_X :
polyOfBits [false, true] = Polynomial.X

Degree one has the fixed irreducible polynomial X.

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

Dispatch degree one, powers of two, and odd-prime powers by raw unary inputs.

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

    The dispatch is one fixed total polynomial-time program.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem MIPRE.LowDegree.BinaryPolynomial.primePowerBitsProg_apply (q r : Cost.Unary) :
      primePowerBitsProg.toFun (q, r) = primePowerBits q r
      source
      theorem MIPRE.LowDegree.BinaryPolynomial.primePowerBits_correct (q e : ℕ) (he : e = 0 ∨ Nat.Prime q) :
      have a := primePowerBits (Cost.unary q) (Cost.unary (q ^ e)); List.getLastD a false = true ∧ (polyOfBits a).Monic ∧ Irreducible (polyOfBits a) ∧ (polyOfBits a).natDegree = q ^ e

      Every prime-power contribution is printed as a canonical monic irreducible polynomial.

      source
      theorem MIPRE.LowDegree.BinaryPolynomial.primePowerBits_factorization_correct (n q : ℕ) :
      have a := primePowerBits (Cost.unary q) (Cost.unary (q ^ n.factorization q)); List.getLastD a false = true ∧ (polyOfBits a).Monic ∧ Irreducible (polyOfBits a) ∧ (polyOfBits a).natDegree = q ^ n.factorization q

      Dispatch correctness includes neutral entries outside the prime factorization support.

      source
      noncomputable def MIPRE.LowDegree.BinaryPolynomial.degreePolynomials (u : Cost.Unary) :
      List Cost.BitStr

      The supplied degree is decomposed into a fixed ordered list of irreducible polynomials.

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

        One polynomial-time program prints the entire prime-power polynomial list.

        Equations
        Instances For
          source
          @[simp]
          theorem MIPRE.LowDegree.BinaryPolynomial.degreePolynomialsProg_apply (u : Cost.Unary) :
          degreePolynomialsProg.toFun u = degreePolynomials u
          source
          theorem MIPRE.LowDegree.BinaryPolynomial.degreePolynomials_correct (n : ℕ) (a : Cost.BitStr) :
          a ∈ degreePolynomials (Cost.unary n) → (polyOfBits a).Monic ∧ Irreducible (polyOfBits a)

          Every printed component polynomial is monic and irreducible.

          source
          theorem MIPRE.LowDegree.BinaryPolynomial.degreePolynomials_degrees (n : ℕ) :
          List.map (fun (a : List Bool) => (polyOfBits a).natDegree) (degreePolynomials (Cost.unary n)) = BinaryDegreeFactors.degreeFactors n

          The polynomial degrees are exactly the mathematical prime-power contribution list.