Exact Common-Spectrum Floor

Abstract

The largest common normalized-Haar component of a rational feature Gram matrix is the least eigenvalue in either whitened coordinate system.

Theorem 1.1 (The exact floor is the common least eigenvalue).

$$\begin{gathered} \forall N\in \mathbb{N},A\in \mathrm{Matrix}(\mathrm{Fin}(N+1),\mathrm{Fin}(N+1),\mathbb{C}),D\in \mathrm{Polynomial}(\mathbb{C}),G\in \mathrm{Matrix}(\mathrm{Fin}(N+1),\mathrm{Fin}(N+1),\mathbb{C}),mu0\in \mathrm{FiniteMeasure}(Circle),hA\in \mathrm{IsUnit}(A),hD\in \left(\forall z\in Circle,\mathrm{eval}(D,z)\ne 0\right),hG\in \mathrm{IsHermitian}(G),hSource\in \left(\forall i\in \mathrm{Fin}(N+1),j\in \mathrm{Fin}(N+1),\mathrm{integral}(z,Circle,\frac{\mathrm{mulVec}(A,(k:\mathrm{Fin}(N+1)\mapsto z^{\mathrm{toNat}(k)}))(i)}{\mathrm{eval}(D,z)}\cdot \mathrm{star}(\frac{\mathrm{mulVec}(A,(k:\mathrm{Fin}(N+1)\mapsto z^{\mathrm{toNat}(k)}))(j)}{\mathrm{eval}(D,z)}),mu0)=G(i,j)\right),\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}wD:Circle\to ENNReal=(z:Circle\mapsto \mathrm{ofReal}(\mathrm{inv}(\mathrm{normSq}(\mathrm{eval}(D,z)))))\\ \mathrm{let}weightedReflected:\mathrm{FiniteMeasure}(Circle)\to \mathrm{Measure}(Circle)=(mu:\mathrm{FiniteMeasure}(Circle)\mapsto \mathrm{map}(inv,\mathrm{withDensity}(\mathrm{toMeasure}(mu),wD)))\\ \mathrm{let}M:\mathrm{FiniteMeasure}(Circle)\to \mathrm{Matrix}(\mathrm{Fin}(N+1),\mathrm{Fin}(N+1),\mathbb{C})=(mu:\mathrm{FiniteMeasure}(Circle)\mapsto \mathrm{toeplitzMatrix}(\mathrm{circleMoment}(weightedReflected(mu)),N))\\ \mathrm{let}{H}_D:\mathrm{Matrix}(\mathrm{Fin}(N+1),\mathrm{Fin}(N+1),\mathbb{C})=M(\mathrm{normalizedCircleHaar}())\\ \mathrm{let}B:\mathrm{Matrix}(\mathrm{Fin}(N+1),\mathrm{Fin}(N+1),\mathbb{C})=A\cdot H_D\cdot \mathrm{conjTranspose}(A)\\ \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))\\ \mathrm{let}F:\mathrm{Set}(NonnegativeReal)=\left\{\exists mu\in \mathrm{FiniteMeasure}(Circle),Gram(mu)=G\wedge \mathrm{toMeasure}(\mathrm{smul}(alpha,\mathrm{normalizedCircleHaar}()))\le \mathrm{toMeasure}(mu)\mid alpha\in NonnegativeReal\right\}\\ \mathrm{let}alphaStar:NonnegativeReal=\mathrm{sSup}(F)\end{array}, \\ \forall hHD\in \mathrm{PosDef}(H_D),\begin{array}{r}\mathrm{let}hT:\mathrm{IsHermitian}(T)=\mathrm{isHermitianConjTransposeMulMul}(\mathrm{conjTranspose}(\mathrm{inv}(A)),hG)\\ \mathrm{let}{W}_D:\mathrm{Matrix}(\mathrm{Fin}(N+1),\mathrm{Fin}(N+1),\mathbb{C})=\mathrm{inv}(\mathrm{sqrt}(H_D))\\ \mathrm{let}{Q}_D:\mathrm{Matrix}(\mathrm{Fin}(N+1),\mathrm{Fin}(N+1),\mathbb{C})=\mathrm{conjTranspose}(W_D)\cdot T\cdot W_D\\ \mathrm{let}hQD:\mathrm{IsHermitian}(Q_D)=\mathrm{isHermitianConjTransposeMulMul}(W_D,hT)\\ \mathrm{let}{W}_B:\mathrm{Matrix}(\mathrm{Fin}(N+1),\mathrm{Fin}(N+1),\mathbb{C})=\mathrm{inv}(\mathrm{sqrt}(B))\\ \mathrm{let}{Q}_B:\mathrm{Matrix}(\mathrm{Fin}(N+1),\mathrm{Fin}(N+1),\mathbb{C})=\mathrm{conjTranspose}(W_B)\cdot G\cdot W_B\\ \mathrm{let}hQB:\mathrm{IsHermitian}(Q_B)=\mathrm{isHermitianConjTransposeMulMul}(W_B,hG)\end{array}, \\ \left(\mathrm{IsGreatest}(\left\{\mathrm{PosSemidef}(\mathrm{sub}(T,\mathrm{smul}(\mathrm{toComplex}(alpha),H_D)))\mid alpha\in \mathbb{R}\right\},\mathrm{toReal}(alphaStar))\wedge \mathrm{toReal}(alphaStar)=eigenvalues0(Q_D,hQD,\mathrm{last}(N))\right)\wedge \mathrm{toReal}(alphaStar)=eigenvalues0(Q_B,hQB,\mathrm{last}(N)) \end{gathered}$$

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

Source. Repository-derived.

Commentary.

The feature family, its rational Gram matrix, the reflected weighted moment matrix, and both congruent reference matrices are constructed from the supplied coefficient matrix, denominator, and finite circle measure.

The forward direction subtracts a dominated normalized-Haar component. The reverse direction represents the positive Toeplitz residual by a finite circle measure, reverses the circle coordinate, and restores the denominator weight.

Positive-definite whitening identifies the greatest feasible real floor with the last ordered Hermitian eigenvalue. Invertible congruence gives the same value for the original Gram matrix and its reference matrix.

References

• Truth anchor: D5/S3/Observer/BlockStructure/ExactCommonSpectrumFloor.exact_common_spectrum_floor
• Dependency: D5/S3/Observer/BlockStructure/CommonSpectrumMasterFeasibility
• Dependency: D5/S3/Observer/BlockStructure/RationalToeplitzCollapse
• Dependency: D5/S3/Weil/TestFunctions/ExactTruncatedHaarFloor