Toeplitz Flat-Floor Multiplicity

Abstract

A contact Gram update has floor omega with the predicted multiplicity.

Theorem 1.1 (Finite contact rank leaves an exact flat spectral floor).

$$\begin{array}{r}\forall N:\mathbb{N},M:\mathbb{N},omega:\mathbb{R},\\ z:\mathrm{Fin}(M)\to \mathrm{unitary}(\mathbb{C}),\\ q:\mathrm{Fin}(M)\to \{x\in \mathbb{R}\mid 0<x\},\\ M<N+1\Rightarrow \\ \mathrm{let}(A:\mathrm{Matrix}(\mathrm{Fin}(M),\mathrm{Fin}(N+1),\mathbb{C}),\forall r:\mathrm{Fin}(M),j:\mathrm{Fin}(N+1),A_{r,j}=\sqrt{q(r)}{z(r{)}^j}^{\ast },T:\mathrm{Matrix}(\mathrm{Fin}(N+1),\mathrm{Fin}(N+1),\mathbb{C})=omegaI+A^{\ast }A)\\ (\forall j:\mathrm{Fin}(N+1),k:\mathrm{Fin}(N+1),T_{jk}=delt{a}_{jk}omega+\sum _{r=1}^{M}q(r)z(r{)}^j{z(r{)}^k}^{\ast })\wedge \\ \mathrm{IsLeast}(\mathrm{spectrum}(\mathbb{R},T),omega)\wedge \\ N+1-M\le \mathrm{finrank}(\mathbb{C},\mathrm{eigenspace}(T,omega)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Tomography/ToeplitzFlatFloorMultiplicity.toeplitz_flat_floor_multiplicity (✓ std3). ∎

Source. Repository-derived.

Commentary.

The contact points live directly in the unitary subtype of the complex unit circle, and every weight lives in the strictly positive real subtype. The weighted analysis matrix is constructed from their contact vectors rather than supplied as an arbitrary matrix.

The first public clause expands the constructed adjoint Gram matrix entry by entry, exposing the scalar white floor and the positive finite contact update on the exact complex Toeplitz carrier.

Adjoint Gram positivity places every real spectral value above omega. Rank-nullity leaves at least N plus one minus M independent kernel directions, and each becomes an omega eigenvector after the scalar floor is added.

The conclusion states the minimum as an IsLeast property of the real spectrum and states the multiplicity as the complex dimension of the omega eigenspace. Hermitian spectral theory identifies this geometric multiplicity with eigenvalue multiplicity.

References

• Truth anchor: D5/S3/Observer/Tomography/ToeplitzFlatFloorMultiplicity.toeplitz_flat_floor_multiplicity