The honest Introspect and Sample measurements

These are the concrete measurements from the completeness proof in introspection.tex. Every answer label is retained. Their products vanish on unrealizable pairs of question labels; source PCC is only used for labels generated by a common seed.

@[reducible, inline]

abbrev MIPRE.Introspection.Honest.CoreType : Type

The first bit selects Sample rather than Introspect; the second is the original role.

Equations

• MIPRE.Introspection.Honest.CoreType = (Bool × Bool)

def MIPRE.Introspection.Honest.coreType {ℓ : ℕ} {P : Type u_4} (t : CoreType) : QuestionType P ℓ

Equations

• MIPRE.Introspection.Honest.coreType t = Sum.inr (if t.1 = true then MIPRE.Introspection.AuxType.sample else MIPRE.Introspection.AuxType.introspect, t.2)

def MIPRE.Introspection.Honest.displayed {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (t : CoreType) (z : ι → F) : ι → F

Equations

• MIPRE.Introspection.Honest.displayed L t z = if t.1 = true then z else (L t.2).eval z

def MIPRE.Introspection.Honest.originalQuestion {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (t : CoreType) (y : ι → F) : ι → F

Equations

• MIPRE.Introspection.Honest.originalQuestion L t y = if t.1 = true then (L t.2).eval y else y

@[simp]

theorem MIPRE.Introspection.Honest.originalQuestion_displayed {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (t : CoreType) (z : ι → F) : originalQuestion L t (displayed L t z) = (L t.2).eval z

@[reducible, inline]

noncomputable abbrev MIPRE.Introspection.Honest.sourceGame {F : Type u_1} {ι : Type u_2} {A : Type u_3} [Field F] [Fintype F] [Fintype ι] [DecidableEq ι] [Fintype A] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) : Game (ι → F) (ι → F) A A

Equations

• MIPRE.Introspection.Honest.sourceGame L D = MIPRE.SampledGame.game (L false).eval (L true).eval D

theorem MIPRE.Introspection.Honest.source_mu_pos {F : Type u_1} {ι : Type u_2} {A : Type u_3} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (z : ι → F) : 0 < (sourceGame L D).doubled.μ (false, (L false).eval z) (true, (L true).eval z)

theorem MIPRE.Introspection.Honest.source_isPVM {F : Type u_1} {ι : Type u_2} {A : Type u_3} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (R : SyncStrategy (sourceGame L D).doubled) (w : Bool) (y : ι → F) : IsPVM (R.P.M (w, y))

theorem MIPRE.Introspection.Honest.source_commute {F : Type u_1} {ι : Type u_2} {A : Type u_3} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (R : SyncStrategy (sourceGame L D).doubled) (hR : R.IsPCC) (w v : Bool) (z : ι → F) (a b : A) : Commute (R.P.M (w, (L w).eval z) a) (R.P.M (v, (L v).eval z) b)

theorem MIPRE.Introspection.Honest.source_reject_zero {F : Type u_1} {ι : Type u_2} {A : Type u_3} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (R : SyncStrategy (sourceGame L D).doubled) (hR : R.IsPCC) (hval : R.value = 1) (z : ι → F) (a b : A) (hD : D ((L false).eval z) ((L true).eval z) a b = false) : R.P.M (false, (L false).eval z) a * R.P.M (true, (L true).eval z) b = 0

def MIPRE.Introspection.Honest.kronReadout {I : Type u_4} {X : Type u_5} {Y : Type u_6} {H : Type u_7} [Fintype I] [DecidableEq I] [DecidableEq X] (f : I → X) (P : X → Y → Matrix H H ℂ) (xa : X × Y) : Matrix (I × H) (I × H) ℂ

The honest conditional readout on the concrete register-auxiliary product: read the question from the seed, then measure the auxiliary system (conditionalReadout in the register model).

Equations

• MIPRE.Introspection.Honest.kronReadout f P xa = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (MIPRE.Introspection.readout f xa.1) (P xa.1 xa.2)

theorem MIPRE.Introspection.Honest.kronReadout_isPVM {I : Type u_4} {X : Type u_5} {Y : Type u_6} {H : Type u_7} [Fintype I] [DecidableEq I] [Fintype X] [DecidableEq X] [Fintype Y] [Fintype H] [DecidableEq H] (f : I → X) (P : X → Y → Matrix H H ℂ) (hP : ∀ (x : X), IsPVM (P x)) : IsPVM (kronReadout f P)

def MIPRE.Introspection.Honest.coreOp {F : Type u_1} {ι : Type u_2} {A : Type u_3} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (R : SyncStrategy (sourceGame L D).doubled) (t : CoreType) (ya : (ι → F) × A) : Matrix ((ι → F) × Fin R.d) ((ι → F) × Fin R.d) ℂ

The actual honest register/auxiliary measurement for each of the four core types.

Equations

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

theorem MIPRE.Introspection.Honest.coreOp_isPVM {F : Type u_1} {ι : Type u_2} {A : Type u_3} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (R : SyncStrategy (sourceGame L D).doubled) (t : CoreType) : IsPVM (coreOp L D R t)

theorem MIPRE.Introspection.Honest.coreOp_mul_apply {F : Type u_1} {ι : Type u_2} {A : Type u_3} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (R : SyncStrategy (sourceGame L D).doubled) (t u : CoreType) (ya zb : (ι → F) × A) (s s' : ι → F) (i j : Fin R.d) : (coreOp L D R t ya * coreOp L D R u zb) (s, i) (s', j) = if s = s' ∧ displayed L t s = ya.1 ∧ displayed L u s = zb.1 then (R.P.M (t.2, (L t.2).eval s) ya.2 * R.P.M (u.2, (L u.2).eval s) zb.2) i j else 0

Each seed block contains exactly the original two auxiliary operators. All impossible claimed labels vanish before any commutation assumption is used.

theorem MIPRE.Introspection.Honest.coreOp_commute {F : Type u_1} {ι : Type u_2} {A : Type u_3} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (R : SyncStrategy (sourceGame L D).doubled) (hR : R.IsPCC) (t u : CoreType) (ya zb : (ι → F) × A) : Commute (coreOp L D R t ya) (coreOp L D R u zb)

The honest core operators commute for every answer label, even labels not realizable by a common seed.