Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Actual Bottom Eigenvectors and All Complex Energy Eigenspaces

Abstract

Actual Bottom Eigenvectors and All Complex Energy Eigenspaces

Under positive original real Gram, original two-sided complex inverse H, integral beta and rational mu with G_Q mu=beta, the minimum constructed from finite sublevels is an ACTUAL eigenvalue of the original-omega moduleL_0 in every rank. Its witness is the original carrier basis at a minimizing charge and zero oscillator exponent. Every complex eigenspace is finite dimensional: any nonzero vector forces its complex eigenvalue into cast(h+N), where finite exact energy fibers apply; outside that image the eigenspace is zero. These are algebraic eigenspaces on the actual carrier, without a Hilbert completion or analytic spectral claim.

Theorem 1.1 (bottom eigenvector).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeDualCosetEnergyEndpoints.bottom_eigenvector

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/Sectors/LatticeDualCosetEnergyEndpoints.bottom_eigenvector (✓ std3). ∎

Source. Repository-derived.

Commentary.

The constructed nonnegative attained minimum has a nonzero actual eigenvector in every rank, including rank zero.

Theorem 1.2 (all eigenspaces finite dimensional).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeDualCosetEnergyEndpoints.all_eigenspaces_finiteDimensional

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/Sectors/LatticeDualCosetEnergyEndpoints.all_eigenspaces_finiteDimensional (✓ std3). ∎

Source. Repository-derived.

Commentary.

For EVERY complex lambda, the actual original-omega L_0 eigenspace is finite dimensional. Outside cast(h+N) it equals zero.

Theorem 1.3 (half shift actual bottom multiplicity).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeDualCosetEnergyEndpoints.half_shift_actual_bottom_multiplicity

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/Sectors/LatticeDualCosetEnergyEndpoints.half_shift_actual_bottom_multiplicity (✓ std3). ∎

Source. Repository-derived.

Commentary.

For Gram [2] and mu=1/2, every charge weight is at least 1/4, and the ACTUAL original-omega L_0 eigenspace at 1/4 contains two linearly independent vectors from distinct minimizing charges.

References