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.

Total momentum and total angular momentum balances for a finite system with antisymmetric pair forces; pairwise central forces make the internal torque vanish

Statement

Let $I \subseteq R$ be an interval with at least two points (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length), let $N \geq 1$ , let $m_{1}, \dots, m_{N} > 0$ , and let $x_{i} : I \to R^{3}$ be twice differentiable, i.e. differentiable with derivative $x_{i}^{'}$ differentiable (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral). Write $p_{i} : = m_{i} x_{i}^{'}$ and suppose there are maps $f_{i} : I \to R^{3}$ and, for every ordered pair $i \neq j$ in ${1, \dots, N}$ , maps $f_{i j} : I \to R^{3}$ such that

$f_{i j} (t) = - f_{j i} (t), p_{i}^{'} (t) = f_{i} (t) + \sum_{j \neq i} f_{i j} (t) (t \in I) .$

Write $P : = \sum_{i} p_{i}$ , $J : = \sum_{i} x_{i} \times p_{i}$ (cross product in $R^{3}$ , The cross product in $R^{3}$ ). Then:

$P$ is differentiable on $I$ with $P^{'} (t) = \sum_{i} f_{i} (t)$ for all $t \in I$ ;
$J$ is differentiable on $I$ with $J^{'} (t) = \sum_{i} x_{i} (t) \times f_{i} (t) + \sum_{i < j} (x_{i} (t) - x_{j} (t)) \times f_{i j} (t) (t \in I);$
if in addition, for every $i < j$ , $f_{i j}$ is parallel to $x_{i} - x_{j}$ — that is, there is a real function $λ_{i j}$ on $I$ with $f_{i j} = λ_{i j} (x_{i} - x_{j})$ — then $J^{'} (t) = \sum_{i} x_{i} (t) \times f_{i} (t)$ for all $t \in I$ .

Facts & Assumptions

Given: An interval $I \subseteq R$ with at least two points, $N \geq 1$ , positive reals $m_{1}, \dots, m_{N}$ , twice differentiable curves $x_{i} : I \to R^{3}$ , velocities $v_{i} : = x_{i}^{'}$ , momenta $p_{i} = m_{i} v_{i}$ , and maps $f_{i}, f_{i j}$ with $f_{i j} = - f_{j i}$ and $p_{i}^{'} = f_{i} + \sum_{j \neq i} f_{i j}$ on $I$ .

[L1]

Sums and scalar multiples of curves differentiable at $t$ are differentiable at $t$ with the expected derivatives (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral).

[L2]

Finite sums over finite sets may be reindexed along bijections and are additive over disjoint unions (Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule clauses 1 and 2); consequently, for vectors $a_{i j}$ indexed by the ordered pairs $(i, j)$ with $i \neq j$ , the set of such pairs is the disjoint union over the unordered pairs $i < j$ of the two-element sets ${(i, j), (j, i)}$ , so $\sum_{i} \sum_{j \neq i} a_{i j} = \sum_{i < j} (a_{i j} + a_{j i})$ . Scalar factors distribute over finite sums (Laws of finite sums and finite products).

[L3]

For differentiable curves $u, v : I \to R^{3}$ and $t \in I$ , the cross product $t \mapsto u (t) \times v (t)$ is differentiable at $t$ with derivative $u^{'} (t) \times v (t) + u (t) \times v^{'} (t)$ (Differentiation of sums, scalar multiples, inner products, cross products and squared norms of differentiable curves in $R^{3}$ ).

[L4]

The cross product is bilinear and alternating, so $u \times u = 0$ , $u \times v = - (v \times u)$ and $u \times (v + w) = u \times v + u \times w$ for $u, v, w \in R^{3}$ (The cross product in $R^{3}$ , The cross product is bilinear, alternating, and orthogonal to both factors).

Proof

technique · direct

1.1givenL1L2algebra

Since $P$ is the finite sum of the differentiable curves $p_{i}$ , [L1] gives $P^{'} = \sum_{i} p_{i}^{'}$ ; substituting the balance equation and using $f_{i j} = - f_{j i}$ with the reindexing rule [L2], $\sum_{i} \sum_{j \neq i} f_{i j} = \sum_{i < j} (f_{i j} + f_{j i}) = 0$ , so $P^{'} = \sum_{i} f_{i}$ ; this is clause 1.

2.1step 1.1givenL1L3

Each term $x_{i} \times p_{i}$ is differentiable on $I$ with derivative $x_{i}^{'} \times p_{i} + x_{i} \times p_{i}^{'}$ by [L3], and [L1] makes their finite sum $J$ differentiable with $J^{'} = \sum_{i} x_{i}^{'} \times p_{i} + \sum_{i} x_{i} \times p_{i}^{'} = \sum_{i} x_{i}^{'} \times p_{i} + \sum_{i} x_{i} \times f_{i} + \sum_{i} \sum_{j \neq i} x_{i} \times f_{i j} .$

3.1step 2.1L4algebra

The first sum in step 2.1 vanishes termwise: $x_{i}^{'} \times p_{i} = m_{i} x_{i}^{'} \times x_{i}^{'} = 0$ by alternation [L4].

4.1step 2.1step 3.1L2L4algebra

The double sum in step 2.1 equals $\sum_{i < j} (x_{i} \times f_{i j} + x_{j} \times f_{j i}) = \sum_{i < j} (x_{i} - x_{j}) \times f_{i j}$ : the first equality reindexes the ordered pairs by the unordered ones [L2], and the second uses $f_{j i} = - f_{i j}$ , bilinearity and $u \times (- w) = - (u \times w)$ [L4]. Combining with steps 2.1 and 3.1 gives clause 2.

5.1step 4.1givenL4algebra∎

Under the parallelism hypothesis, $(x_{i} - x_{j}) \times f_{i j} = λ_{i j} (x_{i} - x_{j}) \times (x_{i} - x_{j}) = 0$ for every $i < j$ by alternation [L4]; hence the double sum in clause 2 vanishes and $J^{'} = \sum_{i} x_{i} \times f_{i}$ , which is clause 3.

Total momentum and total angular momentum balances for a finite system with antisymmetric pair forces; pairwise central forces make the internal torque vanish

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources