Documentation

MIPRE.Foundations.LowDegree.BinaryDegreeDecomposition

Executable prime-power decomposition of a unary requested degree #

source
def MIPRE.LowDegree.DegreeArithmetic.ascendingUnary (u : Cost.Unary) :
List Cost.Unary

Enumerate all candidate prime indices in ascending order.

Equations
Instances For
    source
    theorem MIPRE.LowDegree.DegreeArithmetic.descendingUnary_cons (u : Cost.Unary) :
    descendingUnary (() :: u) = (() :: u) :: descendingUnary u
    source
    theorem MIPRE.LowDegree.DegreeArithmetic.ascendingUnary_eq (u : Cost.Unary) :
    ascendingUnary u = List.ofFn fun (i : Fin (List.length u + 1)) => Cost.unary ↑i

    The enumeration is the bounded canonical unary list from zero to the input.

    source
    noncomputable def MIPRE.LowDegree.DegreeArithmetic.ascendingUnaryProg :
    Cost.PolyTimeFun Cost.Unary (List Cost.Unary)

    A polynomial-time ascending unary enumeration.

    Equations
    Instances For
      source
      @[simp]
      theorem MIPRE.LowDegree.DegreeArithmetic.ascendingUnaryProg_apply (u : Cost.Unary) :
      ascendingUnaryProg.toFun u = ascendingUnary u
      source
      def MIPRE.LowDegree.DegreeArithmetic.primePowerPairs (u : Cost.Unary) :
      List (Cost.Unary × Cost.Unary)

      Prime indices paired with their maximal dividing prime power; neutral entries have power one.

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

        One globally polynomial-time prime-power decomposition program.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem MIPRE.LowDegree.DegreeArithmetic.primePowerPairsProg_apply (u : Cost.Unary) :
          primePowerPairsProg.toFun u = primePowerPairs u
          source
          theorem MIPRE.LowDegree.DegreeArithmetic.primePowerPairs_eq (n : ℕ) :
          primePowerPairs (Cost.unary n) = List.ofFn fun (i : Fin (n + 1)) => (Cost.unary ↑i, Cost.unary (↑i ^ n.factorization ↑i))

          The executing decomposition agrees exactly with the mathematical prime-power factors.

          source
          theorem MIPRE.LowDegree.DegreeArithmetic.primePowerPairs_degrees (n : ℕ) :
          List.map (fun (s : Cost.Unary × Cost.Unary) => List.length s.2) (primePowerPairs (Cost.unary n)) = BinaryDegreeFactors.degreeFactors n

          Decoding the listed powers gives the factor list whose product is the requested degree.

          source
          theorem MIPRE.LowDegree.DegreeArithmetic.primePowerPairs_prod (n : ℕ) (hn : 0 < n) :
          (List.map (fun (s : Cost.Unary × Cost.Unary) => List.length s.2) (primePowerPairs (Cost.unary n))).prod = n

          Every positive degree is the product of the computed prime-power contributions.

          source
          theorem MIPRE.LowDegree.DegreeArithmetic.primePowerPairs_pairwise (n : ℕ) :
          List.Pairwise Nat.Coprime (List.map (fun (s : Cost.Unary × Cost.Unary) => List.length s.2) (primePowerPairs (Cost.unary n)))

          Computed prime-power contributions are pairwise coprime.