LemmaStatement: Literature-sourcedProof: Literature-sourcedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-06

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.

Morse trajectories have a positive energy drop

Statement

If $γ$ is a Morse trajectory from $p$ to $q$ , then

$f (p) - f (q) = \int_{- \infty}^{\infty} ∥ {grad}_{g} f (γ (t)) ∥_{g}^{2} d t > 0.$

Facts & Assumptions

Given: A Morse trajectory $γ : R \to M$ from $p$ to $q$ .

[F1]

Its endpoint limits are $p$ and $q$ and it is nonconstant (A Morse trajectory from one critical point to another).

[F2]

Its energy identity is $(f \circ γ)^{'} = - ∥ {grad}_{g} f ∥_{g}^{2}$ (A negative-gradient trajectory satisfies the energy identity).

[F3]

A nonconstant negative-gradient trajectory strictly decreases $f$ (Nonconstant negative-gradient trajectories strictly decrease the function).

Proof

technique · direct

1.1

Integrating [F2] on $[- T, T]$ gives $f (γ (- T)) - f (γ (T)) = \int_{- T}^{T} ∥ {grad}_{g} f (γ (t)) ∥_{g}^{2} d t$ .

F2given

2.1

Letting $T \to \infty$ and using [F1] and continuity of $f$ yields the stated improper-integral equality.

F1step 1.1

3.1

By [F3], $f \circ γ$ is strictly decreasing, so $f (p) > f (q)$ . The equality in step 2.1 therefore has strictly positive value.

F3step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

9 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, Lemma 13.1 (standard reference, not scraped)