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.

The uniform-force model: translation and boost charges fail across the field while the energy survives, with exact rates and a numerical instance

Physical scope

A worked model check inside the framework: the one-label global potential model (d=0) with U = -m g . x, its explicit maximal motion, the failure of the translation and boost charges in directions with a nonzero component along the field, with the exact rates predicted by the sharpness clauses, a numerical instance at an explicit time, and the survival of the mechanical energy because the potential has no explicit time dependence. The boost direction is dimensionless and its family parameter has velocity units, so the boost charge has mass-length units. All values are model values in a declared idealization; the example reports no measurement and asserts no property of any field of nature.

Example

Work in the one-label uniform-force model of The uniform-force model: explicit global motion of a label under a constant declared field, with uniqueness, dimensions and frame covariance: 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 force map $F (t, x, v) = m g$ for a declared constant parameter $g \in R^{3}$ of dimension $ℓ τ^{- 2}$ (Dimensions and SI unit conventions of the non-relativistic classical mechanics framework). Adopt the potential presentation

$U (t, x) : = - m g \cdot x ((t, x) \in R \times R^{3}),$

of class $C^{\infty}$ and dimension $μ ℓ^{2} τ^{- 2}$ , so that $- \nabla_{x} U = m g = F$ and the model is a global potential model $d \equiv 0$ in the sense of Potential presentations of a force model, potential and mechanical energy, closed versus exact force fields, local potentials and equipotential level sets; declare a nonzero dimensionless $a \in R^{3}$ and consider the motion. For the boost family, its parameter $s$ is measured in velocity units, so $K_{a}$ has units $k g m$ and $K_{a}^{'}$ has units $k g m s^{- 1}$ . For the time-translation datum use a parameter measured in seconds, so its generator value $τ \equiv 1$ is dimensionless and its charge $- E$ is measured in joules. Consider the motion

$x (t) : = x_{0} + v_{0} t + \frac{1}{2} g t^{2} (t \in R)$

with $x_{0}, v_{0} \in R^{3}$ , which is the unique maximal motion through $(0, x_{0}, v_{0})$ by The uniform-force model: explicit global motion of a label under a constant declared field, with uniqueness, dimensions and frame covariance. Verify:

the directional derivative of the potential is $a \cdot \nabla_{x} U (t, x) = - m a \cdot g$ , so the translation condition of Translation symmetry of the model's Lagrangian and conservation of total momentum: exact hypothesis, conservation and its sharpness clause 1 holds exactly when $a \cdot g = 0$ ;
the momentum component is $a \cdot P (t) = m a \cdot v_{0} + m t (a \cdot g)$ , hence constant on $R$ exactly when $a \cdot g = 0$ , with rate $m a \cdot g$ otherwise;
the boost charge is $K_{a} (t) = t (a \cdot P (t)) - m a \cdot x (t) = \frac{1}{2} m t^{2} (a \cdot g) - m a \cdot x_{0}$ , with rate $\frac{d}{d t} K_{a} (t) = t m (a \cdot g)$ ;
the mechanical energy is $E (t) = \frac{1}{2} m ∣ x^{'} (t) ∣^{2} + U (t, x (t)) = \frac{1}{2} m ∣ v_{0} ∣^{2} - m g \cdot x_{0}$ , constant on $R$ , and the potential has no explicit time dependence, so the time-translation identity of Time translation and the mechanical energy of the model: conservation in the autonomous global potential branch and the sharp failure for a time-dependent potential clause 1 holds;
for the numerical instance $m = 1 k g$ , $g = (0, 0, - 1) m s^{- 2}$ , $x_{0} = 0$ , $v_{0} = (1, 0, 0) m s^{- 1}$ and $a = (0, 0, 1)$ : at $t = 2 s$ one has $P (2) = (1, 0, - 2)$ in $k g m s^{- 1}$ , $a \cdot P (2) = - 2 k g m s^{- 1}$ , $K_{a} (2) = - 2 k g m$ and $K_{a}^{'} (2) = - 2 k g m s^{- 1}$ , while the component along $(1, 0, 0)$ is constant at $1 k g m s^{- 1}$ .

All values are model values of the declared idealization: the constant field is an adopted approximation of an external influence and no measurement is reported.

Facts & Assumptions

Given: The one-label uniform-force model, the potential presentation $U$ , the vector $a$ , the constants $x_{0}, v_{0}$ and the motion $x$ .

[F1]

The uniform-force model and its motions (The uniform-force model: explicit global motion of a label under a constant declared field, with uniqueness, dimensions and frame covariance, Adopted force model: force maps, the equation of motion, additive composition of force contributions and frame covariance, The associated first-order system, motions, maximal motions and the Newtonian flow of a force model): $F (t, x, v) = m g$ satisfies the standing hypotheses; the displayed quadratic curve is the unique maximal motion through $(0, x_{0}, v_{0})$ and is defined on all of $R$ ; a motion satisfies $m x^{''} = F$ .

[F2]

The presentation (Potential presentations of a force model, potential and mechanical energy, closed versus exact force fields, local potentials and equipotential level sets, The action functional of a force model with a potential presentation: the mechanical Lagrangian, its chart instance and its dimensions): $U (t, x) = - m g \cdot x$ is $C^{\infty}$ with $\nabla_{x} U = - m g$ , so $F = - \nabla_{x} U$ and $d \equiv 0$ ; the mechanical Lagrangian is $L = \frac{1}{2} m ∣ v ∣^{2} + m g \cdot x$ , and the mechanical energy function is $E (t, x, v) = \frac{1}{2} m ∣ v ∣^{2} - m g \cdot x$ .

[F3]

Translation and boost statements (Translation symmetry of the model's Lagrangian and conservation of total momentum: exact hypothesis, conservation and its sharpness, The Galilean boost charge of the model: exact condition, uniform centre-of-mass motion, the induced motions and the boundary of the conservation law): under the differential condition with $d \equiv 0$ the component $a \cdot P$ is constant along every motion; with dimensionless $a$ and a velocity-valued boost parameter, the boost datum $(0, t (a), m a \cdot x)$ satisfies the model identity exactly under the same condition, and then $K_{a} = a \cdot (t P - m x)$ is constant with dimension $μ ℓ$ , while its general rate $K_{a}^{'} = t a \cdot F_{t o t}$ has dimension $μ ℓ τ^{- 1}$ .

[F4]

The energy statement (Time translation and the mechanical energy of the model: conservation in the autonomous global potential branch and the sharp failure for a time-dependent potential, Continuous symmetries of the mechanical Lagrangian of a potential presentation: symmetry data, the Noether identity, the charge and its dimensions): the datum $τ \equiv 1, ξ \equiv 0, B \equiv 0$ satisfies the model identity exactly when $\partial_{t} U \equiv 0$ , and then the mechanical energy is constant along every motion with $d \equiv 0$ .

[F5]

Calculus (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$ , For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term, 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}$ , 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}$ , $C^{k}$ Euclidean maps and diffeomorphisms, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length, Dimensions and SI unit conventions of the non-relativistic classical mechanics framework, Configuration domain of $N$ labeled particles: open admissible sets, regular holonomic constraints and the mass operator): polynomials in $t$ differentiate by the power rule; the Euclidean inner product is bilinear; the dimensions of $P = m x^{'}$ are $μ ℓ τ^{- 1}$ and, for the dimensionless direction $a$ with a velocity-valued boost parameter, those of $K_{a} = a \cdot (t P - m x)$ are $μ ℓ$ .

Verification

technique · direct; differentiate the explicit potential, momentum, charge and energy along the stated motion and evaluate the numerical instance

1.1F2F3F5algebra

Clause 1: differentiating $U (t, x) = - m g \cdot x$ in the configuration slot gives $\nabla_{x} U (t, x) = - m g$ , hence $a \cdot \nabla_{x} U (t, x) = - m (a \cdot g)$ for every $(t, x)$ , which vanishes identically exactly when $a \cdot g = 0$ ; by [F3] this is precisely the differential translation condition.

1.2F1F5algebra

Clause 2: by [F1] the velocity is $x^{'} (t) = v_{0} + g t$ , so $P (t) = m (v_{0} + g t)$ and $a \cdot P (t) = m (a \cdot v_{0}) + m t (a \cdot g)$ ; this is constant in $t$ exactly when $m (a \cdot g) = 0$ , and otherwise its derivative is $m (a \cdot g)$ .

1.3F1F2F3F5algebra

Clause 3: by the definition of the boost charge and clause 2, $K_{a} (t) = t (m (a \cdot v_{0}) + m t (a \cdot g)) - m a \cdot (x_{0} + v_{0} t + \frac{1}{2} g t^{2}) = \frac{1}{2} m t^{2} (a \cdot g) - m a \cdot x_{0},$ whose derivative is $t m (a \cdot g) = - t a \cdot \nabla_{x} U (t, x (t))$ , in agreement with the general rate $K_{a}^{'} = t a \cdot F_{t o t}$ of [F3] because $F_{t o t} = m g = - \nabla_{x} U$ in one label.

1.4F2F4F5algebra

Clause 4: the potential has $\partial_{t} U \equiv 0$ , so the time-translation datum satisfies the model identity by [F4]; directly, $E (t) = \frac{1}{2} m ∣ v_{0} + g t ∣^{2} - m g \cdot (x_{0} + v_{0} t + \frac{1}{2} g t^{2}) = \frac{1}{2} m (∣ v_{0} ∣^{2} + 2 t g \cdot v_{0} + t^{2} ∣ g ∣^{2}) - m g \cdot x_{0} - m t g \cdot v_{0} - \frac{1}{2} m t^{2} ∣ g ∣^{2} = \frac{1}{2} m ∣ v_{0} ∣^{2} - m g \cdot x_{0},$ constant on $R$ , consistent with the conservation clause of [F4].

2.1step 1.2step 1.3F5algebra

Clause 5, numerical instance: with $m = 1$ , $g = (0, 0, - 1)$ , $x_{0} = 0$ and $v_{0} = (1, 0, 0)$ the velocity is $x^{'} (t) = (1, 0, - t)$ and at $t = 2 s$ one has $P (2) = (1, 0, - 2)$ in $k g m s^{- 1}$ ; with $a = (0, 0, 1)$ clause 2 gives $a \cdot P (2) = m (a \cdot v_{0}) + 2 m (a \cdot g) = 0 + 2 (- 1) = - 2 k g m s^{- 1}$ , clause 3 gives $K_{a} (2) = \frac{1}{2} (1) (4) (- 1) - 0 = - 2 k g m$ and $K_{a}^{'} (2) = 2 (1) (- 1) = - 2 k g m s^{- 1}$ ; with $a = (1, 0, 0)$ one has $a \cdot g = 0$ , so $a \cdot P (t) = m (a \cdot v_{0}) = 1 k g m s^{- 1}$ for every $t$ .

3.1step 1.1step 1.2step 1.3step 1.4step 2.1∎

Clauses 1-5 are steps 1.1, 1.2, 1.3, 1.4 and 2.1; the example exhibits, on explicit data of an adopted model, a force law that breaks the translation and boost charges across the field while the autonomous potential preserves the mechanical energy, and it reports no measurement.

Remarks

Reading of the failure. For this balance comparison, declare the external-plus-pair presentation of Restricted interaction models: pair decompositions, antisymmetry and centrality options, potential forces and the gravitational branch clause (i) with $F_{1}^{e x t} : R \times R^{3} \times R^{3} \to R^{3}$ , $F_{1}^{e x t} (t, x, v) : = m g$ . This map is constant, so it satisfies the standing regularity. There are no pairs for $N = 1$ : the pair sum is zero and the antisymmetry condition of clause (ii)1 is vacuous. Thus $F_{1} = F_{1}^{e x t}$ on the whole state domain, and the total external force along the motion is $m g$ . The rate $m (a \cdot g)$ of the momentum component is the component of the external force along $a$ , in agreement with the balance identity of Total momentum balance and centre-of-mass equation for a model with antisymmetric pair forces read on this single label; the Noether sharpness clause and the balance describe the same failure from different starting points. Directions perpendicular to $g$ retain a conserved momentum component, so the model retains a two-dimensional family of translation charges when $g \neq 0$ , while failing the third. When $g = 0$ , all three components are conserved.
Energy versus momentum. The same model conserves its mechanical energy: the potential is autonomous, and the time-translation datum is available. The example therefore exhibits the independence of the charges of this page: some symmetry data of the framework's model classes hold here and others do not, and the conservation statements must be applied one datum at a time.

The uniform-force model: translation and boost charges fail across the field while the energy survives, with exact rates and a numerical instance

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources