Source-game transport along a concrete coordinate bijection

The value comparison is stated in a value model (Phase 4 of planning/mipco-track.md): the reindexed source game is related to the original one by the coordinate bijection on the questions, so the two have the same value in every value model (quantumValue_eq, through ValueModel.eq_of_equiv); the quantum-value statement is its instance at ValueModel.tensor.

def MIPRE.Introspection.SourceReindex.family {F : Type u_1} {ι : Type u_2} {κ : Type u_3} [Field F] [DecidableEq ι] [DecidableEq κ] {ℓ : ℕ} (e : ι ≃ κ) (L : Bool → CL.CLFun F ι ℓ) (w : Bool) : CL.CLFun F κ ℓ

Equations

• MIPRE.Introspection.SourceReindex.family e L w = MIPRE.CL.CLFun.reindex e (L w)

def MIPRE.Introspection.SourceReindex.decider {F : Type u_1} {ι : Type u_2} {κ : Type u_3} {A : Type u_4} [Field F] (e : ι ≃ κ) (D : (ι → F) → (ι → F) → A → A → Bool) (x y : κ → F) : A → A → Bool

Equations

• MIPRE.Introspection.SourceReindex.decider e D x y = D ((MIPRE.CL.reindexEquiv e).symm x) ((MIPRE.CL.reindexEquiv e).symm y)

theorem MIPRE.Introspection.SourceReindex.exactlyOn {F : Type u_1} {ι : Type u_2} {κ : Type u_3} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] {ℓ : ℕ} (e : ι ≃ κ) (L : Bool → CL.CLFun F ι ℓ) (hL : ∀ (w : Bool), (L w).ExactlyOn Finset.univ) (w : Bool) : (family e L w).ExactlyOn Finset.univ

theorem MIPRE.Introspection.SourceReindex.game_mu {F : Type u_1} {ι : Type u_2} {κ : Type u_3} {A : Type u_4} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] [Fintype A] [DecidableEq A] {ℓ : ℕ} (e : ι ≃ κ) (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (x y : κ → F) : (Honest.sourceGame (family e L) (decider e D)).μ x y = (Honest.sourceGame L D).μ ((CL.reindexEquiv e).symm x) ((CL.reindexEquiv e).symm y)

@[reducible, inline]

noncomputable abbrev MIPRE.Introspection.SourceReindex.strategy {F : Type u_1} {ι : Type u_2} {κ : Type u_3} {A : Type u_4} [Field F] [Fintype F] [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] [Fintype A] [DecidableEq A] {ℓ : ℕ} (e : ι ≃ κ) (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (R : SyncStrategy (Honest.sourceGame L D).doubled) : SyncStrategy (Honest.sourceGame (family e L) (decider e D)).doubled

Equations

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

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

theorem MIPRE.Introspection.SourceReindex.strategy_value {F : Type u_1} {ι : Type u_2} {κ : Type u_3} {A : Type u_4} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] [Fintype A] [DecidableEq A] {ℓ : ℕ} (e : ι ≃ κ) (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (R : SyncStrategy (Honest.sourceGame L D).doubled) : (strategy e L D R).value = R.value

@[simp]

theorem MIPRE.Introspection.SourceReindex.strategy_dimension {F : Type u_1} {ι : Type u_2} {κ : Type u_3} {A : Type u_4} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] [Fintype A] [DecidableEq A] {ℓ : ℕ} (e : ι ≃ κ) (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (R : SyncStrategy (Honest.sourceGame L D).doubled) : (strategy e L D R).d = R.d

theorem MIPRE.Introspection.SourceReindex.quantumValue_eq {F ι κ A : Type} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] [Fintype A] [DecidableEq A] {ℓ : ℕ} (ω : ValueModel) (e : ι ≃ κ) (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) : ω.val (Honest.sourceGame (family e L) (decider e D)) = ω.val (Honest.sourceGame L D)

The reindexed source game has the value of the original one, in every value model: the coordinate bijection carries its question law and decision predicate onto the original ones.