Nonzero Gram Spectrum and Multiplicity

Abstract

Rectangular adjoint Gram matrices have identical nonzero spectra with algebraic multiplicity.

Theorem 1.1 (The nonzero Gram spectra agree with multiplicity).

$$\begin{array}{r}\forall K,m,n:\mathrm{Type},\\ [\mathrm{RCLike}(K)],[\mathrm{Fintype}(m)],[\mathrm{DecidableEq}(m)],\\ [\mathrm{Fintype}(n)],[\mathrm{DecidableEq}(n)],\\ \forall M:\mathrm{Matrix}(m,n,K),lambda:K,\\ lambda\ne 0\Rightarrow (\mathrm{IsRoot}(\mathrm{charpoly}(\mathrm{mul}(\mathrm{conjTranspose}(M),M)),lambda)⟺\mathrm{IsRoot}(\mathrm{charpoly}(\mathrm{mul}(M,\mathrm{conjTranspose}(M))),lambda))\wedge \\ (\mathrm{rootMultiplicity}(lambda,\mathrm{charpoly}(\mathrm{mul}(\mathrm{conjTranspose}(M),M)))=\mathrm{rootMultiplicity}(lambda,\mathrm{charpoly}(\mathrm{mul}(M,\mathrm{conjTranspose}(M))))).\end{array}$$

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

Source. Repository-derived.

Commentary.

The rectangular characteristic-polynomial identity differs only by powers of the polynomial variable. At a nonzero scalar those factors have zero root multiplicity, leaving both root membership and algebraic multiplicity unchanged between the two adjoint Gram products.

References

• Truth anchor: D5/S3/Observer/LinearMemory/GramNonzeroSpectrumMultiplicity.gram_nonzero_spectrum_with_algebraic_multiplicity