Morse inequalities

morse_inequality

Submitter: Kim Morrison.

Notes: §40 of Knill's 'Some Fundamental Theorems in Mathematics' (Marston Morse, 1934). For a Morse function f on a closed smooth finite-dimensional Hausdorff manifold M, ∑_{j≤k}(−1)^{k−j} c_j(f) ≥ ∑_{j≤k}(−1)^{k−j} b_j(M) for every k. The Hausdorff (T2Space) hypothesis is essential: without it the split-circle counterexample (a compact boundaryless non-Hausdorff 1-manifold with b_1 = 2 but one index-0 and one index-1 critical point) violates the inequality at k = 1. Mathlib has the smooth-manifold framework, mfderiv, higher Fréchet derivatives, and singularHomologyFunctor but no Morse functions, Morse index, critical-point counts, Betti numbers as a named definition, or the Morse inequalities. The Challenge ships seven helper definitions (IsCriticalPoint, localHessian, IsNondegenerateCritical, IsMorseFunction, morseIndex, morseCount, bettiNumber, alternatingPartialSum).

Source: M. Morse, The Calculus of Variations in the Large, AMS Colloq. Publ. 18 (1934). Listed as §40 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Strong Morse inequality via the Morse-Smale complex: order the critical points by increasing critical value t_1 < t_2 < … < t_N and consider the sublevel sets M_t = f⁻¹((−∞,t]). Crossing a critical value attaches a k-cell where k is the Morse index, so M_t is obtained from M_{t−} by attaching one k-cell per index-k critical point at level t (Morse lemma + handle attachment). This gives a CW structure on M with c_k cells in dimension k, hence a chain complex C_k = ℤ^{c_k} computing H_k(M; ℤ). The strong inequality follows from the rank-nullity-style relation rank H_k = c_k − rank ∂_{k+1} − rank ∂_k applied to alternating partial sums, combined with subadditivity of rank under boundary maps.

theorem declaration uses `sorry`morse_inequality {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    {H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless]
    {M : Type} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]
    [CompactSpace M] [T2Space M] (f : M → ℝ) (_hf : LeanEval.Geometry.MorseInequalities.IsMorseFunction I f) (k : ℕ) :
    LeanEval.Geometry.MorseInequalities.alternatingPartialSum (bettiNumber M) k ≤
      LeanEval.Geometry.MorseInequalities.alternatingPartialSum (morseCount I f) k := byE:Type u_1inst✝⁹:NormedAddCommGroup Einst✝⁸:NormedSpace ℝ Einst✝⁷:FiniteDimensional ℝ EH:Type u_2inst✝⁶:TopologicalSpace HI:ModelWithCorners ℝ E Hinst✝⁵:I.BoundarylessM:Typeinst✝⁴:TopologicalSpace Minst✝³:ChartedSpace H Minst✝²:IsManifold I ∞ Minst✝¹:CompactSpace Minst✝:T2Space Mf:M → ℝ_hf:IsMorseFunction I fk:ℕ⊢ alternatingPartialSum (bettiNumber M) k ≤ alternatingPartialSum (morseCount I f) k
  sorryAll goals completed! 🐙

Solved by

• @hanwenzhu with Seed Prover (ByteDance) on Jul 22, 2026