CorollaryStatement: 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.

Conserved charges for translation, rotation and boost symmetries of a mechanical Lagrangian

Statement

Let $n \geq 1$ , let $m > 0$ , let $a_{0} < b_{0}$ be reals, let $ε > 0$ , let $U \subseteq R^{n}$ be open and nonempty, let $U_{0} : (a_{0} - ε, b_{0} + ε) \times U \to R$ be of class $C^{2}$ , and let

$L (t, q, v) : = \frac{1}{2} m ∣ v ∣^{2} - U_{0} (t, q)$

be the corresponding Lagrangian chart (A time-dependent Lagrangian chart, its action functional and its fixed-endpoint first variations, The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ). Let $q : I \to U$ be a $C^{2}$ Euler–Lagrange solution on an open interval $[a_{0}, b_{0}] \subseteq I \subseteq (a_{0} - ε, b_{0} + ε)$ . Then:

(translation) if $a \in R^{n}$ and $a \cdot \nabla_{q} U_{0} (t, q) = 0$ for every $(t, q)$ , then $P_{a} (t) : = m a \cdot q^{'} (t)$ is constant on $I$ ;
(rotation) if $n = 3$ , $a \in R^{3}$ and $(a \times q) \cdot \nabla U_{0} (t, q) = 0$ for every $(t, q)$ , then $J_{a} (t) : = m (q (t) \times q^{'} (t)) \cdot a$ is constant on $I$ ;
(boost) if $a \in R^{n}$ and $a \cdot \nabla_{q} U_{0} = 0$ on the whole chart, then $K_{a} (t) : = a \cdot (t m q^{'} (t) - m q (t))$ is constant on $I$ .

Facts & Assumptions

Given: The real $m > 0$ , the $C^{2}$ potential $U_{0}$ , the Lagrangian $L (t, q, v) = \frac{1}{2} m ∣ v ∣^{2} - U_{0} (t, q)$ , a vector $a$ (in $R^{n}$ in clauses 1 and 3, in $R^{3}$ in clause 2), and a $C^{2}$ Euler–Lagrange solution $q : I \to U$ .

[F1]

The Noether theorem (Noether identity for point transformations with time reparametrisation: the conserved charge $p \cdot ξ - E τ - B$ ): if $C^{2}$ data $τ, ξ, B$ satisfy the Noether identity of that theorem, then $C = L_{v} \cdot ξ - E τ - B$ is constant along $q$ . Here $L_{v} = m v$ and $E = \frac{1}{2} m ∣ v ∣^{2} + U_{0}$ . [given, algebraic computation of $L_{v}$ and $E$ from the definition]

[F2]

The cross product is alternating and bilinear, and $(a \times u) \cdot w = a \cdot (u \times w)$ for all $a, u, w \in R^{3}$ (The cross product in $R^{3}$ , The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , 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$ ); in particular $v \cdot (a \times v) = 0$ and $\frac{d}{d t} (a \times q) = a \times q^{'}$ along a differentiable curve (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ , The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length, A function continuous on an interval $I$ whose derivative vanishes at every interior point of $I$ is constant on $I$ ; consequently two such functions with the same derivative differ by a constant).

[F3]

Gradients and directional derivatives: $a \cdot \nabla U_{0}$ is the derivative of $U_{0}$ in the direction $a$ (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}$ ), and for the quadratic potential $U_{0} (q) = \frac{1}{2} k ∣ q ∣^{2}$ one has $\nabla U_{0} = k q$ (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes).

Proof

technique · direct; verify the Noether identity for each of the three families and read off the charge

1.1F1F3given

Translation. Take $τ = 0$ , $ξ (t, q) : = a$ (constant) and $B = 0$ . Then $D_{t} ξ = 0$ and the Noether identity reduces to $L_{q} \cdot a = - a \cdot \nabla U_{0} = 0$ , which holds by hypothesis of clause 1. The charge is $C = L_{v} \cdot a - E \cdot 0 - 0 = m a \cdot q^{'} (t) = P_{a} (t)$ , constant on $I$ by [F1].

1.2F1F2given

Rotation. Take $n = 3$ , $τ = 0$ , $ξ (t, q) : = a \times q$ and $B = 0$ . Then $D_{t} ξ = a \times q^{'}$ , so the identity reads $L_{q} \cdot (a \times q) + L_{v} \cdot (a \times q^{'}) = - (a \times q) \cdot \nabla U_{0} + m q^{'} \cdot (a \times q^{'})$ . The first term vanishes by the hypothesis of clause 2 and the second by [F2] (the scalar triple product with two equal factors $q^{'}$ vanishes). Hence the identity holds and the charge is $C = m q^{'} \cdot (a \times q) = m (q \times q^{'}) \cdot a = J_{a} (t),$ constant on $I$ by [F1].

1.3F1F3givenalgebra

Boost. Take $τ = 0$ , $ξ (t, q) : = t a$ and $B (t, q) : = m a \cdot q$ . Then $D_{t} ξ = a$ and $D_{t} B = m a \cdot q^{'}$ , so the identity reads $L_{q} \cdot t a + L_{v} \cdot a = - t a \cdot \nabla U_{0} + m a \cdot q^{'}$ , which equals $m a \cdot q^{'} = D_{t} B$ by the hypothesis $a \cdot \nabla U_{0} = 0$ . Hence the identity holds with charge $C = m q^{'} (t) \cdot (t a) - m a \cdot q (t) = a \cdot (t m q^{'} (t) - m q (t)) = K_{a} (t),$ constant on $I$ by [F1].

2.1F3given∎

Failure for a quadratic potential. For $U_{0} (q) = \frac{k}{2} ∣ q ∣^{2}$ with $k > 0$ and $a \neq 0$ , the hypotheses of clauses 1 and 3 fail, since $a \cdot \nabla U_{0} = k a \cdot q$ is not identically zero; so the translation and boost identities are not available, and the corollary gives no conserved $P_{a}$ or $K_{a}$ for this potential.

Remarks

Clause 3 is the Galilean boost charge: its defining Noether identity holds when $a \cdot \nabla_{q} U_{0} = 0$ on the chart, giving conservation along every Euler–Lagrange solution. Constancy on a particular solution alone does not imply this whole-chart symmetry. A confining potential such as $\frac{k}{2} ∣ q ∣^{2}$ breaks the boost symmetry even though the Galilean charts of the framework still exist; this is the mathematical content of the warning that a kinematic symmetry need not be a symmetry of the chosen Lagrangian.
All three statements are conditional deductions inside the chart model: they identify conserved quantities of the Euler–Lagrange equation under explicitly stated symmetry hypotheses of the potential. They are mathematical statements about the model and are not claims that any particular physical system possesses the required symmetry.

Conserved charges for translation, rotation and boost symmetries of a mechanical Lagrangian

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources