Weak Morse inequalities

weak_morse_inequality

Submitter: Kim Morrison.

Notes: §40 of Knill's 'Some Fundamental Theorems in Mathematics' (additional statement; the boxed main theorem is the strong Morse inequality). For a Morse function f on a closed smooth finite-dimensional Hausdorff manifold M, b_k(M) ≤ c_k(f) for every k. The Hausdorff (T2Space) hypothesis is essential, as the split-circle counterexample shows. Follows from the strong Morse inequality but is often proved directly via the Morse-Smale CW structure. 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 weak Morse inequality. The Challenge ships seven helper definitions.

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

Informal solution: Direct corollary of the strong Morse inequality: the alternating partial sums of c_k(f) dominate those of b_k(M); take the difference of consecutive partial sums and use that successive partial sums differ by 2·b_k − 2·c_k (with signs), to extract b_k ≤ c_k. Alternatively, prove directly via the Morse-Smale CW structure: the cellular boundary maps ∂_k : ℤ^{c_k} → ℤ^{c_{k−1}} give H_k = ker ∂_k / im ∂_{k+1}, and dim H_k ≤ c_k − rank ∂_k − rank ∂_{k+1} ≤ c_k. The weak inequality is sharper than counting: it asserts the Betti number bound for each k independently, not just the alternating sum.

theorem declaration uses `sorry`weak_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.WeakMorseInequality.IsMorseFunction I f) (k : ℕ) :
    bettiNumber M k ≤ 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:ℕ⊢ bettiNumber M k ≤ morseCount I f k
  sorryAll goals completed! 🐙

Solved by

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