TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-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.

Stationarity of the time-dependent action is equivalent to the vanishing of the Euler-Lagrange expression

Statement

Let $(O, L)$ be a time-dependent Lagrangian chart over $[a, b] \times U$ in the sense of A time-dependent Lagrangian chart, its action functional and its fixed-endpoint first variations and let $q : [a, b] \to U$ be a $C^{2}$ admissible curve. Then $q$ is stationary for the action $S$ if and only if

$E_{L} (q) (t) = 0 for every t \in [a, b] .$

Facts & Assumptions

Given: The chart data $(O, L)$ , a $C^{2}$ curve $q : [a, b] \to U$ , and the notation of A time-dependent Lagrangian chart, its action functional and its fixed-endpoint first variations: the action $S$ , the first variation $δ S (q) [η]$ over variations $η$ , the gradients $L_{q}, L_{v}$ and the Euler–Lagrange expression $E_{L} (q)$ .

[F1]

First variation formula and continuity (The first variation of a time-dependent action on a finite interval: admissibility, the integral formula and continuity of the Euler-Lagrange coefficient): for every variation $η$ the value $δ S (q) [η]$ exists and equals $\int_{a}^{b} [L_{q} (t, q, q^{'}) \cdot η + L_{v} (t, q, q^{'}) \cdot η^{'}] d t,$ and $E_{L} (q)$ is continuous on $[a, b]$ .

[F2]

The bumps of Explicit twice differentiable bumps detect nonzero values of continuous functions: for every open interval $J$ , continuous $E : J \to R$ and $t_{1} \in J$ with $E (t_{1}) \neq 0$ there are $ρ > 0$ with $[t_{1} - ρ, t_{1} + ρ] \subseteq J$ and a $C^{2}$ function $β : R \to R$ vanishing outside $[t_{1} - ρ, t_{1} + ρ]$ , $0 \leq β \leq 1$ and $\int_{t_{1} - ρ}^{t_{1} + ρ} E β \neq 0$ .

[F3]

Integration by parts (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$ ): if $u, v : [a, b] \to R$ are differentiable at every point with integrable derivatives, then $\int_{a}^{b} u v^{'} = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u^{'} v$ . Here $u : = (L_{v} (t, q (t), q^{'} (t)))_{i}$ is $C^{1}$ and $v : = η_{i}$ is $C^{2}$ for a variation $η$ , so both derivatives are continuous, hence integrable (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion, The lower and upper Darboux integrals of a bounded $f$ on $[a, b]$ as $\sup_{P} L (f, P)$ and $\inf_{P} U (f, P)$ , Darboux integrability as their equality, and the notation $\int_{a}^{b} f$ ).

[F4]

Linearity of the integral (Integrable functions on $[a, b]$ form a set closed under sums and scalar multiples, and $\int_{a}^{b} (λ f + μ g) = λ \int_{a}^{b} f + μ \int_{a}^{b} g$ ) permits finite sums and fixed real coefficients to pass through the integral. A map on an open interval is $C^{2}$ precisely when its scalar components are $C^{2}$ ( $C^{k}$ Euclidean maps and diffeomorphisms). In step 1.3 each component of the extended variation is either the given $C^{2}$ bump or the zero function, whose derivatives are zero by The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set; hence that variation has a $C^{2}$ extension as required by A time-dependent Lagrangian chart, its action functional and its fixed-endpoint first variations.

[F5]

Continuity of $E_{L} (q)$ at a point; if $E_{L} (q) (t_{0}) \neq 0$ then for small $δ > 0$ the expression is nonzero throughout $(t_{0} - δ, t_{0} + δ) \cap [a, b]$ (Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point, Absolute value in an ordered field).

Proof

technique · direct; one direction is integration by parts, the other localises a nonzero component of the coefficient with a bump and produces a nonzero first variation

1.1F1F3F4given

Assume $E_{L} (q) = 0$ on $[a, b]$ and let $η$ be any variation. By [F1], $δ S (q) [η] = \sum_{i = 0}^{n - 1} \int_{a}^{b} [(L_{q})_{i} η_{i} + (L_{v})_{i} η_{i}^{'}] d t .$ For each $i$ , [F3] applied to $u = (L_{v})_{i}$ and $v = η_{i}$ gives $\int_{a}^{b} (L_{v})_{i} η_{i}^{'} = - \int_{a}^{b} \frac{d}{d t} (L_{v})_{i} η_{i}$ , because $η_{i} (a) = η_{i} (b) = 0$ . Hence each summand equals $\int_{a}^{b} ((L_{q})_{i} - \frac{d}{d t} (L_{v})_{i}) η_{i} d t$ , and by [F4] and the hypothesis all summands vanish. Thus $δ S (q) [η] = 0$ ; as $η$ was arbitrary, $q$ is stationary.

1.2F5given

Conversely, suppose $E_{L} (q) (t_{0}) \neq 0$ for some $t_{0} \in [a, b]$ . By [F5] the continuous expression $E_{L} (q)$ is nonzero at a point $t_{1}$ interior to $[a, b]$ : if $t_{0} \in (a, b)$ take $t_{1} : = t_{0}$ ; if $t_{0} = a$ , choose $t_{1} \in (a, \min (a + δ, b))$ provided by [F5] applied at $a$ (the interval is nonempty because $a < b$ ), and symmetrically for $t_{0} = b$ . Choose a component $i$ with $(E_{L} (q) (t_{1}))_{i} \neq 0$ .

1.3F2F4

Apply [F2] to the open interval $J : = (a, b)$ , the continuous function $E : = (E_{L} (q))_{i}$ and the point $t_{1}$ : this gives $ρ > 0$ with $[t_{1} - ρ, t_{1} + ρ] \subseteq (a, b)$ and a $C^{2}$ bump $β$ vanishing outside $[t_{1} - ρ, t_{1} + ρ]$ with $\int E β \neq 0$ . Define $η : [a, b] \to R^{n}$ by $η_{i} : = β$ and $η_{j} : = 0$ for $j \neq i$ on $[a, b]$ , extended to an open interval around $[a, b]$ by the same formula. Then $η$ is a variation and, because the support of $β$ lies inside $(a, b)$ , it vanishes near both endpoints.

2.1F1F2step 1.1step 1.3algebra

Evaluate the first variation of $η$ : by [F1] and the reduction of step 1.1 applied to this single component, $δ S (q) [η] = \int_{a}^{b} [(L_{q})_{i} β + (L_{v})_{i} β^{'}] d t = \int_{a}^{b} E (t) β (t) d t \neq 0.$ Hence $q$ is not stationary. Contraposition gives: if $q$ is stationary, then $E_{L} (q) (t_{0}) = 0$ for every $t_{0} \in [a, b]$ .

3.1step 1.1step 2.1∎

Steps 1.1 and 2.1 prove the two implications of the statement.

Remarks

Stationarity is an integral condition; the theorem identifies it with the pointwise vanishing of a continuous coefficient. It does not say that a stationary curve minimises the action, and Scope of stationarity: stationary is not minimum, and no second-variation theory is developed here records the distinction with a counterexample on the companion page.
The proof uses $C^{2}$ variations because the bump of Explicit twice differentiable bumps detect nonzero values of continuous functions is of class $C^{2}$ ; the same argument with a smooth bump would give the $C^{\infty}$ version, but smoothness is not needed by the consuming items of this page.

Stationarity of the time-dependent action is equivalent to the vanishing of the Euler-Lagrange expression

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources