theorem CommutingRepetition.resolver_arena (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [Nonempty A] [Nonempty B] (F : I → A → M.A) (G : J → B → M.A) (hF : ∀ (i : I) (a : A), IsPosElem (F i a)) (hG : ∀ (j : J) (b : B), IsPosElem (G j b)) (hF1 : ∀ (i : I), IsPosElem (1 - ∑ a : A, F i a)) (hG1 : ∀ (j : J), IsPosElem (1 - ∑ b : B, G j b)) : Nonempty (ResolverArena M F G)

Common finite-trace resolver arena (node 1.2.5; 04_resolver_corner.tex, thm common-resolver-arena, consumed form): every pair of finite refined [0,1]-effect families over nonempty answer sets (the manuscript's fallback answers a₀ ∈ A, b₀ ∈ B; without them a POVM over an empty outcome set would be demanded — review #10, R1) admits a resolver arena. The construction — semifinite linking algebra, columns and rows via the resolver integral, polar data, the finite corner, and the normalization unitary — is nodes 1.2.5.1–1.2.5.6 (Stage B).