Dual Gram Kernels

Abstract

The two Gram kernels equal the observation and adjoint kernels.

Theorem 1.1 (The state and protocol Gram kernels are exact).

$$\begin{array}{r}\forall K,V,iota:\mathrm{Type},\\ [\mathrm{RCLike}(K)],[\mathrm{NormedAddCommGroup}(V)],[\mathrm{InnerProductSpace}(K,V)],\\ [\mathrm{FiniteDimensional}(K,V)],[\mathrm{Fintype}(iota)],\\ \forall ell:iota\to \mathrm{LinearMap}(K,V,K),\\ letM:\mathrm{LinearMap}(K,V,\mathrm{PiLp}(2,iota\to K))=\mathrm{comp}(\mathrm{toLinearMap}(\mathrm{symm}(\mathrm{withLpLinearEquiv}(2,K,iota\to K))),\mathrm{linearPi}(ell));\\ \ker (\mathrm{comp}(\mathrm{adjoint}(M),M))=\ker (M)\wedge \\ \ker (\mathrm{comp}(M,\mathrm{adjoint}(M)))=\ker (\mathrm{adjoint}(M)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/LinearMemory/DualGramKernels.dual_gram_kernels (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let a finite indexed family assign a scalar linear readout to every protocol. The observation map is constructed coordinatewise on the same square-summable protocol carrier as the visible-range companion.

The kernel of the adjoint-observation composition is exactly the unseen state kernel. Reversing the composition gives exactly the kernel of the adjoint, which records redundant protocol combinations.

Both clauses directly apply the pinned library’s exact finite-dimensional adjoint-composition kernel lemmas.

References

• Truth anchor: D5/S3/Observer/LinearMemory/DualGramKernels.dual_gram_kernels
• Dependency: D5/S3/Observer/LinearMemory/DualGramVisibleRanges