ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-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.

An exact Kepler ellipse check: $e = 1 / 2$ , $J = 1$ , $μ = κ = 1$ give $a = 4 / 3$ , $b = 2 \sqrt{3} / 3$ , $E = - 3 / 8$ and $T^{2} = 256 π^{2} / 27$

Example

Assume ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )), as required by the ellipse-area and period suppliers; the conic-and-eccentricity theorem does not impose this hypothesis.

Take the attractive Kepler data $μ = κ = 1$ and angular momentum magnitude $J = 1$ , and consider the negative-energy orbit with eccentricity $e = \frac{1}{2}$ . Then the conic data of The Kepler orbit equation is a conic: $u = c (1 + e \cos (φ - θ_{0}))$ with $E = (μ κ^{2} / 2 J^{2}) (e^{2} - 1)$ and The subcritical Kepler conic is an ellipse with semiaxes $a = p / (1 - e^{2})$ , $b = a \sqrt{1 - e^{2}}$ , focus at the origin and area $π a b$ ; its area is also $\frac{1}{2} \int_{0}^{2 π} ϱ^{2}$ are $p = \frac{J^{2}}{μ κ} = 1, a = \frac{p}{1 - e^{2}} = \frac{4}{3}, b = a \sqrt{1 - e^{2}} = \frac{2 \sqrt{3}}{3},$ the energy is $E = \frac{μ κ^{2}}{2 J^{2}} (e^{2} - 1) = - \frac{3}{8}$ , and the period of Completeness and periodicity of the negative-energy Kepler orbit, with $T = 2 π μ a b / J$ and $T^{2} = 4 π^{2} μ a^{3} / κ$ satisfies $T = \frac{2 π μ a b}{J} = \frac{16 π \sqrt{3}}{9}, T^{2} = \frac{256 π^{2}}{27} = \frac{4 π^{2} μ a^{3}}{κ} .$ All numbers are exact; the example checks algebraic consistency of the three theorems and the sign criterion $E < 0 ⟺ e < 1$ , and makes no empirical claim.

Facts & Assumptions

Given: Assume ${A C}_{ω}$ . $μ = κ = 1$ , $J = 1$ , $e = \frac{1}{2}$ and the derived constants $p = 1$ , $a = \frac{4}{3}$ , $b = \frac{2 \sqrt{3}}{3}$ .

[L1]

Conic and eccentricity: for a non-radial attractive Kepler trajectory with $E < 0$ , $p = J^{2} / (μ κ)$ , $a = p / (1 - e^{2})$ , $b = a \sqrt{1 - e^{2}}$ and $E = (μ κ^{2} / 2 J^{2}) (e^{2} - 1)$ (The Kepler orbit equation is a conic: $u = c (1 + e \cos (φ - θ_{0}))$ with $E = (μ κ^{2} / 2 J^{2}) (e^{2} - 1)$ , The subcritical Kepler conic is an ellipse with semiaxes $a = p / (1 - e^{2})$ , $b = a \sqrt{1 - e^{2}}$ , focus at the origin and area $π a b$ ; its area is also $\frac{1}{2} \int_{0}^{2 π} ϱ^{2}$ , Central-force trajectories: the central-force equation, angular momentum, energy and the effective potential).

[L2]

Period: $T = 2 π μ a b / J$ and $T^{2} = 4 π^{2} μ a^{3} / κ$ (Completeness and periodicity of the negative-energy Kepler orbit, with $T = 2 π μ a b / J$ and $T^{2} = 4 π^{2} μ a^{3} / κ$ ).

[L3]

Square roots: $\sqrt{1 - \frac{1}{4}} = \frac{\sqrt{3}}{2}$ and $(\sqrt{3})^{2} = 3$ (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ); $\cos^{2} + \sin^{2} = 1$ provides the value $\sqrt{1 - e^{2}}$ used below via $1 - e^{2} > 0$ (Parity and the Pythagorean identity for sine and cosine).

Verification

technique · direct

1.1givenL1L3algebra

With $μ = κ = J = 1$ : $p = 1$ , $1 - e^{2} = \frac{3}{4}$ , $a = 1 / (\frac{3}{4}) = \frac{4}{3}$ , $\sqrt{1 - e^{2}} = \frac{\sqrt{3}}{2}$ and $b = \frac{4}{3} \cdot \frac{\sqrt{3}}{2} = \frac{2 \sqrt{3}}{3}$ .

1.2givenL1algebra

Energy: $e^{2} - 1 = \frac{1}{4} - 1 = - \frac{3}{4}$ , so $E = \frac{1 \cdot 1}{2 \cdot 1} \cdot (- \frac{3}{4}) = - \frac{3}{8} < 0$ , consistent with $e = \frac{1}{2} < 1$ by the equivalence of [L1].

2.1step 1.1L2algebra

Period: $μ a b = \frac{4}{3} \cdot \frac{2 \sqrt{3}}{3} = \frac{8 \sqrt{3}}{9}$ , so $T = 2 π \cdot \frac{8 \sqrt{3}}{9} = \frac{16 π \sqrt{3}}{9}$ ; squaring, $T^{2} = \frac{256 π^{2} \cdot 3}{81} = \frac{256 π^{2}}{27}$ .

3.1step 1.1step 2.1L2algebra∎

Independent check of the second period formula: $a^{3} = \frac{64}{27}$ , so $4 π^{2} μ a^{3} / κ = 4 π^{2} \cdot \frac{64}{27} = \frac{256 π^{2}}{27} = T^{2}$ , in agreement with step 2.1 and with [L2].

Depends on

Dependency tree · 2 levels

Sources

Konstantin Likharev, Essential Graduate Physics: Classical Mechanics, §3.4, Eqs. (3.59)-(3.65): the eccentricity, semimajor axis and period relations checked numerically here with exact rational data

An exact Kepler ellipse check: e=1/2e=1/2, J=1J=1, μ=κ=1μ=κ=1 give a=4/3a=4/3, b=23/3b=23​/3, E=−3/8E=−3/8 and T2=256π2/27T2=256π2/27