The threshold function of the compression argument

threshold K : PolyTimeFun Prog ℕ computes e ↦ 2 ^ (K + 1 + esize e): the size of the program in unary (sizeProg), plus the constant K + 1 (addConstProg), then the bit string of the power of two (expBitsProg). In the recursive compression argument (planning/compression-track.md, K3 step 4) the constant K is chosen, once and for all, from the overhead polynomials of the toolkit so that n ≥ 2 ^ (K + 1 + |e|) makes every polynomial in |e| + log n at most n.

def MIPRE.Cost.Prog.addConstProg (K : ℕ) : Prog

k ↦ K + k on unary numerals.

Equations

• MIPRE.Cost.Prog.addConstProg K = ((MIPRE.Cost.Prog.const (MIPRE.Cost.Data.ofNat K)).cons (MIPRE.Cost.Prog.var 0)).let_ MIPRE.Cost.Prog.addProg

theorem MIPRE.Cost.Prog.addConstProg_wellScoped (K : ℕ) : WellScoped 1 (addConstProg K)

theorem MIPRE.Cost.Prog.addConstProg_runs (K k : ℕ) : ∃ t ≤ (K + 1) * (4 * K + 2 * k + 15) + 2 * K + 2 * k + 5, (addConstProg K).Runs (Data.ofNat k) (Data.ofNat (K + k)) t

def MIPRE.Cost.Prog.thresholdProg (K : ℕ) : Prog

The threshold program: d ↦ encode (2 ^ (K + 1 + d.size)).

Equations

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

theorem MIPRE.Cost.Prog.thresholdProg_wellScoped (K : ℕ) : WellScoped 1 (thresholdProg K)

theorem MIPRE.Cost.Prog.thresholdProg_runs (K : ℕ) (d : Data) : ∃ t ≤ 40 * (d.size + (K + 4)) ^ 2, (thresholdProg K).Runs d (encode (2 ^ (K + 1 + d.size))) t

noncomputable def MIPRE.Cost.PolyTimeFun.threshold (K : ℕ) : PolyTimeFun Prog ℕ

e ↦ 2 ^ (K + 1 + esize e), in polynomial time.

Equations

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

@[simp]

theorem MIPRE.Cost.PolyTimeFun.threshold_apply (K : ℕ) (e : Prog) : (threshold K).toFun e = 2 ^ (K + 1 + esize e)