The costs of the introspection processor

Issue #281. The linear-constraints processor lpIntroC c U V λ of LpIntro.lean:

• lpIntroC_size, lpIntroC_size_le: its description has size at most C (λ + 1)^C, whatever the input programs V (the clamped description has size at most 19 (λ + 1));
• core_runs_poly: the core runs within a fixed polynomial of any bound v of the input, the clock 2^{(λn + 1)^5} and Q, R (the decision kernel's prog_runs_poly, the unary conversion, and the core's PolyTimeFun on the prepared input);
• lpIntroC_budget: one constant C with the processor within 2^{(λn + 1)^C} at degree C on every input, malformed included, and for every V — the shape of Introspection.budget.

The size of the description

theorem MIPRE.Tailored.Intro.LpIntro.esize_lenWrap (p : Cost.Prog) : Cost.esize (LenIntro.lenWrap p) = Cost.esize p + 54

theorem MIPRE.Tailored.Intro.LpIntro.lpIntroC_size (c : ℕ) (U : Cost.ClockedUniversalMachine) (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam : ℕ) : (lpIntroC c U V lam).size ≤ Cost.esize (core c U) + 19 * (lam + 1) + 89

The size of the processor's description.

theorem MIPRE.Tailored.Intro.LpIntro.lpIntroC_size_le (c : ℕ) (U : Cost.ClockedUniversalMachine) : ∃ (C : ℕ), ∀ (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam : ℕ), (lpIntroC c U V lam).size ≤ C * (lam + 1) ^ C

The processor's description has size at most C (λ + 1)^C, for every input.

The run of the core

noncomputable def MIPRE.Tailored.Intro.LpIntro.bothPoly : Polynomial ℕ

A polynomial for the conversion of (Q, R) to unary.

Equations

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

theorem MIPRE.Tailored.Intro.LpIntro.bothPoly_eval (v : ℕ) : Polynomial.eval v bothPoly = 2 * Introspection.PauliSamplerParameters.unaryMajorant v + 12 * v + 22

theorem MIPRE.Tailored.Intro.LpIntro.esize_le_of_le {x v : ℕ} (h : x ≤ v) : Cost.esize x ≤ 4 * v + 1

theorem MIPRE.Tailored.Intro.LpIntro.bothCost_le {Q R v : ℕ} (hQ : Q ≤ v) (hR : R ≤ v) : Introspection.ClockArithmetic.unaryCost Q + Introspection.ClockArithmetic.unaryCost R + Cost.esize Q + Cost.esize R + 2 * Q + 2 * R + 20 ≤ Polynomial.eval v bothPoly

noncomputable def MIPRE.Tailored.Intro.LpIntro.corePoly (c : ℕ) (U : Cost.ClockedUniversalMachine) : Polynomial ℕ

The polynomial of the core.

Equations

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

theorem MIPRE.Tailored.Intro.LpIntro.core_runs_poly {c v : ℕ} (hc : 1 ≤ c) (U : Cost.ClockedUniversalMachine) (M : InputRuns.Metadata) (x : Cost.Data) (hl : 1 ≤ M.2) (hn : 1 ≤ Introspection.ClockSimulation.indexReader.toFun x) (hz : Cost.esize M + x.size + 1 ≤ v) (hB : Introspection.ansBound 5 M.2 (Introspection.ClockSimulation.indexReader.toFun x) ≤ v) (hQ : Introspection.SourceCompiler.registerBits c M.2 (Introspection.ClockSimulation.indexReader.toFun x) ≤ v) (hR : Introspection.SourceCompiler.originalBound M.2 (Introspection.ClockSimulation.indexReader.toFun x) ≤ v) : ∃ t ≤ Polynomial.eval v (corePoly c U), (core c U).Runs ((Cost.encode M).cons x) (Cost.encode ((kernel U).toFun (kernelInput c M x, Cost.unary (Introspection.SourceCompiler.registerBits c M.2 (Introspection.ClockSimulation.indexReader.toFun x)), Cost.unary (Introspection.SourceCompiler.originalBound M.2 (Introspection.ClockSimulation.indexReader.toFun x))))) t

The core runs within a fixed polynomial of any bound v of the input, the clock, Q and R, at positive λ and index.

The budget

theorem MIPRE.Tailored.Intro.LpIntro.lpIntroC_runs_poly {c v : ℕ} (hc : 1 ≤ c) (U : Cost.ClockedUniversalMachine) (V : Cost.Prog × Cost.Prog × Cost.Prog) {lam n : ℕ} (hl : 1 ≤ lam) (hn : 1 ≤ n) (d : Cost.Data) (hz : 19 * (lam + 1) + 4 * n + d.size + 3 ≤ v) (hB : Introspection.ansBound 5 lam n ≤ v) (hQ : Introspection.SourceCompiler.registerBits c lam n ≤ v) (hR : Introspection.SourceCompiler.originalBound lam n ≤ v) : ∃ (r : Cost.Data), ∃ t ≤ Polynomial.eval v (corePoly c U) + 2 * v + 7, (lpIntroC c U V lam).prog.Runs ((Cost.encode n).cons d) r t

The run of the processor at positive λ and n, on every input, with its cost.

theorem MIPRE.Tailored.Intro.LpIntro.small_le_two_pow {u E : ℕ} (hu : 1 ≤ u) (hE : 3 ≤ E) : 64 * (u + 1) ≤ 2 ^ (u + 1) ^ E

theorem MIPRE.Tailored.Intro.LpIntro.lpIntroC_budget {c : ℕ} (hc : 1 ≤ c) (U : Cost.ClockedUniversalMachine) : ∃ (C : ℕ), ∀ (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam n : ℕ), (lpIntroC c U V lam).TimeBoundAt n (Introspection.ansBound C lam n) C

The costs of the processor, in the shape of Introspection.budget: one constant C with the processor within 2^{(λn + 1)^C} at degree C on every input, for every input description.

At the constant of Introspection.seven

theorem MIPRE.Tailored.Intro.LpIntro.lpIntro_budget : ∃ (C : ℕ), ∀ (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam n : ℕ), (lpIntro V lam).TimeBoundAt n (Introspection.budget C lam n).D (Introspection.budget C lam n).k

The costs of lpIntro, in the shape of Introspection.budget.

theorem MIPRE.Tailored.Intro.LpIntro.lpIntro_size_le : ∃ (C : ℕ), ∀ (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam : ℕ), (lpIntro V lam).size ≤ C * (lam + 1) ^ C

|LP^intro| ≤ C (λ + 1)^C, for every input.