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.

Conservation of the angular momentum vector along a central-force trajectory and its orthogonality to position and velocity

Statement

Let $μ > 0$ , let $J_{0} \subseteq (0, \infty)$ be an open interval, let $U : J_{0} \to R$ be of class $C^{2}$ , let $I \subseteq R$ be an interval with at least two points, and let $r : I \to R^{3}$ be a central-force trajectory for $(μ, U)$ with angular momentum vector $j = μ r \times r^{'}$ (Central-force trajectories: the central-force equation, angular momentum, energy and the effective potential). Then:

$j$ is differentiable on $I$ with $j^{'} (t) = 0$ for every $t \in I$ ; hence $j$ is constant on $I$ ;
for every $t \in I$ , $⟨ r (t), j (t) ⟩ = 0$ and $⟨ r^{'} (t), j (t) ⟩ = 0$ .

Facts & Assumptions

Given: A central-force trajectory $r$ for $(μ, U)$ on an interval $I$ with at least two points.

[L1]

For differentiable curves $u, v : I \to R^{3}$ the cross product $u \times v$ is differentiable with $(u \times v)^{'} = u^{'} \times v + u \times v^{'}$ ; moreover sums, and scalar multiples of curves, differentiate by the usual rules (Differentiation of sums, scalar multiples, inner products, cross products and squared norms of differentiable curves in $R^{3}$ ).

[L2]

The trajectory satisfies $r^{''} = - (U^{'} (∣ r ∣) / (μ ∣ r ∣)) r$ on $I$ , where $∣ x ∣ = ∥ x ∥_{2}$ (Central-force trajectories: the central-force equation, angular momentum, energy and the effective potential, The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral).

[L3]

The cross product is bilinear and alternating, so $u \times u = 0$ and $(u \times v) ⊥ u$ , $(u \times v) ⊥ v$ ; orthogonality means vanishing Euclidean inner product (The cross product is bilinear, alternating, and orthogonal to both factors, The cross product in $R^{3}$ , The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

[L4]

If $f : [a, b] \to R^{3}$ is differentiable with integrable $f^{'}$ , then $\int_{a}^{b} f^{'} = f (b) - f (a)$ (If $f : [a, b] \to R^{m}$ is differentiable with integrable $f^{'}$ then $\int_{a}^{b} f^{'} = f (b) - f (a)$ ; and a bounded derivative makes $f$ Lipschitz, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

Proof

technique · direct

1.1givenL1algebra

By [L1] the curve $j = μ (r \times r^{'})$ is differentiable with $j^{'} = μ (r^{'} \times r^{'} + r \times r^{''}) = μ r \times r^{''} .$

2.1step 1.1L2L3algebra

Substituting [L2] and using alternation [L3], $j^{'} = μ r \times (- \frac{U^{'} (∣ r ∣)}{μ ∣ r ∣} r) = - \frac{U^{'} (∣ r ∣)}{∣ r ∣} r \times r = 0 on I .$

3.1step 2.1L4

Let $a, b \in I$ with $a < b$ . Then [L4] applied to $j$ gives $\int_{a}^{b} j^{'} = j (b) - j (a)$ ; since $j^{'}$ is the zero curve by step 2.1, the integral vanishes and $j (b) = j (a)$ . As $a, b$ were arbitrary, $j$ is constant on $I$ .

4.1L3algebra∎

For every $t \in I$ , [L3] gives $⟨ r (t), j (t) ⟩ = μ ⟨ r (t), r (t) \times r^{'} (t) ⟩ = 0$ and $⟨ r^{'} (t), j (t) ⟩ = μ ⟨ r^{'} (t), r (t) \times r^{'} (t) ⟩ = 0$ : the cross product is orthogonal to each factor.

Conservation of the angular momentum vector along a central-force trajectory and its orthogonality to position and velocity

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources