Z-aligned permutation strategies, without commutation along edges

A Z-aligned permutation strategy of a tailored game (paper I, Definition I:2026; paper II, II:1056) is a TailoredGameValue.PermStrategy without its field commEdges: one signed permutation matrix per formal variable, involutions commuting at each vertex, the identity beyond ℓ(x), and diagonal on the readable variables. Paper I's Proposition I:2279 produces such a strategy from an action passing Checks 1–3 of the associated test, and the commutation along edges plays no part there, nor in the value.

• ZStrat, ZStrat.proj, ZStrat.value: the strategy, its Fourier measurements and its value, spelled as PermStrategy's.
• ZStrat.toSync, ZStrat.value_toSync, ZStrat.value_le_gameValue: it is a synchronous strategy with the same value, so its value bounds the synchronous value from below, as Data/Bridge.lean shows for PermStrategy, whose proof never uses commEdges.
• ZStrat.value_eq_sum_rej: the value is ∑ μ(x, y) (1 - rej(x, y)), with rej(x, y) the probability of a rejected answer pair at (x, y).
• ZStrat.proj_eq_zero_of_not_wellFormatted, ZStrat.proj_mul_proj_of_ne: malformed answers have zero projection, and distinct answers at one vertex orthogonal projections.

structure MIPRE.Tailored.Sofic.ZStrat (g : TailoredGameValue.TailoredGameData) : Type

A Z-aligned permutation strategy for a tailored game: PermStrategy without the commutation along edges.

• m : ℕ

  The dimension.

• m_pos : 0 < self.m
• U : Fin (g.nV + 1) → Fin g.ansLen → Matrix (Fin self.m) (Fin self.m) ℂ

  The observables.

• signedPerm (x : Fin (g.nV + 1)) (i : Fin g.ansLen) : IsSignedPerm (self.U x i)
• invol (x : Fin (g.nV + 1)) (i : Fin g.ansLen) : self.U x i * self.U x i = 1
• comm (x : Fin (g.nV + 1)) (i j : Fin g.ansLen) : self.U x i * self.U x j = self.U x j * self.U x i
• pad (x : Fin (g.nV + 1)) (i : Fin g.ansLen) : g.lenAt ↑x ≤ ↑i → self.U x i = 1
• zAligned (x : Fin (g.nV + 1)) (i : Fin g.ansLen) : ↑i < g.lenRAt ↑x → (self.U x i).IsDiag

noncomputable def MIPRE.Tailored.Sofic.ZStrat.proj {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x : Fin (g.nV + 1)) (a : Fin g.ansLen → Bool) : Matrix (Fin S.m) (Fin S.m) ℂ

The measurement at x, the Fourier transform of the observables.

Equations

• S.proj x a = MIPRE.Tailored.fourierProj (S.U x) a

noncomputable def MIPRE.Tailored.Sofic.ZStrat.value {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) : ℝ

The value, spelled as PermStrategy.value.

Equations

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

theorem MIPRE.Tailored.Sofic.ZStrat.commute_U {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x : Fin (g.nV + 1)) (i j : Fin g.ansLen) : Commute (S.U x i) (S.U x j)

theorem MIPRE.Tailored.Sofic.ZStrat.star_U {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x : Fin (g.nV + 1)) (i : Fin g.ansLen) : star (S.U x i) = S.U x i

The observables are self-adjoint.

theorem MIPRE.Tailored.Sofic.ZStrat.isPVMIn_proj {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x : Fin (g.nV + 1)) : IsPVMIn (S.proj x)

The measurements are projective.

noncomputable def MIPRE.Tailored.Sofic.ZStrat.toSync {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) : SyncStrategy g.syncGame

A Z-aligned permutation strategy is a synchronous strategy.

Equations

• S.toSync = { d := S.m, d_pos := ⋯, P := { M := S.proj, selfAdjoint := ⋯, projective := ⋯, normalized := ⋯ } }

theorem MIPRE.Tailored.Sofic.ZStrat.value_toSync {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) : S.toSync.value = S.value

It has the same value.

theorem MIPRE.Tailored.Sofic.ZStrat.value_le_gameValue {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) : S.value ≤ HaltingGameValue.gameValue g.toGame

The value of a Z-aligned permutation strategy is at most the synchronous value.

Elementary facts about the measurements

theorem MIPRE.Tailored.Sofic.ZStrat.U_mul_proj {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x : Fin (g.nV + 1)) (i : Fin g.ansLen) (a : Fin g.ansLen → Bool) : S.U x i * S.proj x a = bitSign (a i) • S.proj x a

P_a lies in the (-1)^{a_i}-eigenspace of U x i.

theorem MIPRE.Tailored.Sofic.ZStrat.commute_U_proj {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x : Fin (g.nV + 1)) (i : Fin g.ansLen) (a : Fin g.ansLen → Bool) : Commute (S.U x i) (S.proj x a)

theorem MIPRE.Tailored.Sofic.ZStrat.proj_mul_U {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x : Fin (g.nV + 1)) (i : Fin g.ansLen) (a : Fin g.ansLen → Bool) : S.proj x a * S.U x i = bitSign (a i) • S.proj x a

theorem MIPRE.Tailored.Sofic.ZStrat.proj_eq_zero_of_not_wellFormatted {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x : Fin (g.nV + 1)) (a : Fin g.ansLen → Bool) (h : ¬g.WellFormatted x a) : S.proj x a = 0

Malformed answers have zero projection: the padded observables are the identity.

theorem MIPRE.Tailored.Sofic.ZStrat.proj_mul_proj_of_ne {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x : Fin (g.nV + 1)) {a b : Fin g.ansLen → Bool} (h : a ≠ b) : S.proj x a * S.proj x b = 0

Distinct answers at one vertex have orthogonal projections.

theorem MIPRE.Tailored.Sofic.ZStrat.star_proj {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x : Fin (g.nV + 1)) (a : Fin g.ansLen → Bool) : star (S.proj x a) = S.proj x a

theorem MIPRE.Tailored.Sofic.ZStrat.re_trace_proj_mul_proj_nonneg {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x y : Fin (g.nV + 1)) (a b : Fin g.ansLen → Bool) : 0 ≤ (S.proj x a * S.proj y b).trace.re

Tr(P_a Q_b) ≥ 0.

theorem MIPRE.Tailored.Sofic.ZStrat.sum_trace_proj_mul_proj {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x y : Fin (g.nV + 1)) : ∑ a : Fin g.ansLen → Bool, ∑ b : Fin g.ansLen → Bool, (S.proj x a * S.proj y b).trace = ↑S.m

∑_{a, b} Tr(P_a Q_b) = m.

noncomputable def MIPRE.Tailored.Sofic.ZStrat.rej {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x y : Fin (g.nV + 1)) : ℝ

The probability of a rejected answer pair at (x, y).

Equations

• S.rej x y = ∑ a : Fin g.ansLen → Bool, ∑ b : Fin g.ansLen → Bool, (if g.Accepts x y a b then 0 else 1) * ((S.proj x a * S.proj y b).trace.re / ↑S.m)

theorem MIPRE.Tailored.Sofic.ZStrat.rej_nonneg {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x y : Fin (g.nV + 1)) : 0 ≤ S.rej x y

theorem MIPRE.Tailored.Sofic.ZStrat.value_eq_sum_rej {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) : S.value = ∑ x : Fin (g.nV + 1), ∑ y : Fin (g.nV + 1), g.toGame.μ x y * (1 - S.rej x y)

The value as one minus the rejection probability.

def TailoredGameValue.PermStrategy.toZStrat {g : TailoredGameData} (S : PermStrategy g) : MIPRE.Tailored.Sofic.ZStrat g

A permutation strategy, forgetting the commutation along edges.

Equations

• S.toZStrat = { m := S.m, m_pos := ⋯, U := S.U, signedPerm := ⋯, invol := ⋯, comm := ⋯, pad := ⋯, zAligned := ⋯ }

theorem TailoredGameValue.PermStrategy.value_toZStrat {g : TailoredGameData} (S : PermStrategy g) : S.toZStrat.value = S.value