Proof of Calculus of Square-Integrable Noncommutative Laws: Agreement on Bounded Laws, Lipschitz Estimates, Functoriality of Push-Forwards, Moment Formulas, Positivity, the Cost and the Diagonal Coupling

Each result cited below is universally quantified over the data in its own statement. Clauses 1, 2 and 4 are proved for an arbitrary affine datum between arbitrary numbers of variables, and they are used below also for the data $S$, $\mathrm{pr}^{1}$, $\mathrm{pr}^{2}$, $D$ and $\mathrm{diag}$; the order of proof is 1, continuity, 4, 2, 3, 5, 6, and no clause uses a later one.

For $k\in\mathbb{N}$, $(\Sigma_{k},W_{2})$ is a metric space by The Noncommutative Wasserstein Distance Satisfies the Triangle Inequality and is a Metric on Noncommutative Laws §metric, and $(\Sigma^{2}_{k},\widehat{W}_{2})$ is a complete metric space by The Metric Completion is a Complete Metric Space with a Dense Isometric Copy of the Space, and Maps Preserving Cauchy Sequences Extend to It §metric and The Metric Completion is a Complete Metric Space with a Dense Isometric Copy of the Space, and Maps Preserving Cauchy Sequences Extend to It §complete. The real line $(\mathbb{R},d_{\mathbb{R}})$ of The Absolute Value Metric on the Real Line is complete by Every Cauchy Sequence of Real Numbers Converges, because $d_{\mathbb{R}}(a,b)=|a-b|$ makes a sequence Cauchy in the sense of Cauchy Sequence in a Metric Space exactly when it is Cauchy in the sense of Cauchy Sequence of Real Numbers; likewise, since $d_{\mathbb{R}}(a,L)=|a-L|$, a real sequence converges to $L$ in $(\mathbb{R},d_{\mathbb{R}})$ in the sense of Convergent Sequence in a Metric Space exactly when it converges to $L$ in the sense of Limit of a Sequence of Real Numbers, so Arithmetic of Limits of Real Sequences and Order Properties of Limits of Real Sequences apply to such limits. Every $\lambda\in\Sigma_{k}$ is a tracial state on $\mathcal{P}_{k}$ by Noncommutative Laws of Finitely Many Self-Adjoint Variables with a Norm Bound §law.

Three general facts. (F1) If $f:X\to Y$ and $g:Y\to Z$ are continuous maps between metric spaces, then $g\circ f$ is continuous: if $y_{j}\to x$ in $X$, then $f(y_{j})\to f(x)$ and hence $g(f(y_{j}))\to g(f(x))$ by Continuity Between Metric Spaces is Equivalent to Sequential Continuity §sequential, so $g\circ f$ is continuous by Continuity Between Metric Spaces is Equivalent to Sequential Continuity §on-subset (with $A=X$). (F2) If $(X,e)$ is a metric space and $a,a',b,b'\in X$, then $|e(a,b)-e(a',b')|\le e(a,a')+e(b,b')$: by the triangle inequality and the symmetry of $e$ (Metric Space), $e(a,b)\le e(a,a')+e(a',b')+e(b',b)$, and likewise with $(a,b)$ and $(a',b')$ exchanged. (F3) Constant real functions on a metric space are continuous by claim 1 of Continuity of Sums and Products of Real-Valued Functions on a Metric Space, and sums, products and constant multiples of continuous real functions are continuous by claim 5 there; by induction on the number of summands, using the recursion in claim 1 of Properties of Finite Sums, finite sums of continuous real functions are continuous.

Proof of clause 1 (Bounded laws). By Square-Integrable Noncommutative Laws: the Wasserstein Completion of the Laws, Affine Push-Forwards, Moments, Couplings and Cost §push-forward and Square-Integrable Noncommutative Laws: the Wasserstein Completion of the Laws, Affine Push-Forwards, Moments, Couplings and Cost §moments, $T_{\#}$, $\mathrm{m}_{i}$ and $\mathrm{m}_{ij}$ are the extensions of the maps $f_{T}:\lambda\mapsto\kappa_{n}(\lambda\circ\sigma_{T})$, $\lambda\mapsto\lambda(x_{i})$ and $\lambda\mapsto\lambda(x_{i}x_{j})$ on $\Sigma_{m}$ (the moments of Affine Substitutions of Noncommutative Laws: Self-Adjointness, Composition, Moment Formulas and Positivity, and the Coordinate Data §moments), so the identity $\widehat{f}\circ\kappa_{X}=f$ of The Metric Completion is a Complete Metric Space with a Dense Isometric Copy of the Space, and Maps Preserving Cauchy Sequences Extend to It §extension gives the first three formulas. Summing the third over $i=j\in[m]$ gives $\widehat{M}(\kappa_{m}(\lambda))=\sum_{i=1}^{m}\lambda(x_{i}x_{i})=M(\lambda)$ by Square-Integrable Noncommutative Laws: the Wasserstein Completion of the Laws, Affine Push-Forwards, Moments, Couplings and Cost §moments and Noncommutative Laws, Couplings and the Wasserstein Distance: Standing Notation §laws.

Now let $\mu,\nu\in\Sigma_{d}$ and $\gamma\in\Sigma_{2d}$. For $\epsilon\in\{1,2\}$, $\sigma_{\mathrm{pr}^{\epsilon}}=\iota^{\epsilon}$ by Affine Substitutions of Noncommutative Laws: Self-Adjointness, Composition, Moment Formulas and Positivity, and the Coordinate Data §coordinate and $\gamma\circ\iota^{\epsilon}\in\Sigma_{d}$ by Affine Substitutions of Noncommutative Laws: Self-Adjointness, Composition, Moment Formulas and Positivity, and the Coordinate Data §self-adjoint, so the first formula gives

Since $\kappa_{d}$ is injective by The Metric Completion is a Complete Metric Space with a Dense Isometric Copy of the Space, and Maps Preserving Cauchy Sequences Extend to It §isometry, (1) shows that $\mathrm{pr}^{1}_{\#}\kappa_{2d}(\gamma)=\kappa_{d}(\mu)$ holds if and only if $\gamma\circ\iota^{1}=\mu$, and $\mathrm{pr}^{2}_{\#}\kappa_{2d}(\gamma)=\kappa_{d}(\nu)$ if and only if $\gamma\circ\iota^{2}=\nu$. As $\gamma$ is a tracial state on $\mathcal{P}_{2d}$, Square-Integrable Noncommutative Laws: the Wasserstein Completion of the Laws, Affine Push-Forwards, Moments, Couplings and Cost §couplings and Couplings of Two Noncommutative Laws and Their Quadratic Cost §coupling give: $\kappa_{2d}(\gamma)\in\Pi^{2}(\kappa_{d}(\mu),\kappa_{d}(\nu))$ if and only if $\gamma\in\Pi(\mu,\nu)$. In that case $\gamma\circ\sigma_{D}\in\Sigma_{d}$ by Affine Substitutions of Noncommutative Laws: Self-Adjointness, Composition, Moment Formulas and Positivity, and the Coordinate Data §self-adjoint, and Square-Integrable Noncommutative Laws: the Wasserstein Completion of the Laws, Affine Push-Forwards, Moments, Couplings and Cost §cost, the first and the fourth formula (for $d$ variables), Affine Substitutions of Noncommutative Laws: Self-Adjointness, Composition, Moment Formulas and Positivity, and the Coordinate Data §cost-identity and Couplings of Two Noncommutative Laws and Their Quadratic Cost §cost give

Continuity. By the continuity statement of The Metric Completion is a Complete Metric Space with a Dense Isometric Copy of the Space, and Maps Preserving Cauchy Sequences Extend to It §extension, $T_{\#}$, $\mathrm{m}_{i}$ and $\mathrm{m}_{ij}$ are continuous (for every affine datum and all indices), and $\widehat{M}=\sum_{i}\mathrm{m}_{ii}$ is continuous by (F3). This is the last sentence of clause 2; it does not depend on clauses 2 or 4.

Proof of clause 4 (Moments). Each assertion compares two continuous real functions of $\mu\in\Sigma^{2}_{m}$, and follows from The Metric Completion is a Complete Metric Space with a Dense Isometric Copy of the Space, and Maps Preserving Cauchy Sequences Extend to It §uniqueness (for equalities) or The Metric Completion is a Complete Metric Space with a Dense Isometric Copy of the Space, and Maps Preserving Cauchy Sequences Extend to It §inequalities (for inequalities) once it is verified at every point $\kappa_{m}(\lambda)$, $\lambda\in\Sigma_{m}$. Symmetry: $\mathrm{m}_{ij}$ and $\mathrm{m}_{ji}$ are continuous, and at $\kappa_{m}(\lambda)$ they equal $\mathrm{m}_{ij}(\lambda)=\mathrm{m}_{ji}(\lambda)$ by clause 1 and Affine Substitutions of Noncommutative Laws: Self-Adjointness, Composition, Moment Formulas and Positivity, and the Coordinate Data §moments. Next, $\mathrm{m}_{i}\cdot\mathrm{m}_{i}$ and $\mathrm{m}_{ii}$ are continuous by (F3), and by clause 1 and Affine Substitutions of Noncommutative Laws: Self-Adjointness, Composition, Moment Formulas and Positivity, and the Coordinate Data §moments, $\mathrm{m}_{i}(\kappa_{m}(\lambda))^{2}=\mathrm{m}_{i}(\lambda)^{2}\le\mathrm{m}_{ii}(\lambda)=\mathrm{m}_{ii}(\kappa_{m}(\lambda))$. For fixed real $\xi_{1},\dots,\xi_{m}$, the function $\mu\mapsto\sum_{i,j}\xi_{i}\xi_{j}\mathrm{m}_{ij}(\mu)$ is continuous by (F3) and at $\kappa_{m}(\lambda)$ equals $\sum_{i,j}\xi_{i}\xi_{j}\mathrm{m}_{ij}(\lambda)\ge0$ by clause 1 and Affine Substitutions of Noncommutative Laws: Self-Adjointness, Composition, Moment Formulas and Positivity, and the Coordinate Data §moments; compare it with the constant function $0$. Then $\widehat{M}(\mu)=\sum_{i}\mathrm{m}_{ii}(\mu)\ge0$ because $\mathrm{m}_{ii}(\mu)\ge\mathrm{m}_{i}(\mu)^{2}\ge0$ for every $i$, by claim 5 of Properties of Finite Sums.

For the affine formulas fix $i,k\in[n]$. The left sides $\mathrm{m}_{i}\circ T_{\#}$ and $\mathrm{m}_{ik}\circ T_{\#}$ are continuous by (F1), and the right sides are continuous functions of $\mu$ by (F3). Let $\lambda\in\Sigma_{m}$; then $\lambda\circ\sigma_{T}\in\Sigma_{n}$ by Affine Substitutions of Noncommutative Laws: Self-Adjointness, Composition, Moment Formulas and Positivity, and the Coordinate Data §self-adjoint. Clause 1, applied first to $T$ at $\lambda$ and then to the moments on $\Sigma^{2}_{n}$ at $\lambda\circ\sigma_{T}$, gives $\mathrm{m}_{i}(T_{\#}\kappa_{m}(\lambda))=\mathrm{m}_{i}(\lambda\circ\sigma_{T})$ and $\mathrm{m}_{ik}(T_{\#}\kappa_{m}(\lambda))=\mathrm{m}_{ik}(\lambda\circ\sigma_{T})$. By the affine moment formulas of Affine Substitutions of Noncommutative Laws: Self-Adjointness, Composition, Moment Formulas and Positivity, and the Coordinate Data §moments, and clause 1 once more (which replaces $\mathrm{m}_{j}(\lambda)$ and $\mathrm{m}_{jl}(\lambda)$ by $\mathrm{m}_{j}(\kappa_{m}(\lambda))$ and $\mathrm{m}_{jl}(\kappa_{m}(\lambda))$), these numbers equal the right sides evaluated at $\kappa_{m}(\lambda)$.

Proof of clause 2 (Lipschitz estimates). Push-forwards. For $\lambda,\lambda'\in\Sigma_{m}$, The Metric Completion is a Complete Metric Space with a Dense Isometric Copy of the Space, and Maps Preserving Cauchy Sequences Extend to It §isometry and Wasserstein Estimates for Affine Push-Forwards, First and Quadratic Moments, and the Cost of a Joint Law §affine give $\widehat{W}_{2}(f_{T}(\lambda),f_{T}(\lambda'))=W_{2}(\lambda\circ\sigma_{T},\lambda'\circ\sigma_{T})\le\lVert T\rVert\,W_{2}(\lambda,\lambda')$. Thus $f_{T}$ is Lipschitz with constant $\lVert T\rVert$, which is nonnegative by Affine Data and Affine Substitutions of Noncommutative Polynomials §norm, and by The Metric Completion is a Complete Metric Space with a Dense Isometric Copy of the Space, and Maps Preserving Cauchy Sequences Extend to It §extension so is its extension $T_{\#}$; this is the first inequality.

First moments. By Wasserstein Estimates for Affine Push-Forwards, First and Quadratic Moments, and the Cost of a Joint Law §moments, $\lambda\mapsto\mathrm{m}_{i}(\lambda)$ is Lipschitz with constant $1$ from $(\Sigma_{m},W_{2})$ to $(\mathbb{R},d_{\mathbb{R}})$, hence so is its extension $\mathrm{m}_{i}$ by The Metric Completion is a Complete Metric Space with a Dense Isometric Copy of the Space, and Maps Preserving Cauchy Sequences Extend to It §extension; this is the second inequality.

Square root of the second moment. Let $g(\lambda)=M(\lambda)^{1/2}$ for $\lambda\in\Sigma_{m}$. By Wasserstein Estimates for Affine Push-Forwards, First and Quadratic Moments, and the Cost of a Joint Law §moments, $g$ is Lipschitz with constant $1$ into $(\mathbb{R},d_{\mathbb{R}})$, so it maps Cauchy sequences to Cauchy sequences of the complete space $(\mathbb{R},d_{\mathbb{R}})$, and The Metric Completion is a Complete Metric Space with a Dense Isometric Copy of the Space, and Maps Preserving Cauchy Sequences Extend to It §extension provides a continuous map $\widehat{g}:\Sigma^{2}_{m}\to\mathbb{R}$ with $\widehat{g}\circ\kappa_{m}=g$, Lipschitz with constant $1$. Since $\widehat{g}(\kappa_{m}(\lambda))=g(\lambda)\ge0$, The Metric Completion is a Complete Metric Space with a Dense Isometric Copy of the Space, and Maps Preserving Cauchy Sequences Extend to It §inequalities (against the constant function $0$) gives $\widehat{g}\ge0$. The continuous functions $\widehat{g}\cdot\widehat{g}$ (by (F3)) and $\widehat{M}$ satisfy $\widehat{g}(\kappa_{m}(\lambda))^{2}=M(\lambda)=\widehat{M}(\kappa_{m}(\lambda))$ by clause 1, so $\widehat{g}^{2}=\widehat{M}$ by The Metric Completion is a Complete Metric Space with a Dense Isometric Copy of the Space, and Maps Preserving Cauchy Sequences Extend to It §uniqueness. By the uniqueness in Existence and Uniqueness of the Nonnegative Square Root, $\widehat{g}(\mu)=\widehat{M}(\mu)^{1/2}$ for every $\mu\in\Sigma^{2}_{m}$, and the Lipschitz property of $\widehat{g}$ is the third inequality.

Quadratic moments. Fix $\mu,\nu\in\Sigma^{2}_{m}$ and $i,j\in[m]$. By The Metric Completion of a Metric Space §completion, $\mu=[x]$ and $\nu=[y]$ for Cauchy sequences $x=(x_{k})$ and $y=(y_{k})$ in $(\Sigma_{m},W_{2})$, and $\kappa_{m}(x_{k})\to\mu$ and $\kappa_{m}(y_{k})\to\nu$ by The Metric Completion is a Complete Metric Space with a Dense Isometric Copy of the Space, and Maps Preserving Cauchy Sequences Extend to It §density. For every $k$, Wasserstein Estimates for Affine Push-Forwards, First and Quadratic Moments, and the Cost of a Joint Law §moments at $(x_{k},y_{k})$, rewritten with clause 1, $g=\widehat{g}\circ\kappa_{m}$ and The Metric Completion is a Complete Metric Space with a Dense Isometric Copy of the Space, and Maps Preserving Cauchy Sequences Extend to It §isometry, reads

As $k\to\infty$: $\mathrm{m}_{ij}(\kappa_{m}(x_{k}))\to\mathrm{m}_{ij}(\mu)$, $\mathrm{m}_{ij}(\kappa_{m}(y_{k}))\to\mathrm{m}_{ij}(\nu)$, $\widehat{g}(\kappa_{m}(x_{k}))\to\widehat{M}(\mu)^{1/2}$ and $\widehat{g}(\kappa_{m}(y_{k}))\to\widehat{M}(\nu)^{1/2}$, by continuity and Continuity Between Metric Spaces is Equivalent to Sequential Continuity §sequential. By (F2), $|\widehat{W}_{2}(\kappa_{m}(x_{k}),\kappa_{m}(y_{k}))-\widehat{W}_{2}(\mu,\nu)|\le\widehat{W}_{2}(\kappa_{m}(x_{k}),\mu)+\widehat{W}_{2}(\kappa_{m}(y_{k}),\nu)$, whose right side tends to $0$ by claim 1 of Arithmetic of Limits of Real Sequences; so $\widehat{W}_{2}(\kappa_{m}(x_{k}),\kappa_{m}(y_{k}))\to\widehat{W}_{2}(\mu,\nu)$ by claim 3 of Order Properties of Limits of Real Sequences. By claims 1, 2 and 3 of Arithmetic of Limits of Real Sequences and claim 4 of Order Properties of Limits of Real Sequences, the left side of the display tends to $|\mathrm{m}_{ij}(\mu)-\mathrm{m}_{ij}(\nu)|$ and the right side to $\widehat{W}_{2}(\mu,\nu)(\widehat{M}(\mu)^{1/2}+\widehat{M}(\nu)^{1/2})$, and claim 1 of Order Properties of Limits of Real Sequences gives the fourth inequality. The continuity assertions were proved above.

Proof of clause 3 (Functoriality). $S\circ T$ is an affine datum from $m$ to $r$ variables by Affine Data and Affine Substitutions of Noncommutative Polynomials §composite. The maps $(S\circ T)_{\#}$ and $S_{\#}\circ T_{\#}$ from $\Sigma^{2}_{m}$ to $\Sigma^{2}_{r}$ are continuous by clause 2 and (F1). For $\lambda\in\Sigma_{m}$ we have $\lambda\circ\sigma_{T}\in\Sigma_{n}$ (Affine Substitutions of Noncommutative Laws: Self-Adjointness, Composition, Moment Formulas and Positivity, and the Coordinate Data §self-adjoint), and clause 1 (for $T$ at $\lambda$, for $S$ at $\lambda\circ\sigma_{T}$, and for $S\circ T$ at $\lambda$) and Affine Substitutions of Noncommutative Laws: Self-Adjointness, Composition, Moment Formulas and Positivity, and the Coordinate Data §composition give

Hence $(S\circ T)_{\#}=S_{\#}\circ T_{\#}$ by The Metric Completion is a Complete Metric Space with a Dense Isometric Copy of the Space, and Maps Preserving Cauchy Sequences Extend to It §uniqueness. Likewise, $(\mathrm{id}_{m})_{\#}$ and the identity map of $\Sigma^{2}_{m}$ are continuous (the latter with $\delta=\varepsilon$ in Continuous Map Between Metric Spaces), and they agree on $\kappa_{m}(\Sigma_{m})$ since $(\mathrm{id}_{m})_{\#}\kappa_{m}(\lambda)=\kappa_{m}(\lambda\circ\sigma_{\mathrm{id}_{m}})=\kappa_{m}(\lambda)$ by clause 1 and Affine Substitutions of Noncommutative Laws: Self-Adjointness, Composition, Moment Formulas and Positivity, and the Coordinate Data §composition; so they are equal by The Metric Completion is a Complete Metric Space with a Dense Isometric Copy of the Space, and Maps Preserving Cauchy Sequences Extend to It §uniqueness.

Proof of clause 5 (Cost). Let $\gamma\in\Sigma^{2}_{2d}$. By Square-Integrable Noncommutative Laws: the Wasserstein Completion of the Laws, Affine Push-Forwards, Moments, Couplings and Cost §couplings, $\gamma\in\Pi^{2}(\mathrm{pr}^{1}_{\#}\gamma,\mathrm{pr}^{2}_{\#}\gamma)$, and $\mathcal{I}(\gamma)=\widehat{M}(D_{\#}\gamma)\ge0$ by Square-Integrable Noncommutative Laws: the Wasserstein Completion of the Laws, Affine Push-Forwards, Moments, Couplings and Cost §cost and clause 4 (for $d$ variables).

Expansion. The data $D=(P^{1}-P^{2},0)$, $\mathrm{pr}^{1}=(P^{1},0)$ and $\mathrm{pr}^{2}=(P^{2},0)$ from $2d$ to $d$ variables have translation part $0$, so for each of them, with matrix $A$, the formula for $\mathrm{m}_{ik}(T_{\#}\gamma)$ in clause 4 with $i=k=j\in[d]$ reduces to $\sum_{l=1}^{2d}\sum_{l'=1}^{2d}A_{jl}A_{jl'}\,\mathrm{m}_{ll'}(\gamma)$. For $j\in[d]$ we have $j\neq d+j$, and by Affine Data and Affine Substitutions of Noncommutative Polynomials §coordinate the row $l\mapsto P^{1}_{jl}$ is $1$ at $l=j$ and $0$ elsewhere, while $l\mapsto P^{2}_{jl}$ is $1$ at $l=d+j$ and $0$ elsewhere. Using claims 2, 3 and 7 of Properties of Finite Sums and the symmetry in clause 4,

Summing over $j\in[d]$ with claims 2 and 3 of Properties of Finite Sums, and using the definition of $\widehat{M}$ in Square-Integrable Noncommutative Laws: the Wasserstein Completion of the Laws, Affine Push-Forwards, Moments, Couplings and Cost §moments, gives the displayed identity for $\mathcal{I}(\gamma)$.

The distance bound. Let $G(\gamma)=\widehat{W}_{2}(\mathrm{pr}^{1}_{\#}\gamma,\mathrm{pr}^{2}_{\#}\gamma)$ for $\gamma\in\Sigma^{2}_{2d}$. If $\gamma_{k}\to\gamma$ in $\Sigma^{2}_{2d}$, then $\mathrm{pr}^{\epsilon}_{\#}\gamma_{k}\to\mathrm{pr}^{\epsilon}_{\#}\gamma$ for $\epsilon=1,2$ by clause 2 and Continuity Between Metric Spaces is Equivalent to Sequential Continuity §sequential, and (F2), claim 1 of Arithmetic of Limits of Real Sequences and claim 3 of Order Properties of Limits of Real Sequences give $G(\gamma_{k})\to G(\gamma)$; so $G$ is continuous by Continuity Between Metric Spaces is Equivalent to Sequential Continuity §on-subset, and so is $G\cdot G$ by (F3). Also $\mathcal{I}=\widehat{M}\circ D_{\#}$ is continuous by clause 2 and (F1). Let $\gamma_{0}\in\Sigma_{2d}$. By (1) and The Metric Completion is a Complete Metric Space with a Dense Isometric Copy of the Space, and Maps Preserving Cauchy Sequences Extend to It §isometry, $G(\kappa_{2d}(\gamma_{0}))=W_{2}(\gamma_{0}\circ\iota^{1},\gamma_{0}\circ\iota^{2})$; by Wasserstein Estimates for Affine Push-Forwards, First and Quadratic Moments, and the Cost of a Joint Law §cost, $\gamma_{0}\in\Pi(\gamma_{0}\circ\iota^{1},\gamma_{0}\circ\iota^{2})$ and $W_{2}(\gamma_{0}\circ\iota^{1},\gamma_{0}\circ\iota^{2})^{2}\le I(\gamma_{0})$; and $I(\gamma_{0})=\mathcal{I}(\kappa_{2d}(\gamma_{0}))$ by clause 1 (with the laws $\gamma_{0}\circ\iota^{1},\gamma_{0}\circ\iota^{2}$). Hence $G(\kappa_{2d}(\gamma_{0}))^{2}\le\mathcal{I}(\kappa_{2d}(\gamma_{0}))$ for every $\gamma_{0}\in\Sigma_{2d}$, and The Metric Completion is a Complete Metric Space with a Dense Isometric Copy of the Space, and Maps Preserving Cauchy Sequences Extend to It §inequalities gives $G(\gamma)^{2}\le\mathcal{I}(\gamma)$ for every $\gamma\in\Sigma^{2}_{2d}$. Finally, if $\mu,\nu\in\Sigma^{2}_{d}$ and $\gamma\in\Pi^{2}(\mu,\nu)$, then $\mathrm{pr}^{1}_{\#}\gamma=\mu$ and $\mathrm{pr}^{2}_{\#}\gamma=\nu$ by Square-Integrable Noncommutative Laws: the Wasserstein Completion of the Laws, Affine Push-Forwards, Moments, Couplings and Cost §couplings, so $\widehat{W}_{2}(\mu,\nu)^{2}=G(\gamma)^{2}\le\mathcal{I}(\gamma)$.

Proof of clause 6 (Diagonal coupling). Let $\mu\in\Sigma^{2}_{d}$. For $\epsilon=1,2$, clause 3 and Affine Substitutions of Noncommutative Laws: Self-Adjointness, Composition, Moment Formulas and Positivity, and the Coordinate Data §coordinate give $\mathrm{pr}^{\epsilon}_{\#}\mathrm{diag}_{\#}\mu=(\mathrm{pr}^{\epsilon}\circ\mathrm{diag})_{\#}\mu=(\mathrm{id}_{d})_{\#}\mu=\mu$, so $\mathrm{diag}_{\#}\mu\in\Pi^{2}(\mu,\mu)$ by Square-Integrable Noncommutative Laws: the Wasserstein Completion of the Laws, Affine Push-Forwards, Moments, Couplings and Cost §couplings. Let $Z=D\circ\mathrm{diag}$, the affine datum from $d$ to $d$ variables both of whose maps have value $0$, by Affine Substitutions of Noncommutative Laws: Self-Adjointness, Composition, Moment Formulas and Positivity, and the Coordinate Data §coordinate. By Square-Integrable Noncommutative Laws: the Wasserstein Completion of the Laws, Affine Push-Forwards, Moments, Couplings and Cost §cost, clause 3 and Square-Integrable Noncommutative Laws: the Wasserstein Completion of the Laws, Affine Push-Forwards, Moments, Couplings and Cost §moments, $\mathcal{I}(\mathrm{diag}_{\#}\mu)=\widehat{M}(D_{\#}\mathrm{diag}_{\#}\mu)=\widehat{M}(Z_{\#}\mu)=\sum_{j=1}^{d}\mathrm{m}_{jj}(Z_{\#}\mu)$. By the formula for $\mathrm{m}_{ik}(T_{\#}\mu)$ in clause 4 with $T=Z$, $A=0$ and $c=0$, every term of which has a factor $0$, $\mathrm{m}_{jj}(Z_{\#}\mu)=0$ for every $j\in[d]$ (claim 3 of Properties of Finite Sums with $\lambda=0$). Hence $\mathcal{I}(\mathrm{diag}_{\#}\mu)=0$.