A capped unary program for maximal prime-power divisors

@[reducible, inline]

abbrev MIPRE.LowDegree.DegreeArithmetic.PrimePowerState : Type

Target integer, candidate prime, and current prime power, all unary.

Equations

• MIPRE.LowDegree.DegreeArithmetic.PrimePowerState = (MIPRE.Cost.Unary × MIPRE.Cost.Unary × MIPRE.Cost.Unary)

def MIPRE.LowDegree.DegreeArithmetic.primePowerStep (s : PrimePowerState) : PrimePowerState

Advance a dividing prime power, capping every replacement by the target input.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LowDegree.DegreeArithmetic.primePowerStepProg : Cost.PolyTimeFun (PrimePowerState × Unit) PrimePowerState

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.LowDegree.DegreeArithmetic.primePowerStep_shape (s : PrimePowerState) : (primePowerStep s).1 = s.1 ∧ (primePowerStep s).2.1 = s.2.1 ∧ List.length (primePowerStep s).2.2 ≤ max (List.length s.2.2) (List.length s.1)

theorem MIPRE.LowDegree.DegreeArithmetic.fold_primePowerStep_shape (u : Cost.Unary) (s : PrimePowerState) : (List.foldl (fun (s : PrimePowerState) (x : Unit) => primePowerStep s) s u).1 = s.1 ∧ (List.foldl (fun (s : PrimePowerState) (x : Unit) => primePowerStep s) s u).2.1 = s.2.1 ∧ List.length (List.foldl (fun (s : PrimePowerState) (x : Unit) => primePowerStep s) s u).2.2 ≤ max (List.length s.2.2) (List.length s.1)

theorem MIPRE.LowDegree.DegreeArithmetic.primePowerStep_bounded : primePowerStepProg.FoldBounded (6 * Polynomial.X + 6)

def MIPRE.LowDegree.DegreeArithmetic.rawPrimePower (n q : Cost.Unary) : Cost.Unary

The capped maximum-power search.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LowDegree.DegreeArithmetic.rawPrimePowerProg : Cost.PolyTimeFun (Cost.Unary × Cost.Unary) Cost.Unary

Uniform polynomial-time implementation of the capped maximum-power search.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.LowDegree.DegreeArithmetic.rawPrimePowerProg_apply (n q : Cost.Unary) : rawPrimePowerProg.toFun (n, q) = rawPrimePower n q

theorem MIPRE.LowDegree.DegreeArithmetic.primePowerStep_progress (n q j : ℕ) (hn : 0 < n) (hq : Nat.Prime q) (hj : j < n.factorization q) : primePowerStep (Cost.unary n, Cost.unary q, Cost.unary (q ^ j)) = (Cost.unary n, Cost.unary q, Cost.unary (q ^ (j + 1)))

theorem MIPRE.LowDegree.DegreeArithmetic.primePowerStep_fixed (n q : ℕ) (hn : 0 < n) (hq : Nat.Prime q) : primePowerStep (Cost.unary n, Cost.unary q, Cost.unary (q ^ n.factorization q)) = (Cost.unary n, Cost.unary q, Cost.unary (q ^ n.factorization q))

theorem MIPRE.LowDegree.DegreeArithmetic.iterate_primePowerStep (n q t : ℕ) (hn : 0 < n) (hq : Nat.Prime q) : primePowerStep^[t] (Cost.unary n, Cost.unary q, [()]) = (Cost.unary n, Cost.unary q, Cost.unary (q ^ min t (n.factorization q)))

theorem MIPRE.LowDegree.DegreeArithmetic.fold_primePowerStep (u : Cost.Unary) (s : PrimePowerState) : List.foldl (fun (s : PrimePowerState) (x : Unit) => primePowerStep s) s u = primePowerStep^[List.length u] s

theorem MIPRE.LowDegree.DegreeArithmetic.rawPrimePower_correct (n q : ℕ) (hq : Nat.Prime q) : rawPrimePower (Cost.unary n) (Cost.unary q) = Cost.unary (q ^ n.factorization q)

Unary input length supplies enough iterations to reach the maximal prime-power divisor.

def MIPRE.LowDegree.DegreeArithmetic.primePowerUnary (n q : Cost.Unary) : Cost.Unary

Nonprime candidates contribute the neutral degree one.

Equations

• MIPRE.LowDegree.DegreeArithmetic.primePowerUnary n q = if Nat.Prime (List.length q) then MIPRE.LowDegree.DegreeArithmetic.rawPrimePower n q else [()]

noncomputable def MIPRE.LowDegree.DegreeArithmetic.primePowerUnaryProg : Cost.PolyTimeFun (Cost.Unary × Cost.Unary) Cost.Unary

One total polynomial-time program for each prime's contribution to a unary degree.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.LowDegree.DegreeArithmetic.primePowerUnaryProg_apply (n q : Cost.Unary) : primePowerUnaryProg.toFun (n, q) = primePowerUnary n q

theorem MIPRE.LowDegree.DegreeArithmetic.primePowerUnary_correct (n q : ℕ) : primePowerUnary (Cost.unary n) (Cost.unary q) = Cost.unary (q ^ n.factorization q)

The output is exactly the canonical prime-power component of the target degree.