Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generated
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The Morse critical-point sum is the Euler characteristic

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let M be a closed smooth n-manifold with n≥1, and let f:M→R be a Morse function (Morse functions and excellent Morse functions) and let g be a Riemannian metric on M (Every smooth manifold admits a riemannian metric). Then ∑p∈Crit⁡(f)(−1)ind⁡(p)=χ(M), the sum over the finitely many critical points of f.

Facts & Assumptions

Given: A closed smooth n-manifold M, a Morse function f and a Riemannian metric g on M.

[F1]

The field grad⁡gf vanishes exactly at the critical points of f, which are finitely many, and at a critical point of index λ its index is (−1)λ (The Riemannian gradient is the metric dual of the differential, The Riemannian gradient vanishes exactly at the critical points, A Morse gradient zero contributes (−1)λ to the index, Morse functions and excellent Morse functions).

[F2]

Poincare-Hopf: the index sum of a smooth field with only isolated zeros on a closed manifold equals χ(M) (Poincare-Hopf for closed manifolds, Euler characteristic of a compact manifold).

Proof

1.1F1F2algebra

The critical points of a Morse function on a closed manifold are finitely many and each is a nondegenerate zero of grad⁡gf; hence the field has only isolated zeros and [F2] gives ∑pind⁡p(grad⁡gf)=χ(M).

2.1F1step 1.1algebra∎

By [F1] each summand is ind⁡p(grad⁡gf)=(−1)ind⁡(p), so substituting into step 1.1 gives ∑p∈Crit⁡(f)(−1)ind⁡(p)=χ(M).

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

43 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources