structure CommutingRepetition.ResolverArena (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] (F : I → A → M.A) (G : J → B → M.A) : Type 1

The resolver arena, consumed form (node 1.2.5; 04_resolver_corner.tex, thm common-resolver-arena): a finite tracial standard-form algebra N, POVMs 𝖠_i (Alice) and 𝖡_j (Bob) in N, and for every density σ ∈ M and index pair (i, j) a branch vector Φ_{ij} ∈ L²(N) reproducing the exact pairings of the input effect families: ‖Φ_{ij}‖² = τ(σ* F_i σ G_j) (eq joint-branch-norm) and ⟪Φ_{ij}, L(𝖠_i^a) R(𝖡_j^b) Φ_{ij}⟫ = τ(σ* F_i^a σ G_j^b) (eq joint-branch-answer-weight), with the totals F_i = ∑_a F_i^a, G_j = ∑_b G_j^b (eq effect-refinements).

• N : StdTracialAlgebra
• Ameas : I → A → self.N.A
• Bmeas : J → B → self.N.A
• Ameas_pos (i : I) (a : A) : IsPosElem (self.Ameas i a)
• Bmeas_pos (j : J) (b : B) : IsPosElem (self.Bmeas j b)
• Ameas_sum (i : I) : ∑ a : A, self.Ameas i a = 1
• Bmeas_sum (j : J) : ∑ b : B, self.Bmeas j b = 1
• branch : M.A → I → J → self.N.H
• branch_norm (σ : M.A) (i : I) (j : J) : inner ℂ (self.branch σ i j) (self.branch σ i j) = M.τ (star σ * ((∑ a : A, F i a) * σ * ∑ b : B, G j b))
• branch_answer (σ : M.A) (i : I) (j : J) (a : A) (b : B) : inner ℂ (self.branch σ i j) ((self.N.L (self.Ameas i a)) ((self.N.Rop (self.Bmeas j b)) (self.branch σ i j))) = M.τ (star σ * (F i a * σ * G j b))