Proposition. Elimination with orthogonal perfect pairings [fdip-001X]
✍️source

  • October 23, 2026

Let \(X,Y\) be unital modules over a commutative unital ring \(R\), with chosen perfect symmetric pairings \(b_X,b_Y\). On the chosen sum \(M=X\oplus Y\), choose the orthogonal sum form \[b_M((x,y),(x',y'))=b_X(x,x')+b_Y(y,y').\] It is perfect and symmetric, and its injection/projection adjoints are \[\iota _X^\dagger =\pi _X,\quad \pi _X^\dagger =\iota _X,\qquad \iota _Y^\dagger =\pi _Y,\quad \pi _Y^\dagger =\iota _Y.\] Suppose \(Q:M\to M\) is self-adjoint, with components \(A,B,E,C\) and invertible \(C\). Then \[A^\dagger =A,\quad C^\dagger =C,\quad E=B^\dagger ,\qquad S^\dagger =S\quad \text {for }S=A-BC^{-1}E.\] For the triangular factors, \[V^\dagger =U,\qquad Q=V^\dagger DV,\qquad D(x,y)=(Sx,Cy).\] Consequently, with \(K=C^{-1}E\), \[\begin {aligned} b_M((x,y),Q(x,y)) &=b_X(x,Sx)\\ &\quad +b_Y(y+Kx,C(y+Kx)). \end {aligned}\]

Proof. 

  • October 23, 2026

Bilinearity and symmetry of \(b_M\) follow termwise. For a linear functional \(\ell :M\to R\), represent \(\ell \iota _X\) and \(\ell \iota _Y\) uniquely by \(x_\ell \in X,y_\ell \in Y\) using the two perfect pairings. Then for every \((x,y)\), \[\ell (x,y)=\ell \iota _X(x)+\ell \iota _Y(y) =b_X(x,x_\ell )+b_Y(y,y_\ell ).\] This gives a representative \((x_\ell ,y_\ell )\). Uniqueness follows by testing \((x,0)\) and \((0,y)\) separately. The representative depends linearly on \(\ell \), since the two inverse duality maps are linear. Thus the currying map of \(b_M\) is a linear isomorphism.

For example, \(b_M(\iota _Xx,(u,v))=b_X(x,u)=b_X(x,\pi _X(u,v))\). Adjoint uniqueness and involution give the two \(X\) identities, and the same calculation gives those for \(Y\). Adjointing the definitions of the 4 components and using \(Q^\dagger =Q\) gives \(A^\dagger =A\), \(C^\dagger =C\) and \(B^\dagger =E\). The inverse-adjoint law then gives \((C^{-1})^\dagger =C^{-1}\) and \[K^\dagger =(C^{-1}E)^\dagger =BC^{-1},\qquad (BC^{-1}E)^\dagger =BC^{-1}E.\] The latter identity proves \(S^\dagger =S\).

For \(z=(x,y)\) and \(w=(u,v)\), \[\begin {aligned} b_M(Vz,w) &=b_X(x,u)+b_Y(y+Kx,v)\\ &=b_X(x,u+K^\dagger v)+b_Y(y,v)\\ &=b_M(z,Uw). \end {aligned}\] Uniqueness gives \(V^\dagger =U\); factorization yields \(Q=V^\dagger DV\). Finally \(b_M(z,Qz)=b_M(Vz,DVz)\), and expanding the orthogonal sum form gives the stated identity.

This is a direct deduction from chosen dualities and triangular factorization. The real symmetric completion in [boyd2004convex, Appendix A.5.5, p. 650] is its real coordinate specialization. The chosen orthogonal sum is essential: an arbitrary perfect form on \(M\) need not have these injection/projection adjoints. No division by two or recovery of bilinear data from diagonal values is used; the identity remains valid in characteristic two.

TauCeti's LinearMap.BilinForm.prod gives the orthogonal product form, and LinearMap.BilinForm.nondegenerate_prod_iff identifies its radical nondegeneracy. The functional-splitting proof above also proves the surjectivity required for perfection. These declarations alone do not assert the paired-congruence result.