Part 1 — Games, direct repetition, commuting-operator strategies, ω^co

structure MainStatement.Game (X : Type u_1) (Y : Type u_2) (A : Type u_3) (B : Type u_4) [Fintype X] [Fintype Y] [Fintype A] [Fintype B] : Type (max (max (max u_1 u_2) u_3) u_4)

A finite two-player one-round game G = (X, Y, A, B, μ, V): finite nonempty question sets X, Y and answer sets A, B (nonemptiness is assumed at the theorems that need it), a probability distribution μ on X × Y given by questionWeight, and an acceptance function payoff = V(a, b | x, y) ∈ [0,1]. [02_preliminaries.tex, "Games and direct repetition"; audit def game]

• questionWeight : X → Y → ℝ
• weight_nonneg (x : X) (y : Y) : 0 ≤ self.questionWeight x y
• weight_normalized : ∑ x : X, ∑ y : Y, self.questionWeight x y = 1
• payoff : X → Y → A → B → ℝ
• payoff_nonneg (x : X) (y : Y) (a : A) (b : B) : 0 ≤ self.payoff x y a b
• payoff_le_one (x : X) (y : Y) (a : A) (b : B) : self.payoff x y a b ≤ 1

def MainStatement.Game.repeat {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) : Game (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)

Direct n-fold repetition G^{⊗n}: product question law on (Fin n → X) × (Fin n → Y) and product acceptance V^{⊗n}(a^n, b^n | x^n, y^n) = ∏ᵢ V(aᵢ, bᵢ | xᵢ, yᵢ). n = 0 is a total-function extension outside the paper's n ≥ 1 scope (empty products; the main theorem hypothesizes 1 ≤ n). [02_preliminaries.tex, eq for V^{⊗n}; audit def direct_repetition]

Equations

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

structure MainStatement.CommutingStrategy (X Y A B : Type) [Fintype X] [Fintype Y] [Fintype A] [Fintype B] : Type (u + 1)

A commuting-operator strategy over question alphabets X, Y and answer alphabets A, B: a complex Hilbert space H, a unit vector ψ, and POVM families E x (Alice) and F y (Bob) of positive continuous linear maps summing to 1, with every Alice effect commuting with every Bob effect. [02_preliminaries.tex; audit def commuting_strategy]

• H : Type u
• normedAddCommGroup : NormedAddCommGroup self.H
• innerProductSpace : InnerProductSpace ℂ self.H
• completeSpace : CompleteSpace self.H
• ψ : self.H
• ψ_norm : ‖self.ψ‖ = 1
• E : X → A → self.H →L[ℂ] self.H
• F : Y → B → self.H →L[ℂ] self.H
• E_pos (x : X) (a : A) : (self.E x a).IsPositive
• F_pos (y : Y) (b : B) : (self.F y b).IsPositive
• E_sum (x : X) : ∑ a : A, self.E x a = 1
• F_sum (y : Y) : ∑ b : B, self.F y b = 1
• commutes (x : X) (y : Y) (a : A) (b : B) : Commute (self.E x a) (self.F y b)

noncomputable def MainStatement.CommutingStrategy.correlation {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) (x : X) (y : Y) (a : A) (b : B) : ℝ

The correlation table of a strategy: p(a, b | x, y) = ⟪ψ, E_x^a F_y^b ψ⟫ (a real number; the inner product is real because the commuting product of self-adjoint effects is self-adjoint). [02_preliminaries.tex, success-probability display]

Equations

• S.correlation x y a b = (inner ℂ S.ψ ((S.E x a) ((S.F y b) S.ψ))).re

@[reducible, inline]

abbrev MainStatement.Correlation (X : Type u_1) (Y : Type u_2) (A : Type u_3) (B : Type u_4) : Type (max (max (max u_1 u_2) u_3) u_4)

A correlation table on alphabets X, Y, A, B.

Equations

• MainStatement.Correlation X Y A B = (X → Y → A → B → ℝ)

def MainStatement.IsCommutingCorrelation {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (p : Correlation X Y A B) : Prop

Realizability by a commuting-operator strategy at universe 0 (the Hilbert space is a Type; the restriction is disclosed in DIFFERENCES.md, D1, and is content-free for the finite alphabets in scope).

Equations

• MainStatement.IsCommutingCorrelation p = ∃ (S : MainStatement.CommutingStrategy X Y A B), S.correlation = p

def MainStatement.Game.win {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (p : Correlation X Y A B) : ℝ

Expected payoff of a correlation in the game G: win_G(p) = ∑ μ(x,y) V(a,b|x,y) p(a,b|x,y) — a linear functional of the correlation table.

Equations

• G.win p = ∑ x : X, ∑ y : Y, ∑ a : A, ∑ b : B, G.questionWeight x y * G.payoff x y a b * p x y a b

noncomputable def MainStatement.Game.omegaCO {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) : ℝ

The commuting-operator value ω^co(G): the supremum of winning probabilities over commuting-operator strategies. [02_preliminaries.tex, "The supremum of this expression is the commuting value"; non-attainment is never assumed anywhere downstream.]

Equations

• G.omegaCO = sSup (Set.range fun (S : MainStatement.CommutingStrategy X Y A B) => G.win S.correlation)

Part 2 — The tracial standard form and Lin's density theorem

def MainStatement.IsPosElem {A : Type u_1} [AddCommMonoid A] [Mul A] [Star A] (a : A) : Prop

Algebraic positivity: a is a finite sum of hermitian squares ∑ᵢ cᵢ* cᵢ — the algebraic positive cone of a ∗-ring. In a C*-algebra this coincides with the usual positive cone. [DIFFERENCES.md D13]

Equations

• MainStatement.IsPosElem a = ∃ (k : ℕ) (c : Fin k → A), a = ∑ i : Fin k, star (c i) * c i

structure MainStatement.StdTracialAlgebra : Type (u + 1)

Standard form of a tracial ∗-algebra: carrier A with a normalized trace τ, the GNS Hilbert space H = L²(A, τ) with dense embedding ι, commuting left and right actions L, R, and the evaluation identities. [02_preliminaries.tex, "Finite tracial standard form"]

• A : Type u
• ringA : Ring self.A
• starRingA : StarRing self.A
• algebraA : Algebra ℂ self.A
• starModuleA : StarModule ℂ self.A
• τ : self.A →ₗ[ℂ] ℂ
• τ_one : self.τ 1 = 1
• τ_mul_comm (a b : self.A) : self.τ (a * b) = self.τ (b * a)
• τ_star (a : self.A) : self.τ (star a) = star (self.τ a)
• H : Type u
• nacgH : NormedAddCommGroup self.H
• ipsH : InnerProductSpace ℂ self.H
• completeH : CompleteSpace self.H
• ι : self.A →ₗ[ℂ] self.H
• ι_dense : DenseRange ⇑self.ι
• ι_inner (a b : self.A) : inner ℂ (self.ι a) (self.ι b) = self.τ (star a * b)
• L : self.A →⋆ₐ[ℂ] self.H →L[ℂ] self.H
• R : self.Aᵐᵒᵖ →⋆ₐ[ℂ] self.H →L[ℂ] self.H
• L_apply (a b : self.A) : (self.L a) (self.ι b) = self.ι (a * b)
• R_apply (a b : self.A) : (self.R (MulOpposite.op a)) (self.ι b) = self.ι (b * a)
• LR_commute (a b : self.A) : Commute (self.L a) (self.R (MulOpposite.op b))

def MainStatement.l1Dist {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (p q : Correlation X Y A B) : ℝ

ℓ¹ distance between two correlation tables on common finite alphabets.

Equations

• MainStatement.l1Dist p q = ∑ x : X, ∑ y : Y, ∑ a : A, ∑ b : B, |p x y a b - q x y a b|

structure MainStatement.TraciallyEmbeddableCorrelation (Xc Ac : Type) [Fintype Xc] [Fintype Ac] : Type 1

A tracially embeddable correlation on common alphabets, in the exact shape of Lin's Definition 3.1: standard form of a tracial algebra, density σ ∈ M₊ with τ(σ²) = 1, Alice POVMs in M acting on the left, Bob POVMs given by positive operators in the COMMUTANT of the left action.

• M : StdTracialAlgebra
• σ : self.M.A
• σ_pos : IsPosElem self.σ
• σ_normalized : self.M.τ (star self.σ * self.σ) = 1
• E : Xc → Ac → self.M.A
• E_pos (x : Xc) (a : Ac) : IsPosElem (self.E x a)
• E_sum (x : Xc) : ∑ a : Ac, self.E x a = 1
• G : Xc → Ac → self.M.H →L[ℂ] self.M.H
• G_pos (y : Xc) (b : Ac) : (self.G y b).IsPositive
• G_sum (y : Xc) : ∑ b : Ac, self.G y b = 1
• G_commutant (y : Xc) (b : Ac) (m : self.M.A) : Commute (self.G y b) (self.M.L m)

noncomputable def MainStatement.TraciallyEmbeddableCorrelation.toCorrelation {Xc Ac : Type} [Fintype Xc] [Fintype Ac] (q : TraciallyEmbeddableCorrelation Xc Ac) : Correlation Xc Xc Ac Ac

The correlation table realized by a tracially embeddable strategy in commutant form: p(a, b | x, y) = ⟪ι σ, L(E_x^a) G_y^b (ι σ)⟫.

Equations

• q.toCorrelation x y a b = (inner ℂ (q.M.ι q.σ) ((q.M.L (q.E x a)) ((q.G y b) (q.M.ι q.σ)))).re

def MainStatement.TracialDensityHypothesis : Prop

Lin's tracial density theorem (arXiv:2304.01940, Thm 3.2): for all finite common alphabets, every commuting-operator correlation is an ℓ¹-limit of tracially embeddable correlations. The name says "hypothesis" for historical reasons — it was the manuscript's one external input, and the name is load-bearing for scripts/statement_copy_check.py and the fidelity ledger — but the development proves it: MainStatement.tracialDensity in StatementBridge.lean, transferred from CommutingRepetition.Density.tracialDensity. The main theorem therefore takes no hypothesis.

Equations

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

Part 3 — The statement

def MainStatement.UniformParallelRepetition : Prop

Uniform direct parallel repetition for commuting-operator strategies (07_main_theorem.tex, Theorem 7.1), as a proposition: there is a universal c > 0 such that for every finite game G with payoffs in [0,1] and every n ≥ 1, ω^co(G^{⊗n}) ≤ exp(−c·n·ε⁷/(ε + log(|A||B|))) where ε = 1 − ω^co(G) (when ε = log(|A||B|) = 0 the quotient is 0/0 = 0 in Lean, the manuscript's convention). Unconditional: Lin's density theorem (TracialDensityHypothesis above) is itself proved by the development, as MainStatement.tracialDensity. Proved in StatementBridge.lean.

Equations

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