Documentation

MIPRE.Foundations.LowDegree.UnaryPrimality

Polynomial-time trial primality for unary degree parameters #

source
theorem MIPRE.LowDegree.DegreeArithmetic.tail_empty_iff (u : Cost.Unary) :
(List.tail u).isEmpty = true ↔ List.length u ≤ 1
source
def MIPRE.LowDegree.DegreeArithmetic.trialCheck (q d : Cost.Unary) :
Bool

Ignore candidate divisors zero and one, and reject every other actual divisor.

Equations
Instances For
    source
    noncomputable def MIPRE.LowDegree.DegreeArithmetic.trialCheckProg :
    Cost.PolyTimeFun (Cost.Unary × Cost.Unary) Bool
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[reducible, inline]
      abbrev MIPRE.LowDegree.DegreeArithmetic.PrimeState :
      Type
      Equations
      Instances For
        source
        def MIPRE.LowDegree.DegreeArithmetic.primeStep (s : PrimeState) (d : Cost.Unary) :
        PrimeState
        Equations
        Instances For
          source
          theorem MIPRE.LowDegree.DegreeArithmetic.fold_primeStep (ds : List Cost.Unary) (q : Cost.Unary) (b : Bool) :
          List.foldl primeStep (q, b) ds = (q, b && ds.all (trialCheck q))
          source
          noncomputable def MIPRE.LowDegree.DegreeArithmetic.primeStepProg :
          Cost.PolyTimeFun (PrimeState × Cost.Unary) PrimeState
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem MIPRE.LowDegree.DegreeArithmetic.primeStep_growth (s : PrimeState) (d : Cost.Unary) :
            Cost.esize (primeStepProg.toFun (s, d)) ≤ Cost.esize s + Polynomial.eval (Cost.esize d) 2
            source
            noncomputable def MIPRE.LowDegree.DegreeArithmetic.allTrialsProg :
            Cost.PolyTimeFun (List Cost.Unary × Cost.Unary) Bool
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def MIPRE.LowDegree.DegreeArithmetic.primeUnary (q : Cost.Unary) :
              Bool

              The raw trial-division predicate.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                theorem MIPRE.LowDegree.DegreeArithmetic.primeUnary_eq (q : Cost.Unary) :
                primeUnary q = decide (Nat.Prime (List.length q))

                Trial division through all smaller unary candidates is exactly primality.

                source
                noncomputable def MIPRE.LowDegree.DegreeArithmetic.primeUnaryProg :
                Cost.PolyTimeFun Cost.Unary Bool

                One polynomial-time primality program on every unary input.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  @[simp]
                  theorem MIPRE.LowDegree.DegreeArithmetic.primeUnaryProg_apply (q : Cost.Unary) :
                  primeUnaryProg.toFun q = decide (Nat.Prime (List.length q))