Tailored games and Z-aligned permutation strategies

Paper II of the Aldous–Lyons track (Bowen–Chapman–Vidick, arXiv:2501.00173), §2.2–2.4 (II:1008–1290); the plan is planning/aldous-lyons-track.md. This file is the library-side vocabulary of the track: the statement file MIPRE.TailoredGameValue has its own first-order copy, written against Mathlib only, which the library is to be bridged to.

• MIPRE.Tailored.TailoredGame X: a game on the question set X whose question x has lenR x readable and lenL x linear formal variables, and whose decision is given by controlled linear constraints: for questions x, y and readable answers a^R, b^R, a list cons x y a^R b^R of vectors over S_x ⊔ S_y ⊔ {J}. The answers are bit strings, the answer at x of length exactly len x = lenR x + lenL x, readable bits first.
• TailoredGame.Accepts: the paper's canonical decider (II:1757–1787): both answers have the right length, and every constraint c satisfies ⟨c, a b 1⟩ = 0 over F₂ (Satisfies), the last coordinate J being set to 1. The empty list accepts, [rejectConstraint _] rejects.
• TailoredGame.toGame, valStar: the bipartite game, with answers the bit strings of length at most maxLen, and its quantum value. Answers of the wrong length are rejected, so the alphabet is the paper's F₂^{S_x} up to answers that lose.
• TailoredGame.doubled: the game on the doubled question set, Alice asked (false, x) and Bob (true, y) — again a tailored game, bipartite, with no weight on loops; it is the game in which the pipeline's completeness clauses are read, as Verifier.HasPerfectPCC reads the completeness of the existing pipeline on Verifier.doubledGame.
• PermStrategy, HasPerfectZPC (II:1043–1057, II:1279–1283): a strategy whose observables are signed permutation matrices — one per formal variable, involutions, commuting at each question — with diagonal observables for the readable variables (Z-aligned) and commuting across the edges of positive weight (commuting along edges); its measurements are the Fourier transforms P^x_a = ∏_i (1 + (-1)^{a_i} U(x, i)) / 2, and it is perfect when its value is 1. The answer alphabet at x is literally F₂^{len x} here, as in the paper.

One thing is proved, that the definitions are not vacuous: a game that accepts the all-zero answers has a perfect ZPC strategy, the trivial one (hasPerfectZPC_of_accepts_zero). Phase 1 of the plan proves that a permutation strategy is a synchronous strategy commuting on the support with the same value (ZPC → PCC), and the transports between this file and MIPRE.TailoredGameValue.

Linear constraints over F₂

def MIPRE.Tailored.Satisfies (c v : Cost.BitStr) : Prop

A bit vector v satisfies the linear constraint c when they have the same length and ⟨c, v⟩ = 0 over F₂. A constraint of the wrong length is never satisfied, as the paper's canonical decider rejects malformed constraints.

Equations

• MIPRE.Tailored.Satisfies c v = (List.length c = List.length v ∧ Even (List.count true (List.zipWith (fun (x1 x2 : Bool) => x1 && x2) c v)))

@[instance_reducible]

instance MIPRE.Tailored.instDecidableSatisfies (c v : Cost.BitStr) : Decidable (Satisfies c v)

Equations

• MIPRE.Tailored.instDecidableSatisfies c v = id inferInstance

def MIPRE.Tailored.rejectConstraint (d : ℕ) : Cost.BitStr

The constraint J = 0 on d variables and the affine coordinate: never satisfied by a vector whose last coordinate is 1, so a constraint list containing it rejects.

Equations

• MIPRE.Tailored.rejectConstraint d = List.replicate d false ++ [true]

theorem MIPRE.Tailored.not_satisfies_rejectConstraint (d : ℕ) (v : Cost.BitStr) : ¬Satisfies (rejectConstraint d) (v ++ [true])

A vector whose last coordinate is 1 never satisfies the rejecting constraint J = 0.

Tailored games

structure MIPRE.Tailored.TailoredGame (X : Type u_1) [Fintype X] : Type u_1

A tailored game (II:1243) on the finite question set X.

• μ : X → X → ℝ

  The probability of the question pair (x, y).

• μ_nonneg (x y : X) : 0 ≤ self.μ x y
• μ_sum_one : ∑ x : X, ∑ y : X, self.μ x y = 1
• lenR : X → ℕ

  The number of readable variables at a question.

• lenL : X → ℕ

  The number of linear variables at a question.

• cons : X → X → Cost.BitStr → Cost.BitStr → List Cost.BitStr

  The controlled linear constraints L_xy(a^R, b^R): vectors over the variables at x (readable, then linear), those at y, and the affine coordinate J.

def MIPRE.Tailored.TailoredGame.len {X : Type u_1} [Fintype X] (G : TailoredGame X) (x : X) : ℕ

The number of variables at a question, the length of its answers.

Equations

• G.len x = G.lenR x + G.lenL x

def MIPRE.Tailored.TailoredGame.maxLen {X : Type u_1} [Fintype X] (G : TailoredGame X) : ℕ

The largest answer length.

Equations

• G.maxLen = Finset.univ.sup G.len

def MIPRE.Tailored.TailoredGame.Accepts {X : Type u_1} [Fintype X] (G : TailoredGame X) (x y : X) (a b : Cost.BitStr) : Prop

The canonical decider (II:1757–1787): both answers have their lengths, and every constraint of L_xy(a^R, b^R) is satisfied by the two answers followed by J = 1.

Equations

• G.Accepts x y a b = (List.length a = G.len x ∧ List.length b = G.len y ∧ ∀ c ∈ G.cons x y (List.take (G.lenR x) a) (List.take (G.lenR y) b), MIPRE.Tailored.Satisfies c (a ++ b ++ [true]))

@[instance_reducible]

instance MIPRE.Tailored.TailoredGame.instDecidableAccepts {X : Type u_1} [Fintype X] (G : TailoredGame X) (x y : X) (a b : Cost.BitStr) : Decidable (G.Accepts x y a b)

Equations

• G.instDecidableAccepts x y a b = id inferInstance

noncomputable def MIPRE.Tailored.TailoredGame.toGame {X : Type u_1} [Fintype X] (G : TailoredGame X) : Game X X (Verifier.Answers G.maxLen) (Verifier.Answers G.maxLen)

The bipartite game: answers the bit strings of length at most maxLen, accepted by the canonical decider.

Equations

• G.toGame = { μ := G.μ, μ_nonneg := ⋯, μ_sum_one := ⋯, D := fun (x y : X) (a b : MIPRE.Verifier.Answers G.maxLen) => decide (G.Accepts x y ↑a ↑b) }

noncomputable def MIPRE.Tailored.TailoredGame.valStar {X : Type u_1} [Fintype X] (G : TailoredGame X) : ℝ

The quantum value of a tailored game.

Equations

• G.valStar = MIPRE.quantumValue G.toGame

def MIPRE.Tailored.TailoredGame.doubled {X : Type u_1} [Fintype X] (G : TailoredGame X) : TailoredGame (Bool × X)

The game on the doubled question set: Alice is asked (false, x), Bob (true, y), with the weight of (x, y); every other pair has no weight. The variables and constraints are those of the underlying questions.

Equations

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

Z-aligned permutation strategies commuting along edges

def MIPRE.Tailored.bitSign (b : Bool) : ℂ

(-1)^b, as a complex number.

Equations

• MIPRE.Tailored.bitSign b = if b = true then -1 else 1

def MIPRE.Tailored.signedPermMatrix {Ω : Type u_1} [DecidableEq Ω] (σ : Equiv.Perm Ω) (s : Ω → Bool) : Matrix Ω Ω ℂ

The signed permutation matrix e_j ↦ (-1)^{s j} e_{σ j} (II:1043–1053): the action of the signed permutation (σ, s) of Ω_± = {±} × Ω on the anti-symmetric functions, in their standard basis. The combinatorial object and its algebra are MIPRE.Tailored.SignedPerm.

Equations

• MIPRE.Tailored.signedPermMatrix σ s i j = if σ j = i then MIPRE.Tailored.bitSign (s j) else 0

def MIPRE.Tailored.IsSignedPerm {Ω : Type u_1} [DecidableEq Ω] (M : Matrix Ω Ω ℂ) : Prop

A signed permutation matrix.

Equations

• MIPRE.Tailored.IsSignedPerm M = ∃ (σ : Equiv.Perm Ω) (s : Ω → Bool), M = MIPRE.Tailored.signedPermMatrix σ s

noncomputable def MIPRE.Tailored.fourierFactor {R : Type u_1} [Ring R] [Algebra ℂ R] (u : R) (b : Bool) : R

The factor (1 + (-1)^b u) / 2 of a Fourier transform: for an involution u, the projection onto its (-1)^b-eigenspace.

Equations

• MIPRE.Tailored.fourierFactor u b = (1 / 2) • (1 + MIPRE.Tailored.bitSign b • u)

noncomputable def MIPRE.Tailored.fourierProj {R : Type u_1} [Ring R] [Algebra ℂ R] {k : ℕ} (U : Fin k → R) (a : Fin k → Bool) : R

The Fourier transform of a family of commuting involutions U (II:974, II:986): the projective measurement P_a = ∏_i (1 + (-1)^{a_i} U i) / 2, for a ∈ F₂^k, which is the projective form of the measurement whose observable form is U (MIPRE.Tailored.Fourier).

Equations

• MIPRE.Tailored.fourierProj U a = (List.map (fun (i : Fin k) => MIPRE.Tailored.fourierFactor (U i) (a i)) (List.finRange k)).prod

structure MIPRE.Tailored.PermStrategy {X : Type u_1} [Fintype X] (G : TailoredGame X) : Type u_1

A Z-aligned permutation strategy commuting along edges (II:1056, II:1279–1283) for a tailored game: on ℂ^m, an observable U x i for each variable i at each question x, a signed permutation matrix and an involution, the observables at a question commuting; the observables of the readable variables are diagonal, and the observables at the two ends of an edge of positive weight commute.

• m : ℕ

  The dimension.

• m_pos : 0 < self.m
• U (x : X) : Fin (G.len x) → Matrix (Fin self.m) (Fin self.m) ℂ

  The observables.

• signedPerm (x : X) (i : Fin (G.len x)) : IsSignedPerm (self.U x i)
• invol (x : X) (i : Fin (G.len x)) : self.U x i * self.U x i = 1
• comm (x : X) (i j : Fin (G.len x)) : self.U x i * self.U x j = self.U x j * self.U x i
• zAligned (x : X) (i : Fin (G.len x)) : ↑i < G.lenR x → (self.U x i).IsDiag
• commEdges (x y : X) : 0 < G.μ x y → ∀ (i : Fin (G.len x)) (j : Fin (G.len y)), self.U x i * self.U y j = self.U y j * self.U x i

noncomputable def MIPRE.Tailored.PermStrategy.proj {X : Type u_1} [Fintype X] {G : TailoredGame X} (S : PermStrategy G) (x : X) (a : Fin (G.len x) → Bool) : Matrix (Fin S.m) (Fin S.m) ℂ

The measurement at x, the Fourier transform of the observables (II:974): P^x_a = ∏_i (1 + (-1)^{a_i} U(x, i)) / 2, for a ∈ F₂^{len x}.

Equations

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

noncomputable def MIPRE.Tailored.PermStrategy.value {X : Type u_1} [Fintype X] {G : TailoredGame X} (S : PermStrategy G) : ℝ

The value of a permutation strategy (II:1130): the players answer (x, y) with (a, b) with probability Tr(P^x_a P^y_b) / m.

Equations

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

def MIPRE.Tailored.TailoredGame.HasPerfectZPC {X : Type u_1} [Fintype X] (G : TailoredGame X) : Prop

The game has a perfect Z-aligned permutation strategy commuting along edges (II:1279).

Equations

• G.HasPerfectZPC = ∃ (S : MIPRE.Tailored.PermStrategy G), S.value = 1

The trivial strategy

theorem MIPRE.Tailored.half_smul_one_add_one {n : Type u_2} [Fintype n] [DecidableEq n] : (1 / 2) • (1 + 1 • 1) = 1

½(1 + 1) = 1, a factor of the measurement at the answer bit 0 of an observable equal to the identity.

theorem MIPRE.Tailored.half_smul_one_add_neg_one {n : Type u_2} [Fintype n] [DecidableEq n] : (1 / 2) • (1 + -1 • 1) = 0

½(1 - 1) = 0, the factor at the answer bit 1.

theorem MIPRE.Tailored.trace_one_mul_one_div {m : ℕ} (hm : 0 < m) : (1 * 1).trace.re / ↑m = 1

The normalized trace of the identity is 1.

noncomputable def MIPRE.Tailored.PermStrategy.trivial {X : Type u_1} [Fintype X] (G : TailoredGame X) : PermStrategy G

The trivial permutation strategy: one dimension, every observable the identity.

Equations

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

theorem MIPRE.Tailored.PermStrategy.trivial_proj {X : Type u_1} [Fintype X] (G : TailoredGame X) (x : X) (a : Fin (G.len x) → Bool) : (trivial G).proj x a = if a = fun (x : Fin (G.len x)) => false then 1 else 0

The trivial strategy answers 0 to every variable with certainty.

theorem MIPRE.Tailored.hasPerfectZPC_of_accepts_zero {X : Type u_1} [Fintype X] (G : TailoredGame X) (h : ∀ (x y : X), 0 < G.μ x y → G.Accepts x y (List.replicate (G.len x) false) (List.replicate (G.len y) false)) : G.HasPerfectZPC

A game that accepts the all-zero answers has a perfect ZPC strategy (II:1148, the deterministic strategies): the trivial strategy. This is the case of the halting protocol in which the machine has halted (II:1978, item 1), and it shows the definitions are not vacuous.