Polynomial-time unary arithmetic for degree decomposition

noncomputable def MIPRE.LowDegree.DegreeArithmetic.isEmptyProg {α : Type u_1} [Cost.SizedEncoding α] : Cost.PolyTimeFun (List α) Bool

A list emptiness test, uniform in its element encoding.

Equations

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

@[simp]

theorem MIPRE.LowDegree.DegreeArithmetic.isEmptyProg_apply {α : Type u_1} [Cost.SizedEncoding α] (a : List α) : isEmptyProg.toFun a = a.isEmpty

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

Compare unary integers by removing the second length from the first.

Equations

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

@[simp]

theorem MIPRE.LowDegree.DegreeArithmetic.leUnaryProg_apply (u v : Cost.Unary) : leUnaryProg.toFun (u, v) = decide (List.length u ≤ List.length v)

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

Exact equality of unary values.

Equations

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

@[simp]

theorem MIPRE.LowDegree.DegreeArithmetic.eqUnaryProg_apply (u v : Cost.Unary) : eqUnaryProg.toFun (u, v) = decide (List.length u = List.length v)

@[reducible, inline]

abbrev MIPRE.LowDegree.DegreeArithmetic.ModState : Type

Equations

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

def MIPRE.LowDegree.DegreeArithmetic.modStep (s : ModState) : ModState

Increment the remainder and reset it when the modulus is reached.

Equations

• MIPRE.LowDegree.DegreeArithmetic.modStep s = (s.1, if List.length s.2 + 1 = List.length s.1 then [] else () :: s.2)

noncomputable def MIPRE.LowDegree.DegreeArithmetic.modStepProg : Cost.PolyTimeFun (ModState × Unit) ModState

Equations

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

theorem MIPRE.LowDegree.DegreeArithmetic.modStepProg_apply (s : ModState) (x : Unit) : modStepProg.toFun (s, x) = modStep s

theorem MIPRE.LowDegree.DegreeArithmetic.modStep_growth (s : ModState) (x : Unit) : Cost.esize (modStepProg.toFun (s, x)) ≤ Cost.esize s + Polynomial.eval (Cost.esize x) 2

theorem MIPRE.LowDegree.DegreeArithmetic.modStep_mod (d : Cost.Unary) (n : ℕ) : modStep (d, Cost.unary (n % List.length d)) = (d, Cost.unary ((n + 1) % List.length d))

One counter step advances a canonical remainder by one modulo the divisor.

theorem MIPRE.LowDegree.DegreeArithmetic.iterate_modStep (d : Cost.Unary) (n : ℕ) : modStep^[n] (d, []) = (d, Cost.unary (n % List.length d))

theorem MIPRE.LowDegree.DegreeArithmetic.fold_modStep (u : Cost.Unary) (s : ModState) : List.foldl (fun (s : ModState) (x : Unit) => modStep s) s u = modStep^[List.length u] s

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

A globally polynomial-time unary remainder program, including divisor zero.

Equations

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

@[simp]

theorem MIPRE.LowDegree.DegreeArithmetic.modUnaryProg_apply (u d : Cost.Unary) : modUnaryProg.toFun (u, d) = Cost.unary (List.length u % List.length d)

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

A divisibility test on two unary values.

Equations

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

@[simp]

theorem MIPRE.LowDegree.DegreeArithmetic.dvdUnaryProg_apply (d u : Cost.Unary) : dvdUnaryProg.toFun (d, u) = decide (List.length d ∣ List.length u)

theorem MIPRE.LowDegree.DegreeArithmetic.iterate_tail_size (n : ℕ) (u : Cost.Unary) : Cost.esize (Cost.PolyTimeFun.tail.toFun^[n] u) ≤ Polynomial.eval (Cost.esize u) Polynomial.X

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

Enumerate unary values from the input down through zero, without duplicates.

Equations

• MIPRE.LowDegree.DegreeArithmetic.descendingUnary u = MIPRE.Cost.recordIterates List.tail (() :: u) u

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

Every bounded candidate degree can be printed in polynomial time.

Equations

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

@[simp]

theorem MIPRE.LowDegree.DegreeArithmetic.descendingUnaryProg_apply (u : Cost.Unary) : descendingUnaryProg.toFun u = descendingUnary u

theorem MIPRE.LowDegree.DegreeArithmetic.descendingUnary_eq (u : Cost.Unary) : descendingUnary u = List.ofFn fun (i : Fin (List.length u + 1)) => List.drop (↑i) u

The enumeration consists exactly of the successive suffixes.

theorem MIPRE.LowDegree.DegreeArithmetic.mem_descendingUnary_iff (u d : Cost.Unary) : d ∈ descendingUnary u ↔ List.length d ≤ List.length u

A unary value occurs in the descending enumeration exactly when it is bounded by the input.

theorem MIPRE.LowDegree.DegreeArithmetic.esize_unary_list (u : Cost.Unary) : Cost.esize u = 2 * List.length u + 1

Every unary encoding has exact size linear in its value.

@[reducible, inline]

abbrev MIPRE.LowDegree.DegreeArithmetic.MultiplyState : Type

Equations

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

def MIPRE.LowDegree.DegreeArithmetic.multiplyStep (s : MultiplyState) : Unit → MultiplyState

Equations

• MIPRE.LowDegree.DegreeArithmetic.multiplyStep s x✝ = (s.1, s.1 ++ s.2)

theorem MIPRE.LowDegree.DegreeArithmetic.fold_multiplyStep (pre v acc : Cost.Unary) : (List.foldl multiplyStep (v, acc) pre).1 = v ∧ List.length (List.foldl multiplyStep (v, acc) pre).2 = List.length acc + List.length pre * List.length v

noncomputable def MIPRE.LowDegree.DegreeArithmetic.multiplyStepProg : Cost.PolyTimeFun (MultiplyState × Unit) MultiplyState

Equations

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

theorem MIPRE.LowDegree.DegreeArithmetic.multiplyStep_bounded : multiplyStepProg.FoldBounded (10 * Polynomial.X ^ 2 + 10 * Polynomial.X + 10)

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

Unary multiplication has a global quadratic-size fold implementation.

Equations

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

@[simp]

theorem MIPRE.LowDegree.DegreeArithmetic.mulUnaryProg_apply (u v : Cost.Unary) : mulUnaryProg.toFun (u, v) = Cost.unary (List.length u * List.length v)