noncomputable def CommutingRepetition.tracialPairLaw (N : StdTracialAlgebra) {S T A B : Type} (u : S → T → N.H) (E : S → A → N.A) (F : T → B → N.A) (s : S) (t : T) (a : A) (b : B) : ℝ

The pair answer law realized by tracial data: for labels s, t, vectors u s t, Alice effects E s a acting left and Bob effects F t b acting right, q_{st}(a,b) = ⟪u_{st}, L(E_s^a) R(F_t^b) u_{st}⟫. [06_otqcs.tex, display defining q_{st}; 05_prerounding.tex, eq prerounding-ideal-success]

Equations

• CommutingRepetition.tracialPairLaw N u E F s t a b = (inner ℂ (u s t) ((N.L (E s a)) ((N.Rop (F t b)) (u s t)))).re

theorem CommutingRepetition.tracialPairLaw_sum (N : StdTracialAlgebra) {S T A B : Type} [Fintype A] [Fintype B] (u : S → T → N.H) (E : S → A → N.A) (F : T → B → N.A) (hu : ∀ (s : S) (t : T), ‖u s t‖ = 1) (hE : ∀ (s : S), ∑ a : A, E s a = 1) (hF : ∀ (t : T), ∑ b : B, F t b = 1) (s : S) (t : T) : ∑ a : A, ∑ b : B, tracialPairLaw N u E F s t a b = 1

The pair law of full POVM families on a unit vector is a probability law over answers: ∑_{a,b} q_{st}(a,b) = 1 (completeness through L and the right action, as in CommutingStrategy.correlation_sum). The family-level hypotheses are for call-site convenience; per-label instances would suffice.

theorem CommutingRepetition.tracialPairLaw_nonneg (N : StdTracialAlgebra) {S T A B : Type} (u : S → T → N.H) (E : S → A → N.A) (F : T → B → N.A) (hE : ∀ (s : S) (a : A), IsPosElem (E s a)) (hF : ∀ (t : T) (b : B), IsPosElem (F t b)) (s : S) (t : T) (a : A) (b : B) : 0 ≤ tracialPairLaw N u E F s t a b

The pair law is pointwise nonnegative: the joint effect L(E) R(F) of commuting positive actions is a positive operator (Commute.mul_nonneg through the Loewner order, as in jointEffect_isPositive).

noncomputable def CommutingRepetition.piAlignment {S T : Type} [Fintype S] [Fintype T] {H : Type u_1} [NormedAddCommGroup H] (π : S → T → ℝ) (u : S → T → H) (xv : S → H) (yv : T → H) : ℝ

The π-averaged alignment defect Δ = E_π(‖u_{st} − x_s‖² + ‖u_{st} − y_t‖²). [06_otqcs.tex, display defining Δ; 05_prerounding.tex, eq prerounding-delta]

Equations

• CommutingRepetition.piAlignment π u xv yv = ∑ s : S, ∑ t : T, π s t * (‖u s t - xv s‖ ^ 2 + ‖u s t - yv t‖ ^ 2)

structure CommutingRepetition.SamplingResource (S T A B : Type) [Fintype A] [Fintype B] : Type 1

A question-independent sampling resource on label sets S, T and answer alphabets A, B: one standard-form algebra, ONE unit vector Ω (independence from the realized (s,t) is structural — there is a single state field), and full label-indexed POVMs, Alice's used on the left and Bob's on the right. [06_otqcs.tex, thm otqcs, items 1–3]

• N : StdTracialAlgebra
• Ω : self.N.H
• Ω_norm : ‖self.Ω‖ = 1
• E : S → A → self.N.A
• F : T → B → self.N.A
• E_pos (s : S) (a : A) : IsPosElem (self.E s a)
• F_pos (t : T) (b : B) : IsPosElem (self.F t b)
• E_sum (s : S) : ∑ a : A, self.E s a = 1
• F_sum (t : T) : ∑ b : B, self.F t b = 1

noncomputable def CommutingRepetition.SamplingResource.answerLaw {S T A B : Type} [Fintype A] [Fintype B] (R : SamplingResource S T A B) : S → T → A → B → ℝ

The resource's answer law q̂_{st}(a,b) = ⟪Ω, L(Â_s^a) R(B̂_t^b) Ω⟫. [06_otqcs.tex, display defining q̂_{st}]

Equations

• R.answerLaw = CommutingRepetition.tracialPairLaw R.N (fun (x : S) (x_1 : T) => R.Ω) R.E R.F