TheoremStatement: AI-adaptedProof: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14

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.

Euler–Lagrange equations

Statement

A $C^{2}$ fixed-endpoint curve is stationary for $S_{L}$ if and only if, in every coordinate chart along the curve,

$\frac{d}{d t} \frac{\partial L}{\partial v^{i}} (q (t), \dot{q} (t)) - \frac{\partial L}{\partial q^{i}} (q (t), \dot{q} (t)) = 0 (1 \leq i \leq \dim Q) .$

Facts & Assumptions

Given: A smooth Lagrangian $L$ and a $C^{2}$ curve with fixed endpoints.

[F1]

Stationarity is defined using all smooth fixed-endpoint variations. Lagrangian action functional on curves.

[F2]

Integration by parts moves one time derivative and exposes the endpoint term. If $u, v$ are differentiable on $[a, b]$ with $u^{'}, v^{'}$ integrable, then $\int_{a}^{b} u v^{'} = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u^{'} v$ .

Proof

technique · direct

1.1

On a chart subinterval, a variation field $η^{i} (t) = \partial_{s} q_{s}^{i} ∣_{s = 0}$ with zero endpoint values gives, by differentiation under the finite integral, $δ S_{L} = \int_{a}^{b} (L_{q^{i}} η^{i} + L_{v^{i}} {\dot{η}}^{i}) d t .$

F1givenalgebra

2.1

Apply [F2]. The boundary term $[L_{v^{i}} η^{i}]_{a}^{b}$ vanishes, leaving $δ S_{L} = \int_{a}^{b} (L_{q^{i}} - \frac{d}{d t} L_{v^{i}}) η^{i} d t$ . Thus the displayed equations imply stationarity.

F2step 1.1

3.1

Conversely, if one continuous coefficient $E_{i} = L_{q^{i}} - \frac{d}{d t} L_{v^{i}}$ were nonzero at an interior time, it would retain one strict sign on a smaller interval. Choosing a nonnegative smooth bump $η^{i}$ supported there and all other components zero would make the integral in step 2.1 nonzero, contradicting stationarity. Hence all $E_{i}$ vanish. Variations supported in chart subintervals cover the curve, proving the coordinate-independent equivalence.

F1step 2.1construct∎

Depends on

Used by

Equivalence of Euler–Lagrange and Hamilton equations for hyperregular Lagrangians Theorem

Dependency tree · two levels

13 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

Ana Cannas da Silva, Lectures on Symplectic Geometry (standard reference, not scraped)