Proof of The Formal Amalgamated Free Product: the Free Vector Space, Positivity of the Nested-Expectation Form, and Linearity and Formal Adjoints of the Actions

Conventions. For $\varepsilon\in\{1,2\}$ let $V_{\varepsilon}\in\mathcal{L}(\mathcal{H}_{\mu},\mathcal{H}_{\gamma_{\varepsilon}})$ be the operator of Marginals of a Noncommutative Law: the Isometry of GNS Spaces, the Trace-Preserving Embedding of Tracial Algebras and the Conditional Expectation §isometry for $\gamma=\gamma_{\varepsilon}$ and $a=a^{\varepsilon}$ (an operator, not an inner product space); by Two Noncommutative Laws with a Common Marginal: Standing Notation for Their Amalgamated Free Product §embeddings, $\pi_{\varepsilon}$ and $E_{\varepsilon}$ are the embedding and the expectation of that lemma for the same data. By Marginals of a Noncommutative Law: the Isometry of GNS Spaces, the Trace-Preserving Embedding of Tracial Algebras and the Conditional Expectation §homomorphism and Marginals of a Noncommutative Law: the Isometry of GNS Spaces, the Trace-Preserving Embedding of Tracial Algebras and the Conditional Expectation §expectation, $\pi_{\varepsilon}$ and $E_{\varepsilon}$ are linear and, for $S,T\in N$, $c\in A_{\varepsilon}$ and $\zeta,\zeta'\in\mathcal{H}_{\mu}$,

with $T=I$ or $S=I$ this gives $E_{\varepsilon}(\pi_{\varepsilon}(S)c)=S\,E_{\varepsilon}(c)$ and $E_{\varepsilon}(c\,\pi_{\varepsilon}(T))=E_{\varepsilon}(c)\,T$. The GNS spaces $\mathcal{H}_{\mu}$, $\mathcal{H}_{\gamma_{\varepsilon}}$ are complex Hilbert spaces (The Complex GNS Space of a Tracial State on Noncommutative Polynomials §gns) and $N$, $A_{\varepsilon}$ consist of bounded operators on them (The Tracial Algebra of a Noncommutative Law and Its Trace §algebra), so all their elements have adjoints (Bounded Linear Maps between Complex Inner Product Spaces: the Least Bound, Operations, the Underlying Real Structure, Adjoints, Completeness and the Quadratic-Form Bound §adjoint); $N$ and $A_{\varepsilon}$ contain $I$ and are closed under sums, scalar multiples, products and adjoints (The Tracial Algebra of a Noncommutative Law: a Norm-Closed Unital *-Algebra with a Faithful Positive Trace, Determined by Vacuum Vectors, Closed under Square Roots §star-algebra), hence are subspaces of the complex vector spaces of Bounded Linear Maps between Complex Inner Product Spaces: the Least Bound, Operations, the Underlying Real Structure, Adjoints, Completeness and the Quadratic-Form Bound §operations, in which composition distributes over sums and commutes with scalar multiples. The rules $(S+T)^{*}=S^{*}+T^{*}$, $(cT)^{*}=\overline{c}\,T^{*}$, $(ST)^{*}=T^{*}S^{*}$ and $(T^{*})^{*}=T$ of Bounded Linear Maps between Complex Inner Product Spaces: the Least Bound, Operations, the Underlying Real Structure, Adjoints, Completeness and the Quadratic-Form Bound §adjoint-calculus (with Bounded Linear Maps between Complex Inner Product Spaces: the Least Bound, Operations, the Underlying Real Structure, Adjoints, Completeness and the Quadratic-Form Bound §adjoint-unique) are used freely.

As in The Formal Amalgamated Free Product over a Common Marginal: Alternating Tuples, the Free Vector Space, the Nested-Expectation Form and the Formal Actions §space, an alternating tuple $t$ of length $k$ also stands for the label $(k,t)$; the labels $(0,x)$, $x\in N$, are called $N$-labels. By The Formal Amalgamated Free Product over a Common Marginal: Alternating Tuples, the Free Vector Space, the Nested-Expectation Form and the Formal Actions §form:

(Z) $h_{0}(u,v)=0$ unless $u,v$ are both $N$-labels or are tuples of the same length and the same type; in particular $h_{0}(u,v)=0$ if $u,v$ are tuples whose types have different first entries.

Fix the label $o=(0,I)$ and, for $\xi\in\mathcal{F}$, put $F_{\xi}=\operatorname{supp}\xi\cup\{o\}$, a nonempty finite set by claim 1 of Peeling an Element off a Finite Set, and Unions of Finite Sets. A sum over a nonempty finite index set is a finite sum along one bijection from an initial segment (Sum over a Finite Index Set), so claims 2 and 3 of Properties of Finite Sums give

(S) $\sum_{x\in F}(f(x)+g(x))=\sum_{x\in F}f(x)+\sum_{x\in F}g(x)$ and $\sum_{x\in F}c\,f(x)=c\sum_{x\in F}f(x)$ for maps $f,g:F\to\mathbb{C}$ and $c\in\mathbb{C}$.

(C) Centred parts. Let $c,d\in A_{\varepsilon}$. By The Formal Amalgamated Free Product over a Common Marginal: Alternating Tuples, the Free Vector Space, the Nested-Expectation Form and the Formal Actions §centred, $(c^{\circ})^{*}=c^{*}-\pi_{\varepsilon}(E_{\varepsilon}(c))^{*}=c^{*}-\pi_{\varepsilon}(E_{\varepsilon}(c)^{*})$, so by the rules above

In particular, if $c\in A_{\varepsilon}^{\circ}$ or $d\in A_{\varepsilon}^{\circ}$, then $E_{\varepsilon}((c^{\circ})^{*}d)=E_{\varepsilon}(c^{*}d^{\circ})=E_{\varepsilon}(c^{*}d)$, as $E_{\varepsilon}(c)^{*}E_{\varepsilon}(d)=0$.

(X) Comparison of layers. Let $s=(a_{1},\dots,a_{k})$, $t=(b_{1},\dots,b_{k})$ be alternating tuples of length $k$ and common type $(e_{1},\dots,e_{k})$, let $s'=(a'_{1},\dots,a'_{k'})$, $t'=(b'_{1},\dots,b'_{k'})$ be alternating tuples of length $k'$ and common type $(e'_{1},\dots,e'_{k'})$, and let $d\in\{0,1\}$ with $k+d\le k'$. Suppose $X_{1}(s,t)=X_{1+d}(s',t')$ and $(e_{j},a_{j},b_{j})=(e'_{j+d},a'_{j+d},b'_{j+d})$ for every $j\in[k]$ with $j\ge2$. Then $X_{j}(s,t)=X_{j+d}(s',t')$ for every $j\in[k]$. Indeed, let $A$ be the set of $j\in\mathbb{N}$ with $j>k$ or $X_{j}(s,t)=X_{j+d}(s',t')$. Then $1\in A$. If $j\in A$ and $j+1\le k$, then $2\le j+1+d\le k'$ and, by The Formal Amalgamated Free Product over a Common Marginal: Alternating Tuples, the Free Vector Space, the Nested-Expectation Form and the Formal Actions §nested,

if $j+1>k$, then $j+1\in A$ trivially. So $A=\mathbb{N}$ by Principle of Induction for the Natural Numbers.

Claim 1 (vector space). By The Formal Amalgamated Free Product over a Common Marginal: Alternating Tuples, the Free Vector Space, the Nested-Expectation Form and the Formal Actions §space, sums and scalar multiples of elements of $\mathcal{F}$ lie in $\mathcal{F}$, and the zero map lies in $\mathcal{F}$ (its support is empty). Two elements of $\mathcal{F}$ are equal when they agree at every label, and at a label $s$ each of conditions 1--8 of Vector Space over a Field reduces to the corresponding field identity in $\mathbb{C}$ (associativity and commutativity of addition, $\xi(s)+0=\xi(s)$, $\xi(s)+(-1)\xi(s)=0$, $\lambda(\mu\xi(s))=(\lambda\mu)\xi(s)$, $1\xi(s)=\xi(s)$ and the two distributive laws), with the zero map as zero vector and $(-1)\xi$ as the vector $w$ of condition 4. So $\mathcal{F}$ is a complex vector space with zero vector the zero map.

(E) For every $\xi\in\mathcal{F}$ and every nonempty finite $F\supseteq\operatorname{supp}\xi$, $\xi=\sum_{s\in F}\xi(s)\delta_{s}$. At a label $u$ the right side takes the value $\sum_{s\in F}\xi(s)\delta_{s}(u)$ (The Formal Amalgamated Free Product over a Common Marginal: Alternating Tuples, the Free Vector Space, the Nested-Expectation Form and the Formal Actions §space). If $u\in F$, the terms with $s\ne u$ vanish, so by Sums over Finite Index Sets: Finite Unions, Disjoint Unions, Vanishing Terms, Dependent Pairs, Conjugation and the Modulus §vanishing and claim 1 of Peeling, Splitting, and Interchange for Sums over a Finite Index Set the value is $\xi(u)\delta_{u}(u)=\xi(u)$. If $u\notin F$, all terms vanish, so the value is $0$ (Sums over Finite Index Sets: Finite Unions, Disjoint Unions, Vanishing Terms, Dependent Pairs, Conjugation and the Modulus §vanishing), which is $\xi(u)$ because $u\notin\operatorname{supp}\xi$. For $\xi\ne0$ the set $\operatorname{supp}\xi$ is nonempty and finite, and (E) with $F=\operatorname{supp}\xi$ is the asserted expansion.

Claim 2 (symmetry of nested expectations). Let $s=(a_{1},\dots,a_{k})$, $t=(b_{1},\dots,b_{k})$ have type $(e_{1},\dots,e_{k})$, and let $A$ be the set of $j\in\mathbb{N}$ with $j>k$ or $X_{j}(t,s)=X_{j}(s,t)^{*}$. By The Formal Amalgamated Free Product over a Common Marginal: Alternating Tuples, the Free Vector Space, the Nested-Expectation Form and the Formal Actions §nested and the rules of the conventions,

so $1\in A$. Let $j\in A$. If $j+1>k$, then $j+1\in A$. Otherwise $X_{j}(t,s)=X_{j}(s,t)^{*}$, and with $e=e_{j+1}$

So $A=\mathbb{N}$ by Principle of Induction for the Natural Numbers, which gives the claim for every $j\in[k]$.

Claim 3 (positive Gram operators). $\mathcal{H}_{\mu}^{M}$ is a complex Hilbert space (Finite Direct Sums of a Complex Hilbert Space: the Hilbert Structure, Coordinate Inclusions, Block Entries of Bounded Operators and Commutation with Diagonal Operators §hilbert), so $G^{*}\in\mathcal{L}(\mathcal{H}_{\mu}^{M})$ exists (Bounded Linear Maps between Complex Inner Product Spaces: the Least Bound, Operations, the Underlying Real Structure, Adjoints, Completeness and the Quadratic-Form Bound §adjoint), and by Finite Direct Sums of a Complex Hilbert Space: the Hilbert Structure, Coordinate Inclusions, Block Entries of Bounded Operators and Commutation with Diagonal Operators §blocks and Claim 2 (with $j=k$)

By the uniqueness in Finite Direct Sums of a Complex Hilbert Space: the Hilbert Structure, Coordinate Inclusions, Block Entries of Bounded Operators and Commutation with Diagonal Operators §blocks, $G^{*}=G$; so $G$ is an adjoint of itself and hence self-adjoint (Bounded Linear Maps between Complex Inner Product Spaces: the Least Bound, Operations, the Underlying Real Structure, Adjoints, Completeness and the Quadratic-Form Bound §adjoint-calculus). By Complex Hilbert Spaces and Bounded Linear Maps: Standing Notation §maps it remains to show that $G$ is positive semi-definite (Positive Semi-Definite Operator). We use:

(G) Let $e\in\{1,2\}$ and $D\in\mathcal{L}(\mathcal{H}_{\gamma_{e}}^{M})$ be such that, for all $r,q\in[M]$, $(D^{*}D)_{rq}\in A_{e}$ and $G_{rq}=E_{e}((D^{*}D)_{rq})$. Then $\langle\zeta,G\zeta\rangle$ is a real number $\ge0$ for every $\zeta\in\mathcal{H}_{\mu}^{M}$. Here $D^{*}$ exists as above. Put $\eta=(V_{e}\zeta_{1},\dots,V_{e}\zeta_{M})\in\mathcal{H}_{\gamma_{e}}^{M}$. By Finite Direct Sums of a Complex Hilbert Space: the Hilbert Structure, Coordinate Inclusions, Block Entries of Bounded Operators and Commutation with Diagonal Operators §blocks (twice), the identity for $\langle\zeta,E_{e}(c)\zeta'\rangle$ of the conventions, and Bounded Linear Maps between Complex Inner Product Spaces: the Least Bound, Operations, the Underlying Real Structure, Adjoints, Completeness and the Quadratic-Form Bound §adjoint-calculus,

Moreover, by Finite Direct Sums of a Complex Hilbert Space: the Hilbert Structure, Coordinate Inclusions, Block Entries of Bounded Operators and Commutation with Diagonal Operators §blocks, $(D^{*}D)_{rq}=\sum_{j=1}^{M}(D_{jr})^{*}D_{jq}$ for every $D$.

Let $K$ be the set of $k\in\mathbb{N}$ such that, for every $M\in\mathbb{N}$ and all alternating tuples $t^{1},\dots,t^{M}$ of length $k$ and a common type, the operator $G$ of the claim is positive semi-definite.

$1\in K$. Let $t^{r}=((e,a^{r}))$ for $r\in[M]$. Let $D\in\mathcal{L}(\mathcal{H}_{\gamma_{e}}^{M})$ have blocks $D_{1q}=a^{q}$ and $D_{jq}=0$ for $j\ne1$ (Finite Direct Sums of a Complex Hilbert Space: the Hilbert Structure, Coordinate Inclusions, Block Entries of Bounded Operators and Commutation with Diagonal Operators §blocks). The terms with $j\ne1$ of $\sum_{j}(D_{jr})^{*}D_{jq}$ are $0$, so by claim 7 of Properties of Finite Sums of Vectors, $(D^{*}D)_{rq}=(a^{r})^{*}a^{q}\in A_{e}$, and $G_{rq}=X_{1}(t^{r},t^{q})=E_{e}((a^{r})^{*}a^{q})$ (The Formal Amalgamated Free Product over a Common Marginal: Alternating Tuples, the Free Vector Space, the Nested-Expectation Form and the Formal Actions §nested). By (G), $G$ is positive semi-definite.

$k\in K$ implies $k+1\in K$. Let $t^{1},\dots,t^{M}$ have length $k+1$ and common type $(e_{1},\dots,e_{k+1})$; put $e=e_{k+1}$, let $a^{r}$ be the last entry of $t^{r}$, and let $s^{r}$ be the alternating tuple of length $k$ and type $(e_{1},\dots,e_{k})$ formed by the first $k$ entries of $t^{r}$. By (X) with $d=0$, $X_{k}(s^{r},s^{q})=X_{k}(t^{r},t^{q})$. Let $P\in\mathcal{L}(\mathcal{H}_{\mu}^{M})$ have blocks $P_{rq}=X_{k}(s^{r},s^{q})$; since $k\in K$ and $P$ is self-adjoint by the first paragraph, $P\ge0$. Each $P_{rq}$ lies in $N$, so commutes with $R_{p}$ for every $p\in\mathcal{P}_{n}$ (The Tracial Algebra of a Noncommutative Law and Its Trace §algebra); by Finite Direct Sums of a Complex Hilbert Space: the Hilbert Structure, Coordinate Inclusions, Block Entries of Bounded Operators and Commutation with Diagonal Operators §diagonal, $R_{p}^{(M)}\in\mathcal{L}(\mathcal{H}_{\mu}^{M})$ commutes with $P$. Let $C$ be given by Square Roots of Positive Bounded Operators on a Complex Hilbert Space, Commuting with Everything that Commutes with the Operator for $P$: $C\ge0$, $CC=P$ (Square Roots of Positive Bounded Operators on a Complex Hilbert Space, Commuting with Everything that Commutes with the Operator §square-root), and $C$ commutes with every $R_{p}^{(M)}$ (Square Roots of Positive Bounded Operators on a Complex Hilbert Space, Commuting with Everything that Commutes with the Operator §commutation). By Finite Direct Sums of a Complex Hilbert Space: the Hilbert Structure, Coordinate Inclusions, Block Entries of Bounded Operators and Commutation with Diagonal Operators §diagonal, each block $C_{rq}\in\mathcal{L}(\mathcal{H}_{\mu})$ commutes with every $R_{p}$, i.e. $C_{rq}\in N$. As $C$ is self-adjoint, it is its own adjoint (Bounded Linear Maps between Complex Inner Product Spaces: the Least Bound, Operations, the Underlying Real Structure, Adjoints, Completeness and the Quadratic-Form Bound §adjoint-calculus, Bounded Linear Maps between Complex Inner Product Spaces: the Least Bound, Operations, the Underlying Real Structure, Adjoints, Completeness and the Quadratic-Form Bound §adjoint-unique), so $C_{rq}=(C^{*})_{rq}=(C_{qr})^{*}$ and $P_{rq}=(CC)_{rq}=\sum_{j=1}^{M}(C_{jr})^{*}C_{jq}$ (Finite Direct Sums of a Complex Hilbert Space: the Hilbert Structure, Coordinate Inclusions, Block Entries of Bounded Operators and Commutation with Diagonal Operators §blocks). Let $D\in\mathcal{L}(\mathcal{H}_{\gamma_{e}}^{M})$ have blocks $D_{jq}=\pi_{e}(C_{jq})a^{q}\in A_{e}$. Then, using the properties of $\pi_{e}$ and claim 4 of Properties of Finite Sums of Vectors for the linear map $T\mapsto(a^{r})^{*}\pi_{e}(T)a^{q}$ on $N$,

and $G_{rq}=X_{k+1}(t^{r},t^{q})=E_{e}\bigl((a^{r})^{*}\pi_{e}(X_{k}(t^{r},t^{q}))a^{q}\bigr)=E_{e}((D^{*}D)_{rq})$. By (G), $G$ is positive semi-definite, so $k+1\in K$.

By Principle of Induction for the Natural Numbers, $K=\mathbb{N}$; with self-adjointness, $G\ge0$.

Claim 4 (the form). (H) For $\xi,\eta\in\mathcal{F}$ and nonempty finite sets $F\supseteq\operatorname{supp}\xi$, $F'\supseteq\operatorname{supp}\eta$,

If $\xi=0$ or $\eta=0$, every term vanishes and both sides are $0$ (Sums over Finite Index Sets: Finite Unions, Disjoint Unions, Vanishing Terms, Dependent Pairs, Conjugation and the Modulus §vanishing, The Formal Amalgamated Free Product over a Common Marginal: Alternating Tuples, the Free Vector Space, the Nested-Expectation Form and the Formal Actions §form). Otherwise, for each $s$ the terms with $t\notin\operatorname{supp}\eta$ vanish, and for $s\notin\operatorname{supp}\xi$ the whole inner sum vanishes; two applications of Sums over Finite Index Sets: Finite Unions, Disjoint Unions, Vanishing Terms, Dependent Pairs, Conjugation and the Modulus §vanishing reduce the right side to the defining double sum over $\operatorname{supp}\xi\times\operatorname{supp}\eta$.

Linearity in the second argument. With $F=F_{\xi}$ and $F'=F_{\eta}\cup F_{\zeta}$, which contains $\operatorname{supp}\eta$, $\operatorname{supp}\zeta$ and $\operatorname{supp}(\eta+\zeta)$ (The Formal Amalgamated Free Product over a Common Marginal: Alternating Tuples, the Free Vector Space, the Nested-Expectation Form and the Formal Actions §space) and is finite by claim 3 of Peeling an Element off a Finite Set, and Unions of Finite Sets, (H) and (S) give

Likewise, with $F'=F_{\eta}\supseteq\operatorname{supp}(c\eta)$, (H) and (S) give $h(\xi,c\eta)=c\,h(\xi,\eta)$.

Hermitian symmetry. First, $h_{0}(t,s)=\overline{h_{0}(s,t)}$ for all labels $s,t$. For $N$-labels $s=(0,x)$, $t=(0,y)$, by The Tracial Algebra of a Noncommutative Law: a Norm-Closed Unital *-Algebra with a Faithful Positive Trace, Determined by Vacuum Vectors, Closed under Square Roots §trace, $h_{0}(t,s)=\tau_{\mu}(y^{*}x)=\tau_{\mu}((x^{*}y)^{*})=\overline{\tau_{\mu}(x^{*}y)}$. For tuples of the same length $k$ and type, by Claim 2 and The Tracial Algebra of a Noncommutative Law: a Norm-Closed Unital *-Algebra with a Faithful Positive Trace, Determined by Vacuum Vectors, Closed under Square Roots §trace, $h_{0}(t,s)=\tau_{\mu}(X_{k}(s,t)^{*})=\overline{\tau_{\mu}(X_{k}(s,t))}$. For all other pairs both values are $0$, as the condition in (Z) is symmetric. Now take $F=F_{\xi}$, $F'=F_{\eta}$. By (H), claim 5 of Peeling, Splitting, and Interchange for Sums over a Finite Index Set (interchange), and Sums over Finite Index Sets: Finite Unions, Disjoint Unions, Vanishing Terms, Dependent Pairs, Conjugation and the Modulus §conjugate with the rules for conjugates of products,

Basis values. $\delta_{s},\delta_{t}\ne0$ with supports $\{s\}$, $\{t\}$, so by The Formal Amalgamated Free Product over a Common Marginal: Alternating Tuples, the Free Vector Space, the Nested-Expectation Form and the Formal Actions §form and claim 1 of Peeling, Splitting, and Interchange for Sums over a Finite Index Set, $h(\delta_{s},\delta_{t})=\overline{1}\cdot1\cdot h_{0}(s,t)=h_{0}(s,t)$.

Positivity. If $\xi=0$, then $h(\xi,\xi)=0$. Let $\xi\ne0$, $F=\operatorname{supp}\xi$, and $f(s,t)=\overline{\xi(s)}\,\xi(t)\,h_{0}(s,t)$. Let $\kappa((0,x))=0$ and $\kappa(t)=(k,\text{type of }t)$ for a tuple $t$ of length $k$; by (Z), $h_{0}(s,t)=0$ if $\kappa(s)\ne\kappa(t)$. The set $\Gamma=\{\kappa(s):s\in F\}$ is nonempty and finite (claim 4 of Basic Properties of Finite Sets), and each $F_{\gamma}=\{s\in F:\kappa(s)=\gamma\}$, $\gamma\in\Gamma$, is nonempty and finite. For $s\in F_{\gamma}$, $\sum_{t\in F}f(s,t)=\sum_{t\in F_{\gamma}}f(s,t)$ by Sums over Finite Index Sets: Finite Unions, Disjoint Unions, Vanishing Terms, Dependent Pairs, Conjugation and the Modulus §vanishing. The map $(\gamma,s)\mapsto s$ is a bijection from the set of pairs $(\gamma,s)$ with $\gamma\in\Gamma$, $s\in F_{\gamma}$ onto $F$ (inverse $s\mapsto(\kappa(s),s)$), so by Sum over a Finite Index Set (composing bijections) and Sums over Finite Index Sets: Finite Unions, Disjoint Unions, Vanishing Terms, Dependent Pairs, Conjugation and the Modulus §pairs,

Each $Q_{\gamma}$ is a real number $\ge0$. Enumerate $F_{\gamma}$ by a bijection from $[M]$ and compute the sums along it (Sum over a Finite Index Set). If $\gamma=0$, write $F_{0}=\{(0,x_{1}),\dots,(0,x_{M})\}$ and $c_{r}=\xi((0,x_{r}))$; by The Tracial Algebra of a Noncommutative Law and Its Trace §trace, the defining property of the adjoint, and claim 2 of Elementary Properties of a Complex Inner Product, $\overline{c_{r}}c_{q}\tau_{\mu}(x_{r}^{*}x_{q})=\overline{c_{r}}c_{q}\langle x_{r}\Omega_{\mu},x_{q}\Omega_{\mu}\rangle=\langle y_{r},y_{q}\rangle$ with $y_{r}=c_{r}x_{r}\Omega_{\mu}$, so by claim 5 of Properties of Finite Sums of Vectors (twice) $Q_{0}=\langle y,y\rangle=\lVert y\rVert^{2}\ge0$ with $y=\sum_{r=1}^{M}y_{r}$. If $\gamma=(k,e)$, write $F_{\gamma}=\{t^{1},\dots,t^{M}\}$, tuples of length $k$ and common type $e$, and $c_{r}=\xi(t^{r})$; with $G$ as in Claim 3 and $\zeta=(c_{1}\Omega_{\mu},\dots,c_{M}\Omega_{\mu})\in\mathcal{H}_{\mu}^{M}$, The Tracial Algebra of a Noncommutative Law and Its Trace §trace, claim 2 of Elementary Properties of a Complex Inner Product and Finite Direct Sums of a Complex Hilbert Space: the Hilbert Structure, Coordinate Inclusions, Block Entries of Bounded Operators and Commutation with Diagonal Operators §blocks give

a real number $\ge0$ by Claim 3 and Positive Semi-Definite Operator. Hence $h(\xi,\xi)$ is a sum of nonnegative real numbers, a real number $\ge0$ by Nonnegativity and Monotonicity of a Sum over a Finite Index Set §nonnegative.

Claim 5 (formal actions). Write $\rho_{b}=\rho_{\varepsilon,b}$, $\ell(b)=\ell_{\varepsilon}(b)$, $\pi=\pi_{\varepsilon}$, $E=E_{\varepsilon}$. (L) For $\xi\in\mathcal{F}$ and nonempty finite $F\supseteq\operatorname{supp}\xi$, $\ell(b)\xi=\sum_{u\in F}\xi(u)\rho_{b}(u)$: at each label the terms with $u\notin\operatorname{supp}\xi$ vanish, so by Sums over Finite Index Sets: Finite Unions, Disjoint Unions, Vanishing Terms, Dependent Pairs, Conjugation and the Modulus §vanishing the value agrees with The Formal Amalgamated Free Product over a Common Marginal: Alternating Tuples, the Free Vector Space, the Nested-Expectation Form and the Formal Actions §actions (both are $0$ if $\xi=0$). With $F=F_{\xi}\cup F_{\eta}$, (L) and (S) evaluated at each label give $\ell(b)(\xi+\eta)=\ell(b)\xi+\ell(b)\eta$; with $F=F_{\xi}$ they give $\ell(b)(c\xi)=c\,\ell(b)\xi$. So $\ell(b)$ is linear (Linear Map, Claim 1). By (L) with $F=\{u\}$ and claim 1 of Peeling, Splitting, and Interchange for Sums over a Finite Index Set, $\ell(b)\delta_{u}=\rho_{b}(u)$.

(B) Let $U,W$ be nonempty finite sets, $c:U\to\mathbb{C}$, $d:W\to\mathbb{C}$, $\varphi:U\to\mathcal{F}$, $\psi:W\to\mathcal{F}$. Then

Let $S$ be the union of $\{o\}$, of the sets $\operatorname{supp}\varphi(u)$ and of the sets $\operatorname{supp}\psi(w)$; it is finite by Sums over Finite Index Sets: Finite Unions, Disjoint Unions, Vanishing Terms, Dependent Pairs, Conjugation and the Modulus §finite-union and claims 1 and 3 of Peeling an Element off a Finite Set, and Unions of Finite Sets, and it contains the supports of both combinations (The Formal Amalgamated Free Product over a Common Marginal: Alternating Tuples, the Free Vector Space, the Nested-Expectation Form and the Formal Actions §space). Apply (H) with $F=F'=S$ to the left side; expand the conjugate of the first combination at $s$ by Sums over Finite Index Sets: Finite Unions, Disjoint Unions, Vanishing Terms, Dependent Pairs, Conjugation and the Modulus §conjugate, multiply out by (S), interchange the sums over $S$ with those over $U$ and $W$ (claim 5 of Peeling, Splitting, and Interchange for Sums over a Finite Index Set), and pull out $\overline{c(u)}d(w)$ by (S); the remaining double sum over $S\times S$ is $h(\varphi(u),\psi(w))$ by (H).

(D2) For labels $u_{1},u_{2},v$: $h(\delta_{u_{1}}+\delta_{u_{2}},\delta_{v})=h_{0}(u_{1},v)+h_{0}(u_{2},v)$ and $h(\delta_{v},\delta_{u_{1}}+\delta_{u_{2}})=h_{0}(v,u_{1})+h_{0}(v,u_{2})$. The second is additivity and the basis values of Claim 4; the first follows from it by Hermitian symmetry and $h_{0}(u,v)=\overline{h_{0}(v,u)}$ (Claim 4).

Reduction. Let $\xi,\eta\in\mathcal{F}$. By (E), (L), (B) (with $U=F_{\xi}$, $W=F_{\eta}$) and $b^{*}\in A_{\varepsilon}$,

so it suffices to prove, for all labels $u,v$, the statement $(\star)(u,v)$: $h(\rho_{b}(u),\delta_{v})=h(\delta_{u},\rho_{b^{*}}(v))$ for every $b\in A_{\varepsilon}$. If $(\star)(u,v)$ holds, so does $(\star)(v,u)$: for $b\in A_{\varepsilon}$, $(\star)(u,v)$ for $b^{*}$ gives $h(\rho_{b^{*}}(u),\delta_{v})=h(\delta_{u},\rho_{b}(v))$ (as $b^{**}=b$), and conjugating with Hermitian symmetry gives $h(\delta_{v},\rho_{b^{*}}(u))=h(\rho_{b}(v),\delta_{u})$. Every label is an $N$-label, a tuple whose type starts with $\varepsilon$, or one whose type starts with $\bar{\varepsilon}$; so it suffices to treat the six cases below. Each side is evaluated by The Formal Amalgamated Free Product over a Common Marginal: Alternating Tuples, the Free Vector Space, the Nested-Expectation Form and the Formal Actions §actions and (D2), and terms are discarded by (Z).

Case $u=(0,x)$, $v=(0,y)$. Left side: $h_{0}((0,E(b\pi(x))),(0,y))=\tau_{\mu}(E(b\pi(x))^{*}y)=\tau_{\mu}(x^{*}E(b^{*})y)$, since $E(b\pi(x))^{*}=E(\pi(x^{*})b^{*})=x^{*}E(b^{*})$. Right side: $h_{0}((0,x),(0,E(b^{*}\pi(y))))=\tau_{\mu}(x^{*}E(b^{*})y)$. The pairings involving the $1$-tuples vanish.

Case $u=(0,x)$, $v=t=(a_{1},\dots,a_{k})$, type starting with $\varepsilon$. If $k\ge2$, both sides vanish: $\rho_{b}(u)$ consists of a $1$-tuple and an $N$-label, and $\rho_{b^{*}}(t)$ of two tuples. If $k=1$, by (C) (as $a_{1}\in A_{\varepsilon}^{\circ}$) the left side is

and the right side is $h_{0}((0,x),(0,E(b^{*}a_{1})))=\tau_{\mu}(x^{*}E(b^{*}a_{1}))$.

Case $u=(0,x)$, $v=t$ with type starting with $\bar{\varepsilon}$. The $1$-tuple in $\rho_{b}(u)$ has type $(\varepsilon)$, and $\rho_{b^{*}}(t)$ consists of two tuples; both sides are $0$.

Case $u=s=((e_{1},a_{1}),\dots,(e_{k},a_{k}))$, $v=t=((e'_{1},a'_{1}),\dots,(e'_{l},a'_{l}))$, $e_{1}=e'_{1}=\varepsilon$. By clause (c), $\rho_{b}(s)=\delta_{s'}+\delta_{w}$ with $s'=((\varepsilon,(ba_{1})^{\circ}),(e_{2},a_{2}),\dots,(e_{k},a_{k}))$ of the type of $s$, and $w$ an $N$-label ($k=1$) or a tuple of type starting with $e_{2}=\bar{\varepsilon}$; likewise $\rho_{b^{*}}(t)=\delta_{t'}+\delta_{w'}$ with $t'=((\varepsilon,(b^{*}a'_{1})^{\circ}),(e'_{2},a'_{2}),\dots)$ of the type of $t$. So the left side is $h_{0}(s',t)$ and the right side $h_{0}(s,t')$, both $0$ unless $l=k$ and $s,t$ have the same type. In that case, by (C) (as $a_{1},a'_{1}\in A_{\varepsilon}^{\circ}$), $X_{1}(s',t)=E(a_{1}^{*}b^{*}a'_{1})=X_{1}(s,t')$, and the pairs $(s',t)$, $(s,t')$ have the same entries in positions $j\ge2$; so $X_{k}(s',t)=X_{k}(s,t')$ by (X) with $d=0$, and the sides agree.

Case $u=s$ as before ($e_{1}=\varepsilon$), $v=t=((e'_{1},a'_{1}),\dots,(e'_{l},a'_{l}))$, $e'_{1}=\bar{\varepsilon}$. With $\rho_{b}(s)=\delta_{s'}+\delta_{w}$ as before, $h_{0}(s',t)=0$. By clause (b), $\rho_{b^{*}}(t)=\delta_{t^{+}}+\delta_{t^{-}}$ with $t^{+}=((\varepsilon,(b^{*})^{\circ}),(e'_{1},a'_{1}),\dots,(e'_{l},a'_{l}))$ and $t^{-}$ of the type of $t$, so $h_{0}(s,t^{-})=0$. The left side is $h_{0}(w,t)$, the right side $h_{0}(s,t^{+})$. If $k\ge2$, $w=((e_{2},\pi_{e_{2}}(E(ba_{1}))a_{2}),(e_{3},a_{3}),\dots,(e_{k},a_{k}))$ has length $k-1$ and type $(e_{2},\dots,e_{k})$; so both sides vanish unless ($\dagger$) $k=l+1$ and $(e_{2},\dots,e_{k})=(e'_{1},\dots,e'_{l})$ (if $k=1$, $w$ is an $N$-label and ($\dagger$) fails as $l\ge1$). Under ($\dagger$), by (C) (as $a_{1}\in A_{\varepsilon}^{\circ}$) $X_{1}(s,t^{+})=E(a_{1}^{*}b^{*})$, so, as $E(ba_{1})^{*}=E(a_{1}^{*}b^{*})$,