Proof of Couplings of Noncommutative Laws: the Norm Bound, the Cost Identity, the Tensor, Diagonal and Swapped Couplings, Weak-Star Closedness, and Displacement Interpolants

Items used. Definitions: The Algebra of Noncommutative Polynomials in Finitely Many Self-Adjoint Variables §polynomials, The Algebra of Noncommutative Polynomials in Finitely Many Self-Adjoint Variables §linear, The Algebra of Noncommutative Polynomials in Finitely Many Self-Adjoint Variables §monomials, Substitution of Noncommutative Polynomials into the Variables §word-products, Substitution of Noncommutative Polynomials into the Variables §substitution, Noncommutative Laws of Finitely Many Self-Adjoint Variables with a Norm Bound §tracial-state, Noncommutative Laws of Finitely Many Self-Adjoint Variables with a Norm Bound §norm-bound, Noncommutative Laws of Finitely Many Self-Adjoint Variables with a Norm Bound §law, Weak-Star Convergence of Noncommutative Laws §weak-star, Couplings of Two Noncommutative Laws and Their Quadratic Cost §marginals, Couplings of Two Noncommutative Laws and Their Quadratic Cost §coupling, Couplings of Two Noncommutative Laws and Their Quadratic Cost §cost, Positive Semidefinite Kernel on a Finite Set §kernel, Sum over a Finite Index Set, The Complex Numbers, Real and Imaginary Parts of a Complex Number, Subsequence of a Sequence in a Set. Results: Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts §vector-space, Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts §linear-extension, Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts §monomials, Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts §algebra, Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts §adjoint, Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts §self-adjoint; Substitution is the Unique Unital Homomorphism with Prescribed Values on the Variables: Monomials, Products, Adjoints and Composition §values, Substitution is the Unique Unital Homomorphism with Prescribed Values on the Variables: Monomials, Products, Adjoints and Composition §homomorphism, Substitution is the Unique Unital Homomorphism with Prescribed Values on the Variables: Monomials, Products, Adjoints and Composition §adjoint, Substitution is the Unique Unital Homomorphism with Prescribed Values on the Variables: Monomials, Products, Adjoints and Composition §composition, Substitution is the Unique Unital Homomorphism with Prescribed Values on the Variables: Monomials, Products, Adjoints and Composition §identity; Basic Properties of Noncommutative Laws: Adjoints, the Self-Adjoint Pairing, Cauchy-Schwarz, Monotonicity in the Bound, and Laws of Constant Tuples §adjoint, Basic Properties of Noncommutative Laws: Adjoints, the Self-Adjoint Pairing, Cauchy-Schwarz, Monotonicity in the Bound, and Laws of Constant Tuples §pairing; The Norm Bound of a Noncommutative Law: Multiplication by a Variable is Bounded, the Bound is Detected by Even Moments, and Laws Pull Back under Self-Adjoint Substitutions §criterion, The Norm Bound of a Noncommutative Law: Multiplication by a Variable is Bounded, the Bound is Detected by Even Moments, and Laws Pull Back under Self-Adjoint Substitutions §affine; Sequential Weak-Star Compactness of the Noncommutative Laws with a Given Norm Bound §unique, Sequential Weak-Star Compactness of the Noncommutative Laws with a Given Norm Bound §compact; Positive Semidefinite Kernels on a Finite Set: Rank-One Decomposition and the Schur Product §schur; Sums over Finite Index Sets: Finite Unions, Disjoint Unions, Vanishing Terms, Dependent Pairs, Conjugation and the Modulus §vanishing, Sums over Finite Index Sets: Finite Unions, Disjoint Unions, Vanishing Terms, Dependent Pairs, Conjugation and the Modulus §conjugate, Sums over Finite Index Sets: Finite Unions, Disjoint Unions, Vanishing Terms, Dependent Pairs, Conjugation and the Modulus §pairs; claims 1, 2, 3, 5 and 7 of Properties of Finite Sums; claims 2, 3, 4 and 7 of Properties of Finite Sums of Vectors; claims 2 and 3 of Basic Properties of Finite Sets; claim 5 of Basic Properties of Initial Segments of the Natural Numbers; claim 1 of Zero Products and Elementary Identities in a Field; claims 1 and 8 of Properties of Complex Conjugation and Modulus; claims 2 and 3 of Elementary Arithmetic in an Ordered Field; claim 1 of Uniqueness of Limits and Boundedness of Convergent Real Sequences.

Throughout, $x_{j}$ denotes the $j$-th variable of whichever $\mathcal{P}_{n}$ is indicated, $q^{2}=qq$, and for $j\in[d]$ we put $q_{j}=x_{j}-x_{d+j}$ and $r_{j}=x_{j}+x_{d+j}$ in $\mathcal{P}_{2d}$, so that $\Delta_{d}=\sum_{j=1}^{d}q_{j}^{2}$ by Couplings of Two Noncommutative Laws and Their Quadratic Cost §cost. Since $2d=d+d$, claim 5 of Basic Properties of Initial Segments of the Natural Numbers shows that every element of $[2d]$ is either some $j\in[d]$ or $d+k$ for exactly one $k\in[d]$, and $j\neq d+k$ for $j,k\in[d]$.

Step 0 (general facts). (F1) Polynomials are maps $W_{n}\to\mathbb{C}$ and the linear operations are pointwise (The Algebra of Noncommutative Polynomials in Finitely Many Self-Adjoint Variables §linear); hence an identity between linear combinations of polynomials (with no products) holds as soon as the corresponding identity of complex numbers holds at every word. In particular $0q=0$ for every $q\in\mathcal{P}_{n}$, since $0\,q(w)=0$ by claim 1 of Zero Products and Elementary Identities in a Field; and then, writing the zero polynomial as the scalar multiple $c\,0$ with the scalar $c=0\in\mathbb{C}$ (coefficientwise, $0\cdot0=0$ in $\mathbb{C}$), $q0=q(c\,0)=c\,(q0)=0$ by Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts §algebra, the last equality because every coefficient of $c\,(q0)$ is $0$ times a complex number.

(F2) By Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts §self-adjoint, $\mathcal{P}_{n,\mathrm{sa}}$ contains $1$ and every variable and is closed under sums and real multiples. Hence $q_{j}=x_{j}+(-1)x_{d+j}$, $r_{j}$, and $a^{t}_{j}=(1-t)x_{j}+t\,x_{d+j}$ (for real $t$) are self-adjoint, and every tuple substituted in this lemma ($\iota^{1},\iota^{2},\sigma^{1},\sigma^{2},\delta,s,\sigma_{a^{t}}$ and the two tuples of claim 7) consists of self-adjoint polynomials.

(F3) Let $a$ be an $n$-tuple in $\mathcal{P}_{m,\mathrm{sa}}$ and $\lambda$ a tracial state on $\mathcal{P}_{m}$. Then $\lambda\circ\sigma_{a}$ is a tracial state on $\mathcal{P}_{n}$. Indeed it is linear as a composite of linear maps (Substitution of Noncommutative Polynomials into the Variables §substitution); $\lambda(\sigma_{a}(1))=\lambda(1)=1$ by Substitution is the Unique Unital Homomorphism with Prescribed Values on the Variables: Monomials, Products, Adjoints and Composition §values; for $p,q\in\mathcal{P}_{n}$, $\sigma_{a}(p^{*}p)=\sigma_{a}(p)^{*}\sigma_{a}(p)$ by Substitution is the Unique Unital Homomorphism with Prescribed Values on the Variables: Monomials, Products, Adjoints and Composition §homomorphism and Substitution is the Unique Unital Homomorphism with Prescribed Values on the Variables: Monomials, Products, Adjoints and Composition §adjoint, so $\lambda(\sigma_{a}(p^{*}p))$ is real and nonnegative by (b) of Noncommutative Laws of Finitely Many Self-Adjoint Variables with a Norm Bound §tracial-state; and $\lambda(\sigma_{a}(pq))=\lambda(\sigma_{a}(p)\sigma_{a}(q))=\lambda(\sigma_{a}(q)\sigma_{a}(p))=\lambda(\sigma_{a}(qp))$ by the homomorphism clause and (c).

(F4) If $\sigma_{a}:\mathcal{P}_{n}\to\mathcal{P}_{m}$ and $\sigma_{b}:\mathcal{P}_{m}\to\mathcal{P}_{l}$ are substitutions, then $\sigma_{b}\circ\sigma_{a}=\sigma_{c}$ with $c_{j}=\sigma_{b}(a_{j})$, by Substitution is the Unique Unital Homomorphism with Prescribed Values on the Variables: Monomials, Products, Adjoints and Composition §composition; when $a_{j}=x_{k}$ we have $c_{j}=b_{k}$ by Substitution is the Unique Unital Homomorphism with Prescribed Values on the Variables: Monomials, Products, Adjoints and Composition §values. If $c=(x_{1},\dots,x_{n})$, then $\sigma_{c}$ is the identity by Substitution is the Unique Unital Homomorphism with Prescribed Values on the Variables: Monomials, Products, Adjoints and Composition §identity.

(F5) Let $a$ be an $n$-tuple in $\mathcal{P}_{m}$ and $w\in W_{n}$. If every $a_{j}$ is a monomial, then $\sigma_{a}(x_{w})=a_{w}$ is a monomial; if every $a_{j}$ equals $1$, then $\sigma_{a}(x_{w})=1$. Indeed $\sigma_{a}(x_{w})=a_{w}$ by Substitution is the Unique Unital Homomorphism with Prescribed Values on the Variables: Monomials, Products, Adjoints and Composition §values; $a_{\varnothing}=1=x_{\varnothing}$, and for $w$ of length $k$, $a_{w}=\pi(k)$ with $\pi(1)=a_{w_{1}}$ and $\pi(i+1)=\pi(i)a_{w_{i+1}}$ (Substitution of Noncommutative Polynomials into the Variables §word-products). By induction on $i\in[k]$: if $\pi(i)=x_{u}$ and $a_{w_{i+1}}=x_{v}$, then $\pi(i+1)=x_{uv}$; if $\pi(i)=1=a_{w_{i+1}}$, then $\pi(i+1)=1\cdot1=1$ (both by Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts §monomials).

(F6) For $y\in\mathcal{P}_{m}$ and $k\in\mathbb{N}$, $y^{k}$ is, as in The Norm Bound of a Noncommutative Law: Multiplication by a Variable is Bounded, the Bound is Detected by Even Moments, and Laws Pull Back under Self-Adjoint Substitutions, the product along the word $e_{k}\in W_{1}$ of length $k$ all of whose letters are $1$, for the $1$-tuple $(y)$; so $y^{k}=\sigma_{(y)}(x_{e_{k}})$ by Substitution is the Unique Unital Homomorphism with Prescribed Values on the Variables: Monomials, Products, Adjoints and Composition §values. For every substitution $\sigma_{b}:\mathcal{P}_{m}\to\mathcal{P}_{l}$, (F4) and the values clause give $\sigma_{b}(y^{k})=\sigma_{(\sigma_{b}(y))}(x_{e_{k}})=\sigma_{b}(y)^{k}$.

(F7) Two linear maps $\mathcal{P}_{n}\to\mathbb{C}$ agreeing on every monomial are equal, by the uniqueness in (a) of Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts §linear-extension.

(F8) Let $\ell:\mathcal{P}_{n}\to\mathbb{C}$ be linear, $p\in\mathcal{P}_{n}$, and $F$ a nonempty finite subset of $W_{n}$ with $\operatorname{supp}p\subseteq F$. Then (i) $\ell(p)=\sum_{w\in F}p(w)\,\ell(x_{w})$, and (ii) $\ell(p^{*}p)=\sum_{(u,v)\in F\times F}\overline{p(u)}\,p(v)\,\ell(x_{u}^{*}x_{v})$. For (i): $\ell$ is the unique linear map with $\ell(x_{w})=c(w):=\ell(x_{w})$, so the formula of (a) of Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts §linear-extension applies. If $p=0$, then $\ell(p)=0$ and every term $p(w)\ell(x_{w})=0$ (claim 1 of Zero Products and Elementary Identities in a Field), so the sum over $F$ is $0$ by Sums over Finite Index Sets: Finite Unions, Disjoint Unions, Vanishing Terms, Dependent Pairs, Conjugation and the Modulus §vanishing. If $p\neq0$, then $\ell(p)=\sum_{w\in\operatorname{supp}p}p(w)\ell(x_{w})$ with $\operatorname{supp}p$ nonempty, and the terms with $w\in F\setminus\operatorname{supp}p$ vanish, so this equals the sum over $F$ by the same clause. For (ii): for fixed $u$, $q\mapsto\ell(x_{u}^{*}q)$ is linear by Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts §algebra, so (i) gives $\ell(x_{u}^{*}p)=\sum_{v\in F}p(v)\,\ell(x_{u}^{*}x_{v})$. The map $r\mapsto\overline{\ell(r^{*}p)}$ is linear: $(r+r')^{*}p=r^{*}p+r'^{*}p$ and $(cr)^{*}p=\overline{c}\,(r^{*}p)$ by Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts §adjoint and Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts §algebra, and conjugation is additive, multiplicative and involutive (claim 1 of Properties of Complex Conjugation and Modulus). So (i) gives $\overline{\ell(p^{*}p)}=\sum_{u\in F}p(u)\overline{\ell(x_{u}^{*}p)}$; conjugating with Sums over Finite Index Sets: Finite Unions, Disjoint Unions, Vanishing Terms, Dependent Pairs, Conjugation and the Modulus §conjugate and claim 1 of Properties of Complex Conjugation and Modulus,

the constant being moved inside by Sum over a Finite Index Set and claim 3 of Properties of Finite Sums; the iterated sum is the sum over $F\times F$ by Sums over Finite Index Sets: Finite Unions, Disjoint Unions, Vanishing Terms, Dependent Pairs, Conjugation and the Modulus §pairs with $B(u)=F$.

(F9) A finite sum in $\mathbb{C}$ of real numbers is real and equals their finite sum in $\mathbb{R}$, by induction along the recursion of claim 1 of Properties of Finite Sums and condition 1 of The Complex Numbers. By Real and Imaginary Parts of a Complex Number, every $z\in\mathbb{C}$ equals $\operatorname{Re}z+(\operatorname{Im}z)i$, and $\operatorname{Re}z=z$ when $z$ is real (as $z=z+0i$).

Step 1 (claim 1). Let $\mu,\nu\in\Sigma_{d,R}$ and $\gamma\in\Pi(\mu,\nu)$; $\gamma$ is a tracial state on $\mathcal{P}_{2d}$ (Couplings of Two Noncommutative Laws and Their Quadratic Cost §coupling). Let $m\in\mathbb{N}$. For $j\in[d]$, $\iota^{1}(x_{j})=x_{j}$ by Substitution is the Unique Unital Homomorphism with Prescribed Values on the Variables: Monomials, Products, Adjoints and Composition §values, so by (F6) $\iota^{1}(x_{j}^{2m})=x_{j}^{2m}$ and $\gamma(x_{j}^{2m})=(\gamma\circ\iota^{1})(x_{j}^{2m})=\mu(x_{j}^{2m})\le R^{2m}$ by the only-if direction of The Norm Bound of a Noncommutative Law: Multiplication by a Variable is Bounded, the Bound is Detected by Even Moments, and Laws Pull Back under Self-Adjoint Substitutions §criterion for $\mu$. For $k\in[d]$, $\iota^{2}(x_{k})=x_{d+k}$, so likewise $\gamma(x_{d+k}^{2m})=\nu(x_{k}^{2m})\le R^{2m}$. As every element of $[2d]$ is of one of these forms, the if direction of the same clause gives $\gamma\in\Sigma_{2d,R}$.

Step 2 (claim 2). For $j\in[d]$, $x_{j}^{*}=x_{j}$ (Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts §adjoint), so $\mu(x_{j}^{2})=\mu(x_{j}^{*}x_{j})$ is real and nonnegative by (b) of Noncommutative Laws of Finitely Many Self-Adjoint Variables with a Norm Bound §tracial-state; by (F9) and claim 5 of Properties of Finite Sums, $M(\mu)$ is real and nonnegative, and likewise $M(\nu)$. Let $\gamma\in\Pi(\mu,\nu)$ and $j\in[d]$. By Basic Properties of Noncommutative Laws: Adjoints, the Self-Adjoint Pairing, Cauchy-Schwarz, Monotonicity in the Bound, and Laws of Constant Tuples §pairing with $a=x_{j}$, $b=x_{d+j}$, the number $g_{j}=\gamma(x_{j}x_{d+j})$ is real, and $\gamma(x_{d+j}x_{j})=g_{j}$ by (c). By Substitution is the Unique Unital Homomorphism with Prescribed Values on the Variables: Monomials, Products, Adjoints and Composition §homomorphism and Substitution is the Unique Unital Homomorphism with Prescribed Values on the Variables: Monomials, Products, Adjoints and Composition §values, $\iota^{1}(x_{j}x_{j})=x_{j}x_{j}$ and $\iota^{2}(x_{j}x_{j})=x_{d+j}x_{d+j}$, so $\gamma(x_{j}^{2})=\mu(x_{j}^{2})$ and $\gamma(x_{d+j}^{2})=\nu(x_{j}^{2})$. By Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts §algebra and (F1), $q_{j}^{2}=x_{j}^{2}-x_{j}x_{d+j}-x_{d+j}x_{j}+x_{d+j}^{2}$ and $r_{j}^{2}=x_{j}^{2}+x_{j}x_{d+j}+x_{d+j}x_{j}+x_{d+j}^{2}$, so by linearity

By claim 4 of Properties of Finite Sums of Vectors, $I(\gamma)=\gamma(\Delta_{d})=\sum_{j=1}^{d}\gamma(q_{j}^{2})$, and claims 2 and 3 of Properties of Finite Sums give the stated identity. Since $q_{j}$ and $r_{j}$ are self-adjoint (F2), $\gamma(q_{j}^{2})=\gamma(q_{j}^{*}q_{j})$ and $\gamma(r_{j}^{2})=\gamma(r_{j}^{*}r_{j})$ are real and nonnegative; so $I(\gamma)\ge0$ by (F9) and claim 5 of Properties of Finite Sums. Moreover $2\mu(x_{j}^{2})+2\nu(x_{j}^{2})-\gamma(q_{j}^{2})=\gamma(r_{j}^{2})\ge0$, so, summing with claims 2, 3 and 5 of Properties of Finite Sums, $2M(\mu)+2M(\nu)-I(\gamma)\ge0$, i.e. $I(\gamma)\le2M(\mu)+2M(\nu)$ by claim 3 of Elementary Arithmetic in an Ordered Field.

Step 3 (claim 3). Existence and uniqueness of $\tau=\mu\otimes\nu$ is (a) of Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts §linear-extension with $c(w)=\mu(\sigma^{1}(x_{w}))\nu(\sigma^{2}(x_{w}))$. By (F2), $\sigma^{1},\sigma^{2}$ substitute self-adjoint tuples, so they are multiplicative, unital and commute with adjoints (Substitution is the Unique Unital Homomorphism with Prescribed Values on the Variables: Monomials, Products, Adjoints and Composition §values, Substitution is the Unique Unital Homomorphism with Prescribed Values on the Variables: Monomials, Products, Adjoints and Composition §homomorphism, Substitution is the Unique Unital Homomorphism with Prescribed Values on the Variables: Monomials, Products, Adjoints and Composition §adjoint). For $u,v\in W_{2d}$, $x_{u}x_{v}=x_{uv}$ and $x_{u}^{*}x_{v}=x_{u^{\mathrm{rev}}}x_{v}=x_{u^{\mathrm{rev}}v}$ are monomials (Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts §monomials, Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts §adjoint), hence

where $K(u,v)=\mu(\sigma^{1}(x_{u})^{*}\sigma^{1}(x_{v}))$ and $L(u,v)=\nu(\sigma^{2}(x_{u})^{*}\sigma^{2}(x_{v}))$.

(a) $\tau(1)=\tau(x_{\varnothing})=\mu(1)\nu(1)=1$.

(b) Let $p\in\mathcal{P}_{2d}$ and let $F=\operatorname{supp}p$ if $p\neq0$ and $F=\{\varnothing\}$ if $p=0$; $F$ is nonempty and finite (The Algebra of Noncommutative Polynomials in Finitely Many Self-Adjoint Variables §polynomials, claim 2 of Basic Properties of Finite Sets) and contains $\operatorname{supp}p$. We show $K$ (restricted to $F\times F$) is a positive semidefinite kernel on $F$ (Positive Semidefinite Kernel on a Finite Set §kernel). By Basic Properties of Noncommutative Laws: Adjoints, the Self-Adjoint Pairing, Cauchy-Schwarz, Monotonicity in the Bound, and Laws of Constant Tuples §adjoint, $K(v,u)=\mu(\sigma^{1}(x_{v})^{*}\sigma^{1}(x_{u}))=\overline{K(u,v)}$. Given $z:F\to\mathbb{C}$, let $s:W_{2d}\to\mathbb{C}$ be $z$ on $F$ and $0$ elsewhere; $\operatorname{supp}s\subseteq F$ is finite (claim 3 of Basic Properties of Finite Sets), so $s\in\mathcal{P}_{2d}$. By (F8)(ii) for the linear map $\mu\circ\sigma^{1}$, and $\sigma^{1}(x_{u}^{*}x_{v})=\sigma^{1}(x_{u})^{*}\sigma^{1}(x_{v})$,

which is real and nonnegative by (b) of Noncommutative Laws of Finitely Many Self-Adjoint Variables with a Norm Bound §tracial-state. The same argument with $\nu,\sigma^{2}$ shows $L$ is a positive semidefinite kernel on $F$, so $KL$ is one by Positive Semidefinite Kernels on a Finite Set: Rank-One Decomposition and the Schur Product §schur. With $z(u)=p(u)$ $(u\in F)$, (F8)(ii) for $\tau$ gives $\tau(p^{*}p)=\sum_{(u,v)\in F\times F}\overline{z(u)}z(v)K(u,v)L(u,v)=Q_{KL}(z)$, real and nonnegative.

(c) For $u,v\in W_{2d}$, (c) of Noncommutative Laws of Finitely Many Self-Adjoint Variables with a Norm Bound §tracial-state for $\mu$ and $\nu$ and the displayed formula give $\tau(x_{u}x_{v})=\tau(x_{v}x_{u})$. For fixed $u$, $q\mapsto\tau(x_{u}q)$ and $q\mapsto\tau(qx_{u})$ are linear (Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts §algebra) and agree on monomials, so they are equal by (F7); then for fixed $q$, $p\mapsto\tau(pq)$ and $p\mapsto\tau(qp)$ are linear and agree on monomials, so they are equal. Thus $\tau$ is a tracial state.

Marginals. By (F4), $\sigma^{1}\circ\iota^{1}=\sigma_{c}$ with $c_{j}=\sigma^{1}(x_{j})=x_{j}$ $(j\in[d])$, the identity of $\mathcal{P}_{d}$, and $\sigma^{2}\circ\iota^{1}=\sigma_{c'}$ with $c'_{j}=\sigma^{2}(x_{j})=1$. For $w\in W_{d}$, $\iota^{1}(x_{w})$ is a monomial of $\mathcal{P}_{2d}$ by (F5), so $\tau(\iota^{1}(x_{w}))=\mu(\sigma^{1}(\iota^{1}(x_{w})))\,\nu(\sigma^{2}(\iota^{1}(x_{w})))=\mu(x_{w})\nu(1)=\mu(x_{w})$, using (F5) for $c'$. Both $\tau\circ\iota^{1}$ and $\mu$ are linear, so $\tau\circ\iota^{1}=\mu$ by (F7). Symmetrically $\sigma^{1}\circ\iota^{2}$ sends each $x_{j}$ to $1$ and $\sigma^{2}\circ\iota^{2}$ is the identity, so $\tau(\iota^{2}(x_{w}))=\mu(1)\nu(x_{w})=\nu(x_{w})$ and $\tau\circ\iota^{2}=\nu$. Hence $\tau\in\Pi(\mu,\nu)$ by Couplings of Two Noncommutative Laws and Their Quadratic Cost §coupling, and $\Pi(\mu,\nu)\neq\emptyset$.

Step 4 (claim 4). By (F2) and (F3), $\mu\circ\delta$ is a tracial state on $\mathcal{P}_{2d}$. By (F4), $\delta\circ\iota^{1}$ and $\delta\circ\iota^{2}$ are $\sigma_{c}$ with $c_{j}=\delta(x_{j})=x_{j}$, resp. $c_{j}=\delta(x_{d+j})=x_{j}$, i.e. the identity; so $(\mu\circ\delta)\circ\iota^{1}=(\mu\circ\delta)\circ\iota^{2}=\mu$ and $\mu\circ\delta\in\Pi(\mu,\mu)$. By linearity and Substitution is the Unique Unital Homomorphism with Prescribed Values on the Variables: Monomials, Products, Adjoints and Composition §values, $\delta(q_{j})=x_{j}-x_{j}=0$ (F1), so $\delta(q_{j}^{2})=0\cdot0=0$ by Substitution is the Unique Unital Homomorphism with Prescribed Values on the Variables: Monomials, Products, Adjoints and Composition §homomorphism and (F1), and $\delta(\Delta_{d})=\sum_{j=1}^{d}0=0$ by claims 4 and 7 of Properties of Finite Sums of Vectors. Thus $I(\mu\circ\delta)=\mu(0)=0$.

Step 5 (claim 5). Here $s(x_{j})=x_{d+j}$ and $s(x_{d+j})=x_{j}$ for $j\in[d]$. By (F2) and (F3), $\gamma\circ s$ is a tracial state. By (F4), $s\circ\iota^{1}=\sigma_{(x_{d+1},\dots,x_{2d})}=\iota^{2}$ and $s\circ\iota^{2}=\sigma_{(x_{1},\dots,x_{d})}=\iota^{1}$, so $(\gamma\circ s)\circ\iota^{1}=\nu$ and $(\gamma\circ s)\circ\iota^{2}=\mu$, i.e. $\gamma\circ s\in\Pi(\nu,\mu)$. Further $s(q_{j})=x_{d+j}-x_{j}=(-1)q_{j}$ (F1), so $s(q_{j}^{2})=((-1)q_{j})((-1)q_{j})=q_{j}^{2}$ by Substitution is the Unique Unital Homomorphism with Prescribed Values on the Variables: Monomials, Products, Adjoints and Composition §homomorphism and Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts §algebra; by claim 4 of Properties of Finite Sums of Vectors, $s(\Delta_{d})=\Delta_{d}$ and $I(\gamma\circ s)=\gamma(s(\Delta_{d}))=I(\gamma)$.

Step 6 (claim 6). By Step 1, $\gamma_{m}\in\Sigma_{2d,R}$ for all $m$, so Sequential Weak-Star Compactness of the Noncommutative Laws with a Given Norm Bound §compact gives a strictly increasing $(m_{i})_{i\in\mathbb{N}}$ (Subsequence of a Sequence in a Set) and $\gamma\in\Sigma_{2d,R}$ with $\gamma_{m_{i}}\to\gamma$ weak-star; $\gamma$ is a tracial state. By Sequential Weak-Star Compactness of the Noncommutative Laws with a Given Norm Bound §unique (second sentence; $\mu_{m}\in\Sigma_{d}$ by Noncommutative Laws of Finitely Many Self-Adjoint Variables with a Norm Bound §law), $\mu_{m_{i}}\to\mu$ weak-star. Let $p\in\mathcal{P}_{d}$. For every $i$, $\gamma_{m_{i}}(\iota^{1}(p))=\mu_{m_{i}}(p)$, so the real sequence $(\operatorname{Re}\gamma_{m_{i}}(\iota^{1}(p)))_{i}$ converges both to $\operatorname{Re}\mu(p)$ and, by Weak-Star Convergence of Noncommutative Laws §weak-star applied to $\iota^{1}(p)\in\mathcal{P}_{2d}$, to $\operatorname{Re}\gamma(\iota^{1}(p))$; by claim 1 of Uniqueness of Limits and Boundedness of Convergent Real Sequences these are equal, and likewise the imaginary parts. By (F9), $\gamma(\iota^{1}(p))=\mu(p)$. The same argument gives $\gamma\circ\iota^{2}=\nu$, so $\gamma\in\Pi(\mu,\nu)$. Finally $I(\gamma_{m_{i}})=\gamma_{m_{i}}(\Delta_{d})$ and $I(\gamma)=\gamma(\Delta_{d})$ are real by Step 2 (applied to $\mu_{m_{i}},\nu_{m_{i}}$ and to $\mu,\nu$), so by (F9) and weak-star convergence at $\Delta_{d}$, $I(\gamma_{m_{i}})=\operatorname{Re}\gamma_{m_{i}}(\Delta_{d})\to\operatorname{Re}\gamma(\Delta_{d})=I(\gamma)$.

Step 7 (claim 7). By Step 1, $\gamma\in\Sigma_{2d,R}$. For $j\in[d]$ put $c_{j0}=0$, $c_{jj}=1-t$, $c_{j,d+j}=t$ and $c_{jk}=0$ for the other $k\in[2d]$ (well defined since $j\neq d+j$); these are real, and $0\le1-t$ by claim 3 of Elementary Arithmetic in an Ordered Field. Writing $c_{jk}x_{k}=u_{k}+v_{k}$ with $u_{k}=c_{jk}x_{k}$ for $k=j$, $v_{k}=c_{jk}x_{k}$ for $k=d+j$, and all other $u_{k},v_{k}$ equal to $0$ (F1), claims 2 and 7 of Properties of Finite Sums of Vectors give $c_{j0}1+\sum_{k=1}^{2d}c_{jk}x_{k}=a^{t}_{j}$; similarly, by claims 2 and 7 of Properties of Finite Sums and claim 8 of Properties of Complex Conjugation and Modulus, $|c_{j0}|+R\sum_{k=1}^{2d}|c_{jk}|=0+R((1-t)+t)=R$. So The Norm Bound of a Noncommutative Law: Multiplication by a Variable is Bounded, the Bound is Detected by Even Moments, and Laws Pull Back under Self-Adjoint Substitutions §affine (for $\gamma$, with $n=d$ and $S=R$) gives $\gamma_{t}\in\Sigma_{d,R}\subseteq\Sigma_{d}$. By (F1), $a^{0}_{j}=x_{j}$ and $a^{1}_{j}=x_{d+j}$, so $\sigma_{a^{0}}=\iota^{1}$, $\sigma_{a^{1}}=\iota^{2}$, and $\gamma_{0}=\mu$, $\gamma_{1}=\nu$ (Couplings of Two Noncommutative Laws and Their Quadratic Cost §coupling).

Let $b=(x_{1},\dots,x_{d},a^{t}_{1},\dots,a^{t}_{d})$. By (F2) and (F3), $\gamma\circ\sigma_{b}$ is a tracial state; by (F4), $\sigma_{b}\circ\iota^{1}=\sigma_{(x_{1},\dots,x_{d})}=\iota^{1}$ and $\sigma_{b}\circ\iota^{2}=\sigma_{a^{t}}$, so $(\gamma\circ\sigma_{b})\circ\iota^{1}=\mu$ and $(\gamma\circ\sigma_{b})\circ\iota^{2}=\gamma_{t}$, whence $\gamma\circ\sigma_{b}\in\Pi(\mu,\gamma_{t})$. By linearity, Substitution is the Unique Unital Homomorphism with Prescribed Values on the Variables: Monomials, Products, Adjoints and Composition §values and (F1), $\sigma_{b}(q_{j})=x_{j}-a^{t}_{j}=t\,q_{j}$ (at each word, $c-((1-t)c+tc')=t(c-c')$), so $\sigma_{b}(q_{j}^{2})=(tq_{j})(tq_{j})=t^{2}q_{j}^{2}$ by Substitution is the Unique Unital Homomorphism with Prescribed Values on the Variables: Monomials, Products, Adjoints and Composition §homomorphism and Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts §algebra, and $\sigma_{b}(\Delta_{d})=t^{2}\Delta_{d}$ by claims 3 and 4 of Properties of Finite Sums of Vectors. Hence the cost is $\gamma(\sigma_{b}(\Delta_{d}))=t^{2}I(\gamma)$.

Let $b'=(a^{t}_{1},\dots,a^{t}_{d},x_{d+1},\dots,x_{2d})$. As before $\gamma\circ\sigma_{b'}$ is a tracial state, $\sigma_{b'}\circ\iota^{1}=\sigma_{a^{t}}$ and $\sigma_{b'}\circ\iota^{2}=\iota^{2}$, so $\gamma\circ\sigma_{b'}\in\Pi(\gamma_{t},\nu)$; and $\sigma_{b'}(q_{j})=a^{t}_{j}-x_{d+j}=(1-t)q_{j}$, so $\sigma_{b'}(\Delta_{d})=(1-t)^{2}\Delta_{d}$ and the cost is $(1-t)^{2}I(\gamma)$. $\blacksquare$