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.

Polar reduction of a non-radial central-force trajectory: $ρ^{2} θ^{'} = J / μ$ , the effective-potential equation and energy conservation

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)$ whose angular momentum $j = μ r \times r^{'}$ is a nonzero constant vector (Conservation of the angular momentum vector along a central-force trajectory and its orthogonality to position and velocity); write $J : = ∣ j ∣ > 0$ . Let $(e_{1}, e_{2}, e_{3})$ be an oriented orthonormal triad with $e_{3} = j / J$ (Oriented orthonormal triads in $R^{3}$ : existence over any unit vector, and the orthonormal expansion with no fourth orthogonal direction).

Then there are twice differentiable $ρ : I \to (0, \infty)$ and $θ : I \to R$ with

$r (t) = ρ (t) (\cos θ (t) e_{1} + \sin θ (t) e_{2}) (t \in I),$

and for every such pair $(ρ, θ)$ :

$ρ (t) = ∣ r (t) ∣$ for all $t$ ;
$ρ^{2} θ^{'} = J / μ$ on $I$ , so $θ^{'} > 0$ ;
the effective-potential equation $μ ρ^{''} = - (U_{J}^{e f f})^{'} (ρ)$ holds on $I$ , with $U_{J}^{e f f} = U + J^{2} / (2 μ ρ^{2})$ (Central-force trajectories: the central-force equation, angular momentum, energy and the effective potential);
$E : = \frac{1}{2} μ ∥ r^{'} ∥_{2}^{2} + U (∣ r ∣)$ equals $\frac{1}{2} μ ρ^{' 2} + U_{J}^{e f f} (ρ)$ and is constant on $I$ .

Facts & Assumptions

Given: A central-force trajectory $r$ for $(μ, U)$ with constant nonzero angular momentum $j = J e_{3}$ , $J > 0$ , an oriented orthonormal triad $(e_{1}, e_{2}, e_{3})$ , and twice differentiable $ρ, θ$ with $r = ρ (\cos θ e_{1} + \sin θ e_{2})$ .

[L1]

For the oriented orthonormal triad: every $x \in R^{3}$ is $x = ⟨ x, e_{1} ⟩ e_{1} + ⟨ x, e_{2} ⟩ e_{2} + ⟨ x, e_{3} ⟩ e_{3}$ and $∣ x ∣^{2} = \sum_{i} ⟨ x, e_{i} ⟩^{2}$ (Oriented orthonormal triads in $R^{3}$ : existence over any unit vector, and the orthonormal expansion with no fourth orthogonal direction).

[L2]

The angular momentum is orthogonal to $r$ and to $r^{'}$ : $⟨ r, e_{3} ⟩ J = ⟨ r, j ⟩ = 0$ and $⟨ r^{'}, j ⟩ = 0$ (Conservation of the angular momentum vector along a central-force trajectory and its orthogonality to position and velocity).

[L3]

Polar lift: for twice differentiable $ρ_{1}, ρ_{2} : I \to R$ with $(ρ_{1}, ρ_{2}) \neq (0, 0)$ there is a twice differentiable angle function such that $ρ_{1} = r_{0} \cos θ$ , $ρ_{2} = r_{0} \sin θ$ with $r_{0} = \sqrt{ρ_{1}^{2} + ρ_{2}^{2}}$ (Local polar coordinates for a curve with nonvanishing position in the plane: a differentiable angle function with prescribed derivative).

[L4]

Differentiability rules: inner products and cross products of differentiable curves differentiate by the product rule, $⟨ x, y ⟩^{'} = ⟨ x^{'}, y ⟩ + ⟨ x, y^{'} ⟩$ and $(x \times y)^{'} = x^{'} \times y + x \times y^{'}$ ; the chain rule differentiates $\cos θ$ and $\sin θ$ with derivatives $- θ^{'} \sin θ$ and $θ^{'} \cos θ$ ; sums, products and quotients with nonvanishing denominator differentiate by the usual rules (Differentiation of sums, scalar multiples, inner products, cross products and squared norms of differentiable curves in $R^{3}$ , 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$ ).

[L5]

Cross product rules: $e_{1} \times e_{2} = e_{3}$ , $e_{2} \times e_{1} = - e_{3}$ , the product is bilinear, and $e_{i}$ are unit vectors (The cross product in $R^{3}$ , The cross product is bilinear, alternating, and orthogonal to both factors); $\cos^{2} + \sin^{2} = 1$ (Parity and the Pythagorean identity for sine and cosine).

[L6]

A function continuous on $I$ whose derivative vanishes at every interior point is constant on $I$ (A function continuous on an interval $I$ whose derivative vanishes at every interior point of $I$ is constant on $I$ ; consequently two such functions with the same derivative differ by a constant, $C^{k}$ Euclidean maps and diffeomorphisms, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

Proof

technique · direct

1.1givenL1L2L4algebra

Put $ρ_{i} : = ⟨ r, e_{i} ⟩$ for $i = 1, 2$ ; these are twice differentiable by [L4]. They are never both zero: by [L1] and [L2], $r = ρ_{1} e_{1} + ρ_{2} e_{2} + ⟨ r, e_{3} ⟩ e_{3} = ρ_{1} e_{1} + ρ_{2} e_{2}$ , so $ρ_{1} = ρ_{2} = 0$ would give $r = 0$ , contradicting $∣ r ∣ \in J_{0} \subseteq (0, \infty)$ .

1.2givenL1L5algebra

Clause 1 for an arbitrary pair: if $r = ρ (\cos θ e_{1} + \sin θ e_{2})$ , then $∣ r ∣^{2} = ∣ r ∣^{2}$ is computed by [L1] and [L5] as $ρ^{2} (\cos^{2} θ + \sin^{2} θ) = ρ^{2}$ , hence $ρ = ∣ r ∣$ .

1.3givenL4L5algebra

Differentiating [L5]'s expansion $r = ρ n$ with $n : = \cos θ e_{1} + \sin θ e_{2}$ and $n_{⊥} : = - \sin θ e_{1} + \cos θ e_{2}$ by [L4] gives $r^{'} = ρ^{'} n + ρ θ^{'} n_{⊥}, r^{''} = (ρ^{''} - ρ θ^{' 2}) n + (2 ρ^{'} θ^{'} + ρ θ^{''}) n_{⊥} .$ Here $n \times n_{⊥} = e_{3}$ and $n_{⊥} \times n = - e_{3}$ by bilinearity of the cross product and $e_{1} \times e_{2} = e_{3}$ .

2.1step 1.1L1L2L3algebra

Apply the polar lift [L3] to $(ρ_{1}, ρ_{2})$ : there is a twice differentiable $θ$ with $ρ_{1} = r_{0} \cos θ$ , $ρ_{2} = r_{0} \sin θ$ for $r_{0} = \sqrt{ρ_{1}^{2} + ρ_{2}^{2}}$ ; by Parseval in [L1] and $⟨ r, e_{3} ⟩ = 0$ , $r_{0}^{2} = ρ_{1}^{2} + ρ_{2}^{2} = ∣ r ∣^{2}$ , so $r_{0} = ∣ r ∣ = : ρ$ is twice differentiable with values in $J_{0} \subseteq (0, \infty)$ . Substituting into the expansion of step 1.1 gives $r = ρ (\cos θ e_{1} + \sin θ e_{2})$ , so such a pair exists.

2.2givenstep 1.3L5algebra

Clause 2: from step 1.3, $r \times r^{'} = ρ n \times (ρ^{'} n + ρ θ^{'} n_{⊥}) = ρ^{2} θ^{'} e_{3},$ so $j = J e_{3} = μ r \times r^{'} = μ ρ^{2} θ^{'} e_{3}$ , giving $J = μ ρ^{2} θ^{'}$ and hence $ρ^{2} θ^{'} = J / μ > 0$ .

3.1givenstep 1.2step 1.3step 2.2L1L5algebra

Clause 3: the trajectory equation is $μ r^{''} = - (U^{'} (∣ r ∣) / ∣ r ∣) r = - U^{'} (ρ) n$ by clause 1. Comparing with the decomposition of step 1.3 and using the linear independence of $n$ and $n_{⊥}$ — their components in the orthonormal triad are distinct, so $α n + β n_{⊥} = 0$ forces $α = β = 0$ by taking inner products with $n$ and $n_{⊥}$ — the radial component gives $μ (ρ^{''} - ρ θ^{' 2}) = - U^{'} (ρ) .$ Substituting $ρ^{2} θ^{'} = J / μ$ from step 2.2 gives $μ ρ^{''} = - U^{'} (ρ) + μ ρ θ^{' 2} = - U^{'} (ρ) + \frac{J^{2}}{μ ρ^{3}} = - (U_{J}^{e f f})^{'} (ρ)$ , because $(U_{J}^{e f f})^{'} = U^{'} (ρ) - \frac{J^{2}}{μ ρ^{3}}$ .

3.2step 1.3step 2.2L1algebra

Clause 4, the energy identity: from step 1.3 and orthonormality, $∥ r^{'} ∥_{2}^{2} = ρ^{' 2} + ρ^{2} θ^{' 2}$ , so $E = \frac{1}{2} μ ρ^{' 2} + \frac{1}{2} μ ρ^{2} θ^{' 2} + U (ρ) = \frac{1}{2} μ ρ^{' 2} + \frac{J^{2}}{2 μ ρ^{2}} + U (ρ) = \frac{1}{2} μ ρ^{' 2} + U_{J}^{e f f} (ρ)$ by step 2.2.

4.1step 3.1step 3.2L4L6algebra∎

The right-hand side is differentiable on $I$ and its derivative is $μ ρ^{'} ρ^{''} + (U_{J}^{e f f})^{'} (ρ) ρ^{'} = ρ^{'} (μ ρ^{''} + (U_{J}^{e f f})^{'} (ρ)) = 0$ by step 3.1 (the equation holds at every point of $I$ ); hence $E$ is constant on $I$ by [L6].

Polar reduction of a non-radial central-force trajectory: $ρ^{2} θ^{'} = J / μ$ , the effective-potential equation and energy conservation

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

Polar reduction of a non-radial central-force trajectory: ρ2θ′=J/μρ2θ′=J/μ, the effective-potential equation and energy conservation

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

Polar reduction of a non-radial central-force trajectory: $ρ^{2} θ^{'} = J / μ$ , the effective-potential equation and energy conservation