The running times of the typed oracularized decider

Piece O4b of planning/oracularization.md (issue #189): the two running times of the typed oracularized decider of Foundations/OracularDecider.lean.

• The core's, on well-formed inputs, in terms of the input verifier's time bounds at the index (core_timeBound). It is what the simulation budget must cover for completeness (OracleDecider.accepts_complete). The sizes of the intermediate results matter here: the input sampler's answer to a marginal query is read off its correctness clause, a vector of length s(n), and not off its running time — otherwise the input decider's time, polynomial of degree k in its input, would compound into degree k².
• The decider's, on every input, in terms of the budget, the parse cut and the index routine's running time (oracleDecider_timeBound): the clocked universal machine's overhead and nothing of the input verifier, whose time enters only through the budget.

Sizes

theorem MIPRE.OracleDecider.size_marginal_le (w : Player) (j : ℕ) (z : Cost.BitStr) : Cost.esize (CL.Sampler.Query.marginal w j z) ≤ Cost.esize z + Cost.esize j + 13

theorem MIPRE.OracleDecider.size_gInput (sp dp : Cost.Prog) (n : ℕ) (z a₁ a₂ : Cost.BitStr) : (gInput sp dp n z a₁ a₂).size = Cost.esize sp + Cost.esize dp + Cost.esize n + Cost.esize z + Cost.esize a₁ + Cost.esize a₂ + 5

The game check's running time

noncomputable def MIPRE.OracleDecider.gameCost (j G TS TD k : ℕ) : ℕ

The cost of the game check at level j on an input of size at most G, when the input sampler runs within TS (|d| + 1)^k and the input decider within TD (|d| + 1)^k.

Equations

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

theorem MIPRE.OracleDecider.univ_marginal_within {ℓ : ℕ} (S : CL.Sampler ℓ) (n TS k : ℕ) (hS : S.TimeBoundAt n TS k) (j : ℕ) (hj₁ : 1 ≤ j) (hj : j ≤ ℓ) (w : Player) (z : Cost.BitStr) (hz : List.length z = S.dim n) : ∃ t ≤ Polynomial.eval (Cost.esize S.prog + Cost.esize n + Cost.esize z + Cost.esize j + 14 + TS * (Cost.esize z + Cost.esize j + 14) ^ k) Cost.selfUniversal.bound, Cost.selfUniversal.univ.Runs ((Cost.encode S.prog).cons (Cost.encode (n, CL.Sampler.Query.marginal w j z))) (Cost.encode (margBits S n j w z)) t

A marginal call through the universal machine, with its cost and the size of its answer.

theorem MIPRE.OracleDecider.size_margBits_le {ℓ : ℕ} (S : CL.Sampler ℓ) (n j : ℕ) (w : Player) (z : Cost.BitStr) (hz : List.length z = S.dim n) : Cost.esize (margBits S n j w z) ≤ 4 * Cost.esize z + 1

The answer to a marginal query is a vector of the seed's length.

theorem MIPRE.OracleDecider.gameProg_runs_within {ℓ : ℕ} (S : CL.Sampler ℓ) (dp : Cost.Prog) (n TS TD k : ℕ) (hS : S.TimeBoundAt n TS k) (hD : ∀ (d : Cost.Data), Cost.HaltsWithin dp ((Cost.encode n).cons d) (TD * (d.size + 1) ^ k)) (j : ℕ) (hj₁ : 1 ≤ j) (hj : j ≤ ℓ) (z a₁ a₂ : Cost.BitStr) (hz : List.length z = S.dim n) {G : ℕ} (hG : (gInput S.prog dp n z a₁ a₂).size ≤ G) : ∃ (v : Bool) (t : ℕ), (gameProg j).Runs (gInput S.prog dp n z a₁ a₂) (Cost.encode v) t ∧ t ≤ gameCost j G TS TD k

The game check's running time on a well-formed seed.

The core's running time

theorem MIPRE.OracleDecider.affine_le_pow {X a b : ℕ} (hX : 2 ≤ X) : a * X + b ≤ X ^ (a + b)

An affine function of X ≥ 2 is below a power of X.

theorem MIPRE.OracleDecider.size_cInput (sp dp : Cost.Prog) (B n : ℕ) (t : Role) (x : Cost.BitStr) (u : Role) (y a b : Cost.BitStr) : (cInput sp dp B n t x u y a b).size = Cost.esize sp + Cost.esize dp + Cost.esize B + Cost.esize n + Cost.esize t + Cost.esize x + Cost.esize u + Cost.esize y + Cost.esize a + Cost.esize b + 9

theorem MIPRE.OracleDecider.arg₁_of_cond (sp dp : Cost.Prog) (B n : ℕ) (t : Role) (x : Cost.BitStr) (u : Role) (y a b : Cost.BitStr) (h : cond₁.toFun (cInput sp dp B n t x u y a b) = true) : ∃ (a₁ : Cost.BitStr) (a₂ : Cost.BitStr), arg₁.toFun ((Cost.PolyTimeFun.id Cost.Data).toFun (cInput sp dp B n t x u y a b)) = gInput sp dp n x a₁ a₂

When the first game check is called, it is called on a game check's input.

theorem MIPRE.OracleDecider.arg₂_of_cond (sp dp : Cost.Prog) (B n : ℕ) (t : Role) (x : Cost.BitStr) (u : Role) (y a b : Cost.BitStr) (h : cond₂.toFun (cInput sp dp B n t x u y a b) = true) (v : Cost.Data) : ∃ (b₁ : Cost.BitStr) (b₂ : Cost.BitStr), arg₂.toFun (Cost.PolyTimeFun.treeHead.toFun ((cInput sp dp B n t x u y a b).cons v)) = gInput sp dp n y b₁ b₂

When the second game check is called, it is called on a game check's input.

theorem MIPRE.OracleDecider.size_repA_le (sp dp : Cost.Prog) (B n : ℕ) (t : Role) (x : Cost.BitStr) (u : Role) (y a b : Cost.BitStr) : (repA.toFun (cInput sp dp B n t x u y a b)).size ≤ Cost.esize a

theorem MIPRE.OracleDecider.size_repB_le (sp dp : Cost.Prog) (B n : ℕ) (t : Role) (x : Cost.BitStr) (u : Role) (y a b : Cost.BitStr) : (repB.toFun (cInput sp dp B n t x u y a b)).size ≤ Cost.esize b

theorem MIPRE.OracleDecider.size_arg₁_le (sp dp : Cost.Prog) (B n : ℕ) (t : Role) (x : Cost.BitStr) (u : Role) (y a b : Cost.BitStr) : (arg₁.toFun ((Cost.PolyTimeFun.id Cost.Data).toFun (cInput sp dp B n t x u y a b))).size ≤ (cInput sp dp B n t x u y a b).size

theorem MIPRE.OracleDecider.size_arg₂_le (sp dp : Cost.Prog) (B n : ℕ) (t : Role) (x : Cost.BitStr) (u : Role) (y a b : Cost.BitStr) (v : Cost.Data) : (arg₂.toFun (Cost.PolyTimeFun.treeHead.toFun ((cInput sp dp B n t x u y a b).cons v))).size ≤ (cInput sp dp B n t x u y a b).size

theorem MIPRE.OracleDecider.size_encode_bool_le (v : Bool) : (Cost.encode v).size ≤ 3

theorem MIPRE.OracleDecider.gameStage_runs_within (j : ℕ) (cond : Cost.PolyTimeFun Cost.Data Bool) (arg view : Cost.PolyTimeFun Cost.Data Cost.Data) (s : Cost.Data) {A Sz tG : ℕ} (hs : s.size ≤ Sz) (harg : (arg.toFun (view.toFun s)).size ≤ A) (hcall : cond.toFun (view.toFun s) = true → ∃ (v : Bool) (t : ℕ), (gameProg j).Runs (arg.toFun (view.toFun s)) (Cost.encode v) t ∧ t ≤ tG) : ∃ (v : Bool) (t : ℕ), (gameStage j cond arg view).Runs s (s.cons (Cost.encode v)) t ∧ t ≤ Polynomial.eval Sz (gameRoute cond arg view).timeBound + 3 * A + 3 * Sz + 3 + tG + Polynomial.eval (Sz + 4) Cost.PolyTimeFun.treePair.timeBound + 18 + (Sz + 8)

A routed game check's running time, both when it calls and when it does not.

noncomputable def MIPRE.OracleDecider.coreCost (j S₀ TS TD k : ℕ) : ℕ

The cost of the core at level j on an input of size S₀.

Equations

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

theorem MIPRE.OracleDecider.core_runs_within {ℓ : ℕ} (V : Verifier (ℓ + 1)) (B n TS TD k : ℕ) (hS : V.sampler.TimeBoundAt n TS k) (hD : V.decider.TimeBoundAt n TD k) (t u : Role) (x y : V.Questions n) (a b : Cost.BitStr) : ∃ (r : Cost.Data) (time : ℕ), (core (ℓ + 1)).Runs (cInput V.sampler.prog V.decider.prog B n t (CL.toBits x) u (CL.toBits y) a b) r time ∧ time ≤ coreCost (ℓ + 1) (cInput V.sampler.prog V.decider.prog B n t (CL.toBits x) u (CL.toBits y) a b).size TS TD k

The core's running time on a well-formed input, when the input verifier's sampler and decider run within TS (|d| + 1)^k and TD (|d| + 1)^k at the index.

Domination

theorem MIPRE.OracleDecider.dom_mul_pow {W X K TS G a b : ℕ} (hX : 2 ≤ X) (hTS : TS ≤ W) (hG : G ≤ a * X + b) : Repeat.Dom W X K 1 1 (a + b) (TS * G ^ K)

TS · G^K, for TS ≤ W and G affine in X ≥ 2.

theorem MIPRE.OracleDecider.dom_poly (Q : Polynomial ℕ) (cy my ey : ℕ) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ (W X K : ℕ) {y : ℕ}, 1 ≤ X → 1 ≤ y → Repeat.Dom W X K cy my ey y → Repeat.Dom W X K c m e (Polynomial.eval y Q)

A polynomial at a dominated argument.

noncomputable def MIPRE.OracleDecider.gamePoly (j : ℕ) : Polynomial ℕ

The polynomials of the game check.

Equations

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

def MIPRE.OracleDecider.gameArgBound (j G TS TD K : ℕ) : ℕ

The one argument dominating every argument of a polynomial in gameCost.

Equations

• MIPRE.OracleDecider.gameArgBound j G TS TD K = 9 * G + MIPRE.Cost.esize j + 30 + TS * (G + MIPRE.Cost.esize j + 15) ^ K + TD * (G + 2 * (4 * G + 1) + 4) ^ K

theorem MIPRE.OracleDecider.gameCost_le (j G TS TD K : ℕ) : gameCost j G TS TD K ≤ 9 * Polynomial.eval (gameArgBound j G TS TD K) (gamePoly j) + Polynomial.eval (Polynomial.eval (gameArgBound j G TS TD K) (gamePoly j) + 2) CL.Detyping.DeciderProgram.post.timeBound + 23 * gameArgBound j G TS TD K + 74

theorem MIPRE.OracleDecider.dom_gameCost (j : ℕ) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ (W X K G TS TD : ℕ), 2 ≤ X → G ≤ X → TS ≤ W → TD ≤ W → Repeat.Dom W X K c m e (gameCost j G TS TD K)

The game check's cost, dominated.

noncomputable def MIPRE.OracleDecider.corePoly : Polynomial ℕ

The polynomials of the core.

Equations

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

theorem MIPRE.OracleDecider.coreCost_le (j S₀ TS TD K : ℕ) : coreCost j S₀ TS TD K ≤ 2 * gameCost j S₀ TS TD K + 5 * Polynomial.eval (S₀ + 8) corePoly + 14 * S₀ + 76

theorem MIPRE.OracleDecider.dom_coreCost (j : ℕ) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ (W X K S₀ TS TD : ℕ), 2 ≤ X → S₀ + 1 = X → TS ≤ W → TD ≤ W → Repeat.Dom W X K c m e (coreCost j S₀ TS TD K)

The core's cost, dominated.

theorem MIPRE.OracleDecider.core_timeBound (ℓ : ℕ) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ (V : Verifier (ℓ + 1)) (B n TS TD k W : ℕ), V.sampler.TimeBoundAt n TS k → V.decider.TimeBoundAt n TD k → TS ≤ W → TD ≤ W → ∀ (t u : Role) (x y : V.Questions n) (a b : Cost.BitStr), ∃ (r : Cost.Data) (time : ℕ), (core (ℓ + 1)).Runs (cInput V.sampler.prog V.decider.prog B n t (CL.toBits x) u (CL.toBits y) a b) r time ∧ time ≤ c * (W + 1) ^ m * ((cInput V.sampler.prog V.decider.prog B n t (CL.toBits x) u (CL.toBits y) a b).size + 1) ^ (e * (k + 1))

The core's running time, dominated: on a well-formed input c, within c₀ (W + 1)^m (|c| + 1)^{e (k + 1)} whenever the input verifier's sampler and decider run within TS (|d| + 1)^k and TD (|d| + 1)^k at the index and TS, TD ≤ W.

theorem MIPRE.OracleDecider.core_accepting_le (ℓ : ℕ) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ (V : Verifier (ℓ + 1)) (B n TS TD k W : ℕ), V.sampler.TimeBoundAt n TS k → V.decider.TimeBoundAt n TD k → TS ≤ W → TD ≤ W → ∀ (t u : Role) (x y : V.Questions n) (a b : Cost.BitStr) (time : ℕ), (core (ℓ + 1)).Runs (cInput V.sampler.prog V.decider.prog B n t (CL.toBits x) u (CL.toBits y) a b) (Cost.encode true) time → time ≤ c * (W + 1) ^ m * ((cInput V.sampler.prog V.decider.prog B n t (CL.toBits x) u (CL.toBits y) a b).size + 1) ^ (e * (k + 1))

The budget hypothesis, discharged: every accepting run of the core on a well-formed input takes at most c₀ (W + 1)^m (|c| + 1)^{e (k + 1)}.

The decider's running time

noncomputable def MIPRE.OracleDecider.deciderCost (j P N K Bz TI D : ℕ) : ℕ

The cost of the decider on (n, d), with P = |(S̄, D̄, Ī)|, N = |n|, K the budget, Bz the size of the cut, TI the index routine's time and D = |d|.

Equations

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

theorem MIPRE.OracleDecider.oracleDecider_runs_within (j : ℕ) (sp dp : Cost.Prog) (I : Index) (n : ℕ) (d : Cost.Data) {TI : ℕ} (hI : Cost.HaltsWithin I.prog (Cost.encode n) TI) : ∃ (r : Cost.Data) (t : ℕ), (oracleDecider j sp dp I).prog.Runs ((Cost.encode n).cons d) r t ∧ t ≤ deciderCost j (Cost.esize (sp, dp, I.prog)) (Cost.esize n) (I.budget n) (Cost.esize (I.cut n)) TI d.size

The decider's running time on (n, d): the index routine's, the clocked universal machine's overhead on the budget and the input, and nothing of the input programs' behaviour.

noncomputable def MIPRE.OracleDecider.shellPoly (j : ℕ) : Polynomial ℕ

The polynomials of the shell.

Equations

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

noncomputable def MIPRE.OracleDecider.shellArgBound (j P N K Bz TI D : ℕ) : ℕ

The one argument dominating every argument of a polynomial in deciderCost.

Equations

• MIPRE.OracleDecider.shellArgBound j P N K Bz TI D = 3 * K + P + Bz + N + D + TI + MIPRE.Cost.esize (MIPRE.OracleDecider.core j) + 10

theorem MIPRE.OracleDecider.deciderCost_le (j P N K Bz TI D : ℕ) : deciderCost j P N K Bz TI D ≤ 4 * Polynomial.eval (shellArgBound j P N K Bz TI D) (shellPoly j) + Polynomial.eval (Polynomial.eval (shellArgBound j P N K Bz TI D) (shellPoly j) + 1) CL.Detyping.ClockProgram.checkResult.timeBound + 7 * shellArgBound j P N K Bz TI D + 35

theorem MIPRE.OracleDecider.oracleDecider_timeBound (j : ℕ) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ (sp dp : Cost.Prog) (I : Index) (n TI W : ℕ), Cost.HaltsWithin I.prog (Cost.encode n) TI → Cost.esize sp ≤ W → Cost.esize dp ≤ W → Cost.esize I.prog ≤ W → n ≤ W → I.budget n ≤ W → I.cut n ≤ W → TI ≤ W → ∀ (d : Cost.Data), Cost.HaltsWithin (oracleDecider j sp dp I).prog ((Cost.encode n).cons d) (c * (W + 1) ^ m * (d.size + 1) ^ e)

The decider's running time, dominated: on (n, d) within c (W + 1)^m (|d| + 1)^e, whenever the budget, the cut and the index routine's time at n, the description lengths of the three programs and n are at most W. The degree e is fixed: the input verifier's degree enters only through the budget.

Completeness at an explicit budget

theorem MIPRE.OracleDecider.esize_role_le (r : Role) : Cost.esize r ≤ 7

def MIPRE.OracleDecider.coreInputBound {ℓ : ℕ} (V : Verifier (ℓ + 1)) (B n T : ℕ) : ℕ

The size of the core's input on answers within the inner cut.

Equations

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

theorem MIPRE.OracleDecider.size_cInput_le {ℓ : ℕ} (V : Verifier (ℓ + 1)) (B n T : ℕ) (t u : Role) (x y : V.Questions n) (a b : Cost.BitStr) (ha : List.length a ≤ T) (hb : List.length b ≤ T) : (cInput V.sampler.prog V.decider.prog B n t (CL.toBits x) u (CL.toBits y) a b).size ≤ coreInputBound V B n T

theorem MIPRE.OracleDecider.budget_sufficient (ℓ : ℕ) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ (V : Verifier (ℓ + 1)) (I : Index) (T n TS TD k W : ℕ), V.sampler.TimeBoundAt n TS k → V.decider.TimeBoundAt n TD k → TS ≤ W → TD ≤ W → c * (W + 1) ^ m * (coreInputBound V (I.cut n) n T + 1) ^ (e * (k + 1)) ≤ I.budget n → ∀ (t u : Role) (x y : V.Questions n) (a b : Cost.BitStr), List.length a ≤ T → List.length b ≤ T → ∀ (time : ℕ), (core (ℓ + 1)).Runs (cInput V.sampler.prog V.decider.prog (I.cut n) n t (CL.toBits x) u (CL.toBits y) a b) (Cost.encode true) time → time ≤ I.budget n

The budget hypothesis at an explicit budget: every accepting run of the core on answers within the inner cut fits in any budget above c (W + 1)^m (Z + 1)^{e (k + 1)}, Z the bound on the core's input.

theorem MIPRE.OracleDecider.exists_typedPredicate_perfectPCC_within (ℓ : ℕ) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ (V : Verifier (ℓ + 1)) (I : Index) (C : CL.Detyping.CutoffProgram) (n TS TD k W : ℕ), V.sampler.TimeBoundAt n TS k → V.decider.TimeBoundAt n TD k → TS ≤ W → TD ≤ W → 8 * I.cut n + 3 ≤ C.inner n → C.inner n ≤ C.outer n → c * (W + 1) ^ m * (coreInputBound V (I.cut n) n (C.inner n) + 1) ^ (e * (k + 1)) ≤ I.budget n → V.HasPerfectPCC n (I.cut n) → ∃ (R : SyncStrategy (CL.Detyping.typedGame roleGraph roleGraph_nonempty (fun (x : Bool) => roleFamily (V.sampler.cl n)) (CL.Detyping.DeciderProgram.typedPredicate (oracleSampler V.sampler) (oracleDecider (ℓ + 1) V.sampler.prog V.decider.prog I) C n)).doubled), R.IsPCC ∧ R.value = 1

Completeness of the compiled typed game at an explicit budget: a value-1 PCC strategy of 𝒱_n at the parse cut gives one of the doubled typed game, when the inner cut holds every honest encoding and the budget is above the core's running time on answers within the inner cut.