Power-of-two padding with unary output

The inner PCP dimension must itself be a power of two. ceilPower is the least power of two at least its input, with value one at zero. ceilPowerProg produces that many unary slots in polynomial time in the number of input slots. Its loop explicitly caps intermediate vectors, rather than assuming that unrestricted unary exponentiation has polynomial cost.

def MIPRE.SAT.ceilPower (n : ℕ) : ℕ

The least power of two at least n, including ceilPower 0 = 1.

Equations

• MIPRE.SAT.ceilPower n = 2 ^ (n - 1).size

theorem MIPRE.SAT.le_ceilPower (n : ℕ) : n ≤ ceilPower n

theorem MIPRE.SAT.ceilPower_le_twice (n : ℕ) : ceilPower n ≤ 2 * n + 1

theorem MIPRE.SAT.unary_eq_length (u : Cost.Unary) : u = Cost.unary (List.length u)

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

def MIPRE.SAT.growStep (s : Cost.Unary × Cost.Unary) : Bool → Cost.Unary × Cost.Unary

Equations

• MIPRE.SAT.growStep s x✝ = (s.1, List.take (List.length s.1) (s.2 ++ s.2))

theorem MIPRE.SAT.grow_bound (fuel : Cost.BitStr) (cap acc : Cost.Unary) : (List.foldl growStep (cap, acc) fuel).1 = cap ∧ List.length (List.foldl growStep (cap, acc) fuel).2 ≤ max (List.length cap) (List.length acc)

theorem MIPRE.SAT.min_mul_min (c p v : ℕ) (hp : 1 ≤ p) : min c (p * min c v) = min c (p * v)

theorem MIPRE.SAT.grow_length (fuel : Cost.BitStr) (cap acc : Cost.Unary) (ha : List.length acc ≤ List.length cap) : List.length (List.foldl growStep (cap, acc) fuel).2 = min (List.length cap) (2 ^ List.length fuel * List.length acc)

noncomputable def MIPRE.SAT.growStepProg : Cost.PolyTimeFun ((Cost.Unary × Cost.Unary) × Bool) (Cost.Unary × Cost.Unary)

Equations

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

theorem MIPRE.SAT.growStep_bounded : growStepProg.FoldBounded (2 * Polynomial.X + 4)

noncomputable def MIPRE.SAT.ceilPowerProg : Cost.PolyTimeFun Cost.Unary Cost.Unary

Uniform power-of-two padding, with polynomial cost in the supplied unary length.

Equations

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

@[simp]

theorem MIPRE.SAT.ceilPowerProg_apply (u : Cost.Unary) : ceilPowerProg.toFun u = Cost.unary (ceilPower (List.length u))