From 0a53949bef361cc2de8c937ae90e05af34996909 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sat, 23 May 2026 16:47:17 +0000
Subject: [PATCH] feat: add weak Morse inequalities eval problem
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

§40 of Knill's "Some Fundamental Theorems in Mathematics" (additional
statement; the boxed main is the strong inequality). For a Morse
function f on a closed smooth finite-dimensional manifold M,
b_k(M) ≤ c_k(f) for every k. Mathlib has the smooth-manifold framework
and singularHomologyFunctor but no Morse functions or Betti numbers as
a named definition. The Challenge ships seven helper definitions.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 LeanEval/Geometry/WeakMorseInequality.lean    | 105 ++++++++++++++++++
 manifests/problems/weak_morse_inequality.toml |   9 ++
 2 files changed, 114 insertions(+)
 create mode 100644 LeanEval/Geometry/WeakMorseInequality.lean
 create mode 100644 manifests/problems/weak_morse_inequality.toml

diff --git a/LeanEval/Geometry/WeakMorseInequality.lean b/LeanEval/Geometry/WeakMorseInequality.lean
new file mode 100644
index 0000000..eb31605
--- /dev/null
+++ b/LeanEval/Geometry/WeakMorseInequality.lean
@@ -0,0 +1,105 @@
+import Mathlib
+import EvalTools.Markers
+
+namespace LeanEval
+namespace Geometry
+
+/-!
+# Weak Morse inequalities
+
+§40 of Knill's *Some Fundamental Theorems in Mathematics* (an additional
+statement of the section; the boxed main theorem is the strong Morse
+inequality). For a Morse function `f` on a closed smooth finite-dimensional
+manifold `M`,
+
+`b_k(M) ≤ c_k(f)` for every `k`,
+
+i.e. the `k`-th Betti number is bounded by the number of Morse-index-`k`
+critical points. 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.
+-/
+
+open scoped Manifold ContDiff Topology
+open CategoryTheory
+
+/-- A point `x ∈ M` is a **critical point** of `f` if `mfderiv f x = 0`. -/
+def IsCriticalPoint
+    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
+    {H : Type*} [TopologicalSpace H]
+    {M : Type} [TopologicalSpace M] [ChartedSpace H M]
+    (I : ModelWithCorners ℝ E H) (f : M → ℝ) (x : M) : Prop :=
+  mfderiv I (modelWithCornersSelf ℝ ℝ) f x = 0
+
+/-- **Local Hessian** of `f` at `x`, in the preferred extended chart. -/
+noncomputable def localHessian
+    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
+    {H : Type*} [TopologicalSpace H]
+    {M : Type} [TopologicalSpace M] [ChartedSpace H M]
+    (I : ModelWithCorners ℝ E H) (f : M → ℝ) (x : M) :
+    ContinuousMultilinearMap ℝ (fun _ : Fin 2 => E) ℝ :=
+  iteratedFDeriv ℝ 2 (f ∘ (extChartAt I x).symm) (extChartAt I x x)
+
+/-- A critical point `x` is **non-degenerate** when the local Hessian has
+trivial radical. -/
+def IsNondegenerateCritical
+    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
+    {H : Type*} [TopologicalSpace H]
+    {M : Type} [TopologicalSpace M] [ChartedSpace H M]
+    (I : ModelWithCorners ℝ E H) (f : M → ℝ) (x : M) : Prop :=
+  IsCriticalPoint I f x ∧
+    ∀ v : E, (∀ w : E, localHessian I f x ![v, w] = 0) → v = 0
+
+/-- A **Morse function** on `M` is `C^∞`, has finitely many critical points,
+and every critical point is non-degenerate. -/
+structure IsMorseFunction
+    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
+    {H : Type*} [TopologicalSpace H]
+    {M : Type} [TopologicalSpace M] [ChartedSpace H M]
+    (I : ModelWithCorners ℝ E H) [IsManifold I ∞ M] (f : M → ℝ) : Prop where
+  smooth : ContMDiff I (modelWithCornersSelf ℝ ℝ) ∞ f
+  critical_finite : {x : M | IsCriticalPoint I f x}.Finite
+  nondegenerate : ∀ x : M, IsCriticalPoint I f x → IsNondegenerateCritical I f x
+
+/-- The **Morse index** of `f` at `x`. -/
+noncomputable def morseIndex
+    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
+    {H : Type*} [TopologicalSpace H]
+    {M : Type} [TopologicalSpace M] [ChartedSpace H M]
+    (I : ModelWithCorners ℝ E H) (f : M → ℝ) (x : M) : ℕ :=
+  sSup {k : ℕ | ∃ S : Submodule ℝ E,
+    Module.finrank ℝ S = k ∧
+      ∀ v ∈ S, v ≠ 0 → localHessian I f x ![v, v] < 0}
+
+/-- `morseCount f k = c_k(f)`. -/
+noncomputable def morseCount
+    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
+    {H : Type*} [TopologicalSpace H]
+    {M : Type} [TopologicalSpace M] [ChartedSpace H M]
+    (I : ModelWithCorners ℝ E H) (f : M → ℝ) (k : ℕ) : ℕ :=
+  {x : M | IsCriticalPoint I f x ∧ morseIndex I f x = k}.ncard
+
+/-- `b_k(M) := dim_ℝ H_k(M; ℝ)`. -/
+noncomputable def bettiNumber (M : Type) [TopologicalSpace M] (k : ℕ) : ℕ :=
+  Module.finrank ℝ
+    (((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℝ) k).obj
+        (ModuleCat.of ℝ ℝ)).obj (TopCat.of M))
+
+/-- **Weak Morse inequalities.** For a Morse function `f` on a closed
+smooth finite-dimensional manifold `M` and every `k ∈ ℕ`,
+`b_k(M) ≤ c_k(f)`. -/
+@[eval_problem]
+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] (f : M → ℝ) (_hf : IsMorseFunction I f) (k : ℕ) :
+    bettiNumber M k ≤ morseCount I f k := by
+  sorry
+
+end Geometry
+end LeanEval
diff --git a/manifests/problems/weak_morse_inequality.toml b/manifests/problems/weak_morse_inequality.toml
new file mode 100644
index 0000000..36e58e9
--- /dev/null
+++ b/manifests/problems/weak_morse_inequality.toml
@@ -0,0 +1,9 @@
+id = "weak_morse_inequality"
+title = "Weak Morse inequalities"
+test = false
+module = "LeanEval.Geometry.WeakMorseInequality"
+holes = ["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 manifold M, b_k(M) ≤ c_k(f) for every k. 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."