Dual Gram Visible Ranges

Abstract

The two Gram operators of a finite protocol family expose its two visible ranges.

Theorem 1.1 (The state and protocol visible ranges are adjoint duals).

$$\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));\\ \mathrm{range}(\mathrm{comp}(\mathrm{adjoint}(M),M))=\mathrm{range}(\mathrm{adjoint}(M))\wedge \\ \mathrm{range}(\mathrm{comp}(M,\mathrm{adjoint}(M)))=\mathrm{range}(M).\end{array}$$

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

Source. Repository-derived.

Commentary.

Let an indexed family assign a scalar linear readout to every protocol. The observation map is constructed coordinatewise by the canonical linear-map product constructor.

The state Gram operator is the adjoint followed by the observation map, while the protocol Gram operator uses the reverse composition. Their ranges are respectively the adjoint range and the realizable observation range.

The proof directly applies the pinned library’s two exact finite-dimensional adjoint-composition range lemmas.

References

• Truth anchor: D5/S3/Observer/LinearMemory/DualGramVisibleRanges.dual_gram_visible_ranges