ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck 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 free particle: the unique stationary curve between fixed endpoints is the straight uniform motion, and it minimises the action

Physical scope

A worked check of the stationary-action equivalence on the free one-label model: zero force map, zero potential, Cartesian Lagrangian of a free particle; on every closed time interval the stationary curves are exactly the affine uniform motions, for each pair of endpoint configurations there is exactly one, and the action difference to the stationary curve is a nonnegative quadratic functional of the variation, so the stationary curve is a minimiser within the fixed-endpoint class. The mass, position, time and velocity carry dimensions mass, length, time and length per time, respectively. All quantities are model values under the declared idealization of a particle subject to no force.

Example

Declare a one-label model of the force branch of Adopted force model: force maps, the equation of motion, additive composition of force contributions and frame covariance with $N = 1$ , mass $m > 0$ , time window $I_{0} = R$ , configuration domain $Q = R^{3}$ and zero force map $F \equiv 0$ ; this is the global potential model with potential $U \equiv 0$ and no residual forces (Potential presentations of a force model, potential and mechanical energy, closed versus exact force fields, local potentials and equipotential level sets), whose mechanical Lagrangian is $L (t, x, v) = \frac{1}{2} m ∣ v ∣_{2}^{2}$ (The action functional of a force model with a potential presentation: the mechanical Lagrangian, its chart instance and its dimensions). Let $a < b$ , let $x_{a}, x_{b} \in R^{3}$ , and consider the $C^{2}$ curves $x : [a, b] \to R^{3}$ with $x (a) = x_{a}$ and $x (b) = x_{b}$ . Under the units of Dimensions and SI unit conventions of the non-relativistic classical mechanics framework, $[m] = μ$ , $[x] = [x_{a}] = [x_{b}] = ℓ$ , $[t] = [a] = [b] = τ$ , and $[x^{'}] = ℓ τ^{- 1}$ .

Then:

$x$ is stationary for the action $S$ if and only if $x$ is affine, $x (t) = x_{a} + v_{0} (t - a)$ with constant $v_{0} \in R^{3}$ ; consequently there is exactly one stationary curve with the prescribed endpoints, $x_{*} (t) : = x_{a} + \frac{t - a}{b - a} (x_{b} - x_{a}), x_{*}^{'} = \frac{x_{b} - x_{a}}{b - a} .$
For every variation $η$ of $x_{*}$ one has the exact identity $S (x_{*} + η) - S (x_{*}) = \frac{m}{2} \int_{a}^{b} ∣ η^{'} (t) ∣_{2}^{2} d t \geq 0,$ with equality if and only if $η = 0$ ; hence $x_{*}$ is the unique minimiser of $S$ in the class of $C^{2}$ curves with these endpoints.
The global affine curve $x_{\max} : R \to R^{3}$ defined by $x_{\max} (t) = x_{a} + v_{0} (t - a)$ , with $v_{0} : = (x_{b} - x_{a}) / (b - a)$ , is the unique maximal motion through the datum $(a, x_{a}, v_{0})$ , and $x_{*} = x_{\max} ∣_{[a, b]}$ .

All quantities are model values; no measurement is reported.

Facts & Assumptions

Given: The model data of the Example, $a < b$ , the endpoints $x_{a}, x_{b}$ , the curve $x_{*}$ and a variation $η$ with $η (a) = η (b) = 0$ of $x_{*}$ .

[F1]

The chart and the equivalence (The action functional of a force model with a potential presentation: the mechanical Lagrangian, its chart instance and its dimensions, The stationary-action criterion and the potential-part Euler-Lagrange equation): $(O, L)$ with $O = R \times R^{3} \times R^{3}$ is a time-dependent Lagrangian chart, and a $C^{2}$ curve $x$ is stationary for $S$ if and only if $m x^{''} (t) = - \nabla U (t, x (t)) = 0$ for every $t \in [a, b]$ .

[F2]

Motion and maximal motion (Stationary curves of the mechanical action are exactly the restrictions of the model's motions (global potential branch), The associated first-order system, motions, maximal motions and the Newtonian flow of a force model): the stationary curves of $S$ on $[a, b]$ are the restrictions of the motions of the model with interval containing $[a, b]$ ; every motion with $M x^{''} = 0$ is affine, and through each datum there is exactly one maximal motion.

[F3]

Integral and derivative calculus (The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ , 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$ , If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ , A continuous $f \geq 0$ on $[a, b]$ with $\int_{a}^{b} f = 0$ is identically $0$ , 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$ , The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral, 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, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length, The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ , Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ ): the integral is linear and monotone on continuous integrands; a continuous nonnegative function with zero integral vanishes identically; and componentwise the fundamental theorem gives $\int_{u}^{v} f^{'} = f (v) - f (u)$ for the $C^{1}$ functions used here. The derivatives of a $C^{2}$ curve on $[a, b]$ are continuous and the usual derivative algebra applies.

Verification

technique · direct; solve the second-order equation of the free model, then expand the action of a varied curve and integrate by parts

1.1F1F3givenalgebra

Equation and uniqueness: by [F1], stationary means $x^{''} \equiv 0$ on $[a, b]$ because $m > 0$ . Componentwise, [F3] applied to $x^{'}$ gives $x^{'} (t) - x^{'} (a) = \int_{a}^{t} x^{''} (u) d u = 0$ for every $t \in [a, b]$ ; applying it to $x$ then gives $x (t) = x (a) + x^{'} (a) (t - a)$ , so $x$ is affine. Conversely an affine curve has $x^{''} \equiv 0$ and is stationary by [F1]. Its endpoint values force $x^{'} (a) = (x_{b} - x_{a}) / (b - a)$ , well defined because $b > a$ ; hence $x_{*}$ is the unique stationary curve with the prescribed endpoints.

2.1F3step 1.1algebra

Expansion of the action: let $η$ be a variation. Since $L$ is quadratic with no linear term, $S (x_{*} + η) - S (x_{*}) = \frac{m}{2} \int_{a}^{b} (∣ x_{*}^{'} + η^{'} ∣_{2}^{2} - ∣ x_{*}^{'} ∣_{2}^{2}) d t = \frac{m}{2} \int_{a}^{b} (2 x_{*}^{'} \cdot η^{'} + ∣ η^{'} ∣_{2}^{2}) d t .$ The first term vanishes: $x_{*}^{'}$ is the constant vector $v_{0}$ , so by [F3] $\int_{a}^{b} x_{*}^{'} \cdot η^{'} d t = v_{0} \cdot \int_{a}^{b} η^{'} d t = v_{0} \cdot (η (b) - η (a)) = 0$ because $η$ vanishes at both endpoints. Hence $S (x_{*} + η) - S (x_{*}) = \frac{m}{2} \int_{a}^{b} ∣ η^{'} ∣_{2}^{2} d t \geq 0$ by [F3].

3.1F3step 2.1algebra

Equality case: if the integral vanishes, the continuous nonnegative integrand $∣ η^{'} ∣_{2}^{2}$ vanishes identically on $[a, b]$ by [F3], so $η^{'} \equiv 0$ . The fundamental theorem in [F3] gives $η (t) - η (a) = \int_{a}^{t} η^{'} (u) d u = 0$ componentwise; since $η (a) = 0$ , $η \equiv 0$ . Thus the stationary curve is the unique minimiser in the fixed-endpoint class.

4.1F2step 1.1∎

Consistency with the flow: by [F2] the curve $x_{*}$ is the restriction of the maximal motion through $(a, x_{a}, v_{0})$ ; the affine curve $t \mapsto x_{a} + v_{0} (t - a)$ is a motion on all of $R$ , hence the maximal motion is defined for all times and equals $x_{*}$ on $[a, b]$ .

Remarks

The exact identity of step 2.1 shows that for the free particle the stationary curve is a genuine minimiser, not a saddle; the oscillator example of this page exhibits the opposite phenomenon for large intervals. Both computations are model checks of the stationarity theorem; neither is a claim that nature extremises an action.

The free particle: the unique stationary curve between fixed endpoints is the straight uniform motion, and it minimises the action

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources