Oracularization, at the level of games

Blueprint thm:oracularization (paper oracularization.tex, sec:orac-def and fig:oracle-decider) turns a normal form verifier into one where a single player --- the oracle --- receives the sampler's whole seed and answers both original questions, while the other player receives one of the two questions and must answer consistently. That makes the predicate a pointwise function of one player's answer, which is the format answer reduction needs.

This file is the construction and its question distribution, at the level of games: no samplers, no deciders, no types-as-Turing-machine-strings. What oracularization uses of a sampler is only the pair of maps L^𝖠, L^𝖡 on the seed space, so the input here is a SeededGame: a finite seed space, two question maps, and a decision predicate. The original game is the law of (L^𝖠 z, L^𝖡 z) for a uniform seed, the paper's CL distribution (MIPRE.CL.clDist is the same thing for V = 𝔽^ι).

The output SeededGame.oracular is a SynchronousGame on questions Role × V and answers OAns A, and its synchronicity is not an extra hypothesis: equal questions have equal roles, and check 2(a) of fig:oracle-decider rejects unequal answers there.

Scope, and what this file does not do

Two of the four repairs rem:oracularization-repairs records are about the verifier, not the game, and are untouched here: grouping the decider's failed bounded parses into one distinguished outcome (so the oracle families are projective measurements rather than sub-measurements), and the truncation of answers to B_𝒟(n). At a finite game-level answer alphabet there is no parse to fail, so there is nothing to group; saying so is more honest than claiming the repair is discharged. What is modelled is the shape check: an answer whose shape does not match the player's role is rejected (shapeOk), which is the game-level residue of the parse.

Completeness --- a value-1 PCC strategy for the input gives one for the output, with identical measurement operators rather than a symmetric state, which is repair 2 --- and soundness, with its single square root, are separate pieces.

Roles

inductive MIPRE.Role : Type

The three roles of the oracularized game: the oracle, who answers both original questions, and the two isolated players.

• oracle : Role
• alice : Role
• bob : Role

@[instance_reducible]

instance MIPRE.instDecidableEqRole : DecidableEq Role

Equations

• MIPRE.instDecidableEqRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance MIPRE.instFintypeRole : Fintype Role

Equations

• MIPRE.instFintypeRole = { elems := {MIPRE.Role.oracle, MIPRE.Role.alice, MIPRE.Role.bob}, complete := ⋯ }

@[instance_reducible]

instance MIPRE.instInhabitedRole : Inhabited Role

Equations

• MIPRE.instInhabitedRole = { default := MIPRE.Role.oracle }

Seeded games

structure MIPRE.SeededGame (V : Type u_3) (A : Type u_4) : Type (max u_3 u_4)

A seeded game: the question pair is (L^𝖠 z, L^𝖡 z) for a seed z drawn uniformly from a finite space, and the predicate is read off the questions and answers. This is everything oracularization uses of a normal form verifier's sampler.

• LA : V → V

  Alice's question map.

• LB : V → V

  Bob's question map.

• D : V → V → A → A → Bool

  The decision predicate of the original game.

noncomputable def MIPRE.SeededGame.dist {V : Type u_1} {A : Type u_2} [Fintype V] [DecidableEq V] (S : SeededGame V A) (x y : V) : ℝ

The question distribution of the input game: the law of (L^𝖠 z, L^𝖡 z).

Equations

• S.dist x y = ↑{z : V | S.LA z = x ∧ S.LB z = y}.card / ↑(Fintype.card V)

theorem MIPRE.SeededGame.dist_nonneg {V : Type u_1} {A : Type u_2} [Fintype V] [DecidableEq V] (S : SeededGame V A) (x y : V) : 0 ≤ S.dist x y

theorem MIPRE.SeededGame.sum_dist {V : Type u_1} {A : Type u_2} [Fintype V] [DecidableEq V] (S : SeededGame V A) [Nonempty V] : ∑ x : V, ∑ y : V, S.dist x y = 1

noncomputable def MIPRE.SeededGame.toGame {V : Type u_1} {A : Type u_2} [Fintype V] [DecidableEq V] [Fintype A] (S : SeededGame V A) [Nonempty V] : Game V V A A

The input game itself.

Equations

• S.toGame = { μ := S.dist, μ_nonneg := ⋯, μ_sum_one := ⋯, D := S.D }

@[simp]

theorem MIPRE.SeededGame.toGame_μ {V : Type u_1} {A : Type u_2} [Fintype V] [DecidableEq V] [Fintype A] (S : SeededGame V A) [Nonempty V] : S.toGame.μ = S.dist

@[simp]

theorem MIPRE.SeededGame.toGame_D {V : Type u_1} {A : Type u_2} [Fintype V] [DecidableEq V] [Fintype A] (S : SeededGame V A) [Nonempty V] : S.toGame.D = S.D

The oracularized alphabets

inductive MIPRE.OAns (A : Type u_3) : Type u_3

Answers of the oracularized game: a pair, from an oracle, or a single answer, from an isolated player. An answer whose shape does not match the role is rejected.

• pair {A : Type u_3} (a b : A) : OAns A
• single {A : Type u_3} (a : A) : OAns A

@[instance_reducible]

instance MIPRE.instDecidableEqOAns {A✝ : Type u_3} [DecidableEq A✝] : DecidableEq (OAns A✝)

Equations

• MIPRE.instDecidableEqOAns = MIPRE.instDecidableEqOAns.decEq

def MIPRE.instDecidableEqOAns.decEq {A✝ : Type u_3} [DecidableEq A✝] (x✝ x✝¹ : OAns A✝) : Decidable (x✝ = x✝¹)

Equations

• MIPRE.instDecidableEqOAns.decEq (MIPRE.OAns.pair a a_1) (MIPRE.OAns.pair b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• MIPRE.instDecidableEqOAns.decEq (MIPRE.OAns.pair a b) (MIPRE.OAns.single a_1) = isFalse ⋯
• MIPRE.instDecidableEqOAns.decEq (MIPRE.OAns.single a) (MIPRE.OAns.pair a_1 b) = isFalse ⋯
• MIPRE.instDecidableEqOAns.decEq (MIPRE.OAns.single a) (MIPRE.OAns.single b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def MIPRE.OAns.equivSum {A : Type u_2} : OAns A ≃ A × A ⊕ A

OAns A as a sum type. The Fintype instance goes through this rather than through a union of images, so that a sum over OAns A splits into the two blocks (OAns.sum_eq), which is what the measurement's normalization needs.

Equations

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

@[instance_reducible]

instance MIPRE.instFintypeOAns {A : Type u_2} [Fintype A] : Fintype (OAns A)

Equations

• MIPRE.instFintypeOAns = Fintype.ofEquiv (A × A ⊕ A) MIPRE.OAns.equivSum.symm

theorem MIPRE.OAns.sum_eq {A : Type u_2} [Fintype A] {M : Type u_3} [AddCommMonoid M] (f : OAns A → M) : ∑ u : OAns A, f u = ∑ p : A × A, f (pair p.1 p.2) + ∑ a : A, f (single a)

A sum over OAns A splits into the pairs and the singles.

@[instance_reducible]

instance MIPRE.instInhabitedOAns {A : Type u_2} [Inhabited A] : Inhabited (OAns A)

Equations

• MIPRE.instInhabitedOAns = { default := MIPRE.OAns.single default }

def MIPRE.SeededGame.oquestion {V : Type u_1} {A : Type u_2} (S : SeededGame V A) : Role → V → Role × V

The question a player in role r receives on seed z: the oracle gets the seed itself, an isolated player the question the corresponding original player would have received.

Equations

• S.oquestion MIPRE.Role.oracle x✝ = (MIPRE.Role.oracle, x✝)
• S.oquestion MIPRE.Role.alice x✝ = (MIPRE.Role.alice, S.LA x✝)
• S.oquestion MIPRE.Role.bob x✝ = (MIPRE.Role.bob, S.LB x✝)

@[simp]

theorem MIPRE.SeededGame.oquestion_fst {V : Type u_1} {A : Type u_2} (S : SeededGame V A) (r : Role) (z : V) : (S.oquestion r z).1 = r

@[simp]

theorem MIPRE.SeededGame.oquestion_oracle {V : Type u_1} {A : Type u_2} (S : SeededGame V A) (z : V) : S.oquestion Role.oracle z = (Role.oracle, z)

@[simp]

theorem MIPRE.SeededGame.oquestion_alice {V : Type u_1} {A : Type u_2} (S : SeededGame V A) (z : V) : S.oquestion Role.alice z = (Role.alice, S.LA z)

@[simp]

theorem MIPRE.SeededGame.oquestion_bob {V : Type u_1} {A : Type u_2} (S : SeededGame V A) (z : V) : S.oquestion Role.bob z = (Role.bob, S.LB z)

The decision predicate of fig:oracle-decider

def MIPRE.SeededGame.shapeOk {A : Type u_2} : Role → OAns A → Bool

The shape check: an oracle answers a pair, an isolated player a single answer.

Equations

• MIPRE.SeededGame.shapeOk MIPRE.Role.oracle (MIPRE.OAns.pair a b) = true
• MIPRE.SeededGame.shapeOk MIPRE.Role.alice (MIPRE.OAns.single a) = true
• MIPRE.SeededGame.shapeOk MIPRE.Role.bob (MIPRE.OAns.single a) = true
• MIPRE.SeededGame.shapeOk x✝¹ x✝ = false

def MIPRE.SeededGame.gameCheck {V : Type u_1} {A : Type u_2} (S : SeededGame V A) : Role × V → OAns A → Bool

The game check, step 1: an oracle's pair of answers must be accepted by the original predicate at the pair of questions its seed determines.

Equations

• S.gameCheck (MIPRE.Role.oracle, z) (MIPRE.OAns.pair a b) = S.D (S.LA z) (S.LB z) a b
• S.gameCheck x✝¹ x✝ = true

def MIPRE.SeededGame.oracleVsPlayer {V : Type u_1} {A : Type u_2} [DecidableEq A] : Role × V → Role × V → OAns A → OAns A → Bool

Check 2(b): an oracle's component for the other player's role must match that player's answer.

Equations

• MIPRE.SeededGame.oracleVsPlayer (MIPRE.Role.oracle, snd) (MIPRE.Role.alice, snd_1) (MIPRE.OAns.pair a b) (MIPRE.OAns.single a') = decide (a = a')
• MIPRE.SeededGame.oracleVsPlayer (MIPRE.Role.oracle, snd) (MIPRE.Role.bob, snd_1) (MIPRE.OAns.pair a b) (MIPRE.OAns.single b') = decide (b = b')
• MIPRE.SeededGame.oracleVsPlayer x✝³ x✝² x✝¹ x✝ = true

def MIPRE.SeededGame.oaccepts {V : Type u_1} {A : Type u_2} [DecidableEq A] (S : SeededGame V A) (p q : Role × V) (u v : OAns A) : Bool

The predicate of fig:oracle-decider: the shape checks, the game check for each oracle, and the two consistency checks --- equal roles force equal answers, and an oracle's relevant component must match an isolated player's answer.

Equations

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

theorem MIPRE.SeededGame.oaccepts_eq_false_of_ne {V : Type u_1} {A : Type u_2} [DecidableEq A] (S : SeededGame V A) {p : Role × V} {u v : OAns A} (h : u ≠ v) : S.oaccepts p p u v = false

The oracularized game

noncomputable def MIPRE.SeededGame.oDist {V : Type u_1} {A : Type u_2} [Fintype V] [DecidableEq V] (S : SeededGame V A) (p q : Role × V) : ℝ

The uniform distribution over the oracularized game's random choices: the ordered pair of roles and the seed.

Equations

• S.oDist p q = ∑ s : MIPRE.Role × MIPRE.Role × V, (↑(Fintype.card (MIPRE.Role × MIPRE.Role × V)))⁻¹ * if (S.oquestion s.1 s.2.2, S.oquestion s.2.1 s.2.2) = (p, q) then 1 else 0

theorem MIPRE.SeededGame.oDist_nonneg {V : Type u_1} {A : Type u_2} [Fintype V] [DecidableEq V] (S : SeededGame V A) (p q : Role × V) : 0 ≤ S.oDist p q

theorem MIPRE.SeededGame.sum_oDist {V : Type u_1} {A : Type u_2} [Fintype V] [DecidableEq V] (S : SeededGame V A) [Nonempty V] : ∑ p : Role × V, ∑ q : Role × V, S.oDist p q = 1

noncomputable def MIPRE.SeededGame.oracular {V : Type u_1} {A : Type u_2} [Fintype V] [DecidableEq V] [Fintype A] [DecidableEq A] (S : SeededGame V A) [Nonempty V] : SynchronousGame (Role × V) (OAns A)

The oracularized game (blueprint thm:oracularization, paper sec:orac-def). It is synchronous with no further hypothesis: equal questions carry equal roles, and check 2(a) rejects unequal answers there.

Equations

• S.oracular = { μ := S.oDist, μ_nonneg := ⋯, μ_sum_one := ⋯, D := S.oaccepts, synchronous := ⋯ }

@[simp]

theorem MIPRE.SeededGame.oracular_μ {V : Type u_1} {A : Type u_2} [Fintype V] [DecidableEq V] [Fintype A] [DecidableEq A] (S : SeededGame V A) [Nonempty V] : S.oracular.μ = S.oDist

@[simp]

theorem MIPRE.SeededGame.oracular_D {V : Type u_1} {A : Type u_2} [Fintype V] [DecidableEq V] [Fintype A] [DecidableEq A] (S : SeededGame V A) [Nonempty V] : S.oracular.D = S.oaccepts