Proof of Tangent Inequalities for the Wall Energy along Couplings and for the Wall-Confined Free Energy along Optimal Couplings

Each result cited is universally quantified over the data in its own statement. Throughout, $R>0$ is as in the statement. Linear maps commute with finite sums and the distributive laws of Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts §algebra extend to finite sums, by induction along the recursion of Finite Sum Notation in a Vector Space. For a real number $r$ and $z,z'\in\mathbb{C}$: $\operatorname{Re}r=r$, $\operatorname{Re}(z+z')=\operatorname{Re}z+\operatorname{Re}z'$ and $\operatorname{Re}(rz)=r\operatorname{Re}z$. Indeed, write $z=a+bi$ and $z'=a'+b'i$ with $a,b,a',b'$ real (claim 3 of Canonical Form and Arithmetic of Complex Numbers); by claim 1 of that lemma the identities $0,1$ and the additive inverses of real numbers in $\mathbb{C}$ are the real ones, so $r=r+0i$, and by claim 4 of that lemma $z+z'=(a+a')+(b+b')i$ and $rz=(r+0i)(a+bi)=ra+(rb)i$, the operations in the parentheses being those of $\mathbb{R}$; the uniqueness in claim 3 of that lemma and Real and Imaginary Parts of a Complex Number give the three identities. Moreover $\overline{-1}=-1$, as $-1$ is real (claim 1 of Canonical Form and Arithmetic of Complex Numbers) and conjugation fixes real numbers (claim 1 of Properties of Complex Conjugation and Modulus); with claims 1 and 2 of Elementary Properties of a Complex Inner Product this gives $\langle u-u',v\rangle=\langle u,v\rangle-\langle u',v\rangle$ in a complex inner product space. A natural number $N$ used as a real number means $\iota(N)$, with $\iota$ the canonical map of $\mathbb{R}$; $0<\iota(N)$ by claim 3 of Properties of the Canonical Map from the Natural Numbers to an Ordered Field. For $k\in\mathbb{N}$, $R^{2k}\neq0$ and $0\le R^{2k}$ by claims 4 and 5 of Properties of Natural Number Powers in a Field, so $R^{-2k}\neq0$ and $0\le R^{-2k}$ by claim 4 of Elementary Arithmetic in an Ordered Field. For a real $S>0$ we put $S^{0}=1$; then $S^{\ell}S^{\ell'}=S^{\ell+\ell'}$ for all natural or zero $\ell,\ell'$, by Addition of Exponents for Natural Number Powers in a Field when both are natural numbers and trivially otherwise.

Step 0 (Powers). Let $r\in\mathbb{N}$ and $p\in\mathcal{P}_{r}$. For $\ell\in\mathbb{N}$, $p^{\ell}$ is the product along the word $w_{\ell}\in W_{1}$ of length $\ell$ all of whose letters are $1$, for the $1$-tuple $(p)$ (Substitution of Noncommutative Polynomials into the Variables §word-products); this is the meaning of powers in The Wall Energy of a Given Radius and the Wall Force of a Noncommutative Law, Monotonicity of Odd Powers under a Tracial State and 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. We put $p^{0}=1$. By Substitution is the Unique Unital Homomorphism with Prescribed Values on the Variables: Monomials, Products, Adjoints and Composition §values, $p^{\ell}=\sigma_{(p)}(x_{w_{\ell}})$.

(P1) $p^{\ell}p^{\ell'}=p^{\ell+\ell'}$ for natural or zero $\ell,\ell'$: if both are natural numbers, $w_{\ell}w_{\ell'}=w_{\ell+\ell'}$ by Words over a Finite Alphabet: the Empty Word, Concatenation and Reversal §concatenation, and Substitution is the Unique Unital Homomorphism with Prescribed Values on the Variables: Monomials, Products, Adjoints and Composition §values gives $(p)_{w_{\ell}w_{\ell'}}=(p)_{w_{\ell}}(p)_{w_{\ell'}}$; if one of them is $0$, this is $1q=q1=q$ from Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts §monomials.

(P2) If $p\in\mathcal{P}_{r,\mathrm{sa}}$, then $p^{\ell}\in\mathcal{P}_{r,\mathrm{sa}}$ for natural or zero $\ell$: $1$ is self-adjoint by Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts §adjoint; for $\ell\in\mathbb{N}$, $w_{\ell}^{\mathrm{rev}}=w_{\ell}$ by Words over a Finite Alphabet: the Empty Word, Concatenation and Reversal §reversal, so $x_{w_{\ell}}\in\mathcal{P}_{1,\mathrm{sa}}$ by Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts §adjoint, and $\sigma_{(p)}$ maps $\mathcal{P}_{1,\mathrm{sa}}$ into $\mathcal{P}_{r,\mathrm{sa}}$ by Substitution is the Unique Unital Homomorphism with Prescribed Values on the Variables: Monomials, Products, Adjoints and Composition §adjoint.

(P3) For $j\in[d]$ and $\ell\in\mathbb{N}$, $\iota^{1}(x_{j}^{\ell})=x_{j}^{\ell}$ and $\iota^{2}(x_{j}^{\ell})=x_{d+j}^{\ell}$, the right sides being powers in $\mathcal{P}_{2d}$. Indeed, by Couplings of Two Noncommutative Laws and Their Quadratic Cost §marginals, $\iota^{1}=\sigma_{b}$ with $b=(x_{1},\dots,x_{d})$ in $\mathcal{P}_{2d}$, and $\sigma_{b}(x_{j})=x_{j}$ by Substitution is the Unique Unital Homomorphism with Prescribed Values on the Variables: Monomials, Products, Adjoints and Composition §values; so Substitution is the Unique Unital Homomorphism with Prescribed Values on the Variables: Monomials, Products, Adjoints and Composition §composition, applied to the $1$-tuple $(x_{j})$ in $\mathcal{P}_{d}$ and to $b$, gives $\iota^{1}(\sigma_{(x_{j})}(x_{w_{\ell}}))=\sigma'(x_{w_{\ell}})$, where $\sigma'$ is the substitution of the $1$-tuple $(x_{j})$ in $\mathcal{P}_{2d}$, and $\sigma'(x_{w_{\ell}})=x_{j}^{\ell}$ by Substitution is the Unique Unital Homomorphism with Prescribed Values on the Variables: Monomials, Products, Adjoints and Composition §values. The same argument with $b=(x_{d+1},\dots,x_{2d})$ and $\sigma_{b}(x_{j})=x_{d+j}$ gives the claim for $\iota^{2}$.

Step 1 (Setting for Steps 1 to 4, and norm bounds along a segment). In Steps 1 to 4, $\gamma$ is a tracial state on $\mathcal{P}_{2d}$ with $\gamma\in\Sigma_{2d,R'}$ for a real $R'>0$, $j\in[d]$ and $k\in\mathbb{N}$ are fixed, $m=2k$, and $\lVert p\rVert=\lVert p\rVert_{\gamma}$ is the nonnegative square root of $\gamma(p^{*}p)$, 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. Put $a=x_{j}$, $b=x_{d+j}$, $c=b-a$, $a_{t}=a+tc$ for real $t$, and $S=R'+R'$, so $0<S$. The variables are self-adjoint (Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts §adjoint) and $\mathcal{P}_{2d,\mathrm{sa}}$ is closed under sums and real multiples (Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts §self-adjoint), so $c$ and every $a_{t}$ are self-adjoint. By the vector space rules of Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts §vector-space, $a_{0}=a$, $a_{1}=b$, $a_{t'}-a_{t}=(t'-t)c$, and $a_{t}=(1-t)x_{j}+t\,x_{d+j}$.

(i) Let $y=c$, or $y=a_{t}$ with $0\le t\le1$. Then $\lVert yp\rVert\le S\lVert p\rVert$ for every $p\in\mathcal{P}_{2d}$. Indeed, $y=\sum_{i=1}^{2d}c_{i}x_{i}$ with real coefficients, all zero except $c_{j}=-1$, $c_{d+j}=1$ if $y=c$, and $c_{j}=1-t$, $c_{d+j}=t$ if $y=a_{t}$ (the recursion of Finite Sum Notation in a Vector Space; $j\neq d+j$); in both cases $0+R'\sum_{i=1}^{2d}|c_{i}|\le S$, as $|1-t|+|t|=1$ for $0\le t\le1$ (claim 8 of Properties of Complex Conjugation and Modulus) and $R'\le S$. 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, with $2d$ variables and the $1$-tuple $(y)$, gives $\gamma\circ\sigma_{(y)}\in\Sigma_{1,S}$, and 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 this state gives $\gamma(\sigma_{(y)}(x_{1}^{2\ell}))\le S^{2\ell}$ for every $\ell\in\mathbb{N}$. Here $x_{1}^{2\ell}=\sigma_{(x_{1})}(x_{w_{2\ell}})=x_{w_{2\ell}}$ by Substitution is the Unique Unital Homomorphism with Prescribed Values on the Variables: Monomials, Products, Adjoints and Composition §values and Substitution is the Unique Unital Homomorphism with Prescribed Values on the Variables: Monomials, Products, Adjoints and Composition §identity, so $\sigma_{(y)}(x_{1}^{2\ell})=y^{2\ell}$ by Substitution is the Unique Unital Homomorphism with Prescribed Values on the Variables: Monomials, Products, Adjoints and Composition §values. Hence $\gamma(y^{2\ell})\le S^{2\ell}$ for every $\ell$, and 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 §multiplication gives the assertion.

(ii) For $y$ as in (i) and natural or zero $\ell$, $\lVert y^{\ell}p\rVert\le S^{\ell}\lVert p\rVert$ for every $p$: for $\ell=0$ this is $1p=p$; and $y^{\ell+1}p=y(y^{\ell}p)$ by (P1) and associativity (Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts §algebra), so (i) and claim 5 of Elementary Arithmetic in an Ordered Field (multiplying by $S\ge0$) give $\lVert y^{\ell+1}p\rVert\le S\,S^{\ell}\lVert p\rVert=S^{\ell+1}\lVert p\rVert$.

(iii) $|\gamma(P)|\le\lVert P\rVert$ for every $P\in\mathcal{P}_{2d}$, and $\lVert1\rVert=1$. Indeed, $1^{*}=1$ and $1P=P$ (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 §monomials) and $\gamma(1)=1$ (condition (a) of Noncommutative Laws of Finitely Many Self-Adjoint Variables with a Norm Bound §tracial-state), so $\lVert1\rVert=1$ by the uniqueness in Existence and Uniqueness of the Nonnegative Square Root, and Basic Properties of Noncommutative Laws: Adjoints, the Self-Adjoint Pairing, Cauchy-Schwarz, Monotonicity in the Bound, and Laws of Constant Tuples §cauchy-schwarz with $p=P$, $q=1$ gives $|\gamma(P)|^{2}\le\lVert P\rVert^{2}$; both sides being squares of nonnegative reals, claim 2 of Monotonicity of Squaring on the Nonnegative Elements of an Ordered Field gives the assertion.

(iv) For natural or zero $\ell$ and real $t$, the numbers $\gamma(a_{t}^{\ell})$ and $\gamma(a_{t}^{\ell}c)$ are real: $a_{t}^{\ell}$ is self-adjoint by (P2), so Basic Properties of Noncommutative Laws: Adjoints, the Self-Adjoint Pairing, Cauchy-Schwarz, Monotonicity in the Bound, and Laws of Constant Tuples §adjoint and Basic Properties of Noncommutative Laws: Adjoints, the Self-Adjoint Pairing, Cauchy-Schwarz, Monotonicity in the Bound, and Laws of Constant Tuples §pairing apply.

Step 2 (A second-order estimate). First, for $u,v\in\mathcal{P}_{2d}$ and $n'\in\mathbb{N}$,

$$v^{n'}-u^{n'}=\sum_{r=1}^{n'}u^{r-1}(v-u)v^{n'-r}.$$

For $n'=1$ the right side is $1(v-u)1=v-u$. If it holds for $n'$, then by distributivity, (P1) and Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts §algebra, $v^{n'+1}-u^{n'+1}=(v^{n'}-u^{n'})v+u^{n'}(v-u)$, and multiplying the sum for $n'$ on the right by $v$ (with $v^{n'-r}v=v^{n'+1-r}$ by (P1)) and adding the term $u^{n'}(v-u)v^{0}$ gives the sum for $n'+1$ (claim 1 of Properties of Finite Sums, in the form of Finite Sum Notation in a Vector Space).

Now let $0\le t\le t'\le1$, $s=t'-t$, $u=a_{t}$ and $v=a_{t'}$, so $v-u=sc$ (Step 1). We claim that the real number

$$e=\gamma(v^{m})-\gamma(u^{m})-m\,s\,\gamma(u^{m-1}c)$$

(real by Step 1 (iv)) satisfies $-C s^{2}\le e$, where $C=m^{2}S^{m}$. By the identity with $n'=m$ and the linearity of $\gamma$, $\gamma(v^{m})-\gamma(u^{m})=\sum_{\ell=1}^{m}\gamma(u^{\ell-1}(v-u)v^{m-\ell})$. For $\ell\in[m]$, condition (c) of Noncommutative Laws of Finitely Many Self-Adjoint Variables with a Norm Bound §tracial-state with $p=u^{\ell-1}(v-u)$ and $q=u^{m-\ell}$, associativity and (P1) give $\gamma(u^{\ell-1}(v-u)u^{m-\ell})=\gamma(u^{m-1}(v-u))=s\,\gamma(u^{m-1}c)$, the last by Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts §algebra and linearity. Hence, the sum of $m$ equal terms being $m$ times the term (claim 1 of Properties of Finite Sums with claim 1 of Properties of the Canonical Map from the Natural Numbers to an Ordered Field), claim 2 of Properties of Finite Sums and distributivity give

$$e=\sum_{\ell=1}^{m}\gamma\bigl(u^{\ell-1}(v-u)(v^{m-\ell}-u^{m-\ell})\bigr).$$

The summand with $\ell=m$ is $\gamma(u^{m-1}(v-u)(1-1))=0$. For $\ell\in[m-1]$ (note $m-1\in\mathbb{N}$ as $m\ge2$), the identity with $n'=m-\ell$ and $v-u=sc$ give, by Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts §algebra and linearity,

$$\gamma\bigl(u^{\ell-1}(v-u)(v^{m-\ell}-u^{m-\ell})\bigr)=s^{2}\sum_{r=1}^{m-\ell}\gamma(Q_{\ell,r}),\qquad Q_{\ell,r}=u^{\ell-1}c\,u^{r-1}c\,v^{m-\ell-r}.$$

By associativity $Q_{\ell,r}=Q_{\ell,r}1$ is obtained from $1$ by left multiplication with $v^{m-\ell-r}$, $c$, $u^{r-1}$, $c$ and $u^{\ell-1}$ in turn, so Step 1 (i)-(iii), claim 5 of Elementary Arithmetic in an Ordered Field and $S^{m-\ell-r}S\,S^{r-1}S\,S^{\ell-1}=S^{m}$ give $|\gamma(Q_{\ell,r})|\le\lVert Q_{\ell,r}\rVert\le S^{m}$. By the triangle inequality and multiplicativity of the modulus (claims 7 and 4 of Properties of Complex Conjugation and Modulus, along the recursions of the finite sums), $|s^{2}|=s^{2}$ (claim 8 there), and since each of the at most $m$ inner sums has at most $m$ summands, $|e|\le s^{2}m^{2}S^{m}=Cs^{2}$ (claim 5 of Elementary Arithmetic in an Ordered Field and for the counting: a sum of $n$ real terms (here moduli) each at most $B$ is at most $\iota(n)B$, by claim 1 of Comparison and Absolute Value Bounds for Finite Sums of Real Numbers and the recursion of claim 1 of Properties of Finite Sums with claim 1 of Properties of the Canonical Map from the Natural Numbers to an Ordered Field; and $\iota(m-\ell)\le\iota(m)$, $\iota(m-1)\le\iota(m)$ by claim 6 of Properties of the Canonical Map from the Natural Numbers to an Ordered Field). As $e$ is real, $-|e|\le e$ by claims 3 and 8 of Properties of the Absolute Value in an Ordered Field, so $-Cs^{2}\le e$.

Step 3 (Monotonicity of the slope). For $0\le t\le1$, $\gamma(a_{t}^{m-1}c)\ge\gamma(a^{m-1}c)$, both numbers being real by Step 1 (iv). For $t=0$ this is an equality, as $a_{0}=a$. Let $0<t$. Apply Monotonicity of Odd Powers under a Tracial State §monotone with $2d$ in place of its $m$, the tracial state $\gamma$, the self-adjoint polynomials $a_{t}$ and $a$ in place of its $a$ and $b$, and the present $k$, whose odd exponent is $2k-1=m-1$: the number $\gamma((a_{t}^{m-1}-a^{m-1})(a_{t}-a))$ is real and nonnegative. Since $a_{t}-a=tc$, by Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts §algebra and linearity this number equals $t\bigl(\gamma(a_{t}^{m-1}c)-\gamma(a^{m-1}c)\bigr)$. Multiplying by $t^{-1}$, which is nonnegative by claim 4 of Elementary Arithmetic in an Ordered Field, claim 5 there gives $0\le\gamma(a_{t}^{m-1}c)-\gamma(a^{m-1}c)$, and claim 3 there gives the assertion.

Step 4 (The tangent inequality for one even power). We show

$$\gamma(x_{d+j}^{2k})-\gamma(x_{j}^{2k})\ge-2k\,\gamma(x_{j}^{2k-1}h_{j}),$$

all three values of $\gamma$ being real (Step 1 (iv), and Basic Properties of Noncommutative Laws: Adjoints, the Self-Adjoint Pairing, Cauchy-Schwarz, Monotonicity in the Bound, and Laws of Constant Tuples §pairing for the last, $h_{j}=x_{j}-x_{d+j}$ being self-adjoint). Put $g(t)=\gamma(a_{t}^{m})$ for $0\le t\le1$, $X=\gamma(a^{m-1}c)$ and $\Delta=g(1)-g(0)-mX$, all real. Let $N\in\mathbb{N}$ and $s=\iota(N)^{-1}$, so $0<s$ (claim 3 of Properties of the Canonical Map from the Natural Numbers to an Ordered Field); put $t_{0}=0$ and $t_{i}=\iota(i)s$ for $i\in[N]$. By claims 1, 3 and 6 of Properties of the Canonical Map from the Natural Numbers to an Ordered Field and claim 5 of Elementary Arithmetic in an Ordered Field, $0\le t_{i}\le1$, $t_{N}=1$ and $t_{i}-t_{i-1}=s$ for $i\in[N]$. For $i\in[N]$, Step 2 with $t=t_{i-1}$ and $t'=t_{i}$, then Step 3 at $t_{i-1}$ multiplied by $ms\ge0$ (claim 5 of Elementary Arithmetic in an Ordered Field), give

$$g(t_{i})-g(t_{i-1})\ge ms\,\gamma(a_{t_{i-1}}^{m-1}c)-Cs^{2}\ge msX-Cs^{2}.$$

Summing over $i\in[N]$, the left sides telescope to $g(1)-g(0)$ (induction along claim 1 of Properties of Finite Sums), and claims 2, 3 and 5 of Properties of Finite Sums give $g(1)-g(0)\ge\iota(N)(msX-Cs^{2})=mX-Cs$. Multiplying by $\iota(N)\ge0$, $\iota(N)\Delta\ge-C$ for every $N\in\mathbb{N}$. Suppose $\Delta<0$. Then $0<-\Delta$, and claim 2 of The Archimedean Property of the Real Numbers with $x=C$ and $\varepsilon=-\Delta$ gives $N\in\mathbb{N}$ with $C<\iota(N)(-\Delta)$, that is $\iota(N)\Delta<-C$, a contradiction. So $0\le\Delta$, i.e. $g(1)-g(0)\ge mX$. Since $a_{0}=a=x_{j}$, $a_{1}=b=x_{d+j}$, $m=2k$ and $c=-h_{j}$ (vector space rules), linearity gives $X=-\gamma(x_{j}^{2k-1}h_{j})$, which is the assertion.

Step 5 (Claim 1: truncated energies). Let $\mu$, $\nu$ and $\gamma\in\Pi(\mu,\nu)$ be as in claim 1. Since $\mu,\nu\in\mathcal{D}_{R}\subseteq\Sigma_{d}$ (The Wall Energy of a Given Radius and the Wall Force of a Noncommutative Law §domain), Marginal Isometries, Bounded Plans and Displacement Pairings for Noncommutative Laws §bounded-couplings gives a real $R'>0$ with $\gamma\in\Sigma_{2d,R'}$; and $\gamma$ is a tracial state on $\mathcal{P}_{2d}$ with $\gamma\circ\iota^{1}=\mu$ and $\gamma\circ\iota^{2}=\nu$ (Couplings of Two Noncommutative Laws and Their Quadratic Cost §coupling). So Steps 1 to 4 apply to $\gamma$ for every $j\in[d]$ and $k\in\mathbb{N}$, and by (P3), $\gamma(x_{j}^{2k})=\mu(x_{j}^{2k})$ and $\gamma(x_{d+j}^{2k})=\nu(x_{j}^{2k})$. For $n\in\mathbb{N}$ and $j\in[d]$ put

$$G_{n,j}=\sum_{k=1}^{n}2k\,R^{-2k}\,x_{j}^{2k-1}\in\mathcal{P}_{2d},\qquad\Theta_{n}=\sum_{j=1}^{d}\operatorname{Re}\bigl\langle\widehat{G_{n,j}},\widehat{h_{j}}\bigr\rangle_{\mathcal{H}_{\gamma}} .$$

Multiplying the inequality of Step 4 by $R^{-2k}\ge0$ (claim 5 of Elementary Arithmetic in an Ordered Field) and summing over $k\in[n]$ and then over $j\in[d]$ (claims 2, 3 and 5 of Properties of Finite Sums, applied to the nonnegative differences of the two sides), the definition of $E^{R}_{n}$ in The Wall Energy of a Given Radius and the Wall Force of a Noncommutative Law and the linearity of $\gamma$ with distributivity give

$$E^{R}_{n}(\nu)-E^{R}_{n}(\mu)\ge-\sum_{j=1}^{d}\gamma(G_{n,j}h_{j}).$$

Each $x_{j}^{2k-1}$ is self-adjoint by (P2) and the coefficients $2kR^{-2k}$ are real, so $G_{n,j}\in\mathcal{P}_{2d,\mathrm{sa}}$ by Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts §self-adjoint, and $\gamma(G_{n,j}h_{j})$ is real by Basic Properties of Noncommutative Laws: Adjoints, the Self-Adjoint Pairing, Cauchy-Schwarz, Monotonicity in the Bound, and Laws of Constant Tuples §pairing. Moreover $\gamma(G_{n,j}h_{j})=\gamma(G_{n,j}^{*}h_{j})=\langle\widehat{G_{n,j}},\widehat{h_{j}}\rangle_{\mathcal{H}_{\gamma}}$ by The Complex Hilbert Completion is a Complex Hilbert Space Containing a Dense Isometric Image, and Bounded Complex-Linear Maps Extend to It §isometry, as $\mathcal{H}_{\gamma}$, its inner product and its classes are the completion, pairing and canonical images for the form $(p,q)\mapsto\gamma(p^{*}q)$ (The Complex GNS Space of a Tracial State on Noncommutative Polynomials §gns, The Complex GNS Space of a Tracial State on Noncommutative Polynomials §classes). A real number being its real part, the right side above is $-\Theta_{n}$:

$$E^{R}_{n}(\nu)-E^{R}_{n}(\mu)\ge-\Theta_{n}\qquad(n\in\mathbb{N}).$$

Step 6 (Continuity of the pairing). Let $H,K$ be complex Hilbert spaces, $T\in\mathcal{L}(H,K)$, $\eta\in K$, and let $(\xi_{n})$ converge to $\xi$ in $H$. Then $(\operatorname{Re}\langle T\xi_{n},\eta\rangle_{K})_{n}$ converges to $\operatorname{Re}\langle T\xi,\eta\rangle_{K}$. Indeed, by the linearity of $T$, the preamble and the additivity of $\operatorname{Re}$, the difference $\operatorname{Re}\langle T\xi_{n},\eta\rangle-\operatorname{Re}\langle T\xi,\eta\rangle$ equals $\operatorname{Re}z_{n}$ with $z_{n}=\langle T(\xi_{n}-\xi),\eta\rangle$. By claim 6 of Properties of Complex Conjugation and Modulus and claim 6 of Properties of the Absolute Value in an Ordered Field, $|\operatorname{Re}z_{n}|\le|z_{n}|$. By Cauchy-Schwarz Inequality in a Complex Inner Product Space and Norm Induced by a Complex Inner Product, $|z_{n}|^{2}\le(\lVert T(\xi_{n}-\xi)\rVert\,\lVert\eta\rVert)^{2}$, so $|z_{n}|\le\lVert T(\xi_{n}-\xi)\rVert\,\lVert\eta\rVert$ by claim 2 of Monotonicity of Squaring on the Nonnegative Elements of an Ordered Field; and $\lVert T(\xi_{n}-\xi)\rVert\le\lVert T\rVert_{\mathrm{op}}\lVert\xi_{n}-\xi\rVert$ because $\lVert T\rVert_{\mathrm{op}}$ is a bound for $T$ (Bounded Linear Maps between Complex Inner Product Spaces: the Least Bound, Operations, the Underlying Real Structure, Adjoints, Completeness and the Quadratic-Form Bound §least-bound). Thus, by claim 5 of Elementary Arithmetic in an Ordered Field, $\bigl|\operatorname{Re}\langle T\xi_{n},\eta\rangle-\operatorname{Re}\langle T\xi,\eta\rangle\bigr|\le\lVert\eta\rVert\,\lVert T\rVert_{\mathrm{op}}\,\lVert\xi_{n}-\xi\rVert$. The real sequence $(\lVert\xi_{n}-\xi\rVert)_{n}$ converges to $0$ by Convergent Sequence in a Metric Space and Limit of a Sequence of Real Numbers, the metric being $(w,w')\mapsto\lVert w-w'\rVert$ (Complex Hilbert Space); so the right side converges to $0$ by claim 3 of Arithmetic of Limits of Real Sequences, and claim 3 of Order Properties of Limits of Real Sequences gives the assertion.

Step 7 (Claim 1: passage to the limit). By Marginal Isometries, Bounded Plans and Displacement Pairings for Noncommutative Laws §isometries with $\gamma\circ\iota^{1}=\mu$, $V^{1}_{\gamma}\in\mathcal{L}(\mathcal{H}_{\mu},\mathcal{H}_{\gamma})$ and $V^{1}_{\gamma}\widehat{p}^{\,\mu}=\widehat{\iota^{1}(p)}^{\,\gamma}$ for $p\in\mathcal{P}_{d}$. Since $\iota^{1}$ is linear (Substitution of Noncommutative Polynomials into the Variables §substitution), (P3) gives $\iota^{1}(F^{R}_{n,j})=G_{n,j}$, so $V^{1}_{\gamma}\widehat{F^{R}_{n,j}}^{\,\mu}=\widehat{G_{n,j}}^{\,\gamma}$. As $\mu$ has a square-integrable wall force, $(\widehat{F^{R}_{n,j}}^{\,\mu})_{n}$ converges to $F^{R}_{j}(\mu)$ in $\mathcal{H}_{\mu}$ for every $j\in[d]$ (The Wall Energy of a Given Radius and the Wall Force of a Noncommutative Law §force). By Step 6 with $T=V^{1}_{\gamma}$ and $\eta=\widehat{h_{j}}$, the real sequence $(\operatorname{Re}\langle\widehat{G_{n,j}},\widehat{h_{j}}\rangle_{\mathcal{H}_{\gamma}})_{n}$ converges to $\operatorname{Re}\langle V^{1}_{\gamma}F^{R}_{j}(\mu),\widehat{h_{j}}\rangle_{\mathcal{H}_{\gamma}}$; by claim 1 of Arithmetic of Limits of Real Sequences along the recursion of the finite sum over $j$ and by Marginal Isometries, Bounded Plans and Displacement Pairings for Noncommutative Laws §coupling-pairing, $(\Theta_{n})_{n}$ converges to $\mathcal{J}^{1}_{\gamma}(F^{R}(\mu))$, and $(-\Theta_{n})_{n}$ to $-\mathcal{J}^{1}_{\gamma}(F^{R}(\mu))$ by claim 3 there. Since $\mu,\nu\in\mathcal{D}_{R}$, The Wall Energy of a Given Radius and the Wall Force of a Noncommutative Law §energy and claim 3 of Arithmetic of Limits of Real Sequences show that $(E^{R}_{n}(\nu)-E^{R}_{n}(\mu))_{n}$ converges to $\mathcal{W}_{R}(\nu)-\mathcal{W}_{R}(\mu)$. By Step 5 and claim 1 of Order Properties of Limits of Real Sequences, $-\mathcal{J}^{1}_{\gamma}(F^{R}(\mu))\le\mathcal{W}_{R}(\nu)-\mathcal{W}_{R}(\mu)$, which by claim 3 of Elementary Arithmetic in an Ordered Field is claim 1.

Step 8 (Claim 2). Let $\mu$, $\nu$ and $\gamma$ be as in claim 2. By The Wall-Confined Free Energy and Its Score §score and The Wall-Confined Free Energy and Its Score §energy, $\mu\in\mathcal{D}=\mathcal{D}_{0}\cap\mathcal{D}_{R}$, $\mu$ has conjugate variables $\xi_{\mu}\in\mathcal{H}_{\mu}^{d}$ and a square-integrable wall force of radius $R$, and $\Xi(\mu)_{j}=F^{R}_{j}(\mu)-\xi_{\mu,j}$; also $\nu\in\mathcal{D}_{0}\cap\mathcal{D}_{R}$, and $\gamma\in\Pi(\mu,\nu)$. So Free Entropy Penalties: Displacement Convexity with Minus the Conjugate Variables as Gradient §tangent gives $\mathcal{E}_{0}(\nu)\ge\mathcal{E}_{0}(\mu)+\mathcal{J}^{1}_{\gamma}(\xi_{\mu})$, and claim 1, proved in Steps 5 to 7 for every coupling, gives $\mathcal{W}_{R}(\nu)\ge\mathcal{W}_{R}(\mu)-\mathcal{J}^{1}_{\gamma}(F^{R}(\mu))$. Adding (claims 2 and 3 of Elementary Arithmetic in an Ordered Field) and using The Wall-Confined Free Energy and Its Score §energy,

$$\mathcal{E}(\nu)\ge\mathcal{E}(\mu)-\bigl(\mathcal{J}^{1}_{\gamma}(F^{R}(\mu))-\mathcal{J}^{1}_{\gamma}(\xi_{\mu})\bigr).$$

For each $j\in[d]$, $V^{1}_{\gamma}$ is linear, so $V^{1}_{\gamma}\Xi(\mu)_{j}=V^{1}_{\gamma}F^{R}_{j}(\mu)-V^{1}_{\gamma}\xi_{\mu,j}$, and the preamble (the inner product identity, then the additivity of $\operatorname{Re}$ with $\operatorname{Re}(-z)=-\operatorname{Re}z$) gives $\operatorname{Re}\langle V^{1}_{\gamma}\Xi(\mu)_{j},\widehat{h_{j}}\rangle_{\mathcal{H}_{\gamma}}=\operatorname{Re}\langle V^{1}_{\gamma}F^{R}_{j}(\mu),\widehat{h_{j}}\rangle_{\mathcal{H}_{\gamma}}-\operatorname{Re}\langle V^{1}_{\gamma}\xi_{\mu,j},\widehat{h_{j}}\rangle_{\mathcal{H}_{\gamma}}$. Summing over $j$ with claims 2 and 3 of Properties of Finite Sums and Marginal Isometries, Bounded Plans and Displacement Pairings for Noncommutative Laws §coupling-pairing, $\mathcal{J}^{1}_{\gamma}(F^{R}(\mu))-\mathcal{J}^{1}_{\gamma}(\xi_{\mu})=\mathcal{J}^{1}_{\gamma}(\Xi(\mu))$, which proves claim 2.