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.

The point Noether theorem of the model: conservation of the charge of a strict symmetry, and the residual-force rate

Physical scope

The point Noether theorem of the force model with a declared potential presentation in one inertial frame: for a strict symmetry datum of the mechanical Lagrangian that is independent of time, the charge M x' . xi - B is constant along every motion of the global potential branch; for an arbitrary presentation the charge of a strict datum has derivative equal to the residual force paired with the generator, so conservation holds exactly when that pairing vanishes along the motion. The theorem is conditional on the adopted force branch, the declared presentation, the symmetry identity and, in the conservation clause, on the absence of residual forces; it asserts no symmetry of any particular force law and carries no empirical content.

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 $U$ of Potential presentations of a force model, potential and mechanical energy, closed versus exact force fields, local potentials and equipotential level sets, and let $(τ, ξ, B)$ be a symmetry datum of the model's mechanical Lagrangian with $τ \equiv 0$ (Continuous symmetries of the mechanical Lagrangian of a potential presentation: symmetry data, the Noether identity, the charge and its dimensions clause (a)); write

$C (t, x, v) : = (M v) \cdot ξ (t, x) - B (t, x) ((t, x, v) \in O)$

for its charge. Then:

(conservation in the global potential model). If $d \equiv 0$ and $ξ$ is independent of $t$ , then for every motion $x : J \to Q$ 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), the function $t \mapsto C (t, x (t), x^{'} (t))$ is constant on $J$ .
(residual-force rate). For an arbitrary presentation $(U, d)$ , along every motion $x : J \to Q$ the function $t \mapsto C (t, x (t), x^{'} (t))$ is of class $C^{1}$ on $J$ and

$C^{'} (t) = ⟨ d (t, x (t), x^{'} (t)), ξ (t, x (t)) ⟩ (t \in J),$

where the pairing is the Euclidean inner product of $R^{3 N}$ ; consequently $C$ is constant on $J$ if and only if this pairing vanishes for every $t \in J$ .

Clause 1 is the conditional conservation law of the model's global potential branch under a symmetry identity of its Lagrangian; clause 2 quantifies the exact rate at which a residual force destroys it. Neither clause asserts that any model possesses a strict symmetry datum, and neither carries empirical content.

Facts & Assumptions

Given: The model, the presentation $(U, d)$ , the strict symmetry datum $(0, ξ, B)$ and the motion $x : J \to Q$ of the statement.

[F1]

Model data and chart (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, Potential presentations of a force model, potential and mechanical energy, closed versus exact force fields, local potentials and equipotential level sets, Configuration domain of $N$ labeled particles: open admissible sets, regular holonomic constraints and the mass operator): $O = I_{0} \times Q \times R^{3 N}$ is open and $(O, L)$ is a time-dependent Lagrangian chart whenever $Q \neq \emptyset$ and $a < b$ with $[a, b] \subseteq I_{0}$ , over $[a, b] \times Q$ ; $L (t, x, v) = K (v) - U (t, x)$ with $K (v) = \frac{1}{2} v \cdot M v$ , $L_{v} (t, x, v) = M v$ , $L_{x} (t, x, v) = - \nabla_{x} U (t, x)$ and $L_{t} (t, x, v) = - U_{t} (t, x)$ ; the force map is $F_{i} = - \nabla_{x_{i}} U + d_{i}$ .

[F2]

The symmetry datum and its charge (Continuous symmetries of the mechanical Lagrangian of a potential presentation: symmetry data, the Noether identity, the charge and its dimensions, Infinitesimal point symmetry of a time-dependent Lagrangian and its conserved charge): $ξ : I_{0} \times Q \to R^{3 N}$ and $B : I_{0} \times Q \to R$ are of class $C^{2}$ and satisfy the strict identity $L_{x} (t, x, v) \cdot ξ (t, x) + L_{v} (t, x, v) \cdot D_{t} ξ (t, x, v) = D_{t} B (t, x, v)$ on $O$ ; the charge is the displayed function $C$ ; when $ξ$ is independent of $t$ the pair $(ξ, B)$ is an infinitesimal point symmetry of the chart $(O, L)$ in the sense of the cited definition.

[F3]

The mathematical conservation theorem (The charge of an infinitesimal point symmetry is constant along Euler-Lagrange solutions, Stationarity of the time-dependent action is equivalent to the vanishing of the Euler-Lagrange expression): for an infinitesimal point symmetry $(ξ, B)$ of a time-dependent Lagrangian chart and a $C^{2}$ curve $q : I \to U$ on an open interval $I$ with graph in the chart domain that solves the Euler-Lagrange equation $E_{L} (q) = 0$ , the function $t \mapsto L_{v} \cdot ξ - B$ is constant on $I$ .

[F4]

The Euler-Lagrange equivalence in model terms (The stationary-action criterion and the potential-part Euler-Lagrange equation, Stationary curves of the mechanical action are exactly the restrictions of the model's motions (global potential branch)): for every $C^{2}$ admissible curve $z$ of the chart instance and reals $a < b$ with $[a, b] \subseteq I_{0}$ , stationarity for the action, $E_{L} (z) = 0$ on $[a, b]$ and $M z^{''} (t) = - \nabla_{x} U (t, z (t))$ on $[a, b]$ are equivalent; and every motion of the model with $d \equiv 0$ restricts on such an interval to a curve satisfying these conditions.

[F5]

Motions (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): a motion $x : J \to Q$ on an interval with nonempty interior is a $C^{2}$ curve with $J \subseteq I_{0}$ and $m_{i} x_{i}^{''} (t) = F_{i} (t, x (t), x^{'} (t))$ for all $t \in J$ , i.e. $M x^{''} = - \nabla_{x} U + d$ along the motion.

[F6]

Calculus along the motion (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 derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral, The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , 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): the curves $t \mapsto ξ (t, x (t))$ and $t \mapsto B (t, x (t))$ are $C^{1}$ with derivatives $D_{t} ξ (t, x (t), x^{'} (t))$ and $D_{t} B (t, x (t), x^{'} (t))$ ; sums and pairings of differentiable curves differentiate by the product rule; a $C^{1}$ real function on an interval is constant if and only if its derivative vanishes at every point.

[F7]

Regularity of the data ( $C^{k}$ Euclidean maps and diffeomorphisms, 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}$ , Dimensions and SI unit conventions of the non-relativistic classical mechanics framework): $ξ$ and $B$ are $C^{2}$ , $U$ is $C^{2}$ and a motion is $C^{2}$ , so all composites below are at least $C^{1}$ .

Proof

technique · direct; convert a motion into an Euler-Lagrange solution for the conservation clause and instantiate the mathematical Noether theorem, then differentiate the charge along the motion for the residual-force rate

1.1F1F4given

Clause 1, motion as an Euler-Lagrange solution: let $x : J \to Q$ be a motion with $d \equiv 0$ . The interior $J^{\circ}$ is a nonempty open interval. For any $t_{0} \in J^{\circ}$ choose $a < b$ with $t_{0} \in (a, b)$ and $[a, b] \subseteq J^{\circ}$ ; the restriction $x ∣_{[a, b]}$ is a $C^{2}$ admissible curve of the chart instance and is stationary for the action of $L$ by [F4], so it satisfies $E_{L} (x) = 0$ on $[a, b]$ . As this holds for each $t_{0} \in J^{\circ}$ , $E_{L} (x) = 0$ throughout $J^{\circ}$ .

1.2F2F5F6F7algebra

Clause 2, differentiation: along any motion, $t \mapsto C (t, x (t), x^{'} (t))$ is of class $C^{1}$ by [F6] and [F7], and differentiating $C = (M x^{'}) \cdot ξ (t, x) - B (t, x)$ gives $C^{'} = (M x^{''}) \cdot ξ + (M x^{'}) \cdot D_{t} ξ - D_{t} B$ at each $t \in J$ . Substituting the strict identity of [F2] with $(t, x, v) = (t, x (t), x^{'} (t))$ , i.e. $D_{t} B = - \nabla_{x} U \cdot ξ + (M x^{'}) \cdot D_{t} ξ$ , and then $M x^{''} = - \nabla_{x} U + d$ from [F5], gives $C^{'} = (M x^{''}) \cdot ξ + \nabla_{x} U \cdot ξ = (M x^{''} + \nabla_{x} U) \cdot ξ = ⟨ d (t, x (t), x^{'} (t)), ξ (t, x (t)) ⟩ .$

2.1F2F3F7step 1.1

Clause 1, conservation: by [F2] the pair $(ξ, B)$ , with $ξ$ independent of $t$ , is an infinitesimal point symmetry of the chart $(O, L)$ . Step 1.1 shows that $x ∣_{J^{\circ}}$ is a $C^{2}$ curve on the open interval $J^{\circ}$ with graph in $O$ solving $E_{L} = 0$ , so the mathematical conservation theorem [F3] applies there and makes $t \mapsto L_{v} (t, x, x^{'}) \cdot ξ (x) - B (t, x) = (M x^{'} (t)) \cdot ξ (x (t)) - B (t, x (t))$ constant on $J^{\circ}$ . The charge is continuous on $J$ by [F7]; every endpoint of $J$ that belongs to $J$ is a limit of points of $J^{\circ}$ , so continuity gives the same constant value there. Thus the charge is constant on $J$ .

2.2F6step 1.2

Clause 2, conservation criterion: by step 1.2 the derivative of $t \mapsto C (t, x (t), x^{'} (t))$ is the pairing displayed there; by [F6] a $C^{1}$ function on the interval $J$ is constant on $J$ if and only if its derivative vanishes everywhere on $J$ , so $C$ is constant on $J$ exactly when the pairing vanishes for every $t \in J$ .

3.1step 2.1step 2.2∎

Clause 1 is steps 1.1 and 2.1, and clause 2 is steps 1.2 and 2.2; both clauses are conditional deductions from the indicated hypotheses, and no claim of existence of a symmetry datum or of empirical content is made.

Remarks

Where the identity is used. Clause 1 uses the strict identity on the whole chart through the mathematical point-symmetry theorem; clause 2 uses the same identity only at the graph points of the motion and evaluates the motion equation. For a presentation with $d \equiv 0$ the two routes agree, and clause 2 then gives $C^{'} = 0$ directly; the field-theoretic reading is that the potential part of the force does no work against the generator, while the residual part does, at rate $⟨ d, ξ ⟩$ . The specialisation of this statement with $ξ = ξ (x)$ to the mathematical case The charge of an infinitesimal point symmetry is constant along Euler-Lagrange solutions is the reason the framework reuses the chart-level notion of symmetry as its model notion.
Conditional conservation. The pairing criterion makes the conditions explicit: with residual forces the charge of a strict symmetry is conserved exactly if the residual force is orthogonal to the generator along the motion. If the total pairing $⟨ d, ξ ⟩$ is nonzero at a point of the motion — for instance for a nonzero friction force paired with a translation generator — the corresponding charge is not constant on that motion.
What is not claimed. No converse is asserted: from the constancy of $(M x^{'}) \cdot ξ - B$ along the motions one cannot conclude that the identity holds, and the existence of a symmetry datum for a given model is a separate verification against its declared $U$ and masses. The statement is also not an empirical law: it concerns the model's motions under the adopted force branch and the declared presentation.

The point Noether theorem of the model: conservation of the charge of a strict symmetry, and the residual-force rate

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources