Soundness of oracularization

Item 2 of blueprint thm:oracularization (lem:oracular-soundness), at the level of games: a synchronous strategy of value at least 1 - ε for MIPRE.SeededGame.oracular yields one of value at least 1 - 24√ε for the doubled input game.

The loss carries the single square root that repair 1 of rem:oracularization-repairs insists on -- an earlier revision of the blueprint wrote poly(ε), which the campaign found "not merely imprecise but false as stated". It is spent in exactly one place, MIPRE.sum_ntr_mul_ge; everything before it is linear in ε.

The shape of the argument

• The extracted strategy (soundStrategy) is the two isolated players' own measurements, relabelled along OAns.singlePart so that an oracle-shaped answer is grouped into one distinguished outcome. Relabelling is what makes them measurements rather than sub-measurements, which is the game-level residue of repair 3; SyncStrategy.push does it, and a sum over a fibre is a projection because distinct outcomes are orthogonal.
• The budget (budget) is all that is taken from the hypothesis. Each of the nine ordered role pairs carries a ninth of the question weight, so at any one of them a set of outcome pairs the decider rejects carries mass at most 9ε on average over the seed. Three instances (gammaTerm_budget, betaTerm_budget, alphaTerm_budget) are used: the oracle's own pair is accepted, and each isolated player agrees with the oracle's component.
• The closeness estimate (sqDist_le, from MIPRE.sum_hsNormSq_sub_le) bounds the squared Hilbert--Schmidt distance between the oracle's relabelled measurement and the product of the two isolated players' by three times the sum of the two disagreements -- linearly, with no square root.
• The value comparison (valSeed_ge, from MIPRE.sum_ntr_mul_ge) is where the square root enters, and one more Cauchy--Schwarz takes the average inside it.

For a synchronous strategy the state is the normalized trace, so the paper's state-dependent ≈_δ is the normalized Hilbert--Schmidt distance of MIPRE/Foundations/Distances.lean; see blueprint rem:distance-state. MIPRE/Foundations/Closeness.lean is that calculus.

Scope

Nothing here inhabits MIPRE.Oracularization: that is done at the level of verifiers, in Foundations/Pipeline/Oracularization.lean, whose bipartite soundness rests on Foundations/OracularTensor.lean rather than on the synchronous argument here. The complexity clause, the bounded parse and its grouping, the truncation to B_𝒟(n) and the level accounting are all statements about a verifier and none of them appears at this level; rem:oracular-game-level records that.

Relabelling an oracularized answer

def MIPRE.OAns.pairPart {A : Type u_1} [Inhabited A] : OAns A → A × A

An oracularized answer read as a pair: an oracle's answer is the pair it is, and an isolated player's answer is grouped into the distinguished outcome (default, default).

Equations

• (MIPRE.OAns.pair a b).pairPart = (a, b)
• (MIPRE.OAns.single a).pairPart = (default, default)

def MIPRE.OAns.singlePart {A : Type u_1} [Inhabited A] : OAns A → A

An oracularized answer read as a single answer: an isolated player's answer is itself, and an oracle's pair is grouped into the distinguished outcome default.

Equations

• (MIPRE.OAns.single a).singlePart = a
• (MIPRE.OAns.pair a b).singlePart = default

Averages over the seed

Both question distributions are pushforwards of the uniform distribution on the seed space, so every sum against them is an average over seeds.

theorem MIPRE.SeededGame.sum_dist_mul {A : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] (S : SeededGame V A) (F : V → V → ℝ) : ∑ x : V, ∑ y : V, S.dist x y * F x y = (↑(Fintype.card V))⁻¹ * ∑ z : V, F (S.LA z) (S.LB z)

The input game's distribution, against a test function: an average over the seed.

theorem MIPRE.SeededGame.sum_oDist_mul {A : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] (S : SeededGame V A) (F : Role × V → Role × V → ℝ) : ∑ p : Role × V, ∑ q : Role × V, S.oDist p q * F p q = (↑(Fintype.card (Role × Role × V)))⁻¹ * ∑ s : Role × Role × V, F (S.oquestion s.1 s.2.2) (S.oquestion s.2.1 s.2.2)

The oracularized game's distribution, against a test function: an average over the ordered pair of roles and the seed.

The three relabelled families, and the extracted strategy

noncomputable def MIPRE.SeededGame.oFam {A : Type u_1} [Inhabited A] {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) (z : V) (p : A × A) : Matrix (Fin N.d) (Fin N.d) ℂ

The oracle's measurement, read as a measurement on answer pairs: the shape failures are grouped into the distinguished outcome (default, default), which is what makes it a measurement rather than a sub-measurement (repair 3 of rem:oracularization-repairs, at the game level).

Equations

• MIPRE.SeededGame.oFam N z p = (N.push MIPRE.OAns.pairPart).M (MIPRE.Role.oracle, z) p

noncomputable def MIPRE.SeededGame.cFam {A : Type u_1} [Inhabited A] {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) (x : V) (a : A) : Matrix (Fin N.d) (Fin N.d) ℂ

Alice's own measurement, with the oracle-shaped answers grouped into default.

Equations

• MIPRE.SeededGame.cFam N x a = (N.push MIPRE.OAns.singlePart).M (MIPRE.Role.alice, x) a

noncomputable def MIPRE.SeededGame.dFam {A : Type u_1} [Inhabited A] {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) (y : V) (b : A) : Matrix (Fin N.d) (Fin N.d) ℂ

Bob's own measurement, with the oracle-shaped answers grouped into default.

Equations

• MIPRE.SeededGame.dFam N y b = (N.push MIPRE.OAns.singlePart).M (MIPRE.Role.bob, y) b

noncomputable def MIPRE.SeededGame.sideMeas {A : Type u_1} [Inhabited A] {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) : ProjectiveMeasurement (Bool × V) A (Matrix (Fin N.d) (Fin N.d) ℂ)

The isolated players' measurements as one projective measurement on the doubled input game's questions.

Equations

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

noncomputable def MIPRE.SeededGame.soundStrategy {A : Type u_1} [Inhabited A] {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) : SyncStrategy S.toGame.doubled

The extracted strategy for the input game: the two isolated players keep their own measurements.

Equations

• MIPRE.SeededGame.soundStrategy N = { d := N.d, d_pos := ⋯, P := MIPRE.SeededGame.sideMeas N }

@[simp]

theorem MIPRE.SeededGame.soundStrategy_d {A : Type u_1} [Inhabited A] {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) : (soundStrategy N).d = N.d

@[simp]

theorem MIPRE.SeededGame.soundStrategy_false {A : Type u_1} [Inhabited A] {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) (x : V) (a : A) : (soundStrategy N).P.M (false, x) a = cFam N x a

@[simp]

theorem MIPRE.SeededGame.soundStrategy_true {A : Type u_1} [Inhabited A] {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) (y : V) (b : A) : (soundStrategy N).P.M (true, y) b = dFam N y b

The two values, as averages over the seed

theorem MIPRE.SeededGame.soundStrategy_value {A : Type u_1} [Inhabited A] {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) : (soundStrategy N).value = (↑(Fintype.card V))⁻¹ * ∑ z : V, ∑ a : A, ∑ b : A, (if S.D (S.LA z) (S.LB z) a b = true then 1 else 0) * ntr (cFam N (S.LA z) a * dFam N (S.LB z) b)

The extracted strategy's value.

theorem MIPRE.SeededGame.value_oracular {A : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) : N.value = (↑(Fintype.card (Role × Role × V)))⁻¹ * ∑ s : Role × Role × V, ∑ uv : OAns A × OAns A, (if S.oaccepts (S.oquestion s.1 s.2.2) (S.oquestion s.2.1 s.2.2) uv.1 uv.2 = true then 1 else 0) * ntr (N.P.M (S.oquestion s.1 s.2.2) uv.1 * N.P.M (S.oquestion s.2.1 s.2.2) uv.2)

The oracularized value.

theorem MIPRE.SeededGame.sum_ntr_oracular {A : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) : (↑(Fintype.card (Role × Role × V)))⁻¹ * ∑ s : Role × Role × V, ∑ uv : OAns A × OAns A, ntr (N.P.M (S.oquestion s.1 s.2.2) uv.1 * N.P.M (S.oquestion s.2.1 s.2.2) uv.2) = 1

The total mass of the oracularized game: one.

The rejection budget

Everything the argument takes from 1 - ε ≤ val(oracular) is this: at any one ordered pair of roles, a set of outcome pairs the decider rejects carries mass at most 9ε on average over the seed. The 9 is the number of ordered role pairs.

theorem MIPRE.SeededGame.card_role_prod_prod {V : Type u_2} [Fintype V] : ↑(Fintype.card (Role × Role × V)) = 9 * ↑(Fintype.card V)

theorem MIPRE.SeededGame.budget {A : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) {ε : ℝ} (hval : 1 - ε ≤ N.value) (r₁ r₂ : Role) (T : V → Finset (OAns A × OAns A)) (hT : ∀ (z : V), ∀ uv ∈ T z, S.oaccepts (S.oquestion r₁ z) (S.oquestion r₂ z) uv.1 uv.2 = false) : (↑(Fintype.card V))⁻¹ * ∑ z : V, ∑ uv ∈ T z, ntr (N.P.M (S.oquestion r₁ z) uv.1 * N.P.M (S.oquestion r₂ z) uv.2) ≤ 9 * ε

Relabelled sums, unrelabelled

Each budget below is stated about the relabelled families, and the budget lemma is about the strategy's own operators. This is the translation: a sum over a set of relabelled outcome pairs is the sum over the outcome pairs whose labels land in that set.

theorem MIPRE.SeededGame.sum_push_pair {A : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) (p q : Role × V) {B : Type u_3} {C : Type u_4} [Fintype B] [DecidableEq B] [Fintype C] [DecidableEq C] (f : OAns A → B) (g : OAns A → C) (E : Finset (B × C)) : ∑ bc ∈ E, ntr ((N.push f).M p bc.1 * (N.push g).M q bc.2) = ∑ uv : OAns A × OAns A with (f uv.1, g uv.2) ∈ E, ntr (N.P.M p uv.1 * N.P.M q uv.2)

theorem MIPRE.SeededGame.sum_push_single {A : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) (p : Role × V) {B : Type u_3} [Fintype B] [DecidableEq B] (f : OAns A → B) (E : Finset B) : ∑ b ∈ E, ntr ((N.push f).M p b) = ∑ u : OAns A with f u ∈ E, ntr (N.P.M p u)

The three rejection sets, and their budgets

The decider's checks that the argument uses are three: the oracle's own pair must satisfy the input predicate, and each isolated player's answer must agree with the oracle's corresponding component. Each is a set of outcome pairs on which oaccepts is false, so each carries mass at most 9ε.

def MIPRE.SeededGame.TAlice {A : Type u_1} [Inhabited A] [Fintype A] [DecidableEq A] : Finset (OAns A × OAns A)

The outcome pairs on which the oracle's Alice-component and Alice's own answer disagree. It also contains every shape mismatch, which the decider rejects anyway.

Equations

• MIPRE.SeededGame.TAlice = {uv : MIPRE.OAns A × MIPRE.OAns A | ¬uv.1.pairPart.1 = uv.2.singlePart}

def MIPRE.SeededGame.TBob {A : Type u_1} [Inhabited A] [Fintype A] [DecidableEq A] : Finset (OAns A × OAns A)

The outcome pairs on which the oracle's Bob-component and Bob's own answer disagree.

Equations

• MIPRE.SeededGame.TBob = {uv : MIPRE.OAns A × MIPRE.OAns A | ¬uv.1.pairPart.2 = uv.2.singlePart}

def MIPRE.SeededGame.TGame {A : Type u_1} [Inhabited A] {V : Type u_2} [Fintype A] [DecidableEq A] {S : SeededGame V A} (z : V) : Finset (OAns A × OAns A)

The outcome pairs, at a seed, on which the oracle repeats an answer the input predicate rejects.

Equations

• MIPRE.SeededGame.TGame z = Finset.image (fun (u : MIPRE.OAns A) => (u, u)) {u : MIPRE.OAns A | S.D (S.LA z) (S.LB z) u.pairPart.1 u.pairPart.2 = false}

theorem MIPRE.SeededGame.rejected_TAlice {A : Type u_1} [Inhabited A] {V : Type u_2} [Fintype A] [DecidableEq A] {S : SeededGame V A} (z : V) (uv : OAns A × OAns A) : uv ∈ TAlice → S.oaccepts (S.oquestion Role.oracle z) (S.oquestion Role.alice z) uv.1 uv.2 = false

theorem MIPRE.SeededGame.rejected_TBob {A : Type u_1} [Inhabited A] {V : Type u_2} [Fintype A] [DecidableEq A] {S : SeededGame V A} (z : V) (uv : OAns A × OAns A) : uv ∈ TBob → S.oaccepts (S.oquestion Role.oracle z) (S.oquestion Role.bob z) uv.1 uv.2 = false

theorem MIPRE.SeededGame.rejected_TGame {A : Type u_1} [Inhabited A] {V : Type u_2} [Fintype A] [DecidableEq A] {S : SeededGame V A} (z : V) (uv : OAns A × OAns A) : uv ∈ TGame z → S.oaccepts (S.oquestion Role.oracle z) (S.oquestion Role.oracle z) uv.1 uv.2 = false

The three budgets, on the relabelled families

Each budget is now a statement about the relabelled families oFam, cFam, dFam: the oracle's own answer is accepted, and each isolated player agrees with the oracle's component, all but 9ε of the time.

def MIPRE.SeededGame.EAliceAgree {A : Type u_1} [Fintype A] [DecidableEq A] : Finset ((A × A) × A)

Equations

• MIPRE.SeededGame.EAliceAgree = Finset.image (fun (p : A × A) => (p, p.1)) Finset.univ

def MIPRE.SeededGame.EBobAgree {A : Type u_1} [Fintype A] [DecidableEq A] : Finset ((A × A) × A)

Equations

• MIPRE.SeededGame.EBobAgree = Finset.image (fun (p : A × A) => (p, p.2)) Finset.univ

theorem MIPRE.SeededGame.mem_EAliceAgree {A : Type u_1} [Fintype A] [DecidableEq A] (bc : (A × A) × A) : bc ∈ EAliceAgree ↔ bc.1.1 = bc.2

theorem MIPRE.SeededGame.mem_EBobAgree {A : Type u_1} [Fintype A] [DecidableEq A] (bc : (A × A) × A) : bc ∈ EBobAgree ↔ bc.1.2 = bc.2

theorem MIPRE.SeededGame.sum_ntr_pair_eq_one {A : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) (p q : Role × V) : ∑ uv : OAns A × OAns A, ntr (N.P.M p uv.1 * N.P.M q uv.2) = 1

theorem MIPRE.SeededGame.sum_disagree_alice {A : Type u_1} [Inhabited A] {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) (z : V) : 1 - ∑ p : A × A, ntr (oFam N z p * cFam N (S.LA z) p.1) = ∑ uv ∈ TAlice, ntr (N.P.M (Role.oracle, z) uv.1 * N.P.M (Role.alice, S.LA z) uv.2)

The oracle's disagreement with Alice, as a mass on the strategy's own outcomes.

theorem MIPRE.SeededGame.sum_disagree_bob {A : Type u_1} [Inhabited A] {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) (z : V) : 1 - ∑ p : A × A, ntr (oFam N z p * dFam N (S.LB z) p.2) = ∑ uv ∈ TBob, ntr (N.P.M (Role.oracle, z) uv.1 * N.P.M (Role.bob, S.LB z) uv.2)

The oracle's disagreement with Bob.

theorem MIPRE.SeededGame.sum_game_reject {A : Type u_1} [Inhabited A] {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) (z : V) : ∑ p : A × A with S.D (S.LA z) (S.LB z) p.1 p.2 = false, ntr (oFam N z p) = ∑ uv ∈ TGame z, ntr (N.P.M (Role.oracle, z) uv.1 * N.P.M (Role.oracle, z) uv.2)

The mass the oracle puts on pairs the input predicate rejects.

The three families are projective measurements

theorem MIPRE.SeededGame.oFam_selfAdjoint {A : Type u_1} [Inhabited A] {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) (z : V) (p : A × A) : star (oFam N z p) = oFam N z p

theorem MIPRE.SeededGame.oFam_projective {A : Type u_1} [Inhabited A] {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) (z : V) (p : A × A) : oFam N z p * oFam N z p = oFam N z p

theorem MIPRE.SeededGame.cFam_selfAdjoint {A : Type u_1} [Inhabited A] {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) (x : V) (a : A) : star (cFam N x a) = cFam N x a

theorem MIPRE.SeededGame.cFam_projective {A : Type u_1} [Inhabited A] {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) (x : V) (a : A) : cFam N x a * cFam N x a = cFam N x a

theorem MIPRE.SeededGame.dFam_selfAdjoint {A : Type u_1} [Inhabited A] {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) (y : V) (b : A) : star (dFam N y b) = dFam N y b

theorem MIPRE.SeededGame.dFam_projective {A : Type u_1} [Inhabited A] {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) (y : V) (b : A) : dFam N y b * dFam N y b = dFam N y b

theorem MIPRE.SeededGame.sum_ntr_oFam {A : Type u_1} [Inhabited A] {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) (z : V) : ∑ p : A × A, ntr (oFam N z p) = 1

theorem MIPRE.SeededGame.sum_ntr_cFam_dFam {A : Type u_1} [Inhabited A] {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) (x y : V) : ∑ p : A × A, ntr (cFam N x p.1 * dFam N y p.2) = 1

The per-seed quantities

noncomputable def MIPRE.SeededGame.sqDist {A : Type u_1} [Inhabited A] {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) (z : V) : ℝ

The squared Hilbert--Schmidt distance, at one seed, between the oracle's relabelled measurement and the product of the two isolated players'.

Equations

• MIPRE.SeededGame.sqDist N z = ∑ p : A × A, MIPRE.hsNormSq (MIPRE.SeededGame.cFam N (S.LA z) p.1 * MIPRE.SeededGame.dFam N (S.LB z) p.2 - MIPRE.SeededGame.oFam N z p)

noncomputable def MIPRE.SeededGame.alphaTerm {A : Type u_1} [Inhabited A] {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) (z : V) : ℝ

The oracle's disagreement with Bob at one seed.

Equations

• MIPRE.SeededGame.alphaTerm N z = ∑ p : A × A, MIPRE.ntr (MIPRE.SeededGame.oFam N z p * (1 - MIPRE.SeededGame.dFam N (S.LB z) p.2))

noncomputable def MIPRE.SeededGame.betaTerm {A : Type u_1} [Inhabited A] {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) (z : V) : ℝ

The oracle's disagreement with Alice at one seed.

Equations

• MIPRE.SeededGame.betaTerm N z = ∑ p : A × A, MIPRE.ntr (MIPRE.SeededGame.oFam N z p * (1 - MIPRE.SeededGame.cFam N (S.LA z) p.1))

noncomputable def MIPRE.SeededGame.gammaTerm {A : Type u_1} [Inhabited A] {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) (z : V) : ℝ

The mass the oracle puts on pairs the input predicate rejects, at one seed.

Equations

• MIPRE.SeededGame.gammaTerm N z = ∑ p : A × A with S.D (S.LA z) (S.LB z) p.1 p.2 = false, MIPRE.ntr (MIPRE.SeededGame.oFam N z p)

theorem MIPRE.SeededGame.alphaTerm_eq {A : Type u_1} [Inhabited A] {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) (z : V) : alphaTerm N z = 1 - ∑ p : A × A, ntr (oFam N z p * dFam N (S.LB z) p.2)

theorem MIPRE.SeededGame.betaTerm_eq {A : Type u_1} [Inhabited A] {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) (z : V) : betaTerm N z = 1 - ∑ p : A × A, ntr (oFam N z p * cFam N (S.LA z) p.1)

theorem MIPRE.SeededGame.sqDist_le {A : Type u_1} [Inhabited A] {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) (z : V) : sqDist N z ≤ 3 * (alphaTerm N z + betaTerm N z)

The closeness estimate at one seed, linear in the two disagreements.

theorem MIPRE.SeededGame.valSeed_ge {A : Type u_1} [Inhabited A] {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) (z : V) : 1 - gammaTerm N z - 2 * √(sqDist N z) ≤ ∑ a : A, ∑ b : A, (if S.D (S.LA z) (S.LB z) a b = true then 1 else 0) * ntr (cFam N (S.LA z) a * dFam N (S.LB z) b)

The value comparison at one seed, where the square root is spent.

The three budgets, averaged over the seed

theorem MIPRE.SeededGame.betaTerm_budget {A : Type u_1} [Inhabited A] {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) {ε : ℝ} (hval : 1 - ε ≤ N.value) : (↑(Fintype.card V))⁻¹ * ∑ z : V, betaTerm N z ≤ 9 * ε

theorem MIPRE.SeededGame.alphaTerm_budget {A : Type u_1} [Inhabited A] {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) {ε : ℝ} (hval : 1 - ε ≤ N.value) : (↑(Fintype.card V))⁻¹ * ∑ z : V, alphaTerm N z ≤ 9 * ε

theorem MIPRE.SeededGame.gammaTerm_budget {A : Type u_1} [Inhabited A] {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) {ε : ℝ} (hval : 1 - ε ≤ N.value) : (↑(Fintype.card V))⁻¹ * ∑ z : V, gammaTerm N z ≤ 9 * ε

Soundness

theorem MIPRE.SeededGame.soundStrategy_value_ge {A : Type u_1} [Inhabited A] {V : Type u_2} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] {S : SeededGame V A} (N : SyncStrategy S.oracular) {ε : ℝ} (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) (hval : 1 - ε ≤ N.value) : 1 - 24 * √ε ≤ (soundStrategy N).value

Soundness of oracularization (item 2 of blueprint thm:oracularization), at the level of games: a synchronous strategy of value at least 1 - ε for the oracularized game yields one of value at least 1 - 24 √ε for the doubled input game. The loss carries the single square root of repair 1 of rem:oracularization-repairs, and it is spent in exactly one place, MIPRE.sum_ntr_mul_ge.