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

A tracially embeddable strategy on alphabets X, Y, A, B: a tracial standard-form algebra (M, τ), a positive density σ ∈ M₊ with τ(σ²) = 1, Alice POVMs in M (acting from the left), and Bob POVMs in M (acting from the right, i.e. already pulled back through the canonical anti-isomorphism of node 1.1.4). [03_tracial_reduction.tex; audit def tracially_embeddable]

• M : StdTracialAlgebra
• σ : self.M.A
• σ_pos : IsPosElem self.σ
• σ_normalized : self.M.τ (star self.σ * self.σ) = 1
• E : X → A → self.M.A
• F : Y → B → self.M.A
• E_pos (x : X) (a : A) : IsPosElem (self.E x a)
• F_pos (y : Y) (b : B) : IsPosElem (self.F y b)
• E_sum (x : X) : ∑ a : A, self.E x a = 1
• F_sum (y : Y) : ∑ b : B, self.F y b = 1

def CommutingRepetition.TracialStrategy.correlation {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (T : TracialStrategy X Y A B) (x : X) (y : Y) (a : A) (b : B) : ℝ

The tracial correlation q(a, b | x, y) = τ(σ* E_x^a σ F_y^b). [03_tracial_reduction.tex, eq tracial-correlation-formula]

Equations

• T.correlation x y a b = (T.M.τ (star T.σ * (T.E x a * T.σ * T.F y b))).re

theorem CommutingRepetition.TracialStrategy.correlation_nonneg {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (T : TracialStrategy X Y A B) (x : X) (y : Y) (a : A) (b : B) : 0 ≤ T.correlation x y a b

The tracial correlation is entrywise nonnegative — Born-rule positivity through the standard form (pairing_nonneg).

noncomputable def CommutingRepetition.TracialStrategy.toCommutingStrategy {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (T : TracialStrategy X Y A B) : CommutingStrategy X Y A B

Legality: every tracially embeddable strategy is a commuting-operator strategy — Alice through the left representation, Bob through the right, on the standard-form Hilbert space, with state ι σ. This is what closes the final contradiction against omegaCO. The obligations (positivity transport via L_isPositive/Rop_isPositive, unit norm, commutation) are discharged here. [03_tracial_reduction.tex, eq left-right-actions]

Equations

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

theorem CommutingRepetition.TracialStrategy.toCommutingStrategy_correlation {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (T : TracialStrategy X Y A B) : T.toCommutingStrategy.correlation = T.correlation

The commuting strategy induced by a tracial one realizes exactly the tracial correlation, via the evaluation identity inner_L_R.