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.

A total-derivative Lagrangian on explicit data: the endpoint term and the unchanged equations

Physical scope

A worked gauge check on the free one-label model in three-dimensional configuration space: adding the total time derivative of F(t,x)=alphatx_1 to the free Lagrangian changes the action by endpoint values and leaves the Euler-Lagrange expression equal to the original one, hence leaves stationary curves and the model equation unchanged. The position is a vector of length dimension, time has time dimension, alpha has force dimension, and F has action dimension. The potential normalization U + gammat is the special case F = -gammat^2/2, with gamma of energy-per-time dimension. The values are exact model values of a declared computation.

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; the 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 $t_{0} > 0$ be a time scale, fix the interval $[t_{0}, 2 t_{0}]$ , a dimensioned parameter $α$ with $[α] = μ ℓ τ^{- 2}$ , and the $C^{2}$ function

$F (t, x) : = α t x_{1}, L^{'} (t, x, v) : = L (t, x, v) + F_{t} (t, x) + F_{x} (t, x) \cdot v = \frac{1}{2} m ∣ v ∣_{2}^{2} + α x_{1} + α t v_{1},$

so that $L^{'}$ is the Lagrangian $L$ plus the total time derivative of $F$ (Total-derivative Lagrangians, the potential representative and scaling: invariant stationary curves with endpoint terms). Under Dimensions and SI unit conventions of the non-relativistic classical mechanics framework, $[m] = μ$ , $[x] = ℓ$ , $[t] = [t_{0}] = τ$ , and $[F] = [S] = μ ℓ^{2} τ^{- 1}$ . Fix a unit vector $e_{1} = (1, 0, 0)$ and a velocity $v_{0}$ with $[v_{0}] = ℓ τ^{- 1}$ , and consider the dimensionally consistent affine curve $x_{*} (t) : = v_{0} (t - t_{0})$ on $[t_{0}, 2 t_{0}]$ .

Then:

for every $C^{2}$ curve $x : [t_{0}, 2 t_{0}] \to R^{3}$ one has $E_{L^{'}} (x) (t) = E_{L} (x) (t) = - m x^{''} (t)$ at every $t \in [t_{0}, 2 t_{0}]$ , and the stationary curves of $S$ and $S^{'}$ coincide;
for the curve $x_{*}$ the actions satisfy $S^{'} (x_{*}) - S (x_{*}) = F (2 t_{0}, x_{*} (2 t_{0})) - F (t_{0}, x_{*} (t_{0})) = 2 α t_{0}^{2} (e_{1} \cdot v_{0}),$ with $S (x_{*}) = \frac{1}{2} m ∣ v_{0} ∣_{2}^{2} t_{0}$ and $S^{'} (x_{*}) = S (x_{*}) + 2 α t_{0}^{2} (e_{1} \cdot v_{0})$ ;
for the reference-unit choice $m = 1 k g$ , $t_{0} = 1 s$ , $v_{0} = (1 m s^{- 1}) e_{1}$ and $α = 1 k g m s^{- 2}$ , these values are $S = 0.5 k g m^{2} s^{- 1}$ , $S^{'} = 2.5 k g m^{2} s^{- 1}$ and endpoint term $2 k g m^{2} s^{- 1}$ , all of dimension $μ ℓ^{2} τ^{- 1}$ , while the equation of motion and stationary curves are unchanged.

Facts & Assumptions

Given: The model and functions of the Example, the curve $x_{*}$ , and a $C^{2}$ curve $x : [t_{0}, 2 t_{0}] \to R^{3}$ .

[F1]

The gauge theorem (Total-derivative Lagrangians, the potential representative and scaling: invariant stationary curves with endpoint terms): for the mechanical Lagrangian $L$ and the $C^{3}$ function $F$ defined throughout the chart time-configuration domain with action dimension, the Lagrangian $L^{'} = L + F_{t} + \nabla_{x} F \cdot v$ is $C^{2}$ , satisfies $E_{L^{'}} = E_{L}$ and $S^{'} (x) = S (x) + F (b, x (b)) - F (a, x (a))$ for every $C^{2}$ admissible curve, and has the same stationary curves; a potential normalization $\tilde{U} = U + γ t$ uses $F (t, x) = - γ t^{2} / 2$ , where $[γ] = μ ℓ^{2} τ^{- 3}$ .

[F2]

Stationarity criterion (The stationary-action criterion and the potential-part Euler-Lagrange equation, The action functional of a force model with a potential presentation: the mechanical Lagrangian, its chart instance and its dimensions): a $C^{2}$ curve is stationary for the action of a mechanical Lagrangian if and only if it satisfies $m x^{''} = - \nabla_{x} U$ ; for the free model this is $x^{''} = 0$ , whose solutions on $[t_{0}, 2 t_{0}]$ are the affine vector curves.

[F3]

Calculus facts (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)$ , 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$ , 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$ , 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 Jacobian matrix of partial derivatives and the gradient in the scalar-valued case, Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to 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): for this $F$ one has $F_{t} = α x_{1}$ and $\nabla_{x} F = α t e_{1}$ , so $\frac{d}{d t} F (t, x (t)) = F_{t} + \nabla_{x} F \cdot x^{'}$ ; its integral over $[t_{0}, 2 t_{0}]$ is the endpoint difference. Also $S (x_{*}) = \int_{t_{0}}^{2 t_{0}} \frac{1}{2} m ∣ v_{0} ∣_{2}^{2} d t = \frac{1}{2} m ∣ v_{0} ∣_{2}^{2} t_{0}$ .

Verification

technique · direct; compute the two Euler-Lagrange expressions on a general curve and evaluate the endpoint term and both actions on explicit data

1.1F1F2F3givenalgebra

The displayed $F (t, x) = α t x_{1}$ is a polynomial, hence $C^{\infty}$ (in particular $C^{3}$ ), throughout the chart projection $R \times R^{3}$ . For a $C^{2}$ curve $x$ on $[t_{0}, 2 t_{0}]$ , $\nabla_{x} L^{'} = α e_{1}$ and $L_{v}^{'} = m x^{'} + α t e_{1}$ , so $E_{L^{'}} (x) (t) = α e_{1} - \frac{d}{d t} (m x^{'} (t) + α t e_{1}) = - m x^{''} (t) = E_{L} (x) (t)$ pointwise; hence the vanishing sets on this interval coincide and, by [F2], so do the stationary curves.

1.2F1F3givenalgebra

Endpoint term on the explicit curve: $x_{*} (t_{0}) = 0$ and $x_{*} (2 t_{0}) = v_{0} t_{0}$ , so $F (t_{0}, x_{*} (t_{0})) = 0$ and $F (2 t_{0}, x_{*} (2 t_{0})) = 2 α t_{0}^{2} (e_{1} \cdot v_{0})$ . By [F1] this is $S^{'} (x_{*}) - S (x_{*})$ .

2.1F1F3step 1.2algebra

Actions: $S (x_{*}) = \frac{1}{2} m ∣ v_{0} ∣_{2}^{2} t_{0}$ by [F3], and step 1.2 gives $S^{'} (x_{*}) = S (x_{*}) + 2 α t_{0}^{2} (e_{1} \cdot v_{0})$ .

3.1F2step 1.1step 2.1algebra

Reference-unit data: substituting the specified $m, t_{0}, v_{0}, α$ into step 2.1 gives $S = (1 / 2) k g m^{2} s^{- 1}$ and $S^{'} = (5 / 2) k g m^{2} s^{- 1}$ , differing by endpoint term $2 k g m^{2} s^{- 1}$ . Their numerical values in that SI action unit are $0.5$ , $2.5$ and $2$ , respectively; the dimension is $μ ℓ^{2} τ^{- 1}$ . The curve $x_{*}$ is affine, hence stationary for both actions by [F2], and the model equation $x^{''} = 0$ is the same for both.

4.1step 1.1step 1.2step 2.1step 3.1F1∎

Clauses 1-3 are verified: the total-derivative modification changes the action by the endpoint value of $F$ and leaves the Euler-Lagrange expression, the stationary curves and the model equation unchanged; the potential normalization is the case $F = - γ t^{2} / 2$ by [F1].

Remarks

The endpoint value $2 α t_{0}^{2} (e_{1} \cdot v_{0})$ is not the difference of a physical energy: it depends on the chosen $F$ and the endpoints. The illustration complements the gauge theorem of this page, which licenses reading the potential's arbitrary $c (t)$ as such a total derivative.

A total-derivative Lagrangian on explicit data: the endpoint term and the unchanged equations

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources