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.

Circular orbits of a non-radial central-force trajectory: the critical-point condition and the squared frequency of the linearised radial equation

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$ be an interval with at least two points, and let $r : I \to R^{3}$ be a central-force trajectory for $(μ, U)$ with constant nonzero angular momentum $j = J e_{3}$ , $J > 0$ , and polar data $(ρ, θ)$ as in Polar reduction of a non-radial central-force trajectory: $ρ^{2} θ^{'} = J / μ$ , the effective-potential equation and energy conservation, so that $ρ^{2} θ^{'} = J / μ$ and $μ ρ^{''} = - (U_{J}^{e f f})^{'} (ρ)$ on $I$ . Fix $r_{0} \in J_{0}$ . Then:

(Necessity.) If $ρ \equiv r_{0}$ is constant on $I$ , then $(U_{J}^{e f f})^{'} (r_{0}) = 0$ and $θ^{'} \equiv J / (μ r_{0}^{2})$ is constant; the trajectory is the uniform rotation $r (t) = r_{0} (\cos θ (t) e_{1} + \sin θ (t) e_{2})$ .
(Existence.) Conversely, if $(U_{J}^{e f f})^{'} (r_{0}) = 0$ , then for every $θ_{0} \in R$ the curve $r^{\circ} (t) : = r_{0} (\cos (θ_{0} + ω t) e_{1} + \sin (θ_{0} + ω t) e_{2}), ω : = \frac{J}{μ r_{0}^{2}},$ is a central-force trajectory for $(μ, U)$ defined on $R$ , with angular momentum $j = J e_{3}$ and constant energy $E = \frac{1}{2} μ r_{0}^{2} ω^{2} + U (r_{0}) = U_{J}^{e f f} (r_{0})$ .
(Linearised radial equation.) Let $ρ$ be a solution of the reduced equation $μ ρ^{''} = - (U_{J}^{e f f})^{'} (ρ)$ on $I$ with $(U_{J}^{e f f})^{'} (r_{0}) = 0$ , and put $δ : = ρ - r_{0}$ . Then $μ δ^{''} = - (U_{J}^{e f f})^{''} (r_{0}) δ + g (δ), g (x) : = (U_{J}^{e f f})^{''} (r_{0}) x - (U_{J}^{e f f})^{'} (r_{0} + x),$ where $g (x) / x \to 0$ as $x \to 0$ ; if moreover $(U_{J}^{e f f})^{''} (r_{0}) > 0$ , then the associated linearised equation $μ δ^{''} = - (U_{J}^{e f f})^{''} (r_{0}) δ$ has exactly the solutions $δ (t) = A \cos (ω_{l i n} (t - t_{0})) + B \sin (ω_{l i n} (t - t_{0}))$ with $A, B \in R$ and $ω_{l i n} : = \sqrt{(U_{J}^{e f f})^{''} (r_{0}) / μ} > 0$ , for any $t_{0} \in I$ . This is a statement about the quadratic radial approximation; no nonlinear stability of the circular orbit is asserted.

Facts & Assumptions

Given: The central-force data with constant nonzero angular momentum $j = J e_{3}$ and polar data $(ρ, θ)$ from Polar reduction of a non-radial central-force trajectory: $ρ^{2} θ^{'} = J / μ$ , the effective-potential equation and energy conservation, a radius $r_{0} \in J_{0}$ , and the functions $n (θ) : = \cos θ e_{1} + \sin θ e_{2}$ , $n_{⊥} (θ) : = - \sin θ e_{1} + \cos θ e_{2}$ .

[L1]

Polar reduction: $r = ρ n (θ)$ with $ρ = ∣ r ∣$ , $ρ^{2} θ^{'} = J / μ$ , $μ ρ^{''} = - (U_{J}^{e f f})^{'} (ρ)$ , and the energy is constant (Polar reduction of a non-radial central-force trajectory: $ρ^{2} θ^{'} = J / μ$ , the effective-potential equation and energy conservation).

[L2]

Derivative rules: the chain rule, the product rule and the trigonometric derivatives $(\cos)^{'} = - \sin$ , $(\sin)^{'} = \cos$ ; the cross product differentiates by the product rule; $e_{1} \times e_{2} = e_{3}$ and $e_{2} \times e_{1} = - e_{3}$ and the cross product is bilinear (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 derivatives of sine and cosine are cosine and minus sine, Differentiation of sums, scalar multiples, inner products, cross products and squared norms of differentiable curves in $R^{3}$ , Oriented orthonormal triads in $R^{3}$ : existence over any unit vector, and the orthonormal expansion with no fourth orthogonal direction).

[L3]

$\sin^{2} + \cos^{2} = 1$ ; and for the linearised equation: the solutions of $v^{''} + ω^{2} v = 0$ on an interval with $ω > 0$ are exactly $A \cos (ω (t - t_{0})) + B \sin (ω (t - t_{0}))$ (Parity and the Pythagorean identity for sine and cosine, Solutions of $v^{''} + ω^{2} v = 0$ are exactly the functions $A \cos (ω (t - t_{0})) + B \sin (ω (t - t_{0}))$ , $C^{k}$ Euclidean maps and diffeomorphisms).

[L4]

The derivative of $(U_{J}^{e f f})^{'}$ at $r_{0}$ is $(U_{J}^{e f f})^{''} (r_{0})$ : for every $ε > 0$ there is $η > 0$ with $∣ (U_{J}^{e f f})^{'} (r_{0} + x) - (U_{J}^{e f f})^{'} (r_{0}) - (U_{J}^{e f f})^{''} (r_{0}) x ∣ \leq ε ∣ x ∣$ for $∣ x ∣ < η$ (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, Limit point, isolated point, adherent point, derived set, and dense subset of $R$ , Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

Proof

technique · direct

1.1givenL1algebra

Clause 1: if $ρ \equiv r_{0}$ then $ρ^{''} = 0$ , so the reduced equation of [L1] gives $(U_{J}^{e f f})^{'} (r_{0}) = 0$ ; and $θ^{'} = J / (μ ρ^{2}) = J / (μ r_{0}^{2})$ is constant by [L1].

1.2givenL2L3algebraconstruct

Clause 2, the kinematics: for $r^{\circ} (t) = r_{0} n (θ_{0} + ω t)$ with $ω = J / (μ r_{0}^{2})$ , [L2] gives $(r^{\circ})^{'} = r_{0} ω n_{⊥} (θ_{0} + ω t)$ and $(r^{\circ})^{''} = - r_{0} ω^{2} n (θ_{0} + ω t)$ ; hence $j = μ r^{\circ} \times (r^{\circ})^{'} = μ r_{0}^{2} ω e_{3} = J e_{3}$ and $∥ (r^{\circ})^{'} ∥_{2}^{2} = r_{0}^{2} ω^{2}$ , using [L2] and [L3].

1.3givenL1L4algebra

Clause 3, the remainder: by [L4] applied to $(U_{J}^{e f f})^{'}$ at $r_{0}$ , for every $ε > 0$ there is $η > 0$ with $∣ g (x) ∣ \leq ε ∣ x ∣$ for $∣ x ∣ < η$ , where $g (x) = (U_{J}^{e f f})^{''} (r_{0}) x - (U_{J}^{e f f})^{'} (r_{0} + x)$ and $(U_{J}^{e f f})^{'} (r_{0}) = 0$ ; that is, $g (x) / x \to 0$ . Substituting $ρ = r_{0} + δ$ into the reduced equation of [L1] and expanding gives $μ δ^{''} = - (U_{J}^{e f f})^{'} (r_{0} + δ) = - (U_{J}^{e f f})^{''} (r_{0}) δ + g (δ)$ .

2.1givenstep 1.2L1algebra

Clause 2, the equation of motion: from step 1.2 and $ω^{2} = J^{2} / (μ^{2} r_{0}^{4})$ , $μ (r^{\circ})^{''} = - μ r_{0} ω^{2} n = - \frac{J^{2}}{μ r_{0}^{3}} n,$ while $- (U^{'} (r_{0}) / r_{0}) r^{\circ} = - U^{'} (r_{0}) n$ ; the two agree because $(U_{J}^{e f f})^{'} (r_{0}) = 0$ means $U^{'} (r_{0}) = J^{2} / (μ r_{0}^{3})$ . The energy is $\frac{1}{2} μ r_{0}^{2} ω^{2} + U (r_{0}) = \frac{J^{2}}{2 μ r_{0}^{2}} + U (r_{0}) = U_{J}^{e f f} (r_{0})$ , and it is constant because the equation is satisfied and the trajectory is periodic; more directly it equals the constant right-hand side of clause 4 of [L1] along this motion.

3.1step 1.3L3algebra∎

Clause 3, the linearised solutions: if $(U_{J}^{e f f})^{''} (r_{0}) > 0$ then $ω_{l i n}^{2} = (U_{J}^{e f f})^{''} (r_{0}) / μ > 0$ and the linearised equation reads $δ^{''} + ω_{l i n}^{2} δ = 0$ ; by [L3] its solutions on $I$ are exactly the displayed trigonometric functions for any $t_{0} \in I$ .

Circular orbits of a non-radial central-force trajectory: the critical-point condition and the squared frequency of the linearised radial equation

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources