ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedprecheck pass

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.

The gravitational two-body model on an elliptic orbit: two simple turning points of the effective potential and $J_{a}^{'} (E) = T / (2 π) = \sqrt{μ / κ} a^{3 / 2}$

Physical scope

Assuming countable choice for the orbit suppliers, A worked instance inside the two-label gravitational model of the framework's force branch: on the unique global central-force extension of an elliptic relative orbit ( $j = J e_{3}$ , $J > 0$ , $E < 0$ , eccentricity $0 \leq e < 1$ ), the Kepler effective potential has exactly two simple turning points on the energy window between its minimum and $0$ ; the one-dimensional action variable of the radial problem is $C^{1}$ there with derivative $T / (2 π)$ ; and for a noncircular orbit the radial quadrature is the orbital period, so $J_{a}^{'} (E) = T / (2 π) = \sqrt{μ / κ} a^{3 / 2}$ with $T^{2} = 4 π^{2} μ a^{3} / κ$ . The example uses only the model's declared couplings $κ = G_{N} m_{1}^{g} m_{2}^{g}$ and masses; no measured value of $G_{N}$ and no empirical premise is used, and no real orbit is claimed to obey the model.

Example

Assume ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )), as required by the conic, ellipse and period suppliers.

Adopt the two-label gravitational model of Adopted two-label gravitational model: the inverse-square pair potential with coupling parameters, the empirical mass identification, and the measured value and uncertainty of the Newtonian constant clause (i) inside the central-force model of Adopted central-force model class: static central pair potentials, the reduced one-label problem, the fixed-centre idealization, reading conventions and exclusions: inertial masses $m_{1}, m_{2} > 0$ , $M = m_{1} + m_{2}$ , reduced mass $μ = m_{1} m_{2} / M$ , gravitational couplings $m_{1}^{g}, m_{2}^{g} > 0$ , $κ = G_{N} m_{1}^{g} m_{2}^{g} > 0$ and the pair potential of Two-body reduction of a static central pair-potential model: the relative coordinate is a central-force trajectory for the reduced mass, the centre of mass moves uniformly, and the reconstruction is a bijection. Let $x : I \to Q$ be a motion whose relative coordinate $r$ has constant angular momentum $j = J e_{3}$ with $J > 0$ and constant energy $E < 0$ . Let $\overset{ˉ}{r} : R \to R^{3} ∖ {0}$ be the unique global central-force extension of $r$ supplied by Completeness and periodicity of the negative-energy Kepler orbit, with $T = 2 π μ a b / J$ and $T^{2} = 4 π^{2} μ a^{3} / κ$ clause 1 and Kepler's third law for the gravitational two-label model: the relative period is $T = 2 π μ a b / J = 2 π \sqrt{μ / κ} a^{3 / 2}$ , so $T^{2} = 4 π^{2} a^{3} / (G_{N} M)$ under the mass identification, and both labels are periodic relative to the centre of mass clause 1. In all subsequent period and quadrature statements, write $r : = \overset{ˉ}{r}$ , $ρ : = ∣ \overset{ˉ}{r} ∣$ and let $θ : R \to R$ be its increasing polar-angle lift. Its restriction to the initial interval is the original relative motion; no global physical time window is assumed. Let $0 \leq e < 1$ , $θ_{0}$ ,

$p = \frac{J^{2}}{μ κ}, a = \frac{p}{1 - e^{2}}, b = a \sqrt{1 - e^{2}}, T = 2 π \sqrt{\frac{μ}{κ}} a^{3 / 2}$ be its conic data (The Kepler orbit equation is a conic: $u = c (1 + e \cos (φ - θ_{0}))$ with $E = (μ κ^{2} / 2 J^{2}) (e^{2} - 1)$ , Kepler's third law for the gravitational two-label model: the relative period is $T = 2 π μ a b / J = 2 π \sqrt{μ / κ} a^{3 / 2}$ , so $T^{2} = 4 π^{2} a^{3} / (G_{N} M)$ under the mass identification, and both labels are periodic relative to the centre of mass). Write

$I_{0} : = (- \frac{μ κ^{2}}{2 J^{2}}, 0), r_{*} : = \frac{J^{2}}{μ κ} = p, U^{e f f} (ρ) : = - \frac{κ}{ρ} + \frac{J^{2}}{2 μ ρ^{2}} (ρ > 0)$ for the effective potential of Reduction of the central problem to the effective one-dimensional potential: $μ ρ^{''} = - (U_{J}^{e f f})^{'} (ρ)$ , the energy identity, and the converse reconstruction of the planar trajectory from the radial data (its effective potential $U_{J}^{e f f}$ ). The example verifies:

(two simple turning points) $U^{e f f}$ is of class $C^{\infty}$ on $(0, \infty)$ , has the unique critical point $r_{*}$ with $U^{e f f} (r_{*}) = - μ κ^{2} / (2 J^{2})$ , is strictly decreasing on $(0, r_{*})$ and strictly increasing on $(r_{*}, \infty)$ ; hence for every $E \in I_{0}$ there are exactly two solutions $0 < r_{-} (E) < r_{*} < r_{+} (E)$ of $U^{e f f} (ρ) = E$ , with $(U^{e f f})^{'} (r_{-} (E)) < 0 < (U^{e f f})^{'} (r_{+} (E))$ and $U^{e f f} < E$ between them, and the datum $(J_{0}, U^{e f f}, μ)$ with $J_{0} = (0, \infty)$ satisfies the hypotheses of The action variable of a two-simple-turning-point family is $C^{1}$ with derivative $T (E) / (2 π)$ , the period quadrature over $2 π$ on the energy window $I_{0}$ .
(action derivative) consequently the action variable $J_{a}$ of The one-dimensional action variable of a family of two-turning-point energy levels is of class $C^{1}$ on $I_{0}$ with $J_{a}^{'} (E) = \frac{T_{r a d} (E)}{2 π}, T_{r a d} (E) = \sqrt{2 μ} \int_{r_{-} (E)}^{r_{+} (E)} \frac{d ρ}{\sqrt{E - U^{e f f} (ρ)}} \in (0, \infty) .$
(quadrature equals the orbital period) for a noncircular orbit $0 < e < 1$ (equivalently $E \in I_{0}$ ), the radial coordinate of this global extension solves the one-dimensional problem of clause 1 of Reduction of the central problem to the effective one-dimensional potential: $μ ρ^{''} = - (U_{J}^{e f f})^{'} (ρ)$ , the energy identity, and the converse reconstruction of the planar trajectory from the radial data with the same energy, and its least positive period is the orbital period $T$ of the conic data; the time quadrature of that problem is $T_{r a d} (E) = T$ , so that $J_{a}^{'} (E) = \frac{T}{2 π} = \sqrt{\frac{μ}{κ}} a^{3 / 2}, T^{2} = \frac{4 π^{2} μ a^{3}}{κ} .$
(sharpness of the hypotheses) for $e = 0$ the two turning points coalesce at the critical point $r_{*} = a$ and the simple-turning-point hypothesis of the action-variable theorem fails; the value $J = 0$ is outside this example (no two-sided bound radial motion), so both hypotheses of the construction are genuinely used.

The couplings $κ$ and the masses are declared model parameters; no measured value of $G_{N}$ and no empirical premise enters.

Facts & Assumptions

Given: Assume ${A C}_{ω}$ . The gravitational model data $m_{1}, m_{2}, κ > 0$ , the motion with $j = J e_{3}$ , $J > 0$ , $E < 0$ , its unique global relative extension $r$ with $ρ = ∣ r ∣$ and polar lift $θ$ , the conic data $p, e, a, b, T$ , the effective potential $U^{e f f}$ and the energy window $I_{0}$ .

[L1]

Model and reduction (Adopted two-label gravitational model: the inverse-square pair potential with coupling parameters, the empirical mass identification, and the measured value and uncertainty of the Newtonian constant, Adopted central-force model class: static central pair potentials, the reduced one-label problem, the fixed-centre idealization, reading conventions and exclusions, Two-body reduction of a static central pair-potential model: the relative coordinate is a central-force trajectory for the reduced mass, the centre of mass moves uniformly, and the reconstruction is a bijection, Reduction of the central problem to the effective one-dimensional potential: $μ ρ^{''} = - (U_{J}^{e f f})^{'} (ρ)$ , the energy identity, and the converse reconstruction of the planar trajectory from the radial data): the relative coordinate of the motion and its global extension $r$ are central-force trajectories for $(μ, u)$ with $u (ρ) = - κ / ρ$ , and its $ρ = ∣ r ∣$ solves the one-dimensional problem of mass $μ$ in the potential $U^{e f f}$ : $μ ρ^{''} = - (U^{e f f})^{'} (ρ)$ , with $E = \frac{1}{2} μ (ρ^{'})^{2} + U^{e f f} (ρ)$ constant; moreover $ρ^{2} θ^{'} = J / μ > 0$ for the polar angle $θ$ .

[L2]

Conic geometry (The Kepler orbit equation is a conic: $u = c (1 + e \cos (φ - θ_{0}))$ with $E = (μ κ^{2} / 2 J^{2}) (e^{2} - 1)$ , Completeness and periodicity of the negative-energy Kepler orbit, with $T = 2 π μ a b / J$ and $T^{2} = 4 π^{2} μ a^{3} / κ$ , Kepler's third law for the gravitational two-label model: the relative period is $T = 2 π μ a b / J = 2 π \sqrt{μ / κ} a^{3 / 2}$ , so $T^{2} = 4 π^{2} a^{3} / (G_{N} M)$ under the mass identification, and both labels are periodic relative to the centre of mass, Polar reduction of a non-radial central-force trajectory: $ρ^{2} θ^{'} = J / μ$ , the effective-potential equation and energy conservation): with $e \geq 0$ and $θ_{0}$ as in the cited conic theorem, $ρ (t) = p / (1 + e \cos (θ (t) - θ_{0}))$ and $E = \frac{μ κ^{2}}{2 J^{2}} (e^{2} - 1)$ ; consequently $e < 1$ is equivalent to $E < 0$ , and for $0 < e < 1$ the radial coordinate is $T$ -periodic, $ρ (t + T) = ρ (t)$ and $ρ^{'} (t + T) = ρ^{'} (t)$ , with $T = 2 π \sqrt{μ / κ} a^{3 / 2} = 2 π μ a b / J$ , and the polar angle is a strictly increasing bijection $θ : R \to R$ with $θ (t + T) = θ (t) + 2 π$ .

[L3]

Calculus and integrals (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, For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term, 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 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)$ , The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ , Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on $[a, b]$ takes every value between $f (a)$ and $f (b)$ , Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point, $C^{k}$ Euclidean maps and diffeomorphisms, Derivative of an inverse: if $f$ is continuous and injective on a nondegenerate interval $I$ and differentiable at $c \in I$ with $f^{'} (c) \neq 0$ , then the inverse $g$ is differentiable at $f (c)$ with $g^{'} (f (c)) = 1 / f^{'} (c)$ ; and if $f^{'} (c) = 0$ then $g$ is not differentiable at $f (c)$ , Substitution: if $φ$ is differentiable on $[c, d]$ with $φ^{'}$ integrable and $f$ is continuous on an interval containing $φ ([c, d])$ , then $\int_{φ (c)}^{φ (d)} f = \int_{c}^{d} (f \circ φ) φ^{'}$ , 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, The lower and upper Darboux integrals of a bounded $f$ on $[a, b]$ as $\sup_{P} L (f, P)$ and $\inf_{P} U (f, P)$ , Darboux integrability as their equality, and the notation $\int_{a}^{b} f$ , Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length): sums, quotients with nonzero denominator and powers of class $C^{\infty}$ are $C^{\infty}$ ; the derivative of $ρ \mapsto κ / ρ$ is $- κ / ρ^{2}$ and that of $ρ \mapsto J^{2} / (2 μ ρ^{2})$ is $- J^{2} / (μ ρ^{3})$ ; the mean-value theorem, the intermediate value theorem and the one-variable inverse-function rule hold on intervals; a continuous integrand on a compact interval is Riemann integrable, substitution is available for strictly monotone $C^{1}$ changes of variables, and $\int_{c}^{d} u^{'} = u (d) - u (c)$ for a $C^{1}$ function $u$ on $[c, d]$ .

[L4]

Action-variable theorems (The one-dimensional action variable of a family of two-turning-point energy levels, The action variable of a two-simple-turning-point family is $C^{1}$ with derivative $T (E) / (2 π)$ , the period quadrature over $2 π$ ): for the datum $(J_{0}, U^{e f f}, μ)$ with the two simple turning points $a (E) < b (E)$ on an energy interval $(E_{0}, E_{1})$ and $(U^{e f f})^{'} (a) < 0 < (U^{e f f})^{'} (b)$ , the action variable $J_{a}$ is $C^{1}$ and $J_{a}^{'} (E) = T (E) / (2 π)$ with the displayed quadrature $T (E)$ .

Verification

Proof technique: direct; compute the effective potential's derivative and signs, produce the two simple roots by the intermediate-value and mean-value theorems, apply the one-dimensional action-variable theorem, and identify the time quadrature with the orbital period.

1.1L3algebra

Derivative and critical point: by [L3], $(U^{e f f})^{'} (ρ) = \frac{κ}{ρ^{2}} - \frac{J^{2}}{μ ρ^{3}} = \frac{κ ρ - J^{2} / μ}{ρ^{3}} = \frac{κ (ρ - r_{*})}{ρ^{3}},$ which vanishes exactly at $ρ = r_{*} = J^{2} / (μ κ)$ and has the sign of $ρ - r_{*}$ ; and $U^{e f f} (r_{*}) = - κ μ κ / J^{2} + J^{2} μ^{2} κ^{2} / (2 μ J^{4}) = - μ κ^{2} / (2 J^{2})$ . Also $U^{e f f} (r_{*} / 2) = - 2 μ κ^{2} / J^{2} + 2 μ κ^{2} / J^{2} = 0$ , and for any $E \in I_{0}$ and $R : = r_{*} + κ / ∣ E ∣$ one has $U^{e f f} (R) > - κ / R > - ∣ E ∣ = E$ .

2.1L3step 1.1algebra

Monotonicity and the two simple roots: if $0 < ρ_{1} < ρ_{2} \leq r_{*}$ , then by [L3] the mean-value theorem applied to $U^{e f f}$ on $[ρ_{1}, ρ_{2}]$ gives $U^{e f f} (ρ_{2}) - U^{e f f} (ρ_{1}) = (U^{e f f})^{'} (ξ) (ρ_{2} - ρ_{1}) < 0$ ; hence $U^{e f f}$ is strictly decreasing on $(0, r_{*}]$ . Similarly, on $r_{*} \leq ρ_{1} < ρ_{2}$ , the increment is positive, so $U^{e f f}$ is strictly increasing on $[r_{*}, \infty)$ . Now fix $E \in I_{0}$ . By step 1.1, $U^{e f f} (r_{*}) < E < 0 = U^{e f f} (r_{*} / 2)$ ; since $U^{e f f}$ is continuous, the intermediate-value theorem gives $r_{-} (E) \in (r_{*} / 2, r_{*})$ with $U^{e f f} (r_{-} (E)) = E$ , and strict monotonicity makes it unique on $(0, r_{*}]$ . Likewise $U^{e f f} (r_{*}) < E < U^{e f f} (R)$ gives a unique $r_{+} (E) \in (r_{*}, R)$ with $U^{e f f} (r_{+} (E)) = E$ , and monotonicity makes the root unique on $[r_{*}, \infty)$ . The intermediate values on $(r_{-} (E), r_{+} (E))$ lie below $E$ because the only point where $U^{e f f}$ could reach $E$ again would be a third root. The roots are simple: $(U^{e f f})^{'} (r_{-} (E)) < 0 < (U^{e f f})^{'} (r_{+} (E))$ because $r_{-} (E) < r_{*} < r_{+} (E)$ and the sign computation of step 1.1. The assignments $E \mapsto r_{\pm} (E)$ therefore have the properties required in [L4] on the energy interval $I_{0}$ .

3.1L4step 2.1algebra

Applying the action-variable theorem: by step 2.1 the datum $(J_{0}, U^{e f f}, μ)$ satisfies the hypotheses of [L4] on $I_{0} = (E_{0}, E_{1})$ ; hence $J_{a}$ is $C^{1}$ on $I_{0}$ and $J_{a}^{'} (E) = T_{r a d} (E) / (2 π)$ with the quadrature $T_{r a d} (E) = \sqrt{2 μ} \int_{r_{-} (E)}^{r_{+} (E)} d ρ / \sqrt{E - U^{e f f} (ρ)} > 0$ , which is claim 2.

4.1L1L2L3step 2.1step 3.1algebra

The quadrature measures one radial cycle: for $0 < e < 1$ , choose a periastron time $t_{-}$ of the global extension, and let $t_{+}$ and $t_{1}$ be the unique times with polar-angle increments $π$ and $2 π$ from it, respectively. These exist by the increasing bijection of [L2]. The conic formula of [L2] gives endpoint radii $r_{-} = p / (1 + e)$ , $r_{+} = p / (1 - e)$ , the roots of step 2.1 by the energy identity of [L1], and places $ρ$ strictly between them on each open leg. Energy then makes $ρ^{'}$ nonzero there. At periastron $ρ^{'} = 0$ and $ρ^{''} = - (U^{e f f})^{'} (r_{-}) / μ > 0$ , so continuity makes $ρ^{'} > 0$ immediately afterwards and throughout $(t_{-}, t_{+})$ , since it cannot change sign without vanishing. At apastron $ρ^{''} = - (U^{e f f})^{'} (r_{+}) / μ < 0$ gives $ρ^{'} < 0$ on $(t_{+}, t_{1})$ by the same reasoning. On the increasing leg its inverse $t (ρ)$ is differentiable for $r_{-} < ρ < r_{+}$ , with $t^{'} (ρ) = \sqrt{μ / 2} / \sqrt{E - U^{e f f} (ρ)}$ by [L1] and the inverse rule in [L3]. For $0 < δ < (r_{+} - r_{-}) / 2$ , FTC on the interior compact interval gives $t (r_{+} - δ) - t (r_{-} + δ) = \sqrt{μ / 2} \int_{r_{-} + δ}^{r_{+} - δ} (E - U^{e f f} (ρ))^{- 1 / 2} d ρ$ . Letting $δ ↓ 0$ , continuity of the inverse at its endpoint limits gives $t_{+} - t_{-}$ on the left, and the convergent improper integral of step 3.1 gives the limit on the right. On the decreasing leg the same interior calculation with $t^{'} (ρ) = - \sqrt{μ / 2} / \sqrt{E - U^{e f f} (ρ)}$ gives the identical duration $t_{1} - t_{+}$ . Thus $t_{1} - t_{-} = T_{r a d} (E)$ ; no derivative or compact-interval substitution at a turning endpoint is used.

5.1L2step 3.1step 4.1algebra

Least period and the value of the derivative: by [L2] the radial coordinate satisfies $ρ (t + T) = ρ (t)$ with $T$ the orbital period of the conic data. Since $θ : R \to R$ is a strictly increasing bijection with $θ (t + T) = θ (t) + 2 π$ and $ρ (t) = p / (1 + e \cos (θ (t) - θ_{0}))$ with $0 < e < 1$ , the periastron value $r_{-} (E) = p / (1 + e)$ and the apastron value $r_{+} (E) = p / (1 - e)$ are attained exactly once in every half-open interval of the form $[t_{0}, t_{0} + T)$ . Every positive period must carry a periastron time to another periastron time. The strictly increasing polar angle attains successive periastra at increments of $2 π$ , and $θ (t + T) = θ (t) + 2 π$ shows their successive times differ by $T$ ; hence any positive period is at least $T$ . Since $T$ is a period, it is the least positive radial period. Therefore $T_{r a d} (E) = T$ by step 4.1, and $J_{a}^{'} (E) = \frac{T}{2 π} = \frac{μ a b}{J} = \sqrt{\frac{μ}{κ}} a^{3 / 2},$ where the last identity uses $J = \sqrt{μ κ a (1 - e^{2})}$ and $b = a \sqrt{1 - e^{2}}$ : explicitly $μ a b / J = μ a^{2} \sqrt{1 - e^{2}} / \sqrt{μ κ a (1 - e^{2})} = \sqrt{μ / κ} a^{3 / 2}$ . Squaring $T = 2 π \sqrt{μ / κ} a^{3 / 2}$ returns $T^{2} = 4 π^{2} μ a^{3} / κ$ . This is claim 3.

6.1L2step 2.1step 5.1

Sharpness: if $e = 0$ then $r_{-} (E) = r_{+} (E) = a = r_{*}$ and $E = U^{e f f} (r_{*})$ , the lower endpoint of $I_{0}$ ; there is no energy interval containing this circular energy on which two distinct simple turning points exist, so the hypothesis of [L4] fails, in agreement with the circular orbit having a constant radial coordinate and no radial oscillation. The case $J = 0$ has no term $J^{2} / (2 μ ρ^{2})$ and no critical point with the stated two-sided conservation, so it is outside the example by hypothesis. This is claim 4.

7.1step 1.1step 2.1step 3.1step 4.1step 5.1step 6.1∎

Claims 1-4 are verified by steps 1.1 and 2.1, by step 3.1, by steps 4.1 and 5.1, and by step 6.1 respectively; the example is verified.

Remarks

What is checked and what is cited. The elementary computations (the critical point of the effective potential, the two simple roots, the period quadrature) are verified here; the orbit theory that supplies $ρ (t) = p / (1 + e \cos (θ (t) - θ_{0}))$ , the energy relation $E = μ κ^{2} (e^{2} - 1) / (2 J^{2})$ and the period $T = 2 π \sqrt{μ / κ} a^{3 / 2}$ is cited from the mathematical central-force development collected on the page cm-math-central. The example uses only the model's declared couplings and no measured constant.
Conventions. $J_{a}$ here is the radian action $J_{a} = \frac{1}{2 π} \oint p d q$ of The one-dimensional action variable of a family of two-turning-point energy levels; the corresponding period-one action of Action-angle coordinates of a completely integrable presentation: period-one angles, action coordinates, $H = h (I)$ and linear motion on the tori is its $2 π$ -multiple. The identity $J_{a}^{'} (E) = T / (2 π)$ is the one-dimensional case of the action-period relation used by the action-angle items of this page.

The gravitational two-body model on an elliptic orbit: two simple turning points of the effective potential and $J_{a}^{'} (E) = T / (2 π) = \sqrt{μ / κ} a^{3 / 2}$

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources

The gravitational two-body model on an elliptic orbit: two simple turning points of the effective potential and Ja′(E)=T/(2π)=μ/κ a3/2Ja′​(E)=T/(2π)=μ/κ​a3/2

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources

The gravitational two-body model on an elliptic orbit: two simple turning points of the effective potential and $J_{a}^{'} (E) = T / (2 π) = \sqrt{μ / κ} a^{3 / 2}$