The output indicator at constant parameters #

At a fixed index, the parameters (ℓ, ◇) of the output indicator are a constant p, and the parameter program is PolyTimeFun.const p. Three facts about lstarProg (const p) L P:

its check runs within a polynomial, independent of p, of the size of its input plus esize p (lstarFinal_const_timeBound), so the indicator accepts what it accepts within 2^(E (k + 1) (τ + ρ + 1)) for one universal constant E, when the two programs run within T (|d| + 1)^k with T ≤ 2^τ and the input and p have size below 2^ρ (lstar_const_acceptsWithin_pow);
the program is a polynomial-time function of (L, P, p) (lstarProgF, lstarProgF_apply);
its size is a constant plus 4 |L| + |P| + |p| (esize_lstarProg_const): L occurs four times, P once and p once, as the constant the parameter program const p outputs.

Polynomials below powers #

source

theorem MIPRE.Tailored.AnsRed.polynomial_eval_le_add_two_pow (Q : Polynomial ℕ) :

∃ (D : ℕ), ∀ (x : ℕ), Polynomial.eval x Q ≤ (x + 2) ^ D

Every polynomial over ℕ is at most (x + 2)^D for some D.

The time bound of the check #

source

theorem MIPRE.Tailored.AnsRed.lstarFinal_const_timeBound_eq (p : Cost.Unary × Cost.Unary) :

(lstarFinal (Cost.PolyTimeFun.const p)).timeBound = Polynomial.X + 1 + (lstarIdx.timeBound + (Polynomial.C (Cost.esize p)).comp lstarIdx.timeBound + 1) + 1 + lstarCore.timeBound.comp (Polynomial.X + 1 + (lstarIdx.timeBound + (Polynomial.C (Cost.esize p)).comp lstarIdx.timeBound + 1) + 1) + 1

The time bound of the check at the constant parameters p, unfolded.

source

theorem MIPRE.Tailored.AnsRed.lstarFinal_const_timeBound :

∃ (G : Polynomial ℕ), ∀ (p : Cost.Unary × Cost.Unary) (A : ℕ), Polynomial.eval A (lstarFinal (Cost.PolyTimeFun.const p)).timeBound ≤ Polynomial.eval (A + Cost.esize p) G

The check at constant parameters runs within a polynomial independent of the parameters, of the size of its input plus that of the parameters.

Acceptance within a power of two #

source

theorem MIPRE.Decider.AcceptsWithin.mono {D : Decider} {n : ℕ} {x y a b : Cost.BitStr} {T T' : ℕ} (h : D.AcceptsWithin n x y a b T) (hT : T ≤ T') :

D.AcceptsWithin n x y a b T'

source

theorem MIPRE.Tailored.AnsRed.lstarBound_const_le :

∃ (H : Polynomial ℕ), ∀ (p : Cost.Unary × Cost.Unary) (T k S Z : ℕ), lstarBound (Cost.PolyTimeFun.const p) T k S Z ≤ Polynomial.eval (T * Z ^ k + S + Cost.esize p) H

lstarBound at constant parameters is at most a fixed polynomial of T Z^k + S + |p|.

source

theorem MIPRE.Tailored.AnsRed.lstar_const_acceptsWithin_pow :

∃ (E : ℕ), 1 ≤ E ∧ ∀ (p : Cost.Unary × Cost.Unary) {ℓ : ℕ} (V : TailoredVerifier ℓ) {n T k τ ρ : ℕ} {x y a b : Cost.BitStr}, V.len.TimeBoundAt n T k → V.lp.TimeBoundAt n T k → T ≤ 2 ^ τ → Cost.esize (n, x, y, a, b) + 1 ≤ 2 ^ ρ → Cost.esize p ≤ 2 ^ ρ → (lstar (Cost.PolyTimeFun.const p) V).Accepts n x y a b → (lstar (Cost.PolyTimeFun.const p) V).AcceptsWithin n x y a b (2 ^ (E * (k + 1) * (τ + ρ + 1)))

The output indicator at constant parameters accepts within 2^(E (k+1) (τ+ρ+1)) whatever it accepts, when its two programs run within T (|d| + 1)^k with T ≤ 2^τ, and the input and the parameters have size below 2^ρ; E is one universal constant.

The program, as a polynomial-time function of its data #

source

noncomputable def MIPRE.Tailored.AnsRed.consProgF :

Cost.PolyTimeFun (Cost.Prog × Cost.Prog) Cost.Prog

(h, t) ↦ cons h t, in polynomial time.

Equations

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

Instances For

source

@[simp]

theorem MIPRE.Tailored.AnsRed.consProgF_apply (h t : Cost.Prog) :

consProgF.toFun (h, t) = h.cons t

source

noncomputable def MIPRE.Tailored.AnsRed.constProgF {α : Type u_1} [Cost.SizedEncoding α] :

Cost.PolyTimeFun α Cost.Prog

p ↦ const (encode p), the program outputting p, in polynomial time.

Equations

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

Instances For

source

@[simp]

theorem MIPRE.Tailored.AnsRed.constProgF_apply {α : Type u_1} [Cost.SizedEncoding α] (a : α) :

constProgF.toFun a = Cost.Prog.const (Cost.encode a)

source

noncomputable def MIPRE.Tailored.AnsRed.pushProgF (F : Cost.Prog) :

Cost.PolyTimeFun Cost.Prog Cost.Prog

P ↦ pushProg F P, in polynomial time.

Equations

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

Instances For

source

@[simp]

theorem MIPRE.Tailored.AnsRed.pushProgF_apply (F P : Cost.Prog) :

(pushProgF F).toFun P = F.pushProg P

source

theorem MIPRE.Tailored.AnsRed.lstarFinal_const_code (p : Cost.Unary × Cost.Unary) :

(lstarFinal (Cost.PolyTimeFun.const p)).code = ((Cost.Prog.var 0).cons (lstarIdx.code.let_ (Cost.Prog.const (Cost.encode p)))).let_ lstarCore.code

The program of the check at constant parameters: the parameter-free check on the input and the constant p.

source

noncomputable def MIPRE.Tailored.AnsRed.lstarFinalCodeF :

Cost.PolyTimeFun (Cost.Unary × Cost.Unary) Cost.Prog

p ↦ (lstarFinal (const p)).code, in polynomial time.

Equations

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

Instances For

source

@[simp]

theorem MIPRE.Tailored.AnsRed.lstarFinalCodeF_apply (p : Cost.Unary × Cost.Unary) :

lstarFinalCodeF.toFun p = (lstarFinal (Cost.PolyTimeFun.const p)).code

source

noncomputable def MIPRE.Tailored.AnsRed.lstarProgF :

Cost.PolyTimeFun ((Cost.Prog × Cost.Prog) × Cost.Unary × Cost.Unary) Cost.Prog

The output indicator at constant parameters, as a polynomial-time function of the answer-length calculator, the processor and the parameters.

Equations

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

Instances For

source

theorem MIPRE.Tailored.AnsRed.lstarProgF_apply (L P : Cost.Prog) (p : Cost.Unary × Cost.Unary) :

lstarProgF.toFun ((L, P), p) = lstarProg (Cost.PolyTimeFun.const p) L P

The size of the program #

source

noncomputable def MIPRE.Tailored.AnsRed.lstarProgSize₀ :

ℕ

The constant part of the size of the output indicator at constant parameters (esize_lstarProg_const): the five input builders of the canonical decider, the index projection and the parameter-free check, and 366 for the wiring.

Instances For

source