Oracularization

Blueprint thm:oracularization (paper oracularization.tex, sec:orac-def, thm:oracle-completeness and thm:oracle-soundness; ledger node 1.3.5): the structure Oracularization ℓ, the specification of the typed oracularized verifier of an ℓ + 1-level normal form verifier, and its inhabitant Oracularization.construction, which is the theorem.

The structure was first stated as an untyped, level-preserving transformation with value transfers as fields. That statement was vacuous (planning/oracularization.md, finding 1): the identity transformation with a length check satisfies it, because no field sees the oracle form of the output — that one player's answer alone decides the game check, and the other's must equal one of its components — which is the only property of oracularization answer reduction uses. So it is restated as the specification of the construction itself:

• the sampler is oracleSampler (lem:oracle-typed-sampler): the identity for the oracle and the input's CL functions for the isolated players, the oracle form of the sampler being definitional;
• the decider is a total typed decider of the input programs and an index routine, computable in polynomial time, whose acceptance implies O2's predicate oraclePred at the routine's parse cut (sound: the oracle form of the decider), which accepts what oraclePred accepts once the routine's budget covers the input verifier's running time at the index (complete), and which runs within a polynomial of the budget, the cut and its input (time).

The index routine replaces the paper's timeout-counter form, which the ambient model does not have (Foundations/OracularDecider.lean). Completeness therefore carries the budget hypothesis: it is the input verifier's running time at the index, which the paper's timeout bound supplies.

The value transfers are theorems about every instance: for the typed game (typed_soundness, typed_completeness), with the soundness loss 24√ε of lem:oracular-soundness-tensor; and for the detyped verifier with ℓ + 3 levels (detyped, detyped_completeness, detyped_soundness), with the loss 1536√ε — the factor 16³ of the detyping compiler on three types under the square root. In the paper oracularization is not detyped on its own (finding 3): it is internal to answer reduction, whose single detyping is at its exterior. The composition MIPRE.GapCompression.ofPipeline does not consume this structure.

The two soundness transfers hold in every value model in which oracularization is sound (ValueModel.OracularSound, Foundations/OracularValue.lean): typed_soundness_val and detyped_soundness_val, in Verifier.val ω, of which typed_soundness and detyped_soundness are the tensor-product cases; the commuting-operator model is the other instance (ValueModel.commuting_oracularSound).

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

The size of the core's input at the index, construction-independent: the description lengths of the input programs, the parse cut, the index, the dimension and the answer cut.

Equations

• MIPRE.Oracularization.inputSize V B n T = MIPRE.Cost.esize V.sampler.prog + MIPRE.Cost.esize V.decider.prog + MIPRE.Cost.esize B + MIPRE.Cost.esize n + V.sampler.dim n + T

structure MIPRE.Oracularization (ℓ : ℕ) : Type

Oracularization (blueprint thm:oracularization), for ℓ + 1-level inputs: the specification of the typed oracularized decider, the sampler being oracleSampler. An instance is the theorem (Oracularization.construction).

• decider : Cost.Prog → Cost.Prog → OracleDecider.Index → CL.Detyping.TypedDecider Role

  The typed decider, of the input sampler's and decider's programs and an index routine.

• compute : Cost.PolyTimeFun (Cost.Prog × Cost.Prog × Cost.Prog) Cost.Prog

  Its program, a polynomial-time function of the three programs.

• compute_eq (sp dp : Cost.Prog) (I : OracleDecider.Index) : self.compute.toFun (sp, dp, I.prog) = (self.decider sp dp I).prog
• total (sp dp : Cost.Prog) (I : OracleDecider.Index) : (self.decider sp dp I).Total

  It halts on every input, whatever the input programs do.

• sound (V : Verifier (ℓ + 1)) (I : OracleDecider.Index) (n : ℕ) (t u : Role) (x y : V.Questions n) (a b : Cost.BitStr) : (self.decider V.sampler.prog V.decider.prog I).Accepts n t (CL.toBits x) u (CL.toBits y) a b → oraclePred (V.seeded n (I.cut n)) (t, x) (u, y) a b = true

  The oracle form: it accepts only what oraclePred accepts at the routine's cut.

• budgetCoeff : ℕ

  The constants of the budget.

• budgetDeg : ℕ
• budgetExp : ℕ
• complete (V : Verifier (ℓ + 1)) (I : OracleDecider.Index) (T n TS TD k W : ℕ) : V.sampler.TimeBoundAt n TS k → V.decider.TimeBoundAt n TD k → TS ≤ W → TD ≤ W → self.budgetCoeff * (W + 1) ^ self.budgetDeg * (inputSize V (I.cut n) n T + 1) ^ (self.budgetExp * (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 → oraclePred (V.seeded n (I.cut n)) (t, x) (u, y) a b = true → (self.decider V.sampler.prog V.decider.prog I).Accepts n t (CL.toBits x) u (CL.toBits y) a b

  Completeness of the acceptance law: it accepts what oraclePred accepts, on answers within an answer cut T, once the budget covers the input verifier's running time.

• timeCoeff : ℕ

  The constants of the running time.

• timeDeg : ℕ
• timeExp : ℕ
• time (sp dp : Cost.Prog) (I : OracleDecider.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 (self.decider sp dp I).prog ((Cost.encode n).cons d) (self.timeCoeff * (W + 1) ^ self.timeDeg * (d.size + 1) ^ self.timeExp)

  The running time: within a polynomial of the budget, the cut, the index routine's time, the description lengths and the index, at a degree in the input that does not depend on the input verifier.

The typed game

@[reducible, inline]

noncomputable abbrev MIPRE.Oracularization.typedGame {ℓ : ℕ} (O : Oracularization ℓ) (V : Verifier (ℓ + 1)) (I : OracleDecider.Index) (C : CL.Detyping.CutoffProgram) (n : ℕ) : Game (CL.Detyping.Question Role (Fin (V.sampler.dim n))) (CL.Detyping.Question Role (Fin (V.sampler.dim n))) (Verifier.Answers (C.outer n)) (Verifier.Answers (C.outer n))

The typed game of the oracularized verifier of 𝒱 at index n: the detyping compiler's typed game of oracleSampler and the decider, on the complete graph over the roles.

Equations

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

theorem MIPRE.Oracularization.typed_soundness_val {ℓ : ℕ} (O : Oracularization ℓ) (V : Verifier (ℓ + 1)) (I : OracleDecider.Index) (C : CL.Detyping.CutoffProgram) {ω : ValueModel} (hω : ω.OracularSound) (n : ℕ) {ε : ℝ} (hε : 0 < ε) (h : 1 - ε < ω.val (O.typedGame V I C n)) : 1 - 24 * √ε ≤ V.val ω n (I.cut n)

Soundness of the typed oracularized verifier, in a value model where oracularization is sound: its typed game's value above 1 - ε puts ω(𝒱_n) at the parse cut at least 1 - 24√ε, whatever the budget.

theorem MIPRE.Oracularization.typed_soundness {ℓ : ℕ} (O : Oracularization ℓ) (V : Verifier (ℓ + 1)) (I : OracleDecider.Index) (C : CL.Detyping.CutoffProgram) (n : ℕ) {ε : ℝ} (hε : 0 < ε) (h : 1 - ε < quantumValue (O.typedGame V I C n)) : 1 - 24 * √ε ≤ V.valStar n (I.cut n)

Soundness of the typed oracularized verifier: its typed game's quantum value above 1 - ε puts val*(𝒱_n) at the parse cut at least 1 - 24√ε, whatever the budget — typed_soundness_val in the tensor-product model.

theorem MIPRE.Oracularization.typed_completeness {ℓ : ℕ} (O : Oracularization ℓ) (V : Verifier (ℓ + 1)) (I : OracleDecider.Index) (C : CL.Detyping.CutoffProgram) (n TS TD k W : ℕ) (hS : V.sampler.TimeBoundAt n TS k) (hD : V.decider.TimeBoundAt n TD k) (hTS : TS ≤ W) (hTD : TD ≤ W) (hin : 8 * I.cut n + 3 ≤ C.inner n) (hout : C.inner n ≤ C.outer n) (hK : O.budgetCoeff * (W + 1) ^ O.budgetDeg * (inputSize V (I.cut n) n (C.inner n) + 1) ^ (O.budgetExp * (k + 1)) ≤ I.budget n) (hV : V.HasPerfectPCC n (I.cut n)) : ∃ (R : SyncStrategy (O.typedGame V I C n).doubled), R.IsPCC ∧ R.value = 1

Completeness of the typed oracularized verifier: a value-1 PCC strategy of 𝒱_n at the parse cut gives one of the doubled typed game, with identical operators for the two players (the synchronous framework's), when the inner cut holds every honest encoding and the budget covers the input verifier's running time.

The detyped verifier

noncomputable def MIPRE.Oracularization.detyped {ℓ : ℕ} (O : Oracularization ℓ) (V : Verifier (ℓ + 1)) (I : OracleDecider.Index) (C : CL.Detyping.CutoffProgram) : Verifier (ℓ + 1 + 2)

The detyped oracularized verifier, with ℓ + 3 levels: the typed oracularized verifier through the detyping compiler (lem:detype-compiler) at the cutoff program C.

Equations

• O.detyped V I C = MIPRE.CL.Detyping.DeciderProgram.verifier MIPRE.roleGraph (MIPRE.oracleSampler V.sampler) (O.decider V.sampler.prog V.decider.prog I) C ⋯ ⋯

theorem MIPRE.Oracularization.detyped_completeness {ℓ : ℕ} (O : Oracularization ℓ) (V : Verifier (ℓ + 1)) (I : OracleDecider.Index) (C : CL.Detyping.CutoffProgram) (n TS TD k W : ℕ) (hS : V.sampler.TimeBoundAt n TS k) (hD : V.decider.TimeBoundAt n TD k) (hTS : TS ≤ W) (hTD : TD ≤ W) (hin : 8 * I.cut n + 3 ≤ C.inner n) (hout : C.inner n ≤ C.outer n) (hK : O.budgetCoeff * (W + 1) ^ O.budgetDeg * (inputSize V (I.cut n) n (C.inner n) + 1) ^ (O.budgetExp * (k + 1)) ≤ I.budget n) (hV : V.HasPerfectPCC n (I.cut n)) : (O.detyped V I C).HasPerfectPCC n (C.outer n)

Completeness of the detyped oracularized verifier.

theorem MIPRE.Oracularization.card_role : Fintype.card Role = 3

theorem MIPRE.Oracularization.detyped_soundness_val {ℓ : ℕ} (O : Oracularization ℓ) (V : Verifier (ℓ + 1)) (I : OracleDecider.Index) (C : CL.Detyping.CutoffProgram) {ω : ValueModel} (hω : ω.OracularSound) (n : ℕ) {ε : ℝ} (hε : 0 < ε) (h : 1 - ε < (O.detyped V I C).val ω n (C.outer n)) : 1 - 1536 * √ε ≤ V.val ω n (I.cut n)

Soundness of the detyped oracularized verifier, in a value model where oracularization is sound: ω above 1 - ε at the outer cut puts ω(𝒱_n) at the parse cut at least 1 - 1536√ε, whatever the budget — the detyping factor 16³ on the three roles, under the square root, times the 24 of the typed game.

theorem MIPRE.Oracularization.detyped_soundness {ℓ : ℕ} (O : Oracularization ℓ) (V : Verifier (ℓ + 1)) (I : OracleDecider.Index) (C : CL.Detyping.CutoffProgram) (n : ℕ) {ε : ℝ} (hε : 0 < ε) (h : 1 - ε < (O.detyped V I C).valStar n (C.outer n)) : 1 - 1536 * √ε ≤ V.valStar n (I.cut n)

Soundness of the detyped oracularized verifier: val* above 1 - ε at the outer cut puts val*(𝒱_n) at the parse cut at least 1 - 1536√ε, whatever the budget — detyped_soundness_val in the tensor-product model.

The construction

theorem MIPRE.Oracularization.coreInputBound_le {ℓ : ℕ} (V : Verifier (ℓ + 1)) (B n T : ℕ) : OracleDecider.coreInputBound V B n T + 1 ≤ (inputSize V B n T + 1) ^ 28

The core's input bound is below a power of the construction-independent one.

noncomputable def MIPRE.Oracularization.construction (ℓ : ℕ) : Oracularization ℓ

Oracularization (blueprint thm:oracularization): the typed oracularized decider of Foundations/OracularDecider.lean, with the running times of Foundations/OracularDeciderCost.lean, inhabits the specification.

Equations

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