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.

The charge of an infinitesimal point symmetry is constant along Euler-Lagrange solutions

Statement

Let $(O, L)$ be a time-dependent Lagrangian chart over $[a, b] \times U$ , let $(ξ, B)$ be an infinitesimal point symmetry of $L$ with charge $C (t, q, v) = L_{v} (t, q, v) \cdot ξ (q) - B (t, q)$ (Infinitesimal point symmetry of a time-dependent Lagrangian and its conserved charge), and let $q : I \to U$ be a $C^{2}$ curve on an open interval $I \supseteq [a, b]$ with $(t, q (t), q^{'} (t)) \in O$ for all $t \in I$ that solves the Euler–Lagrange equation

$E_{L} (q) (t) = 0 (t \in I),$

i.e. $\frac{d}{d t} L_{v} (t, q, q^{'}) = L_{q} (t, q, q^{'})$ (A time-dependent Lagrangian chart, its action functional and its fixed-endpoint first variations, Stationarity of the time-dependent action is equivalent to the vanishing of the Euler-Lagrange expression). Then the function

$t ⟼ C (t, q (t), q^{'} (t)) = L_{v} (t, q (t), q^{'} (t)) \cdot ξ (q (t)) - B (t, q (t))$

is constant on $I$ .

Facts & Assumptions

Given: The chart data $(O, L)$ , an infinitesimal point symmetry $(ξ, B)$ , and a $C^{2}$ Euler–Lagrange solution $q : I \to U$ .

[F1]

The symmetry identity of Infinitesimal point symmetry of a time-dependent Lagrangian and its conserved charge: $L_{q} (t, q, v) \cdot ξ (q) + L_{v} (t, q, v) \cdot D ξ (q) v = B_{t} (t, q) + B_{q} (t, q) \cdot v$ for all $(t, q, v) \in O$ , and the Euler–Lagrange equation $\frac{d}{d t} L_{v} (t, q, q^{'}) = L_{q} (t, q, q^{'})$ along $q$ .

[F2]

Chain rule and algebra of differentiable curves (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): the curve $t \mapsto ξ (q (t))$ is $C^{1}$ with derivative $D ξ (q (t)) q^{'} (t)$ , and the curve $t \mapsto B (t, q (t))$ is $C^{1}$ with derivative $B_{t} (t, q (t)) + B_{q} (t, q (t)) \cdot q^{'} (t)$ .

[F3]

A continuous real function on an interval whose derivative vanishes at every interior point is constant there (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).

Proof

Proof technique: direct; differentiate the charge along the solution and substitute the symmetry identity.

1.1F1F2given

The charge $C (t) = C (t, q (t), q^{'} (t))$ is differentiable on $I$ , because $L_{v}$ , $ξ$ , $B$ and $q$ are $C^{1}$ . By [F2], $C^{'} (t) = (\frac{d}{d t} L_{v} (t, q, q^{'})) \cdot ξ (q (t)) + L_{v} (t, q, q^{'}) \cdot D ξ (q (t)) q^{'} (t) - B_{t} (t, q (t)) - B_{q} (t, q (t)) \cdot q^{'} (t) .$

2.1F1step 1.1algebra

Substituting the Euler–Lagrange equation of [F1] in the first term and the symmetry identity with $(t, q, v) = (t, q (t), q^{'} (t))$ in the remaining three terms gives $C^{'} (t) = 0$ for every $t \in I$ .

3.1F3step 2.1∎

Since $C$ is differentiable with $C^{'} = 0$ , [F3] makes $C$ constant on $I$ .

Remarks

The theorem is a deduction inside the chart model: conservation holds for solutions of the Euler–Lagrange equation whenever the identity of Infinitesimal point symmetry of a time-dependent Lagrangian and its conserved charge holds. It does not assert that any particular Lagrangian occurring in a physical model possesses such a symmetry, and it makes no empirical claim.
The analogous statement with time reparametrisation, the compensating term $E τ$ in the charge, and the reduction to the present theorem at $τ = 0$ with time-independent $ξ$ is Noether identity for point transformations with time reparametrisation: the conserved charge $p \cdot ξ - E τ - B$ .

The charge of an infinitesimal point symmetry is constant along Euler-Lagrange solutions

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources