Dual Gram Condition Number

Abstract

Dual Gram operators have one positive-spectrum condition number and paired weak modes.

Theorem 1.1 (State and protocol conditioning are dual).

$$\forall K\in \mathrm{Type},V\in \mathrm{Type},iota\in \mathrm{Type},ell\in iota\to \mathrm{LinearMap}\left(K,V,K\right),\left(\mathrm{RCLike}\left(K\right)\wedge \left(\mathrm{NormedAddCommGroup}\left(V\right)\wedge \left(\mathrm{InnerProductSpace}\left(K,V\right)\wedge \left(\mathrm{FiniteDimensional}\left(K,V\right)\wedge \mathrm{Fintype}\left(iota\right)\right)\right)\right)\right)\Rightarrow \mathrm{let}M:\mathrm{LinearMap}\left(K,V,\mathrm{PiLp}\left(2,iota\to K\right)\right)=\mathrm{comp}\left(\mathrm{toLinearMap}\left(\mathrm{symm}\left(\mathrm{withLpLinearEquiv}\left(2,K,iota\to K\right)\right)\right),\mathrm{linearPi}\left(ell\right)\right);\mathrm{let}stateSpectrum:\mathrm{Set}\left(\mathbb{R}\right)=\left\{0<lambda\wedge \mathrm{HasEigenvalue}\left(\mathrm{comp}\left(\mathrm{adjoint}\left(M\right),M\right),\mathrm{ofReal}\left(K,lambda\right)\right)\mid lambda\in \mathbb{R}\right\};\mathrm{let}protocolSpectrum:\mathrm{Set}\left(\mathbb{R}\right)=\left\{0<lambda\wedge \mathrm{HasEigenvalue}\left(\mathrm{comp}\left(M,\mathrm{adjoint}\left(M\right)\right),\mathrm{ofReal}\left(K,lambda\right)\right)\mid lambda\in \mathbb{R}\right\};\frac{\mathrm{sSup}\left(stateSpectrum\right)}{\mathrm{sInf}\left(stateSpectrum\right)}=\frac{\mathrm{sSup}\left(protocolSpectrum\right)}{\mathrm{sInf}\left(protocolSpectrum\right)}\wedge \left(\forall sigma\in \mathbb{R},0<sigma\Rightarrow \left(\left(\exists v\in V,\mathrm{HasEigenvector}\left(\mathrm{comp}\left(\mathrm{adjoint}\left(M\right),M\right),\mathrm{ofReal}\left(K,sigm{a}^2\right),v\right)\right)\iff \left(\exists a\in \mathrm{PiLp}\left(2,iota\to K\right),\mathrm{HasEigenvector}\left(\mathrm{comp}\left(M,\mathrm{adjoint}\left(M\right)\right),\mathrm{ofReal}\left(K,sigm{a}^2\right),a\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

A finite indexed family of scalar readouts constructs the observation map coordinatewise on the square-summable protocol carrier. The positive state and protocol Gram spectra are displayed as literal sets.

Their supremum-to-infimum ratios agree. For every positive singular value, the observation map and its adjoint transfer nonzero eigenvectors between the state and protocol Gram operators at the same square.

The proof applies the pinned library’s eigenspace and linear-map laws; the observation map is the canonical coordinatewise construction already used by the dual-Gram family.

References

• Truth anchor: D5/S3/Observer/LinearMemory/DualGramConditionNumber.dual_gram_condition_number