Physics theoremStatement: AI-adaptedProof: 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.

Stationary curves of the mechanical action are exactly the restrictions of the model's motions (global potential branch)

Physical scope

The stationary-action principle for the global potential branch of the force model: every motion of the model restricts to a stationary curve of the mechanical action on each closed subinterval, and conversely every C^2 stationary curve on a closed interval is the restriction of the unique maximal motion of the model through its initial datum, so that the stationary curves are exactly the restrictions of motions. The equivalence is conditional on the adopted force branch, on the declared potential presentation with no residual forces, and on the cited existence, uniqueness and continuation theorems; it asserts no global existence, no minimisation property and no empirical statement.

Statement

Adopt the force model with potential presentation $(U, d)$ and mechanical Lagrangian $L = K - U$ of The action functional of a force model with a potential presentation: the mechanical Lagrangian, its chart instance and its dimensions, with masses $m_{1}, \dots, m_{N} > 0$ , open configuration domain $Q \subseteq R^{3 N}$ , time window $I_{0}$ , mass operator $M$ and $C^{2}$ potential $U : I_{0} \times Q \to R$ (Potential presentations of a force model, potential and mechanical energy, closed versus exact force fields, local potentials and equipotential level sets). Assume the presentation has no residual forces, $d \equiv 0$ , so that the force map itself is $F_{i} (t, x, v) = - \nabla_{x_{i}} U (t, x)$ . Then:

motions are stationary. If $x : J \to Q$ is a motion of the model on an interval $J$ with nonempty interior (The associated first-order system, motions, maximal motions and the Newtonian flow of a force model) and $a < b$ with $[a, b] \subseteq J \cap I_{0}$ , then the restriction $x ∣_{[a, b]}$ is stationary for the action $S$ on $[a, b]$ .
stationary curves are restrictions of motions. If $a < b$ with $[a, b] \subseteq I_{0}$ and $x : [a, b] \to Q$ is a $C^{2}$ admissible curve that is stationary for $S$ , then $x$ is the restriction to $[a, b]$ of the maximal motion of the model through the initial datum $(a, x (a), x^{'} (a))$ (whose existence and uniqueness are Local existence and uniqueness for the Newtonian initial-value problem, with the quantitative Picard-Lindelöf cylinder clause 4); in particular the maximal interval of that motion contains $[a, b]$ .
identification. Consequently the $C^{2}$ curves $x : [a, b] \to Q$ that are stationary for the action are exactly the restrictions to $[a, b]$ of the motions of the model whose maximal interval contains $[a, b]$ , and the model equation satisfied is $M x^{''} = - \nabla_{x} U$ on that interval.

The statement is conditional on the adopted force branch and on the declared potential presentation with $d \equiv 0$ ; it asserts no existence of stationary curves for arbitrary endpoint data, no minimisation and no empirical value.

Facts & Assumptions

Given: The model data and presentation of the statement with $d \equiv 0$ , reals $a < b$ with $[a, b] \subseteq I_{0}$ , and the curves occurring in clauses 1-3.

[F1]

The chart instance (The action functional of a force model with a potential presentation: the mechanical Lagrangian, its chart instance and its dimensions, A time-dependent Lagrangian chart, its action functional and its fixed-endpoint first variations): $(O, L)$ with $O = I_{0} \times Q \times R^{3 N}$ is a time-dependent Lagrangian chart, and stationarity of admissible curves is the stationarity of that chart.

[F2]

The identification of stationarity with the model's potential-part equation on the interval (The stationary-action criterion and the potential-part Euler-Lagrange equation): for a $C^{2}$ admissible curve $x : [a, b] \to Q$ , stationarity for $S$ , the vanishing of $E_{L} (x)$ on $[a, b]$ and the equation $M x^{''} (t) = - \nabla_{x} U (t, x (t))$ on $[a, b]$ are equivalent.

[F3]

Motions and the maximal motion (The associated first-order system, motions, maximal motions and the Newtonian flow of a force model, Adopted force model: force maps, the equation of motion, additive composition of force contributions and frame covariance clause (iv), Potential presentations of a force model, potential and mechanical energy, closed versus exact force fields, local potentials and equipotential level sets clause (a), Local existence and uniqueness for the Newtonian initial-value problem, with the quantitative Picard-Lindelöf cylinder): a motion on an interval $J$ with nonempty interior is a $C^{2}$ curve $x : J \to Q$ with $J \subseteq I_{0}$ satisfying $M x^{''} (t) = F (t, x (t), x^{'} (t))$ for all $t \in J$ , i.e. with $F_{i} = - \nabla_{x_{i}} U$ the equation $M x^{''} = - \nabla_{x} U$ ; and through every datum $(t_{0}, x_{0}, v_{0}) \in I_{0} \times Q \times R^{3 N}$ there is exactly one maximal motion, whose maximal interval $J_{\max}$ is an open interval containing $t_{0}$ and contained in $I_{0}$ , and every motion with that datum is a restriction of it. In particular two motions with the same datum agree on the intersection of their intervals.

[F4]

Continuation at a finite endpoint (Maximal Newtonian motions and the compact-continuation criterion: finite-time breakdown requires escape from every compact subset of the time-state domain, clauses 1-2): let $x_{\max} : J_{\max} \to Q$ be the maximal motion with a datum, $J_{\max} = (a_{0}, b_{0})$ , and $z_{\max} = (x_{\max}, x_{\max}^{}) : J_{\max} \to Q \times R^{3 N}$ its state curve, with time-state domain $D : = I_{0} \times Q \times R^{3 N}$ . If $b_{0} < + \infty$ , then for every compact $K \subseteq D$ and every $η > 0$ with $(b_{0} - η, b_{0}) \cap J_{\max} \neq \emptyset$ there is $t \in (b_{0} - η, b_{0}) \cap J_{\max}$ with $(t, z_{\max} (t)) \notin K$ ; equivalently, if a compact $K \subseteq D$ and $δ > 0$ satisfy $(t, z_{\max} (t)) \in K$ for all $t \in (b_{0} - δ, b_{0}) \cap J_{\max}$ , then $x_{\max}$ extends to a motion on a strictly larger interval than $J_{\max}$ , so $J_{\max}$ cannot have right endpoint $b_{0}$ .

[F5]

Compactness of a $C^{2}$ graph in the state domain (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line, The image of a compact metric space under a continuous map is compact, and so is the image of any compact subset, 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, The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral, $C^{k}$ Euclidean maps and diffeomorphisms, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length): if $x : [c, d] \to Q$ is $C^{2}$ then the graph $K : = {(t, x (t), x^{'} (t)) : t \in [c, d]}$ is the image of the compact interval $[c, d]$ under the continuous map $t \mapsto (t, x (t), x^{'} (t))$ , hence compact, and it is contained in the open state domain $D = I_{0} \times Q \times R^{3 N}$ because $[c, d] \subseteq I_{0}$ and $x$ takes values in $Q$ .

Proof

technique · direct; read the equivalence of stationarity with the model equation from the preceding theorem, and compare a stationary curve with the maximal motion through its initial datum by uniqueness and the compact continuation criterion

1.1F1F2F3given

Clause 1: let $x : J \to Q$ be a motion with $[a, b] \subseteq J \cap I_{0}$ . By [F3] the curve $x$ satisfies $M x^{''} (t) = - \nabla_{x} U (t, x (t))$ on $J$ , in particular on $[a, b]$ . By [F3], $x$ is the restriction of the maximal motion through $(a, x (a), x^{'} (a))$ , whose open interval contains $J$ , hence $[a, b]$ . This maximal motion supplies a $C^{2}$ extension to an open interval around $[a, b]$ , so $x ∣_{[a, b]}$ is an admissible curve of [F1], and condition 3 of [F2] holds on $[a, b]$ ; hence by [F2] it is stationary for $S$ .

1.2F2F3given

Clause 2, setup: let $x : [a, b] \to Q$ be stationary. By [F2] the curve satisfies $M x^{''} (t) = - \nabla_{x} U (t, x (t))$ for every $t \in [a, b]$ ; the datum $(a, x (a), x^{'} (a))$ lies in $I_{0} \times Q \times R^{3 N}$ because $[a, b] \subseteq I_{0}$ and $x$ takes values in $Q$ . Let $x_{\max} : J_{\max} \to Q$ be the maximal motion with this datum and $J_{\max} = (α, β)$ its maximal interval; by [F3], $α < a < β$ . The restriction $x ∣_{[a, b]}$ is a motion on $[a, b]$ with the same datum, so by the uniqueness clause of [F3], $x_{\max}$ and $x$ agree on $J_{\max} \cap [a, b]$ .

2.1step 1.2algebra

The intersection $J_{\max} \cap [a, b]$ equals $[a, β)$ if $β \leq b$ and $[a, b]$ if $β > b$ , because $α < a$ ; hence agreement in step 1.2 says that $x_{\max} = x$ on $[a, \min (β, b))$ with the intersection half-open when $β \leq b$ and closed when $β > b$ .

3.1F4F5step 2.1algebra

Claim: $β > b$ . Suppose first $β < b$ . By step 2.1, $x_{\max} = x$ on $[a, β)$ ; by [F5] applied to $x ∣_{[a, β]}$ the set $K : = {(t, x (t), x^{'} (t)) : t \in [a, β]}$ is a compact subset of $D$ . Choose $η : = β - a > 0$ ; for every $t \in (β - η, β) \cap J_{\max} = (a, β)$ one has $(t, z_{\max} (t)) = (t, x (t), x^{'} (t)) \in K$ . The extension form of [F4] then extends $x_{\max}$ beyond $β$ , contradicting the maximality of $J_{\max}$ . Hence $β \geq b$ .

3.2F4F5step 2.1algebra

Claim: $β = b$ is impossible. If $β = b$ , then by step 2.1 $x_{\max} = x$ on $[a, b)$ and ${(t, x (t), x^{'} (t)) : t \in [a, b]}$ is a compact subset $K$ of $D$ by [F5]; taking $δ : = b - a > 0$ , every $t \in (b - δ, b) \cap J_{\max} = (a, b)$ satisfies $(t, z_{\max} (t)) \in K$ , so the extension form of [F4] extends $x_{\max}$ beyond $b$ , again contradicting maximality.

4.1step 2.1step 3.1step 3.2

By steps 3.1 and 3.2, $β > b$ ; with step 2.1 this gives $J_{\max} \cap [a, b] = [a, b]$ , so $[a, b] \subseteq J_{\max}$ and $x = x_{\max} ∣_{[a, b]}$ : the curve $x$ is the restriction of the maximal motion through its initial datum, which is clause 2.

5.1step 1.1step 4.1F2F3∎

Clause 3: clause 1 shows that every restriction of a motion with $[a, b] \subseteq J \cap I_{0}$ is stationary, and clause 2 shows that every stationary curve is such a restriction; the equation satisfied is $M x^{''} = - \nabla_{x} U$ by [F2] and [F3].

Remarks

What the converse uses. The passage from a stationary curve to a motion uses the local existence and uniqueness theorem, the compact continuation criterion and the compactness of a $C^{2}$ graph in the open state domain. None of these hypotheses is automatic for curves defined on open intervals with boundary singularities; the statement is confined to closed intervals inside the time window.
No global existence. Clause 2 produces the maximal motion through the datum; its maximal interval is guaranteed to contain $[a, b]$ but need not be all of $I_{0}$ . Finite-time breakdown of the model's dynamics is thereby compatible with the equivalence, which concerns only curves that exist on the given interval.

Stationary curves of the mechanical action are exactly the restrictions of the model's motions (global potential branch)

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources