Eigenfunctions of distinct eigenvalues with the same winding number are never parallel
ProvedFiniteEnergyPlane.loopEigen_apply_ne_smul_of_hasLoopEigenWindconley-zehnder-indexpseudoholomorphic-curvessymplectic-geometrywinding-numbers
Let be a -periodic loop of symmetric matrices and on -periodic loops in . Let be eigenvalues of such that every eigenfunction of and every eigenfunction of has the same winding number . If are eigenfunctions with eigenvalues , then for every and every ,
The values of such eigenfunctions are linearly independent in at every time. This controls how eigenfunctions of one winding number can combine.
Formalization Note Eigenfunctions are IsLoopEigen Sinf μ e (FiniteEnergyPlane_Asymptotics); the winding hypothesis on is HasLoopEigenWind Sinf μⱼ k (FiniteEnergyPlane_Winding: has an eigenfunction and all its eigenfunctions have winding as loops in via vecToC); IsSymLoop Sinf and smoothness of the entries are hypotheses.
Preamble
import Definitions.Def_FiniteEnergyPlane_Winding
Formal statement
namespace FiniteEnergyPlane
open scoped ContDiff
/-- Eigenfunctions of `A = -J₀ ∂ₜ - S∞` for two distinct eigenvalues with the same winding
number are pointwise linearly independent: their values are never parallel. -/
theorem loopEigen_apply_ne_smul_of_hasLoopEigenWind (Sinf : ℝ → CauchyRiemannIndex.Mat 1)
(hSinf : CauchyRiemannIndex.IsSymLoop Sinf)
(hSinf' : ∀ i j, ContDiff ℝ ∞ (fun t => Sinf t i j)) {μ₁ μ₂ : ℝ} {k : ℤ} (hμ : μ₁ ≠ μ₂)
(h₁ : HasLoopEigenWind Sinf μ₁ k) (h₂ : HasLoopEigenWind Sinf μ₂ k)
{e₁ e₂ : ℝ → CauchyRiemannIndex.Vec 1} (he₁ : IsLoopEigen Sinf μ₁ e₁)
(he₂ : IsLoopEigen Sinf μ₂ e₂) (t c : ℝ) : e₂ t ≠ c • e₁ t := by
sorry
end FiniteEnergyPlane
Source
C. Wendl, Lectures on Symplectic Field Theory (2026 notes), arXiv:1612.01009, Section 3.7, Theorem 3.7.1; H. Hofer, K. Wysocki, E. Zehnder, GAFA 5 (1995), Section 3.