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 two-body Hooke model with an exact circular relative motion: momentum, kinetic splitting, moving-origin angular momentum, energy conservation and the kinetic boost law checked on explicit data

Physical scope

A worked model check inside the two-body potential branch: for a declared Hooke pair potential with spring constant, mass, separation and centre-of-mass velocity data, the displayed circular relative motion is the unique maximal motion of the model, and along it the total momentum, centre-of-mass motion, kinetic splitting, angular momentum about fixed and moving reference points, mechanical energy and boosted kinetic energy take the values the balance theorems predict. The item asserts no measured value, models no physical spring and claims no empirical agreement.

Example

Fix the two-body model of Restricted interaction models: pair decompositions, antisymmetry and centrality options, potential forces and the gravitational branch clause (iv) (the general pair-potential example) with $N = 2$ , masses $m_{1} = m_{2} = m > 0$ , time window $R$ , configuration domain $Q = R^{6}$ (the potential below is smooth everywhere, so no collision exclusion is needed), and the Hooke pair potential $U (x_{1}, x_{2}) : = \frac{1}{2} k ∥ x_{1} - x_{2} ∥_{2}^{2},$ with a declared spring constant $k > 0$ of dimension $μ τ^{- 2}$ (Dimensions and SI unit conventions of the non-relativistic classical mechanics framework), so that $U$ has energy dimension. The force map is $F_{1} (x) = - k (x_{1} - x_{2}), F_{2} (x) = k (x_{1} - x_{2}),$ the two negative gradients of $U$ ; it is linear in the positions and independent of time and velocities, with $∥ F (x) - F (x^{'}) ∥_{2} \leq 2 k ∥ x - x^{'} ∥_{2}$ , hence continuous and state-locally Lipschitz with the uniform constant $2 k$ . The model therefore satisfies the standing hypotheses of Adopted force model: force maps, the equation of motion, additive composition of force contributions and frame covariance clause (iii), it has no external forces ( $F_{i}^{e x t} \equiv 0$ ), and its pair force is central: $F_{12} = - k (x_{1} - x_{2})$ is parallel to $x_{1} - x_{2}$ . It presents its force map through the global potential $U$ 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 clause (a).

Fix an oriented orthonormal triple $(e_{1}, e_{2}, e_{3})$ with $e_{3} = e_{1} \times e_{2}$ , a constant centre-of-mass velocity $V \in R^{3}$ of dimension $ℓ τ^{- 1}$ , and a length $R > 0$ , and set $ω : = \sqrt{2 k / m}$ (dimension $τ^{- 1}$ ). Define $e (t) : = \cos (ω t) e_{1} + \sin (ω t) e_{2}, x_{1} (t) : = V t - \frac{R}{2} e (t), x_{2} (t) : = V t + \frac{R}{2} e (t) (t \in R) .$ Then $x = (x_{1}, x_{2})$ is the unique maximal motion of the model with the datum $x_{1} (0) = - \frac{R}{2} e_{1}$ , $x_{2} (0) = \frac{R}{2} e_{1}$ , ${\dot{x}}_{1} (0) = V - \frac{R}{2} ω e_{2}$ , ${\dot{x}}_{2} (0) = V + \frac{R}{2} ω e_{2}$ , and along it:

the total momentum is $P = 2 m V$ , constant, and the centre of mass is $X (t) = V t$ with $V_{c m} = V$ ;
the kinetic energy is $K = m ∥ V ∥_{2}^{2} + \frac{1}{4} m R^{2} ω^{2}$ , and its centre-of-mass/relative splitting holds with reduced mass $μ = m / 2$ and relative coordinate $r = x_{1} - x_{2}$ ;
the angular momentum about the origin is $J_{0} = \frac{1}{2} m R^{2} ω e_{3}$ , constant, while for the moving reference curve $o (t) = W t$ with a constant velocity $W \in R^{3}$ of dimension $ℓ τ^{- 1}$ and $W ⊥ V$ one has $J_{o}^{'} = - 2 m (W \times V)$ , in agreement with the moving-origin correction; this correction is nonzero when both $W$ and $V$ are nonzero;
the mechanical energy is $E = m ∥ V ∥_{2}^{2} + k R^{2}$ , constant, and the power identity $K^{'} = P$ holds with $P$ equal to the negative time derivative of the potential energy $\frac{1}{2} k ∥ r ∥_{2}^{2}$ ;
under the Galilean change to the centre-of-mass frame ( $b = 0$ , $a_{0} = 0$ , $R_{r o t} = I_{3}$ , $v_{b o o s t} = - V$ ) the transformed quantities are $\tilde{P} = 0$ , $\tilde{K} = \frac{1}{2} k R^{2}$ and $\tilde{E} = k R^{2}$ , in agreement with Transformation of the state quantities under a change of inertial frame: centre of mass, total momentum, kinetic energy, angular momentum, torque, power, work and mechanical energy clauses 2 and 5.

Facts & Assumptions

Given: The model and data of the example: the Hooke pair model with $m, k > 0$ on $Q = R^{6}$ , $ω = \sqrt{2 k / m}$ , an oriented orthonormal triple with $e_{3} = e_{1} \times e_{2}$ , a constant velocity $V \in R^{3}$ , a length $R > 0$ , the curves $e$ , $x_{1}$ , $x_{2}$ , and the reference curve $o (t) = W t$ with constant velocity $W ⊥ V$ .

[L1]

Model notions (The associated first-order system, motions, maximal motions and the Newtonian flow of a force model, Total mass, total momentum, centre of mass, angular momentum, torque, kinetic energy, power and work of a particle model in an inertial frame): a motion is a $C^{2}$ curve $x : R \to R^{6}$ with $m_{i} {\ddot{x}}_{i} = F_{i} (x)$ ; along it $p_{i} = m_{i} {\dot{x}}_{i}$ , $P = p_{1} + p_{2}$ , $M = m_{1} + m_{2} = 2 m$ , $X = M^{- 1} (m_{1} x_{1} + m_{2} x_{2})$ , $V_{c m} = X^{'}$ , $K = \frac{1}{2} \sum_{i} m_{i} ∥ {\dot{x}}_{i} ∥_{2}^{2}$ , $J_{o} = \sum_{i} (x_{i} - o) \times p_{i}$ for a differentiable reference curve $o$ , and $E = K + U (x_{1}, x_{2})$ for the declared potential. The model is the pair-potential branch of Restricted interaction models: pair decompositions, antisymmetry and centrality options, potential forces and the gravitational branch with $F_{1} = - k (x_{1} - x_{2})$ , $F_{2} = k (x_{1} - x_{2})$ , no external forces and central pairs.

[L2]

Existence and uniqueness (Local existence and uniqueness for the Newtonian initial-value problem, with the quantitative Picard-Lindelöf cylinder clauses 1, 2 and 4): the force map is continuous and state-locally Lipschitz, so every datum has a unique maximal motion and every motion with that datum is a restriction of it; in particular a motion with the datum whose interval is the whole time window $R$ is the maximal motion.

[L3]

Trigonometric and product rules (The derivatives of sine and cosine are cosine and minus sine, The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , 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 $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, Parity and the Pythagorean identity for sine and cosine): the curve $e (t) = \cos (ω t) e_{1} + \sin (ω t) e_{2}$ is $C^{2}$ with $e^{'} (t) = ω η (t), η (t) : = - \sin (ω t) e_{1} + \cos (ω t) e_{2}, e^{''} (t) = - ω^{2} e (t),$ and $∥ e ∥_{2} = ∥ η ∥_{2} = 1$ , $⟨ e, η ⟩ = 0$ .

[L4]

Euclidean and cross-product algebra (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , The cross product in $R^{3}$ , The cross product is bilinear, alternating, and orthogonal to both factors): bilinearity and symmetry of the inner product, $u \times u = 0$ and $u \times v = - (v \times u)$ ; from the oriented orthonormal triple, $e \times η = e_{3}$ . Finite sums and scalar multiples are linear (Laws of finite sums and finite products, The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral).

[L5]

Balance and transform laws (Total momentum balance and centre-of-mass equation for a model with antisymmetric pair forces, Total momentum equals total mass times centre-of-mass velocity, and the kinetic energy splits into centre-of-mass and relative parts (two-body reduced mass), Angular momentum balance about a fixed or moving reference point, the internal torque sum, and the centrality case, Power of the total force and the work-energy theorem: $K^{'} = P$ and $K (t_{1}) - K (t_{0}) = W ([t_{0}, t_{1}])$ along a motion, Mechanical energy balance for a potential presentation: $E^{'} = \partial_{t} U$ plus the residual power, conservation for a static potential with no residual forces, and the integrated work form clauses 1 and 2, Transformation of the state quantities under a change of inertial frame: centre of mass, total momentum, kinetic energy, angular momentum, torque, power, work and mechanical energy clauses 2 and 5): the general statements whose values are checked below; the interval $J = R$ has nonempty interior (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

Verification

technique · direct; differentiate the displayed curves, substitute into the equations of motion and evaluate each quantity, comparing with the balance statements

1.1L3L4algebra

The curves are $C^{2}$ : $e$ is $C^{2}$ by [L3], and $x_{i}$ is $C^{2}$ as a sum of the linear curve $t \mapsto V t$ and a scalar multiple of $e$ [L4]. With $η$ of [L3], ${\dot{x}}_{1} = V - \frac{R}{2} ω η, {\dot{x}}_{2} = V + \frac{R}{2} ω η, {\ddot{x}}_{1} = \frac{R}{2} ω^{2} e, {\ddot{x}}_{2} = - \frac{R}{2} ω^{2} e .$

2.1step 1.1givenL1L2algebra

Equations of motion. Since $ω^{2} = 2 k / m$ , on the one hand $m {\ddot{x}}_{1} = m \frac{R}{2} ω^{2} e = k R e$ ; on the other $F_{1} (x_{1}, x_{2}) = - k (x_{1} - x_{2}) = - k (- R e) = k R e$ , and these agree. Likewise $m {\ddot{x}}_{2} = - k R e = - k (x_{2} - x_{1}) = F_{2}$ . Hence $x$ is a motion of the model on the whole time window $R$ , and by [L2] it is the unique maximal motion with its datum.

2.2step 1.1L1L4L5algebra

Total momentum and centre of mass. By step 1.1, $P = m {\dot{x}}_{1} + m {\dot{x}}_{2} = 2 m V, X = \frac{1}{2} (x_{1} + x_{2}) = V t, V_{c m} = X^{'} = V,$ so $P = 2 m V$ is constant and equals $M V_{c m}$ ; the model has no external forces, consistent with clauses 1 and 2 of Total momentum balance and centre-of-mass equation for a model with antisymmetric pair forces.

2.3step 1.1L1L3L4algebra

Angular momentum about the origin. By step 1.1, $p_{1} = m V - m \frac{R}{2} ω η, p_{2} = m V + m \frac{R}{2} ω η .$ Expanding $J_{0} = x_{1} \times p_{1} + x_{2} \times p_{2}$ with $x_{1} = V t - \frac{R}{2} e$ and $x_{2} = V t + \frac{R}{2} e$ by bilinearity [L4], the four types of terms combine as follows: the terms $(V t) \times m V$ occur twice and gives $2 (V t) \times m V = 0$ since $V \times V = 0$ ; the two terms pairing $V t$ with $η$ are equal with opposite signs and cancel; the two terms pairing $e$ with $V$ are equal with opposite signs and cancel; and the two terms pairing $e$ with $η$ add: $J_{0} = 2 (\frac{R}{2})^{2} m ω (e \times η) = \frac{1}{2} m R^{2} ω e_{3},$ where $e \times η = e_{3}$ by [L4]. This is constant in $t$ .

3.1step 1.1step 2.2L1L3L4L5algebra

Kinetic splitting. With $r = x_{1} - x_{2} = - R e$ one has $\dot{r} = - R ω η$ and $∥ \dot{r} ∥_{2} = R ω$ by [L3], so the two-body clause of Total momentum equals total mass times centre-of-mass velocity, and the kinetic energy splits into centre-of-mass and relative parts (two-body reduced mass) predicts $K = \frac{1}{2} M ∥ V_{c m} ∥_{2}^{2} + \frac{1}{2} μ ∥ \dot{r} ∥_{2}^{2} = m ∥ V ∥_{2}^{2} + \frac{1}{2} \cdot \frac{m}{2} \cdot R^{2} ω^{2} = m ∥ V ∥_{2}^{2} + \frac{1}{4} m R^{2} ω^{2} .$ Directly, with $a : = \frac{R}{2} ω η$ and $∥ a ∥_{2} = \frac{R}{2} ω$ , bilinearity gives $∥ V - a ∥_{2}^{2} + ∥ V + a ∥_{2}^{2} = 2 ∥ V ∥_{2}^{2} + 2 ∥ a ∥_{2}^{2}$ , so $K = \frac{1}{2} m (∥ V - a ∥_{2}^{2} + ∥ V + a ∥_{2}^{2}) = m ∥ V ∥_{2}^{2} + m ∥ a ∥_{2}^{2} = m ∥ V ∥_{2}^{2} + \frac{1}{4} m R^{2} ω^{2},$ the same value. The relative positions are $ρ_{1} = - \frac{R}{2} e$ and $ρ_{2} = \frac{R}{2} e$ , so $m ρ_{1} + m ρ_{2} = 0$ .

3.2step 2.2step 2.3L1L4L5algebra

Moving origin. For $o (t) = W t$ one has $J_{o} = \sum_{i} (x_{i} - o) \times p_{i} = J_{0} - o \times P,$ because $o$ is common to both terms and $\sum_{i} p_{i} = P$ ; hence, by steps 2.3 and 2.2, $J_{o} = \frac{1}{2} m R^{2} ω e_{3} - (W t) \times (2 m V) = \frac{1}{2} m R^{2} ω e_{3} - 2 m t (W \times V),$ so $J_{o}^{'} = - 2 m (W \times V)$ . The angular-momentum balance clause 2 of Angular momentum balance about a fixed or moving reference point, the internal torque sum, and the centrality case reads $J_{o}^{'} = T_{o}^{e x t} + I - o^{'} \times P$ ; here $T_{o}^{e x t} = 0$ (no external forces) and $I = 0$ because the pair force is central ( $F_{12} ∥ x_{1} - x_{2}$ ), while $o^{'} \times P = W \times (2 m V) = 2 m (W \times V)$ , so the balance gives the same value $- 2 m (W \times V)$ .

4.1step 3.1L1L3L4L5algebra

Mechanical energy and power. Here $U (x (t)) = \frac{1}{2} k ∥ r ∥_{2}^{2} = \frac{1}{2} k R^{2}$ is constant in time, and by step 3.1 and $ω^{2} = 2 k / m$ , $E = K + U = m ∥ V ∥_{2}^{2} + \frac{1}{4} m R^{2} ω^{2} + \frac{1}{2} k R^{2} = m ∥ V ∥_{2}^{2} + \frac{1}{2} k R^{2} + \frac{1}{2} k R^{2} = m ∥ V ∥_{2}^{2} + k R^{2},$ constant, as clause 2 of Mechanical energy balance for a potential presentation: $E^{'} = \partial_{t} U$ plus the residual power, conservation for a static potential with no residual forces, and the integrated work form predicts (the potential is static and there are no residual forces). For the power identity, using $F_{1} = - k r$ , $F_{2} = k r$ and $\dot{r} = {\dot{x}}_{1} - {\dot{x}}_{2}$ , $P = ⟨ F_{1}, {\dot{x}}_{1} ⟩ + ⟨ F_{2}, {\dot{x}}_{2} ⟩ = - k ⟨ r, {\dot{x}}_{1} ⟩ + k ⟨ r, {\dot{x}}_{2} ⟩ = - k ⟨ r, \dot{r} ⟩ = - \frac{1}{2} k \frac{d}{d t} ∥ r ∥_{2}^{2},$ so the power is the negative derivative of the potential energy; clause 1 of Power of the total force and the work-energy theorem: $K^{'} = P$ and $K (t_{1}) - K (t_{0}) = W ([t_{0}, t_{1}])$ along a motion gives $K^{'} = P$ , consistent with $E^{'} = 0$ and clause 1 of Mechanical energy balance for a potential presentation: $E^{'} = \partial_{t} U$ plus the residual power, conservation for a static potential with no residual forces, and the integrated work form.

5.1step 2.2step 4.1L1L3L4L5algebra∎

Boost to the centre-of-mass frame. Take the second frame with $b = 0$ , $a_{0} = 0$ , $R_{r o t} = I_{3}$ and $v_{b o o s t} = - V$ ; the description of the curves is $η_{i} (t) = x_{i} (t) - V t = \mp \frac{R}{2} e (t)$ , so $\tilde{P} = m {\dot{η}}_{1} + m {\dot{η}}_{2} = 0$ and, by [L3], $\tilde{K} = \frac{1}{2} m ∥ - \frac{R}{2} ω η ∥_{2}^{2} + \frac{1}{2} m ∥ \frac{R}{2} ω η ∥_{2}^{2} = \frac{1}{4} m R^{2} ω^{2} = \frac{1}{2} k R^{2} .$ The frame law of clause 2 of Transformation of the state quantities under a change of inertial frame: centre of mass, total momentum, kinetic energy, angular momentum, torque, power, work and mechanical energy gives $\tilde{K} = K + ⟨ v_{b o o s t}, P ⟩ + \frac{1}{2} M ∥ v_{b o o s t} ∥_{2}^{2} = (m ∥ V ∥_{2}^{2} + \frac{1}{2} k R^{2}) - 2 m ∥ V ∥_{2}^{2} + m ∥ V ∥_{2}^{2} = \frac{1}{2} k R^{2},$ the same value. Finally the scalar transfer of the potential is $U_{*} = U$ at corresponding data because $U$ depends only on $x_{1} - x_{2} = η_{1} - η_{2}$ , so $\tilde{E} = \tilde{K} + U = \frac{1}{2} k R^{2} + \frac{1}{2} k R^{2} = k R^{2}$ , and clause 5 gives $\tilde{E} = E + ⟨ v_{b o o s t}, P ⟩ + \frac{1}{2} M ∥ v_{b o o s t} ∥_{2}^{2} = (m ∥ V ∥_{2}^{2} + k R^{2}) - 2 m ∥ V ∥_{2}^{2} + m ∥ V ∥_{2}^{2} = k R^{2},$ again the same value.

Remarks

What the check exhibits. The example exercises the balances of the page on one explicit motion: the algebraic splitting, the momentum law with vanishing total external force, the angular-momentum law with a moving reference point (where the correction $- o^{'} \times P$ is nonzero when both chosen velocities $W$ and $V$ are nonzero and perpendicular, while the torque vanishes), the work-energy and mechanical-energy balances, and the transformation laws of the kinetic and mechanical energies. The centrality clause of Angular momentum balance about a fixed or moving reference point, the internal torque sum, and the centrality case applies here; the companion counterexample exhibits a model where the same conservation conclusion holds without centrality.
Scope. The parameters $m$ , $k$ , $R$ , $V$ and $W$ are declared data of this computation; no measured value is asserted, no physical spring is claimed to obey the Hooke law in any regime, and the check is a deduction inside the model, not evidence about nature.

A two-body Hooke model with an exact circular relative motion: momentum, kinetic splitting, moving-origin angular momentum, energy conservation and the kinetic boost law checked on explicit data

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources