Adjoint-Kernel Redundancy

Abstract

The adjoint kernel is exactly the space of redundant protocol coefficients.

Theorem 1.1 (Adjoint-kernel coefficients are exactly vanishing protocol combinations).

$$\begin{array}{r}\forall V,iota:\mathrm{Type},\\ [\mathrm{NormedAddCommGroup}(V)],[\mathrm{InnerProductSpace}(\mathbb{R},V)],\\ [\mathrm{FiniteDimensional}(\mathbb{R},V)],[\mathrm{Fintype}(iota)],\\ \forall ell:iota\to V,a:\mathrm{EuclideanSpace}(\mathbb{R},iota),\\ letM:\mathrm{LinearMap}(\mathbb{R},V,\mathrm{EuclideanSpace}(\mathbb{R},iota))=\mathrm{comp}(\mathrm{toLinearMap}(\mathrm{symm}(\mathrm{withLpLinearEquiv}(2,\mathbb{R},iota\to \mathbb{R}))),\mathrm{linearPi}((i:iota\mapsto \mathrm{innerSL}(\mathbb{R},ell\left(i\right)))));\\ a\in \ker (\mathrm{adjoint}(M))\iff \mathrm{finSum}((i:iota\mapsto \mathrm{smul}(a\left(i\right),ell\left(i\right))))=0.\end{array}$$

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

Source. Repository-derived.

Commentary.

Let a finite family ell consist of protocol representatives in a finite-dimensional real Hilbert state space. The analysis map M records the inner product with every representative.

For every Euclidean coefficient vector a, the adjoint M-star applied to a is the finite synthesis sum of a_i times ell_i. Consequently a lies in the adjoint kernel exactly when that linear combination vanishes.

Thus a protocol-side residual direction need not mean the absence of a state. It records an exact linear dependence among the selected protocol representatives.

References

• Truth anchor: D5/S3/Observer/LinearMemory/AdjointKernelRedundancy.adjoint_kernel_redundancy