A smooth symmetric loop, possibly degenerate, has index $\alpha^- + \alpha^+$

import Definitions.Def_FiniteEnergyPlane_Winding

namespace FiniteEnergyPlane

open scoped ContDiff Real

/-- For a smooth symmetric loop `S∞`, not necessarily nondegenerate, there are integers `a, b` with
`b ∈ {a, a + 1}` such that `a` is the largest winding number of a negative eigenvalue of
`-J₀ ∂ₜ - S∞`, `b` is the smallest winding number of a nonnegative eigenvalue, and the fundamental
solution has `czIndexOfPath` equal to `a + b`. -/
theorem exists_loopAlpha_czIndexOfPath_eq_of_symLoop (Sinf : ℝ → CauchyRiemannIndex.Mat 1)
    (hSinf : CauchyRiemannIndex.IsSymLoop Sinf)
    (hSinf' : ∀ i j, ContDiff ℝ ∞ (fun t => Sinf t i j)) :
    ∃ a b : ℤ,
      ((∃ μ < 0, HasLoopEigenWind Sinf μ a) ∧
        ∀ μ < 0, ∀ k : ℤ, HasLoopEigenWind Sinf μ k → k ≤ a) ∧
      ((∃ μ, 0 ≤ μ ∧ HasLoopEigenWind Sinf μ b) ∧
        ∀ μ, 0 ≤ μ → ∀ k : ℤ, HasLoopEigenWind Sinf μ k → b ≤ k) ∧
      (b = a ∨ b = a + 1) ∧
      ∀ Ψ : ℝ → CauchyRiemannIndex.Mat 1, CauchyRiemannIndex.IsFundamentalSolution Sinf Ψ →
        HryniewiczCriterion.czIndexOfPath
          (fun τ => Matrix.reindex finSumFinEquiv finSumFinEquiv (Ψ τ)) = a + b := by
  sorry

end FiniteEnergyPlane