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.
Length-energy inequality and constant-speed equality case
Statement
For every piecewise smooth curve with , Equality holds if and only if is constant almost everywhere, equivalently if its continuous restriction to the interior of every smooth piece is one common constant.
Facts & Assumptions
Given: A piecewise smooth curve on with , a finite smooth subdivision, and its nonnegative piecewise continuous speed .
Riemannian speed and length gives , interpreted as the finite sum over the pieces, and Energy of a piecewise smooth curve gives with the same convention.
A nonnegative continuous function on a compact interval has zero Riemann integral exactly when it vanishes identically (A continuous on with is identically ).
Proof
Put and . Finite additivity and ordinary integral algebra on the smooth pieces give Multiplying by proves .
Conversely, if almost everywhere, changing finitely many breakpoint values does not affect either integral, so and . Hence . The same computation applies when .
If equality holds, step 1.1 gives a zero total integral of . Every piece integral is nonnegative, so each is zero. On the interior of each piece, is continuous; applying [F2] on compact subintervals contained in that interior gives there. Thus away from the finitely many breakpoints, hence almost everywhere, and it has the same constant value on every smooth piece.
Steps 2.1 and 1.2 prove both directions of the equality characterization. A constant curve has and realizes equality. In dimension zero every curve is locally constant, so the same case applies; dimension one is unchanged. A curve on a nonempty interval cannot have empty target. The hypothesis excludes division by a zero interval length; endpoint and corner values occur on a finite set and do not alter the integrals. No point or representative is chosen from an indexed family, so the proof is choice-free.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
18 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
- Ved Datar, Lectures on Riemannian Geometry, discussion after Definition 16.1.3, p.120 (standard reference, not scraped)