CorollaryStatement: Literature-sourcedProof: Literature-sourcedPipeline-generatedjudge pass (gpt-6.1-sol)

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.

Strong Morse inequalities

Statement

Assume ${A C}_{ω}$ . In the situation of the Morse polynomial identity (Morse polynomial identity), for every $k$ $\sum_{i = 0}^{k} (- 1)^{k - i} m_{i} (f) \geq \sum_{i = 0}^{k} (- 1)^{k - i} b_{i} (M; F),$ and the difference of the two sides equals the coefficient $q_{k}$ of the correction polynomial $Q$ ; for $k \geq n$ the two sides are equal, the common value being $(- 1)^{k} \sum_{i} (- 1)^{i} m_{i} (f) = (- 1)^{k} \sum_{i} (- 1)^{i} b_{i} (M; F)$ .

Facts & Assumptions

Given: A closed smooth $n$ -manifold $M$ , a Morse function $f : M \to R$ , a field $F$ , the correction polynomial $Q (t) = \sum_{k} q_{k} t^{k}$ of the Morse polynomial identity with $q_{k} \geq 0$ , and the Morse and Betti numbers $m_{k} = m_{k} (f)$ , $b_{k} = b_{k} (M; F)$ .

[F1]

$M_{f} (t) = P_{M, F} (t) + (1 + t) Q (t)$ with $Q \in Z [t]$ having nonnegative coefficients, and $M_{f} (t) = \sum_{k = 0}^{n} m_{k} (f) t^{k}$ , $P_{M, F} (t) = \sum_{k} b_{k} (M; F) t^{k}$ (Morse polynomial identity, Morse numbers and the Morse polynomial, Poincare polynomial of a space and of a pair over a field).

[F2]

The partial sums recover the coefficients: $\sum_{i = 0}^{k} (- 1)^{k - i} (\dim A_{i} + \dim C_{i} - \dim B_{i})$ is the coefficient $q_{k} = \dim \ker (A_{k} \to B_{k}) \geq 0$ of the correction polynomial of a long exact sequence (Rank bookkeeping for a long exact sequence of finite-dimensional vector spaces).

Proof

technique · coefficient-comparison

1.1F1givenalgebra

Comparing coefficients in the identity of [F1], the coefficient of $t^{k}$ in $M_{f} - P_{M, F}$ is $m_{k} - b_{k}$ , and the coefficient of $t^{k}$ in $(1 + t) Q$ is $q_{k} + q_{k - 1}$ with $q_{- 1} : = 0$ ; hence $m_{k} - b_{k} = q_{k} + q_{k - 1}$ for every $k$ .

2.1F2step 1.1algebra

Telescoping the identities of step 1.1 over $i = 0, \dots, k$ gives $\sum_{i = 0}^{k} (- 1)^{k - i} (m_{i} - b_{i}) = \sum_{i = 0}^{k} (- 1)^{k - i} (q_{i} + q_{i - 1}) = q_{k} \geq 0,$ which is the displayed strong inequality and identifies the difference of the two sides with $q_{k}$ . This restates the dimension bookkeeping of [F2] in the present notation.

2.2step 1.1F1algebra

Since $M_{f}$ and $P_{M, F}$ have degree at most $n$ , the left side $M_{f} - P_{M, F} = (1 + t) Q$ also has all coefficients zero in degrees $> n$ . If $q_{K} \neq 0$ for some $K \geq n$ , take $K$ maximal with this property; then the coefficient identity of step 1.1 at $k = K + 1 > n$ reads $0 = m_{K + 1} - b_{K + 1} = q_{K + 1} + q_{K} = 0 + q_{K}$ , a contradiction. Hence $q_{k} = 0$ for every $k \geq n$ .

3.1step 2.1step 2.2F1∎

For $k \geq n$ step 2.1 then gives equality of the two alternating partial sums; all terms with $i > n$ vanish, so the common value alternates in sign with $k$ , so the common value is $\sum_{i = 0}^{n} (- 1)^{k - i} m_{i} = \sum_{i = 0}^{n} (- 1)^{k - i} b_{i}$ .

Remarks

Weak form. Adding the nonnegative differences in degrees $k$ and $k - 1$ gives $m_{k} - b_{k} = q_{k} + q_{k - 1} \geq 0$ ; this is recorded separately.
Euler case. At $k = n$ the common value is $(- 1)^{n} \sum_{i} (- 1)^{i} m_{i} = (- 1)^{n} \sum_{i} (- 1)^{i} b_{i}$ ; the identification of either sum with $(- 1)^{n} χ (M)$ is the Euler characteristic identity proved below.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

35 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

Ralph L. Cohen, Bundles, Manifolds, and Homotopy, Chapter 12 Section 5, printed pp. 489-493 (PDF pp. 501-505) (standard reference, not scraped)
Alexander Ritter, Morse Homology (Cambridge Part III lecture notes), Lecture 21, PDF pp. 96-101 (standard reference, not scraped)
C. T. C. Wall, Differential Topology, Sections 5.1-5.4, printed pp. 129-148 (PDF pp. 137-151) (standard reference, not scraped)