structure CommutingRepetition.PreroundedStrategy (X Y A B : Type) [Fintype X] [Fintype Y] [Fintype A] [Fintype B] : Type 1

The output package of tracial pre-rounding (05_prerounding.tex, prop tracial-prerounding): a finite standard-form algebra N; a finite shared history alphabet Hist (the manuscript's tuples (i, r)); the ideal posterior tuple law Q on Hist × X × Y; unit vectors u_{st} (indexed by the full label rectangle (Hist × X) × (Hist × Y)), x_s, y_t; full POVMs (A_s^a), (B_t^b) in N, Alice's used on the left and Bob's on the right; and one finite shared classical seed with its two local history samplers.

• N : StdTracialAlgebra
• Hist : Type
• histFintype : Fintype self.Hist
• histDecEq : DecidableEq self.Hist
• Q : self.Hist → X → Y → ℝ
• Q_nonneg (h : self.Hist) (x : X) (y : Y) : 0 ≤ self.Q h x y
• Q_sum : ∑ h : self.Hist, ∑ x : X, ∑ y : Y, self.Q h x y = 1
• u : self.Hist × X → self.Hist × Y → self.N.H
• xvec : self.Hist × X → self.N.H
• yvec : self.Hist × Y → self.N.H
• u_norm (s : self.Hist × X) (t : self.Hist × Y) : ‖self.u s t‖ = 1
• xvec_norm (s : self.Hist × X) : ‖self.xvec s‖ = 1
• yvec_norm (t : self.Hist × Y) : ‖self.yvec t‖ = 1
• A_ : self.Hist × X → A → self.N.A
• B_ : self.Hist × Y → B → self.N.A
• A_pos (s : self.Hist × X) (a : A) : IsPosElem (self.A_ s a)
• B_pos (t : self.Hist × Y) (b : B) : IsPosElem (self.B_ t b)
• A_sum (s : self.Hist × X) : ∑ a : A, self.A_ s a = 1
• B_sum (t : self.Hist × Y) : ∑ b : B, self.B_ t b = 1
• Seed : Type
• seedFintype : Fintype self.Seed
• ν : self.Seed → ℝ
• ν_nonneg (ω : self.Seed) : 0 ≤ self.ν ω
• ν_sum : ∑ ω : self.Seed, self.ν ω = 1
• rA : self.Seed → X → self.Hist
• rB : self.Seed → Y → self.Hist

noncomputable def CommutingRepetition.PreroundedStrategy.idealCorrelation {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : PreroundedStrategy X Y A B) : P.Hist × X → P.Hist × Y → A → B → ℝ

The ideal pair answer law q_{st}(a,b) = ⟪u_{st}, L(A_s^a) R(B_t^b) u_{st}⟫, defined on the full label rectangle.

Equations

• P.idealCorrelation = CommutingRepetition.tracialPairLaw P.N P.u P.A_ P.B_

def CommutingRepetition.PreroundedStrategy.labelLaw {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : PreroundedStrategy X Y A B) (s : P.Hist × X) (t : P.Hist × Y) : ℝ

The label law π on S × T: the pushforward of the ideal posterior tuple law under (h, x, y) ↦ ((h, x), (h, y)) — supported on matching histories. [05_prerounding.tex, label-law-pi]

Equations

• P.labelLaw s t = if s.1 = t.1 then P.Q s.1 s.2 t.2 else 0

noncomputable def CommutingRepetition.PreroundedStrategy.idealSuccess {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : PreroundedStrategy X Y A B) (G : Game X Y A B) : ℝ

The π-averaged ideal success E_π ∑_{a,b} V(a,b | x(s), y(t)) ⟪u_{st}, L(A_s^a) R(B_t^b) u_{st}⟫. [05_prerounding.tex, eq prerounding-ideal-success]

Equations

• P.idealSuccess G = ∑ h : P.Hist, ∑ x : X, ∑ y : Y, P.Q h x y * ∑ a : A, ∑ b : B, G.payoff x y a b * P.idealCorrelation (h, x) (h, y) a b

noncomputable def CommutingRepetition.PreroundedStrategy.alignment {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : PreroundedStrategy X Y A B) : ℝ

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

Equations

• P.alignment = ∑ h : P.Hist, ∑ x : X, ∑ y : Y, P.Q h x y * (‖P.u (h, x) (h, y) - P.xvec (h, x)‖ ^ 2 + ‖P.u (h, x) (h, y) - P.yvec (h, y)‖ ^ 2)

def CommutingRepetition.PreroundedStrategy.JA {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : PreroundedStrategy X Y A B) (G : Game X Y A B) (h : P.Hist) (x : X) (y : Y) : ℝ

The locally generated Alice tuple law J_A: the exact law of (r_A(ω, x), x, y) when ω ∼ ν and (x, y) ∼ μ. [05_prerounding.tex, eq prerounding-tv context; 07_main_theorem.tex, "The exact Alice tuple marginal in the actual classical experiment is J_A"]

Equations

• P.JA G h x y = (∑ ω : P.Seed, P.ν ω * if P.rA ω x = h then 1 else 0) * G.questionWeight x y

def CommutingRepetition.PreroundedStrategy.JB {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : PreroundedStrategy X Y A B) (G : Game X Y A B) (h : P.Hist) (x : X) (y : Y) : ℝ

The locally generated Bob tuple law J_B: the exact law of (r_B(ω, y), x, y).

Equations

• P.JB G h x y = (∑ ω : P.Seed, P.ν ω * if P.rB ω y = h then 1 else 0) * G.questionWeight x y

def CommutingRepetition.PreroundedStrategy.mismatchProb {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : PreroundedStrategy X Y A B) (G : Game X Y A B) : ℝ

The history mismatch probability Pr[r_A ≠ r_B] under ω ∼ ν, (x, y) ∼ μ. [05_prerounding.tex, eq prerounding-mismatch]

Equations

• P.mismatchProb G = ∑ ω : P.Seed, ∑ x : X, ∑ y : Y, P.ν ω * G.questionWeight x y * if P.rA ω x = P.rB ω y then 0 else 1

def CommutingRepetition.PreroundedStrategy.Qflat {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : PreroundedStrategy X Y A B) (t : P.Hist × X × Y) : ℝ

The tuple law Q flattened to the tuple type, for divergence and total-variation statements.

Equations

• P.Qflat t = P.Q t.1 t.2.1 t.2.2

def CommutingRepetition.PreroundedStrategy.JAflat {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : PreroundedStrategy X Y A B) (G : Game X Y A B) (t : P.Hist × X × Y) : ℝ

J_A flattened to the tuple type.

Equations

• P.JAflat G t = P.JA G t.1 t.2.1 t.2.2

def CommutingRepetition.PreroundedStrategy.JBflat {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : PreroundedStrategy X Y A B) (G : Game X Y A B) (t : P.Hist × X × Y) : ℝ

J_B flattened to the tuple type.

Equations

• P.JBflat G t = P.JB G t.1 t.2.1 t.2.2

theorem CommutingRepetition.PreroundedStrategy.sum_labelLaw_mul {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : PreroundedStrategy X Y A B) (f : P.Hist × X → P.Hist × Y → ℝ) : ∑ s : P.Hist × X, ∑ t : P.Hist × Y, P.labelLaw s t * f s t = ∑ h : P.Hist, ∑ x : X, ∑ y : Y, P.Q h x y * f (h, x) (h, y)

Master conversion: a π-average over the label rectangle collapses to a Q-average over tuples, since labelLaw is supported on matching histories.

theorem CommutingRepetition.PreroundedStrategy.labelLaw_nonneg {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : PreroundedStrategy X Y A B) (s : P.Hist × X) (t : P.Hist × Y) : 0 ≤ P.labelLaw s t

theorem CommutingRepetition.PreroundedStrategy.labelLaw_sum {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : PreroundedStrategy X Y A B) : ∑ s : P.Hist × X, ∑ t : P.Hist × Y, P.labelLaw s t = 1

The label law is a probability law on the rectangle.

theorem CommutingRepetition.PreroundedStrategy.alignment_nonneg {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : PreroundedStrategy X Y A B) : 0 ≤ P.alignment

theorem CommutingRepetition.PreroundedStrategy.piAlignment_labelLaw {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : PreroundedStrategy X Y A B) : piAlignment P.labelLaw P.u P.xvec P.yvec = P.alignment

The abstract π-alignment of the package's data is its alignment.

theorem CommutingRepetition.PreroundedStrategy.Qflat_nonneg {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : PreroundedStrategy X Y A B) (t : P.Hist × X × Y) : 0 ≤ P.Qflat t

theorem CommutingRepetition.PreroundedStrategy.Qflat_sum {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : PreroundedStrategy X Y A B) : ∑ t : P.Hist × X × Y, P.Qflat t = 1

theorem CommutingRepetition.PreroundedStrategy.sum_JAflat_mul {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : PreroundedStrategy X Y A B) (G : Game X Y A B) (f : P.Hist × X × Y → ℝ) : ∑ t : P.Hist × X × Y, P.JAflat G t * f t = ∑ ω : P.Seed, ∑ x : X, ∑ y : Y, P.ν ω * G.questionWeight x y * f (P.rA ω x, x, y)

Pushforward identity for the locally generated Alice law: a J_A-average over tuples is the seeded-experiment average (ω ∼ ν, (x,y) ∼ μ, tuple (r_A(ω,x), x, y)).

theorem CommutingRepetition.PreroundedStrategy.JAflat_nonneg {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : PreroundedStrategy X Y A B) (G : Game X Y A B) (t : P.Hist × X × Y) : 0 ≤ P.JAflat G t

theorem CommutingRepetition.PreroundedStrategy.JAflat_sum {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : PreroundedStrategy X Y A B) (G : Game X Y A B) : ∑ t : P.Hist × X × Y, P.JAflat G t = 1

theorem CommutingRepetition.weighted_tracial_prerounding {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] (G : Game X Y A B) (hQ : ∀ (x : X) (y : Y) (a : A) (b : B), ∃ (r : ℚ), G.payoff x y a b = ↑r) (n : ℕ) (hn : 1 ≤ n) (Trep : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {ε γ : ℝ} (hε0 : 0 < ε) (hε1 : ε ≤ 1) (hγ : γ ≤ ε / 8) (hθ : Real.exp (-(γ * ↑n)) < (G.repeat n).win Trep.correlation) : ∃ (P : PreroundedStrategy X Y A B) (η : ℝ), 0 ≤ η ∧ η ≤ 8 * γ * ((ε + Real.log (↑(Fintype.card A) * ↑(Fintype.card B))) / ε) ∧ 1 - ε / 4 ≤ P.idealSuccess G ∧ P.alignment ≤ 16 * η ∧ (∀ (t : P.Hist × X × Y), P.JAflat G t = 0 → P.Qflat t = 0) ∧ (∀ (t : P.Hist × X × Y), P.JBflat G t = 0 → P.Qflat t = 0) ∧ Pinsker.finiteRelativeEntropy P.Qflat (P.JAflat G) ≤ 3 * η ∧ Pinsker.finiteRelativeEntropy P.Qflat (P.JBflat G) ≤ 3 * η ∧ Pinsker.finiteTotalVariation P.Qflat (P.JAflat G) ≤ √(3 * η / 2) ∧ Pinsker.finiteTotalVariation P.Qflat (P.JBflat G) ≤ √(3 * η / 2) ∧ P.mismatchProb G ≤ 4 * √(3 * η / 2)

Weighted tracial pre-rounding (nodes 1.2 + 1.6.2; 05_prerounding.tex, prop tracial-prerounding, run as modified by 07_main_theorem.tex sec 7.4 for rational payoff tables): the referee declares acceptance per coordinate with a fresh finite private coin of bias V(aᵢ, bᵢ | xᵢ, yᵢ) — possible exactly because the payoffs are rational — and the coins are never revealed, so no effect, sampler, or label depends on them. The Section 5 machinery runs with the core indicator replaced by the weight w_D ∈ [0,1] (eq private-coin-core-weight), the accepted-word budget by the weighted entropy inequality w·H₁(a) ≤ H₁(w·a) plus log-sum (eq weighted-accepted-word-entropy), and the history budget by data processing from the private-coin space; the manuscript notes every constant is unchanged, so the conclusion is form-identical to the predicate case, of which this statement is the generalization (the predicate case is the specialization to {0,1}-valued — hence rational — payoffs). Conclusion shape as in tracial_prerounding below.

theorem CommutingRepetition.tracial_prerounding {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] (G : Game X Y A B) (hV : G.IsPredicate) (n : ℕ) (hn : 1 ≤ n) (Trep : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {ε γ : ℝ} (hε0 : 0 < ε) (hε1 : ε ≤ 1) (hγ : γ ≤ ε / 8) (hθ : Real.exp (-(γ * ↑n)) < (G.repeat n).win Trep.correlation) : ∃ (P : PreroundedStrategy X Y A B) (η : ℝ), 0 ≤ η ∧ η ≤ 8 * γ * ((ε + Real.log (↑(Fintype.card A) * ↑(Fintype.card B))) / ε) ∧ 1 - ε / 4 ≤ P.idealSuccess G ∧ P.alignment ≤ 16 * η ∧ (∀ (t : P.Hist × X × Y), P.JAflat G t = 0 → P.Qflat t = 0) ∧ (∀ (t : P.Hist × X × Y), P.JBflat G t = 0 → P.Qflat t = 0) ∧ Pinsker.finiteRelativeEntropy P.Qflat (P.JAflat G) ≤ 3 * η ∧ Pinsker.finiteRelativeEntropy P.Qflat (P.JBflat G) ≤ 3 * η ∧ Pinsker.finiteTotalVariation P.Qflat (P.JAflat G) ≤ √(3 * η / 2) ∧ Pinsker.finiteTotalVariation P.Qflat (P.JBflat G) ≤ √(3 * η / 2) ∧ P.mismatchProb G ≤ 4 * √(3 * η / 2)

Tracial pre-rounding (node 1.2; 05_prerounding.tex, prop tracial-prerounding). Standing assumption of Section 5: the payoff is a predicate. Given a tracially embeddable strategy for G^{⊗n} with success θ > e^{−γn}, 0 < ε ≤ 1, γ ≤ ε/8, and ℓ = log(|A||B|), there is a pre-rounded package and an η ≤ 8γ(ε + ℓ)/ε with: ideal success ≥ 1 − ε/4; alignment Δ ≤ 16η; D(Q‖J_A), D(Q‖J_B) ≤ 3η (with the absolute continuity finiteness implies); d_TV(Q, J_A), d_TV(Q, J_B) ≤ κ = √(3η/2); and sampler mismatch Pr[r_A ≠ r_B] ≤ 4κ. The samplers' marginals ARE J_A, J_B by definition of the package. Obtained from the weighted form above: a predicate payoff is 0 or 1, both rational.