The form is linear in the second argument because \(\omega \) is.

It is conjugate-linear in the first because \((\lambda x)^*=\overline \lambda \,x^*\).

It is Hermitian because \(\langle y,x\rangle \) equals \(\omega ((x^*y)^*)\), and Hermitian positivity makes that the conjugate of \(\omega (x^*y)\). The square \(\langle x,x\rangle =\omega (x^*x)\) is nonnegative by the state.

The inequality of Cauchy and Schwarz is \(\lvert \langle x,y\rangle \rvert ^2\le \langle x,x\rangle \langle y,y\rangle \). Over \(\mathbb C\), if \(\langle x,y\rangle \) is not zero, choose a scalar \(u\) of modulus \(1\) with \(u\langle x,y\rangle =\lvert \langle x,y\rangle \rvert \), and replace \(y\) by \(uy\). The new square \(\langle y,y\rangle \) is unchanged, and the new inner product is real and nonnegative. Over \(\mathbb R\) no phase is required. For every real \(t\), \[\langle x+ty,x+ty\rangle =\langle x,x\rangle +2t\langle x,y\rangle +t^2\langle y,y\rangle \ge 0.\] If \(\langle y,y\rangle =0\), the values \(2t\langle x,y\rangle \) cannot stay above \(- \langle x,x\rangle \) for every real \(t\) unless \(\langle x,y\rangle =0\). If \(\langle y,y\rangle >0\), complete the square. The same quadratic is \[\langle y,y\rangle \Bigl (t+\frac {\langle x,y\rangle }{\langle y,y\rangle }\Bigr )^2 +\langle x,x\rangle -\frac {\langle x,y\rangle ^2}{\langle y,y\rangle }.\] The squared term can be made zero, so the remaining term is nonnegative. Thus the inequality holds. Over \(\mathbb C\), putting the unimodular factor back into \(y\) multiplies \(\langle x,y\rangle \) by a scalar of modulus \(1\) and does not change \(\langle y,y\rangle \).

If \(\langle x,x\rangle =0\), the inequality forces \(\langle x,y\rangle =0\) for every \(y\). Conversely the case \(y=x\) shows that the radical is exactly \(N\). It is a subspace. If \(x,y\in N\) and \(\lambda \in K\), then \[\begin {aligned} \langle x+\lambda y,x+\lambda y\rangle ={}&\langle x,x\rangle +\lambda \langle x,y\rangle \\ &+\overline {\lambda }\langle y,x\rangle +\lvert \lambda \rvert ^2\langle y,y\rangle . \end {aligned}\] The two squares vanish because \(x,y\in N\). The two cross terms vanish because an element of \(N\) is orthogonal to every vector. It is a left ideal. For \(b\in A\) and \(x\in N\), \(\langle bx,bx\rangle =\omega (x^*b^*bx)=\langle x,(b^*b)x\rangle =0\).

The form therefore descends to the quotient. If \(x-x'\) and \(y-y'\) lie in \(N\), then \(\langle x,y\rangle -\langle x',y'\rangle =\langle x-x',y\rangle +\langle x',y-y'\rangle \). The first summand vanishes because \(x-x'\) is in the radical. The second is the conjugate of \(\langle y-y',x'\rangle \), which vanishes for the same reason. The descended form is positive definite, and finite dimensionality makes the quotient a Hilbert space with no further completion. Its dimension is \(\dim A-\dim N\).

On a basis \(e_1,\ldots ,e_n\), the matrix \(G_{ij}=\langle e_i,e_j\rangle =\omega (e_i^*e_j)\) is Hermitian. A vector \(v\) represents \(x=\sum _i v_i e_i\). Hermitian symmetry gives \(G_{ji}=\overline {G_{ij}}\). The number \(\langle x,e_j\rangle =\sum _i\overline {v_i}G_{ij}\) vanishes for every \(j\) if and only if \(x\in N\): the forward direction was proved for every vector, and the converse is linearity in the second argument. Conjugating those sums and replacing \(\overline {G_{ij}}\) by \(G_{ji}\) produces \((Gv)_j=0\). Rank-nullity gives \(\operatorname {rank} G=n-\dim N=\dim H_\omega \). The class of \(a\) has squared length \(\omega (a^*a)\). The operator \(\pi _\omega (a)\) is well defined because \(N\) is a left ideal, and \(\langle \pi _\omega (a)\Omega ,\pi _\omega (b)\Omega \rangle =\langle a,b\rangle =\omega (a^*b)\).

On the direct sum, the product and the involution act blockwise, so \(\omega (a^*a)=\sum _i\mathrm {Tr}(\rho _i a_i^*a_i)\). The trace is invariant under a cyclic permutation, and \(\mathrm {Tr}(b^*b)\) is the sum of the squared moduli of the entries of \(b\). Hence \[\mathrm {Tr}(\rho _i a_i^*a_i) =\mathrm {Tr}(c_i a_i^*a_i c_i^*) =\mathrm {Tr}\bigl ((a_i c_i^*)^*(a_i c_i^*)\bigr ),\] which is nonnegative. The functional is therefore positive. It is normalized because \(\omega (1)=\sum _i\mathrm {Tr}(\rho _i)=1\). Each \(\rho _i=c_i^*c_i\) is self-adjoint. The trace of a conjugate transpose is the conjugate of the trace, and \((a_i\rho _i)^*=\rho _i a_i^*\), so \(\mathrm {Tr}(\rho _i a_i^*)=\overline {\mathrm {Tr}(\rho _i a_i)}\). Thus \(\omega \) is Hermitian.

The same identity shows that \(\omega (a^*a)=0\) if and only if \(a_i c_i^*=0\) for every \(i\). Different blocks occupy complementary summands, so \(\dim N=\sum _i\dim \{a_i:a_i c_i^*=0\}\). A matrix vanishes on a subspace precisely when it factors through the quotient by that subspace. The image of \(c_i^*\) has dimension \(\operatorname {rank} c_i^*\). The matrices vanishing on it are determined by their values on a complement, so their space has dimension \(m_i\bigl (m_i-\operatorname {rank} c_i^*\bigr )\). The quotient of that block therefore has dimension \(m_i\operatorname {rank} c_i^*\). Summing over the blocks gives \(\dim H_\omega =\sum _i m_i\operatorname {rank} c_i^*\).

It remains to match that rank with \(\operatorname {rank}\rho _i\). For the standard inner product, \(\|c_i v\|^2=\langle c_i^*c_i v,v\rangle \). If \(c_i^*c_i v=0\), the right-hand side vanishes, so \(c_i v=0\). The converse is immediate, and rank-nullity gives \(\operatorname {rank}\rho _i=\operatorname {rank} c_i\). A minor of a transpose is the transpose of a minor, and the determinant is unchanged by transposition. A minor of a conjugate transpose is the conjugate of a minor of the transpose. The largest size of a nonzero minor is therefore the same for \(c_i\), \(c_i^T\) and \(c_i^*\). Hence \(\operatorname {rank} c_i^*=\operatorname {rank}\rho _i\), and \(\dim H_\omega =\sum _i m_i\operatorname {rank}\rho _i\). On \(M_2\), \(\mathrm {diag}(2/3,1/3)\) is the square of \(\mathrm {diag}(\sqrt {2/3},\sqrt {1/3})\), so its rank is \(2\). \(\mathrm {diag}(1,0)\) is the square of \(\mathrm {diag}(1,0)\), and its only nonzero minor has size \(1\). The formula gives dimensions \(4\) and \(2\).

On functions, the indicator basis is orthogonal for the Gram form. Indeed \(\omega (1_x^*1_y)=\delta _{xy}w(x)\), so the Gram matrix is diagonal with entries \(w(x)\). Its rank is the number of strictly positive weights. A function lies in \(N\) exactly when it vanishes on \(\operatorname {supp} w\), because \(\omega (f^*f)=\sum _x w(x)\lvert f(x)\rvert ^2\). Two functions determine the same class exactly when they agree on that support, and every function on the support arises in this way. The descended inner product is \[\langle f,g\rangle =\sum _{w(x)>0}w(x)\overline {f(x)}\,g(x).\] Every function on a finite set is square-summable, so the space is \(\ell ^2(\operatorname {supp} w)\).

The constant \(1\) does not involve the residual indeterminates, and the Wick value of \(1\) is \(1\), so \(E_R(1)=1\). A polynomial \(g\in A[x_R]\) is a coefficient for the residual Wick functional. That functional is linear over \(A[x_R]\), hence \(E_R(gf)=gE_R(f)\). The polynomial ring is commutative, so the two sides of the bimodule identity agree. The moment theorem gives \(\omega _Q(h)=\omega _Q(E_R(h))\) for every polynomial \(h\). Taking \(h=gf\) yields \(\omega _Q(gE_R(f))=\omega _Q(gf)\). The image lies in \(A[x_R]\) by that same theorem.

Apply the moment theorem to the partition \((R',U')\). The residual \(z'=x_{U'}+L'x_{R'}\) is uncorrelated with \(x_{R'}\), and its covariance is \(Q_{U'U'}^{-1}\). The same theorem, applied to the invertible precision \(S'\) and the partition \((R,V)\), produces a residual \(z_V\) in the variables \(x_{R'}\) whose covariance is \((S')_{VV}^{-1}\) and which is uncorrelated with \(x_R\). Second moments of polynomials in \(x_{R'}\) agree under \(\omega _Q\) and under the Wick state of \(S'\), so these two covariances are the moments of \(\omega _Q\). Since \(z_V\) is linear in \(x_{R'}\) and \(z'\) is uncorrelated with \(x_{R'}\), one has \(\omega _Q(z_Vz')=0\).

The moment theorem defines the Schur complement after eliminating \(U'\) by \(S'=Q_{R'R'}-Q_{R'U'}Q_{U'U'}^{-1}Q_{U'R'}\). Its block on \(V\) is therefore \((S')_{VV}=Q_{VV}-Q_{VU'}Q_{U'U'}^{-1}Q_{U'V}\). The same expression is the Schur complement of the invertible block \(Q_{U'U'}\) inside \(Q_{UU}\). That theorem says that, once the eliminated block is invertible, the block matrix is invertible if and only if that Schur complement is. Both are invertible, so \(Q_{UU}\) is invertible, and the one-step map \(E_R\) is defined. Substitute \[x_V=B_Vx_R+z_V\] and then \[x_{U'}=B'x_{R'}+z'.\] The second substitution expands to a retained linear form plus \(B'_Vz_V+z'\). In residual coordinates the change of variables is \[z_U= \begin {pmatrix}I&0\\ B'_V&I\end {pmatrix} \begin {pmatrix}z_V\\ z'\end {pmatrix}.\] The triangular factor has determinant \(1\) and an inverse over \(A\). Both \(z_V\) and \(z'\) are uncorrelated with \(x_R\), so the residual is uncorrelated with \(x_R\). Its retained coefficient is therefore the regression of the moment theorem: the covariance \(C_{RR}\) is invertible, and \(C(x_U,x_R)=BC_{RR}\) determines that coefficient. The one-step residual \(z_U\) is this triangular image.

A pairing in the joint residual that joins \(z_V\) to \(z'\) contributes \(0\). Every surviving pairing is a \(z_V\) pairing times a \(z'\) pairing, so the joint Wick average is the iterated average. The polynomial obtained after the two substitutions is the same polynomial of \(z_U\), and Isserlis' rule depends only on the pairwise covariances of those linear forms. Substitution of \(x_V=B_Vx_R+z_V\) is a ring homomorphism, and the residual Wick functional is linear on coefficients, so the \(z'\) average commutes with that substitution. The average in \(z'\) alone is \(E_{R'}(f)\). Once that polynomial no longer involves \(z'\), the one-step residual average uses only \(z_V\), with covariance \((S')_{VV}^{-1}\). On \(A[x_{R'}]\) that average is \(E_R\). The iterated average is therefore \(E_R(E_{R'}(f))\), and it equals \(E_R(f)\).

For the Grassmann state, the exponential is a sum of even elements. An even element commutes with every homogeneous element, by the Grassmann algebra. The eliminated top word is even, so passing it through the retained polynomial \(F\) contributes no sign. The partial coefficient formula therefore gives \[J_U(F e^{-\bar \psi K\psi }) =\det (D)\,F e^{-\bar \psi _R S\psi _R}.\] Applying \(J_R\) and dividing by \(\det K=\det (D)\det S\) produces \(\omega _S(F)\). The scalar conventions of the empty blocks remain those of the partial formula.