def CommutingRepetition.Game.tagged {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (H : Game X Y A B) : Game (X ⊕ Y) (X ⊕ Y) (A ⊕ B) (A ⊕ B)

The tagged common-alphabet game of the strict tracial reduction (03_tracial_reduction.tex, eq tagged-alphabets and following): question law supported on (Alice-tag, Bob-tag) pairs where it equals μ, payoff the zero-extended tagged payoff — equal to V on correctly tagged question/answer pairs, zero otherwise. Its win is the manuscript's "continuous linear functional of the common-alphabet correlation table".

Equations

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

theorem CommutingRepetition.Game.abs_win_sub_win_le_l1Dist {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (p q : Correlation X Y A B) : |G.win p - G.win q| ≤ l1Dist p q

The winning functional is 1-Lipschitz for the unhalved ℓ¹ distance on correlation tables (03_tracial_reduction.tex: "Apply Theorem 3.1 closely enough that its value changes by less than ρ/2"; coefficients μ·V ∈ [0,1] entrywise).

theorem CommutingRepetition.Game.tagged_win_eq {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (H : Game X Y A B) (q : Correlation (X ⊕ Y) (X ⊕ Y) (A ⊕ B) (A ⊕ B)) : H.tagged.win q = ∑ x : X, ∑ y : Y, ∑ a : A, ∑ b : B, H.questionWeight x y * H.payoff x y a b * q (Sum.inl x) (Sum.inr y) (Sum.inl a) (Sum.inr b)

Unfolding computation for the tagged winning functional: only the (Alice-tag question, Bob-tag question, Alice-tag answer, Bob-tag answer) entries of a common-alphabet correlation carry weight (03_tracial_reduction.tex, eq tagged-alphabets: the tagged question law and payoff vanish off the correctly tagged block). Auxiliary lemma.

theorem CommutingRepetition.Game.tagged_symmetrization {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Nonempty A] [Nonempty B] (H : Game X Y A B) {p : Correlation X Y A B} (hp : IsCommutingCorrelation p) : ∃ (pt : Correlation (X ⊕ Y) (X ⊕ Y) (A ⊕ B) (A ⊕ B)), IsCommutingCorrelation pt ∧ H.tagged.win pt = H.win p

Tagged symmetrization (node 1.1.2; 03_tracial_reduction.tex, eq tagged-alphabets and following): every commuting correlation for the asymmetric game H induces a commuting correlation on the tagged common alphabets with the same tagged payoff — original measurements on own-tag questions, fixed outputs on wrong-tag questions, zero wrong-tag answer effects.

theorem CommutingRepetition.TraciallyEmbeddableCorrelation.exists_tracialStrategy {Xc Ac : Type} [Fintype Xc] [Fintype Ac] (q : TraciallyEmbeddableCorrelation Xc Ac) : ∃ (T : TracialStrategy Xc Xc Ac Ac), T.correlation = q.toCorrelation

Commutant pullback, consumed form (node 1.1.4; 03_tracial_reduction.tex, eqs left-right-actions, tracial-correlation-formula): every tracially embeddable correlation (Bob in the commutant of the left action) is realized by a TracialStrategy — Bob's effects pulled back through the canonical anti-isomorphism R to a POVM in the algebra, after passing to the generated von Neumann algebra in its standard form. This is the Stage-B tracial-Tomita obligation L(M)′ = R(M); it is proved, never assumed.

theorem CommutingRepetition.Game.detag {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Nonempty A] [Nonempty B] (H : Game X Y A B) (qt : TraciallyEmbeddableCorrelation (X ⊕ Y) (A ⊕ B)) : ∃ (T : TracialStrategy X Y A B), H.tagged.win qt.toCorrelation ≤ H.win T.correlation

Detagging (node 1.1.3; 03_tracial_reduction.tex, proof of prop strict-tracial-reduction): local deterministic postprocessing — wrong-tag outputs to a fixed valid answer, tags stripped — of a tracially embeddable common-alphabet correlation yields a tracial strategy for the original asymmetric game whose winning probability is at least the zero-extended tagged payoff (postprocessing is an ℓ¹ contraction that cannot decrease the nonnegative tagged payoff, and coarse-graining POVM effects preserves tracial embeddability). The output type deliberately folds the node-1.1.4 pullback into this statement — the 1.1.3/1.1.4 proof-obligation boundary differs from the audit tree's, with the composition unchanged.

theorem CommutingRepetition.strict_tracial_reduction {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] (H : Game X Y A B) {lam : ℝ} (hlam : lam < H.omegaCO) : ∃ (T : TracialStrategy X Y A B), lam < H.win T.correlation

Strict tracial reduction (node 1.1; 03_tracial_reduction.tex, prop strict-tracial-reduction): for every finite game H (possibly asymmetric alphabets) and every λ < ω^co(H), H has an exact tracially embeddable commuting strategy with winning probability strictly greater than λ. Applied downstream with H = G^{⊗n} and λ = e^{−γn} (node 1.5.2). No attainment of the supremum is assumed.