LemmaStatement: Literature-sourcedProof: Literature-sourcedPipeline-generatedprecheck pass

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 continuation energy identity

Statement

Assume ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )) for the smooth-bundle setup. Let $(f_{s}, g_{s})$ be a continuation datum from $(f^{-}, g^{-})$ to $(f^{+}, g^{+})$ on a closed manifold $M$ , and let $u$ be a solution of the continuation equation with limits $p \in Crit (f^{-})$ , $q \in Crit (f^{+})$ (A regular continuation datum between Morse--Smale pairs, Continuation solutions have critical limits and exponential decay). Write $E (u) = \int_{R} ∣ \partial_{s} u (s) ∣_{g_{s}}^{2} d s$ and $(\partial_{s} f_{s}) (x) = \frac{\partial f_{s}}{\partial s} (x)$ . Then $E (u) = f^{-} (p) - f^{+} (q) + \int_{R} (\partial_{s} f_{s}) (u (s)) d s .$ Since $\partial_{s} f_{s} = 0$ on $M \times ((- \infty, - S] \cup [S, \infty))$ and $(\partial_{s} f_{s}) (u (s))$ is integrable by smoothness and compact support, in particular $0 \leq E (u) \leq f^{-} (p) - f^{+} (q) + 2 S \max_{(s, x) \in [- S, S] \times M} ∣ (\partial_{s} f_{s}) (x) ∣ .$ For a constant datum ( $f_{s} = f$ , $g_{s} = g$ for all $s$ ) the identity reduces to the classical energy identity $\int_{R} ∣ \dot{u} ∣^{2} = f (p) - f (q)$ of A negative-gradient trajectory satisfies the energy identity.

Facts & Assumptions

Given: ${A C}_{ω}$ , a closed manifold $M$ , a continuation datum $(f_{s}, g_{s})$ with threshold $S > 0$ , and a solution $u$ of the continuation equation with limits $p, q$ .

[F1]

The datum is constant on the two half-lines: $(f_{s}, g_{s}) = (f^{-}, g^{-})$ for $s \leq - S$ and $(f_{s}, g_{s}) = (f^{+}, g^{+})$ for $s \geq S$ (A regular continuation datum between Morse--Smale pairs).

[F2]

The gradient is characterized by $g_{s} (\nabla^{g_{s}} f_{s}, v) = d f_{s} (v)$ for every $v$ , so along a solution $d f_{s} (\partial_{s} u) = g_{s} (\nabla^{g_{s}} f_{s} (u), \partial_{s} u) = - ∣ \partial_{s} u ∣_{g_{s}}^{2}$ (The Riemannian gradient is the metric dual of the differential).

[F3]

The stated limits and continuity give $f^{-} (u (s)) \to f^{-} (p)$ and $f^{+} (u (s)) \to f^{+} (q)$ . The function $(\partial_{s} f_{s}) (u (s))$ is smooth and supported in $[- S, S]$ , hence integrable. These facts use the given limits, not a choice-dependent existence or exponential-decay theorem.

[F4]

Along an autonomous negative-gradient curve, $\frac{d}{d s} f (u) = - ∣ \dot{u} ∣^{2}$ (A negative-gradient trajectory satisfies the energy identity). Integrating on finite intervals and taking the given limits yields $\int_{R} ∣ \dot{u} ∣^{2} = f (p) - f (q)$ , including constant curves.

Proof

technique · direct

1.1givenalgebra

The curve $s \mapsto f_{s} (u (s))$ is smooth, and differentiating it gives $\frac{d}{d s} (f_{s} \circ u) = d f_{s} (\partial_{s} u) + (\partial_{s} f_{s}) (u)$ , the two terms being the derivatives through the second argument and through the explicit $s$ -dependence of $f_{s}$ .

2.1F2step 1.1algebra

Substituting the continuation equation $\partial_{s} u = - \nabla^{g_{s}} f_{s} (u)$ into [F2] gives $d f_{s} (\partial_{s} u) = - ∣ \partial_{s} u ∣_{g_{s}}^{2}$ ; combining with step 1.1 yields $\frac{d}{d s} (f_{s} \circ u) = - ∣ \partial_{s} u ∣_{g_{s}}^{2} + (\partial_{s} f_{s}) (u)$ .

3.1step 2.1algebra

Integrate step 2.1 over $[- S^{'}, S^{'}]$ and apply the fundamental theorem of calculus: $f_{S^{'}} (u (S^{'})) - f_{- S^{'}} (u (- S^{'})) = - \int_{- S^{'}}^{S^{'}} ∣ \partial_{s} u ∣_{g_{s}}^{2} d s + \int_{- S^{'}}^{S^{'}} (\partial_{s} f_{s}) (u (s)) d s$ .

4.1F1F3step 3.1

By [F3] the endpoints converge, $f_{- S^{'}} (u (- S^{'})) = f^{-} (u (- S^{'})) \to f^{-} (p)$ and $f_{S^{'}} (u (S^{'})) = f^{+} (u (S^{'})) \to f^{+} (q)$ , while the integral of $(\partial_{s} f_{s}) (u (s))$ is already constant for $S^{'} > S$ . The identity of step 3.1 therefore makes the nonnegative integrals $\int_{- S^{'}}^{S^{'}} ∣ \partial_{s} u ∣_{g_{s}}^{2}$ converge to a finite limit as $S^{'} \to \infty$ ; by the definition of the improper integral, this gives $E (u) = f^{-} (p) - f^{+} (q) + \int_{R} (\partial_{s} f_{s}) (u (s)) d s$ .

5.1F1F4step 4.1algebra∎

By [F1] the integrand $(\partial_{s} f_{s}) (u (s))$ vanishes off $[- S, S]$ , so its integral is bounded by $2 S \max_{[- S, S] \times M} ∣ (\partial_{s} f_{s}) ∣$ , and $E (u) \geq 0$ by definition; this gives the displayed two-sided bound. For a constant datum $(\partial_{s} f_{s}) = 0$ and step 4.1 becomes exactly [F4].

Depends on

Used by

Dependency tree · two levels

38 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

Alexander F. Ritter, Part III Morse Homology (Cambridge lecture notes, complete author PDF, 115 pp.) (standard reference, not scraped)
Liviu I. Nicolaescu, An Invitation to Morse Theory, 2nd ed. (complete author PDF, 291 pp.) (standard reference, not scraped)
Michele Audin and Mihai Damian, Morse Theory and Floer Homology (complete author PDF of the English book, 628 pp.) (standard reference, not scraped)