TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generated

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.

Centre of mass, the identity $\sum_{i} m_{i} ρ_{i} = 0$ , and the splitting of the kinetic sum $\sum_{i} m_{i} ∥ x_{i}^{'} ∥_{2}^{2}$ into centre-of-mass and relative parts (with the two-body reduced-mass case)

Statement

Let $N \in N$ , $N \geq 1$ , let $I \subseteq R$ be an interval with at least two points (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length), let $m_{1}, \dots, m_{N} > 0$ and let $x_{i} : I \to R^{3}$ be differentiable at every point of $I$ (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral). All sums over $i$ range over $1, \dots, N$ : for a real family $a_{1}, \dots, a_{N}$ , define $\sum_{i} a_{i} : = \sum_{k < N} b_{k}$ , where $b : N \to R$ has $b_{k} = a_{k + 1}$ for $k < N$ and $b_{k} = 0$ for $k \geq N$ , using the finite sums of Laws of finite sums and finite products; vector sums are defined coordinatewise, and sums of curves pointwise. Put $M : = \sum_{i} m_{i} > 0$ , $X : = M^{- 1} \sum_{i} m_{i} x_{i}$ and $ρ_{i} : = x_{i} - X$ . The symbols $⟨ \cdot, \cdot ⟩$ and $∥ \cdot ∥_{2}$ denote the Euclidean inner product and norm on $R^{3}$ (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ). Then:

$X$ and every $ρ_{i}$ are differentiable on $I$ , with $X^{'} = M^{- 1} \sum_{i} m_{i} x_{i}^{'}$ and $ρ_{i}^{'} = x_{i}^{'} - X^{'}$ , and the identities $\sum_{i} m_{i} ρ_{i} = 0$ and $\sum_{i} m_{i} ρ_{i}^{'} = 0$ hold on $I$ ;
for every $t \in I$ , $\sum_{i} m_{i} ∥ x_{i}^{'} (t) ∥_{2}^{2} = M ∥ X^{'} (t) ∥_{2}^{2} + \sum_{i} m_{i} ∥ ρ_{i}^{'} (t) ∥_{2}^{2};$
if $N = 2$ , then with $r : = x_{1} - x_{2}$ and $μ : = m_{1} m_{2} / M$ one has $\sum_{i} m_{i} ∥ ρ_{i}^{'} (t) ∥_{2}^{2} = μ ∥ r^{'} (t) ∥_{2}^{2}$ and hence $\sum_{i} m_{i} ∥ x_{i}^{'} (t) ∥_{2}^{2} = M ∥ X^{'} (t) ∥_{2}^{2} + μ ∥ r^{'} (t) ∥_{2}^{2}$ for every $t \in I$ .

Facts & Assumptions

Given: A natural $N \geq 1$ , an interval $I \subseteq R$ with at least two points, positive reals $m_{1}, \dots, m_{N}$ and curves $x_{i} : I \to R^{3}$ differentiable at every point of $I$ .

[L1]

If $f, g : I \to R^{m}$ are differentiable at $t$ and $μ \in R$ , then $f + g$ and $μ f$ are differentiable at $t$ with $(f + g)^{'} (t) = f^{'} (t) + g^{'} (t)$ and $(μ f)^{'} (t) = μ f^{'} (t)$ ; a vector-valued function is differentiable exactly when all its components are (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral).

[L2]

The Euclidean inner product is bilinear and symmetric, $⟨ u, w ⟩ = \sum_{k < 3} u_{k} w_{k}$ , and $∥ u ∥_{2}^{2} = ⟨ u, u ⟩$ (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

[L3]

Under the statement's shifted indexing convention, additivity and scaling in Laws of finite sums and finite products clauses 1–2 give $\sum_{i} (α a_{i} + β b_{i}) = α \sum_{i} a_{i} + β \sum_{i} b_{i}$ for real families and, by applying those scalar laws to each coordinate, vector families. Clause 4 also gives $\sum_{i} a_{i} \geq a_{j}$ for every $1 \leq j \leq N$ when all $a_{i} \geq 0$ .

Proof

technique · direct

1.1givenL1L3

Since $N \geq 1$ and all masses are positive, [L3] gives $M \geq m_{1} > 0$ , so $M^{- 1}$ is defined. Each $x_{i}$ is differentiable on $I$ , so repeated application of [L1] makes the finite sum $\sum_{i} m_{i} x_{i}$ and its scalar multiple $X = M^{- 1} \sum_{i} m_{i} x_{i}$ differentiable on $I$ with $X^{'} = M^{- 1} \sum_{i} m_{i} x_{i}^{'}$ , and then every $ρ_{i} = x_{i} - X$ is differentiable on $I$ with $ρ_{i}^{'} = x_{i}^{'} - X^{'}$ .

2.1step 1.1L1L3algebra

Using the definition of $X$ and [L3], $\sum_{i} m_{i} ρ_{i} = \sum_{i} m_{i} x_{i} - M X = \sum_{i} m_{i} x_{i} - \sum_{i} m_{i} x_{i} = 0$ on $I$ ; differentiating this identity through the sum formula of step 1.1 gives $\sum_{i} m_{i} ρ_{i}^{'} = 0$ on $I$ .

3.1step 2.1L2L3algebra

For every $t \in I$ , substituting $x_{i}^{'} = X^{'} + ρ_{i}^{'}$ and expanding with bilinearity and symmetry [L2], $\sum_{i} m_{i} ∥ x_{i}^{'} ∥_{2}^{2} = \sum_{i} m_{i} (∥ X^{'} ∥_{2}^{2} + 2 ⟨ X^{'}, ρ_{i}^{'} ⟩ + ∥ ρ_{i}^{'} ∥_{2}^{2}) = M ∥ X^{'} ∥_{2}^{2} + 2 ⟨ X^{'}, \sum_{i} m_{i} ρ_{i}^{'} ⟩ + \sum_{i} m_{i} ∥ ρ_{i}^{'} ∥_{2}^{2},$ and the middle term vanishes by step 2.1; this is clause 2.

4.1step 3.1L1L2L3algebra∎

Let $N = 2$ . From the definitions, $X = \frac{m_{1} x_{1} + m_{2} x_{2}}{M}$ and $r = x_{1} - x_{2}$ , so $ρ_{1} = x_{1} - X = \frac{M x_{1} - m_{1} x_{1} - m_{2} x_{2}}{M} = \frac{m_{2}}{M} r$ and $ρ_{2} = x_{2} - X = \frac{M x_{2} - m_{1} x_{1} - m_{2} x_{2}}{M} = - \frac{m_{1}}{M} r$ ; differentiating by [L1] and expanding squared norms by [L2] gives $\sum_{i} m_{i} ∥ ρ_{i}^{'} ∥_{2}^{2} = (\frac{m_{1} m_{2}^{2} + m_{2} m_{1}^{2}}{M^{2}}) ∥ r^{'} ∥_{2}^{2} = \frac{m_{1} m_{2} (m_{1} + m_{2})}{M^{2}} ∥ r^{'} ∥_{2}^{2} = μ ∥ r^{'} ∥_{2}^{2}$ , because $M = m_{1} + m_{2}$ . Substitution into clause 2 gives clause 3.

Centre of mass, the identity $\sum_{i} m_{i} ρ_{i} = 0$ , and the splitting of the kinetic sum $\sum_{i} m_{i} ∥ x_{i}^{'} ∥_{2}^{2}$ into centre-of-mass and relative parts (with the two-body reduced-mass case)

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

Centre of mass, the identity ∑imiρi=0∑i​mi​ρi​=0, and the splitting of the kinetic sum ∑imi∥xi′∥22∑i​mi​∥xi′​∥22​ into centre-of-mass and relative parts (with the two-body reduced-mass case)

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

Centre of mass, the identity $\sum_{i} m_{i} ρ_{i} = 0$ , and the splitting of the kinetic sum $\sum_{i} m_{i} ∥ x_{i}^{'} ∥_{2}^{2}$ into centre-of-mass and relative parts (with the two-body reduced-mass case)