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 rotating hoop: reduced Lagrangian, the equation $θ^{''} = Ω^{2} \sin θ \cos θ - (g / a) \sin θ$ , and the reduced energy versus the inertial mechanical energy

Example

Let $a, m, g > 0$ and $Ω \in R$ , and let

$X : R \times R \to R^{3}, X (θ, t) : = (a \sin θ \cos (Ω t), a \sin θ \sin (Ω t), a (1 - \cos θ)),$

the position of a point of a circle of radius $a$ rotating about the vertical axis with constant angular speed $Ω$ . For an open interval $I$ and a $C^{2}$ curve $θ : I \to R$ put $x (t) : = X (θ (t), t)$ . Stationarity on $I$ means stationarity of the restricted curve on every $[t_{1}, t_{2}] \subseteq I$ with $t_{1} < t_{2}$ , using fixed-endpoint variations. Then:

$\dot{x} = X_{θ} θ^{'} + X_{t}$ and $\frac{1}{2} m ∣ \dot{x} ∣^{2} = \frac{1}{2} m a^{2} (θ^{' 2} + Ω^{2} \sin^{2} θ)$ , while $\ddot{x} \cdot X_{θ} = a^{2} θ^{''} - a^{2} Ω^{2} \sin θ \cos θ$ ;
the curves $θ$ that are stationary for the action of the time-dependent Lagrangian chart $L (θ, v) : = \frac{1}{2} m a^{2} (v^{2} + Ω^{2} \sin^{2} θ) - m g a (1 - \cos θ)$ on $O : = R \times R \times R$ are exactly the $C^{2}$ solutions of

$θ^{''} = Ω^{2} \sin θ \cos θ - \frac{g}{a} \sin θ;$

the reduced energy $E (θ, v) : = \frac{1}{2} m a^{2} v^{2} - \frac{1}{2} m a^{2} Ω^{2} \sin^{2} θ - m g a \cos θ$ is constant along every $C^{2}$ solution, whereas the inertial kinetic-plus-potential energy $K + U_{g} = \frac{1}{2} m ∣ \dot{x} ∣^{2} + m g a (1 - \cos θ)$ satisfies

$\frac{d}{d t} (K + U_{g}) = 2 m a^{2} Ω^{2} \sin θ \cos θ θ^{'} = m a^{2} Ω^{2} \frac{d}{d t} \sin^{2} θ$

along every solution, and equals $E + m a^{2} Ω^{2} \sin^{2} θ + m g a$ ; it is therefore in general not conserved, and it differs from $E$ by $m a^{2} Ω^{2} \sin^{2} θ + m g a$ ; 4. if the ambient motion is additionally modelled by $m \ddot{x} = (0, 0, - m g) + R$ with an ideal reaction satisfying $R (t) \cdot X_{θ} (θ (t), t) = 0$ , then the same equation of part 2 holds, and the reaction power is

$R \cdot \dot{x} = \frac{d}{d t} (K + U_{g}) = 2 m a^{2} Ω^{2} \sin θ \cos θ θ^{'},$

generally nonzero: the prescribed rotation can do work on the point; 5. if $a Ω^{2} \leq g$ , then $0$ is a strict local minimum of $U_{e f f} (θ) : = - \frac{1}{2} m a^{2} Ω^{2} \sin^{2} θ - m g a \cos θ$ with $U_{e f f}^{'} (0) = 0$ , and the equilibrium $(0, 0)$ of $θ^{'} = v, v^{'} = Ω^{2} \sin θ \cos θ - (g / a) \sin θ$ is Lyapunov stable; if $a Ω^{2} > g$ , then $0$ is not a local minimum of $U_{e f f}$ and the stability criterion does not apply.

Facts & Assumptions

Given: The constants $a, m, g > 0$ and $Ω \in R$ , the map $X$ displayed in the Example, an open interval $I$ (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length) and a $C^{2}$ curve $θ : I \to R$ with $x : = X (θ (\cdot), \cdot)$ ; the Lagrangian $L$ and the reduced potential $U_{e f f}$ of the Example.

[F1]

Derivatives and inner products of the carrier (The derivatives of sine and cosine are cosine and minus sine, Sine and cosine defined by their real power series, Parity and the Pythagorean identity for sine and cosine, The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ , 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 Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral, $C^{k}$ Euclidean maps and diffeomorphisms): $X$ is $C^{\infty}$ , and with $c : = \cos (Ω t)$ , $s : = \sin (Ω t)$ , $X_{θ} = (a \cos θ c, a \cos θ s, a \sin θ), X_{t} = (- a Ω \sin θ s, a Ω \sin θ c, 0),$ $X_{θ θ} = (- a \sin θ c, - a \sin θ s, a \cos θ), X_{θ t} = (- a Ω \cos θ s, a Ω \cos θ c, 0), X_{t t} = (- a Ω^{2} \sin θ c, - a Ω^{2} \sin θ s, 0),$ and the six identities $∣ X_{θ} ∣^{2} = a^{2}, ∣ X_{t} ∣^{2} = a^{2} Ω^{2} \sin^{2} θ, X_{θ} \cdot X_{t} = 0,$ $X_{θ} \cdot X_{θ θ} = 0, X_{θ} \cdot X_{θ t} = 0, X_{θ} \cdot X_{t t} = - a^{2} Ω^{2} \sin θ \cos θ$ hold; each is expansion of the displayed components together with $\cos^{2} + \sin^{2} = 1$ .

[F2]

Chain rule along the curve (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ): if $x (t) = X (θ (t), t)$ with $θ$ of class $C^{2}$ , then $\dot{x} = X_{θ} θ^{'} + X_{t}$ and $\ddot{x} = X_{θ θ} θ^{' 2} + 2 X_{θ t} θ^{'} + X_{t t} + X_{θ} θ^{''}$ , all derivatives being evaluated at $(θ (t), t)$ .

[F3]

The chart and its Euler–Lagrange expression (A time-dependent Lagrangian chart, its action functional and its fixed-endpoint first variations): $L$ is $C^{\infty}$ on $O = R \times R \times R$ , so $(O, L)$ is a time-dependent Lagrangian chart over every $[t_{1}, t_{2}] \times R$ ; its gradients are $L_{θ} = m a^{2} Ω^{2} \sin θ \cos θ - m g a \sin θ$ , $L_{v} = m a^{2} v$ , and its Euler–Lagrange expression along a $C^{2}$ curve is $E_{L} (θ) = m a^{2} Ω^{2} \sin θ \cos θ - m g a \sin θ - m a^{2} θ^{''}$ . By Stationarity of the time-dependent action is equivalent to the vanishing of the Euler-Lagrange expression a $C^{2}$ curve is stationary for the action if and only if $E_{L} (θ) = 0$ .

[F4]

Calculus rules for the energy: sums and products of differentiable functions are differentiable (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$ ), and a differentiable function on an interval whose derivative vanishes identically is constant (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, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[F5]

Ideal reactions (A regular holonomic constraint, its virtual displacements and the ideal-reaction law): a reaction that performs no virtual work on the moving constraint satisfies $R (t) \cdot δ x = 0$ for every fixed-time virtual displacement; for the circle at time $t$ the virtual displacements are the multiples of $X_{θ} (θ (t), t)$ , so the hypothesis used below is $R \cdot X_{θ} = 0$ .

[F6]

The batch-3 energy-stability theorem (A strict local minimum of the potential gives a Lyapunov stable equilibrium of the mechanical system, by energy conservation, The mechanical first-order field, Lagrangian and energy of a configuration-dependent kinetic metric in a chart): for a $C^{2}$ potential $U : R \to R$ and $q_{0}$ with $U^{'} (q_{0}) = 0$ a strict local minimum of $U$ , the equilibrium $(q_{0}, 0)$ of $q^{'} = v$ , $v^{'} = - U^{'} (q) / M_{0}$ with the constant $M_{0} = m a^{2} > 0$ is Lyapunov stable.

Verification

technique · direct; compute the kinematics of the carrier, identify the reduced Lagrangian and its Euler–Lagrange equation, differentiate the two energies along solutions, and contract the ambient equation with the tangent vector for the reaction power

1.1F1F2algebra

By [F2] and [F1], $\dot{x} = X_{θ} θ^{'} + X_{t}$ and $∣ \dot{x} ∣^{2} = ∣ X_{θ} ∣^{2} θ^{' 2} + 2 θ^{'} X_{θ} \cdot X_{t} + ∣ X_{t} ∣^{2} = a^{2} θ^{' 2} + a^{2} Ω^{2} \sin^{2} θ,$ which gives the velocity formula of part 1.

1.2F1F2algebra

By [F2] and [F1], $\ddot{x} \cdot X_{θ} = θ^{''} ∣ X_{θ} ∣^{2} + 2 θ^{'} X_{θ t} \cdot X_{θ} + θ^{' 2} X_{θ θ} \cdot X_{θ} + X_{t t} \cdot X_{θ} = a^{2} θ^{''} - a^{2} Ω^{2} \sin θ \cos θ,$ which is the acceleration formula of part 1.

1.3F3algebra

By [F3], $E_{L} (θ) = m a^{2} Ω^{2} \sin θ \cos θ - m g a \sin θ - m a^{2} θ^{''}$ , so $E_{L} (θ) = 0$ if and only if $m a^{2} θ^{''} = m a^{2} Ω^{2} \sin θ \cos θ - m g a \sin θ$ , that is, if and only if $θ^{''} = Ω^{2} \sin θ \cos θ - (g / a) \sin θ$ ; by the equivalence of [F3] the stationary curves are exactly the $C^{2}$ solutions, which is part 2.

2.1F4step 1.3algebra

Let $θ$ be a $C^{2}$ solution. By [F4] the function $t \mapsto E (θ (t), θ^{'} (t))$ is differentiable on $I$ with $\frac{d}{d t} E (θ, θ^{'}) = m a^{2} θ^{'} θ^{''} - m a^{2} Ω^{2} \sin θ \cos θ θ^{'} + m g a \sin θ θ^{'} = θ^{'} (m a^{2} θ^{''} - m a^{2} Ω^{2} \sin θ \cos θ + m g a \sin θ) = 0$ by step 1.3; hence $E (θ, θ^{'})$ is constant on $I$ by [F4]. This is the first assertion of part 3.

2.2F1F5step 1.2algebra

Assume now the ambient model $m \ddot{x} = (0, 0, - m g) + R$ with $R \cdot X_{θ} = 0$ as in [F5]. Contracting with $X_{θ}$ kills $R$ , and $(0, 0, - m g) \cdot X_{θ} = - m g a \sin θ$ by [F1]; by step 1.2, $m (a^{2} θ^{''} - a^{2} Ω^{2} \sin θ \cos θ) = - m g a \sin θ,$ i.e. $θ^{''} = Ω^{2} \sin θ \cos θ - (g / a) \sin θ$ after division by $m a^{2} > 0$ . This is the first assertion of part 4.

2.3F1F6step 1.3algebra

Part 5: $U_{e f f}^{'} (θ) = - m a^{2} Ω^{2} \sin θ \cos θ + m g a \sin θ$ , so $U_{e f f}^{'} (0) = 0$ , and the mechanical system of [F6] with $M_{0} = m a^{2}$ and this potential is exactly $θ^{'} = v$ , $v^{'} = Ω^{2} \sin θ \cos θ - (g / a) \sin θ$ ; moreover the exact factorization $U_{e f f} (θ) - U_{e f f} (0) = m g a (1 - \cos θ) - \frac{1}{2} m a^{2} Ω^{2} \sin^{2} θ = m a (1 - \cos θ) [g - \frac{1}{2} a Ω^{2} (1 + \cos θ)]$ together with $\cos θ \leq 1$ and $1 - \cos θ = 2 \sin^{2} (θ / 2)$ (The addition formulas for sine and cosine), which with The zero sets of sine and cosine and the least positive common period 2 pi gives $\cos θ = 1 ⟺ θ \in 2 π Z$ shows that for $a Ω^{2} \leq g$ one has $U_{e f f} (θ) > U_{e f f} (0)$ for $0 < ∣ θ ∣ < 2 π$ : the product is nonnegative and the bracket is at least $g - a Ω^{2} \geq 0$ , vanishing only if $g = a Ω^{2}$ and $\cos θ = 1$ . Hence $0$ is a strict local minimum of $U_{e f f}$ , and [F6] makes $(0, 0)$ Lyapunov stable. If $a Ω^{2} > g$ , the bracket is negative for $∣ θ ∣$ small (continuity at $θ = 0$ , where it equals $g - a Ω^{2}$ ), while $1 - \cos θ > 0$ for small nonzero $θ$ , so $U_{e f f} (θ) < U_{e f f} (0)$ there and $0$ is not a local minimum; [F6] gives no conclusion in that case.

3.1F1F4step 1.1step 2.1algebra

By steps 1.1 and 2.1, $K + U_{g} = \frac{1}{2} m a^{2} (θ^{' 2} + Ω^{2} \sin^{2} θ) + m g a (1 - \cos θ) = E (θ, θ^{'}) + m a^{2} Ω^{2} \sin^{2} θ + m g a$ ; along a solution, by [F4] and step 1.3, $\frac{d}{d t} (K + U_{g}) = \frac{d}{d t} (m a^{2} Ω^{2} \sin^{2} θ) = 2 m a^{2} Ω^{2} \sin θ \cos θ θ^{'} .$ The phase field $(θ, v) \mapsto (v, Ω^{2} \sin θ \cos θ - (g / a) \sin θ)$ is $C^{1}$ on $R^{2}$ , hence locally Lipschitz (A $C^{1}$ map is locally Lipschitz on compact coordinate subsets); Picard-Lindelöf local existence and uniqueness for first-order systems supplies a solution through $(π / 4, 1)$ . If $Ω \neq 0$ the displayed derivative is nonzero at the initial time of this solution, where it equals $m a^{2} Ω^{2}$ , so $K + U_{g}$ is not conserved along all solutions; as functions on the full phase space, $K + U_{g}$ agrees with $E$ up to the constant $m g a$ precisely when the term $m a^{2} Ω^{2} \sin^{2} θ$ is absent, i.e. when $Ω = 0$ . This is the second assertion of part 3.

4.1F1F2F4F5step 3.1step 2.2algebra

Under the hypotheses of step 2.2, $K + U_{g}$ has derivative $m \ddot{x} \cdot \dot{x} + m g a \sin θ θ^{'}$ by [F4], and $\dot{z} = a \sin θ θ^{'}$ for the third coordinate $z = a (1 - \cos θ)$ of $x$ ; substituting $m \ddot{x} = (0, 0, - m g) + R$ gives $m \ddot{x} \cdot \dot{x} = - m g \dot{z} + R \cdot \dot{x}$ , so $\frac{d}{d t} (K + U_{g}) = R \cdot \dot{x} - m g \dot{z} + m g a \sin θ θ^{'} = R \cdot \dot{x} .$ Since $\dot{x} = X_{θ} θ^{'} + X_{t}$ and $R \cdot X_{θ} = 0$ , also $R \cdot \dot{x} = R \cdot X_{t}$ ; by step 3.1 the common value is $2 m a^{2} Ω^{2} \sin θ \cos θ θ^{'}$ , generally nonzero. This is the second assertion of part 4.

5.1step 1.1step 1.2step 1.3step 2.1step 3.1step 2.2step 4.1step 2.3∎

Parts 1-5 are proved.

Remarks

The reduced energy is Jacobi's generalized energy of the chart: $E = v L_{v} - L$ with the additive constant $m g a$ dropped. Since $L$ does not depend on $t$ , $E$ is conserved; the inertial energy $K + U_{g}$ instead contains the term $m a^{2} Ω^{2} \sin^{2} θ$ of the prescribed rotation and is not conserved. This is the mechanism of the rheonomic constraint of The ideal holonomic system in a possibly time-dependent chart: explicit acceleration, constraint preservation, local existence and reaction power, whose reaction power $R \cdot q^{'} = - Λ \cdot G_{t}$ need not vanish; part 4 computes that power directly for this carrier.
The model is the ideal frictionless threading of a point on a circle rotating with prescribed constant angular speed; the reaction $R$ and the power identity are properties of that ideal model. Statements about a real hoop (friction, forcing torque, deformations, measured frequencies) require apparatus and empirical assumptions that are not part of this item.
The stability clause is Lyapunov stability of the equilibrium of the exact reduced equation on the chart $R$ ; no asymptotic stability, and no analysis of the supercritical equilibria $\cos θ = g / (a Ω^{2})$ or of the inverted point, is asserted.

The rotating hoop: reduced Lagrangian, the equation $θ^{''} = Ω^{2} \sin θ \cos θ - (g / a) \sin θ$ , and the reduced energy versus the inertial mechanical energy

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources

The rotating hoop: reduced Lagrangian, the equation θ′′=Ω2sin⁡θcos⁡θ−(g/a)sin⁡θθ′′=Ω2sinθcosθ−(g/a)sinθ, and the reduced energy versus the inertial mechanical energy

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources

The rotating hoop: reduced Lagrangian, the equation $θ^{''} = Ω^{2} \sin θ \cos θ - (g / a) \sin θ$ , and the reduced energy versus the inertial mechanical energy