Finite Common-Spectrum Criterion

Abstract

A finite rational-feature Gram exists exactly when its inverse coefficient congruence is a positive Hermitian Toeplitz matrix.

Theorem 1.1 (Finite rational Grams are exactly positive Toeplitz transforms).

$$\begin{gathered} \forall N\in \mathbb{N},A\in \mathrm{Matrix}(\mathrm{Fin}(N+1),\mathrm{Fin}(N+1),\mathbb{C}),hA\in \mathrm{IsUnit}(A),D\in \mathrm{Polynomial}(\mathbb{C}),hD\in \left(\forall z\in Circle,\mathrm{eval}(D,z)\ne 0\right),G\in \mathrm{Matrix}(\mathrm{Fin}(N+1),\mathrm{Fin}(N+1),\mathbb{C}),\begin{array}{r}\mathrm{let}v:Circle\to \left(\mathrm{Fin}(N+1)\to \mathbb{C}\right)=(z:Circle\mapsto (j:\mathrm{Fin}(N+1)\mapsto z^{\mathrm{toNat}(j)}))\\ \mathrm{let}\psi :Circle\to \left(\mathrm{Fin}(N+1)\to \mathbb{C}\right)=(z:Circle\mapsto (i:\mathrm{Fin}(N+1)\mapsto \frac{\mathrm{mulVec}(A,v(z))(i)}{\mathrm{eval}(D,z)}))\\ \mathrm{let}Gram:\mathrm{FiniteMeasure}(Circle)\to \mathrm{Matrix}(\mathrm{Fin}(N+1),\mathrm{Fin}(N+1),\mathbb{C})=(mu:\mathrm{FiniteMeasure}(Circle)\mapsto \mathrm{Matrix}((i:\mathrm{Fin}(N+1)\mapsto (j:\mathrm{Fin}(N+1)\mapsto \mathrm{integral}(z,Circle,\psi (z)(i)\cdot \mathrm{star}(\psi (z)(j)),mu)))))\\ \mathrm{let}T:\mathrm{Matrix}(\mathrm{Fin}(N+1),\mathrm{Fin}(N+1),\mathbb{C})=\mathrm{inv}(A)\cdot G\cdot \mathrm{conjTranspose}(\mathrm{inv}(A))\end{array}, \\ \left(\exists mu\in \mathrm{FiniteMeasure}(Circle),G=Gram(mu)\right)\iff \left(\mathrm{PosSemidef}(T)\wedge \left(\exists y\in \mathbb{Z}\to \mathbb{C},\left(\forall k\in \mathbb{Z},y(-k)=\mathrm{star}(y(k))\right)\wedge T=\mathrm{toeplitzMatrix}(y,N)\right)\right) \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Observer/BlockStructure/FiniteCommonSpectrumCriterion.finite_common_spectrum_criterion (✓ std3). ∎

Source. Repository-derived.

Commentary.

The supplied invertible coefficient matrix and polynomial without unit-circle zeros construct the complete common-denominator rational feature family.

The forward implication applies the rational Gram congruence after reciprocal denominator weighting and circle reflection.

For the converse, the truncated Toeplitz moment theorem constructs a finite positive circle measure. Restoring the denominator weight and cancelling the invertible congruence recovers the given Gram.

Conjugate symmetry of the displayed moment sequence is the public Hermitian condition. No separate Hermitian premise on the given matrix is needed because either side of the equivalence forces it.

References

• Truth anchor: D5/S3/Observer/BlockStructure/FiniteCommonSpectrumCriterion.finite_common_spectrum_criterion
• Dependency: D5/S3/Observer/BlockStructure/RationalToeplitzCollapse
• Dependency: D5/S3/Weil/CayleyLaguerre/TruncatedCircleMomentBridge
• Dependency: D5/S3/Weil/TestFunctions/LiCurvatureCriterion