Weak Morse inequalities

weak_morse_inequality — a formalization challenge from the lean-eval benchmark.

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.

Formal statement

/-- **Weak Morse inequalities.** For a Morse function `f` on a closed
smooth finite-dimensional Hausdorff manifold `M` and every `k ∈ ℕ`,
`b_k(M) ≤ c_k(f)`. -/
theorem 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 : IsMorseFunction I f) (k : ℕ) :
    bettiNumber M k ≤ morseCount I f k := by
  sorry

Informal solution sketch

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.

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).

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: weak_morse_inequality
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.