Theorem. Wick states over a ring [fdip-008N]

Let \(A\) be a commutative ring in which \(2\) is a unit, and let \(Q\) be a symmetric \(n\times n\) matrix over \(A\) with an inverse \(C=Q^{-1}\) in \(M_n(A)\). Write \(A[x]=A[x_1,\ldots ,x_n]\). The Wick functional \(\omega _Q\) is the \(A\)-linear map \(A[x]\to A\) with \(\omega _Q(1)=1\) determined by Isserlis' pairing rule. On a product of an odd number of factors the value is \(0\). On a product of \(2m\) factors, not necessarily distinct, sum over the pairings of those \(2m\) factor positions the product of the \(m\) entries of \(C\) on the paired positions. There are \((2m-1)!!\) such pairings, so \(\omega _Q(x_i^4)=3C_{ii}^2\). The value depends only on those entries. It uses no order on \(A\) and no measure on \(A^n\). The same pairing rule is the one applied to centered real Gaussians in the quartic elimination, which cites [etingof2024mathematical, v2, Theorem 3.1 and Example 3.2, p. 29] for these contractions. Here the rule is the definition of \(\omega _Q\).

Order the coordinates as a retained set \(R\) and an eliminated set \(U\), and assume that the block \(Q_{UU}\) is invertible over \(A\). Define \[\begin {aligned} L&=Q_{UU}^{-1}Q_{UR},\\ B&=-L,\\ S&=Q_{RR}-Q_{RU}L. \end {aligned}\] Symmetry of \(Q\) makes \(S\) symmetric. For \(f\in A[x]\), substitute \(x_U=Bx_R+z\) and apply the Wick functional of covariance \(Q_{UU}^{-1}\) in the indeterminates \(z\), treating the retained variables as coefficients. Call the result \(E[f\mid x_R]\in A[x_R]\).

The block \(S\) is invertible, and \(C_{RR}=S^{-1}\). Restriction of \(\omega _Q\) to \(A[x_R]\) is the Wick functional \(\omega _S\). Furthermore \(E[f\mid x_R]\) is a polynomial and \[\omega _Q(f)=\omega _S(E[f\mid x_R]).\] The identity \(2^{-1}x^TQx=2^{-1}z^TQ_{UU}z+2^{-1}x_R^TSx_R\), with \(z=x_U-Bx_R\), is the quadratic completion that names these blocks. The moment proof does not integrate that quadratic.

The correspondence with formal libraries is partial. Mathlib's Matrix.fromBlocks_eq_of_invertible₂₂ is the block factorization over a commutative ring, and Matrix.isUnit_fromBlocks_iff_of_invertible₂₂ is the criterion that, once the eliminated block is invertible, the matrix is a unit if and only if the Schur complement is. Matrix.det_fromBlocks₂₂ is the determinant identity. No Mathlib or TauCeti declaration supplies the Isserlis pairing rule or the tower identity over a commutative ring. TauCeti's Matrix.PosDef.gaussianCondCov is the real positive-definite case only, as already recorded for the real elimination theorem.

On the four-cycle matrix of the chapter, \(Q_{UU}=\begin {pmatrix}3&-1\\-1&3\end {pmatrix}\) has determinant \(8\), and \[B=\frac 18\begin {pmatrix}1&3\\3&1\end {pmatrix},\qquad \det S=45/8.\] The product of the determinants is \(\det Q_{UU}\cdot \det S=45=\det Q\). Take \(f=x_2^2x_3x_0+x_2^3x_1\). Exact rational evaluation of the two Wick functionals gives \(\omega _Q(f)=\omega _S(E[f\mid x_R])=32/75\). The conditional expectation lies in \(\mathbb Q[x_0,x_1]\).

The rule is not the odd Wick rule, whose matrix is alternating and whose value is a Pfaffian. It defines no measure on \(A^n\), no finite-field character sum, and no Euler product. Characteristic \(2\) is outside the hypothesis; the half-turn example is the place where an algebra in that characteristic is treated. Nothing here evaluates the real normalizer or compares these moments with the logarithm of a determinant.