Padding the original CL source game without changing its strategy

Unused seed coordinates are ignored. On every sampled padded question pair, the pulled-back questions have one common original seed. This suffices to preserve perfect PCC play with exactly the original Hilbert-space dimension.

noncomputable def MIPRE.Introspection.SourcePadding.family {F : Type u_1} {I : Type u_2} {J : Type u_3} [Field F] [DecidableEq I] [DecidableEq J] {ℓ : ℕ} (e : I ↪ J) (L : Bool → CL.CLFun F I ℓ) (w : Bool) : CL.CLFun F J ℓ

Equations

• MIPRE.Introspection.SourcePadding.family e L w = MIPRE.CL.CLFun.embed e (L w)

def MIPRE.Introspection.SourcePadding.decider {F : Type u_1} {I : Type u_2} {J : Type u_3} {A : Type u_4} (e : I ↪ J) (D : (I → F) → (I → F) → A → A → Bool) (x y : J → F) : A → A → Bool

Equations

• MIPRE.Introspection.SourcePadding.decider e D x y = D (MIPRE.CL.pull e x) (MIPRE.CL.pull e y)

theorem MIPRE.Introspection.SourcePadding.supported_embed {F : Type u_1} {I : Type u_2} {J : Type u_3} [Field F] [Fintype F] [DecidableEq F] [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] (e : I ↪ J) {k : ℕ} (P : CL.CLFun F I k) (S : Finset I) (hP : P.SupportedOn S) : (CL.CLFun.embed e P).SupportedOn (Finset.map e S)

theorem MIPRE.Introspection.SourcePadding.family_supported {F : Type u_1} {I : Type u_2} {J : Type u_3} [Field F] [Fintype F] [DecidableEq F] [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] {ℓ : ℕ} (e : I ↪ J) (L : Bool → CL.CLFun F I ℓ) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (w : Bool) : (family e L w).SupportedOn Finset.univ

theorem MIPRE.Introspection.SourcePadding.pull_family {F : Type u_1} {I : Type u_2} {J : Type u_3} [Field F] [Fintype F] [DecidableEq F] [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] {ℓ : ℕ} (e : I ↪ J) (L : Bool → CL.CLFun F I ℓ) (w : Bool) (x : J → F) : CL.pull e ((family e L w).eval x) = (L w).eval (CL.pull e x)

noncomputable def MIPRE.Introspection.SourcePadding.depthFamily {F : Type u_1} {I : Type u_2} {J : Type u_3} [Field F] [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] {ℓ : ℕ} (e : I ↪ J) (L : Bool → CL.CLFun F I ℓ) (w : Bool) : CL.CLFun F J ℓ

Consume unused coordinates by the zero part of the existing first factor, preserving the original depth.

Equations

• MIPRE.Introspection.SourcePadding.depthFamily e L w = (MIPRE.Introspection.SourcePadding.family e L w).directSum (MIPRE.CL.CLFun.zeroOn (Finset.map e Finset.univ)ᶜ ℓ)

theorem MIPRE.Introspection.SourcePadding.depthFamily_exactlyOn {F : Type u_1} {I : Type u_2} {J : Type u_3} [Field F] [Fintype F] [DecidableEq F] [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] {ℓ : ℕ} (e : I ↪ J) (L : Bool → CL.CLFun F I ℓ) (hℓ : 0 < ℓ) (hL : ∀ (w : Bool), (L w).ExactlyOn Finset.univ) (w : Bool) : (depthFamily e L w).ExactlyOn Finset.univ

theorem MIPRE.Introspection.SourcePadding.depthFamily_eval {F : Type u_1} {I : Type u_2} {J : Type u_3} [Field F] [Fintype F] [DecidableEq F] [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] {ℓ : ℕ} (e : I ↪ J) (L : Bool → CL.CLFun F I ℓ) (hℓ : 0 < ℓ) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (w : Bool) (x : J → F) : (depthFamily e L w).eval x = (family e L w).eval x

theorem MIPRE.Introspection.SourcePadding.sourceGame_depthFamily {F : Type u_1} {I : Type u_2} {J : Type u_3} {A : Type u_4} [Field F] [Fintype F] [DecidableEq F] [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype A] [DecidableEq A] {ℓ : ℕ} (e : I ↪ J) (L : Bool → CL.CLFun F I ℓ) (D : (I → F) → (I → F) → A → A → Bool) (hℓ : 0 < ℓ) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) : Honest.sourceGame (depthFamily e L) (decider e D) = Honest.sourceGame (family e L) (decider e D)

def MIPRE.Introspection.SourcePadding.strategy {F : Type u_1} {I : Type u_2} {J : Type u_3} {A : Type u_4} [Field F] [Fintype F] [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype A] [DecidableEq A] {ℓ : ℕ} (e : I ↪ J) (L : Bool → CL.CLFun F I ℓ) (D : (I → F) → (I → F) → A → A → Bool) (R : SyncStrategy (Honest.sourceGame L D).doubled) : SyncStrategy (Honest.sourceGame (family e L) (decider e D)).doubled

The common source measurement rule just restricts question coordinates.

Equations

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

theorem MIPRE.Introspection.SourcePadding.positive_seed {F : Type u_1} {I : Type u_2} {J : Type u_3} {A : Type u_4} [Field F] [Fintype F] [DecidableEq F] [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype A] [DecidableEq A] {ℓ : ℕ} (e : I ↪ J) (L : Bool → CL.CLFun F I ℓ) (D : (I → F) → (I → F) → A → A → Bool) (q r : Bool × (J → F)) (h : 0 < (Honest.sourceGame (family e L) (decider e D)).doubled.μ q r) : ∃ (x : J → F), q = (false, (family e L false).eval x) ∧ r = (true, (family e L true).eval x)

theorem MIPRE.Introspection.SourcePadding.strategy_isPCC {F : Type u_1} {I : Type u_2} {J : Type u_3} {A : Type u_4} [Field F] [Fintype F] [DecidableEq F] [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype A] [DecidableEq A] {ℓ : ℕ} (e : I ↪ J) (L : Bool → CL.CLFun F I ℓ) (D : (I → F) → (I → F) → A → A → Bool) (R : SyncStrategy (Honest.sourceGame L D).doubled) (hR : R.IsPCC) : (strategy e L D R).IsPCC

theorem MIPRE.Introspection.SourcePadding.strategy_value {F : Type u_1} {I : Type u_2} {J : Type u_3} {A : Type u_4} [Field F] [Fintype F] [DecidableEq F] [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype A] [DecidableEq A] {ℓ : ℕ} (e : I ↪ J) (L : Bool → CL.CLFun F I ℓ) (D : (I → F) → (I → F) → A → A → Bool) (R : SyncStrategy (Honest.sourceGame L D).doubled) (hR : R.IsPCC) (hv : R.value = 1) : (strategy e L D R).value = 1

theorem MIPRE.Introspection.SourcePadding.exists_perfectPCC {F : Type u_1} {I : Type u_2} {J : Type u_3} {A : Type u_4} [Field F] [Fintype F] [DecidableEq F] [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype A] [DecidableEq A] {ℓ : ℕ} (e : I ↪ J) (L : Bool → CL.CLFun F I ℓ) (D : (I → F) → (I → F) → A → A → Bool) (R : SyncStrategy (Honest.sourceGame L D).doubled) (hR : R.IsPCC) (hv : R.value = 1) : ∃ (Q : SyncStrategy (Honest.sourceGame (family e L) (decider e D)).doubled), Q.IsPCC ∧ Q.value = 1 ∧ Q.d = R.d

Padding does not cost auxiliary dimension or perfect PCC value.