ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck 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.

A bead on a uniformly rotating straight wire: the rheonomic ideal constraint, its reaction, and the work it performs

Physical scope

A worked model check of the rheonomic ideal-constraint branch: one label of mass m constrained without friction to a straight wire through the origin that rotates uniformly in a horizontal plane, under the declared uniform downward field; the verification exhibits the unique maximal constrained motion through consistent data, computes the multiplier and the reaction, verifies the reaction-power identity and the mechanical-energy balance, and shows on explicit model data that an ideal rheonomic constraint performs positive work. The example is a model computation with declared idealizations (frictionless bead, massless rigid wire, prescribed uniform rotation, uniform field with the wire supporting the weight); every number is a model value, not a measurement.

Example

Declare a one-label model of the force branch of Adopted force model: force maps, the equation of motion, additive composition of force contributions and frame covariance with $N = 1$ , mass $m > 0$ , time window $I_{0} = R$ , configuration domain $Q = R^{3}$ and force map $F : I_{0} \times Q \times R^{3} ⟶ R^{3}, F (t, x, v) : = (0, 0, - m g),$ where $[m] = μ$ and $g > 0$ has dimension $ℓ τ^{- 2}$ (the uniform downward field; conventions of Dimensions and SI unit conventions of the non-relativistic classical mechanics framework). Constrain the label, without friction, to the straight wire through the origin that rotates in the plane $z = 0$ about the $z$ -axis with constant angular speed $Ω > 0$ , and to that plane, by the regular holonomic-constraint datum $O : = R \times R^{3}, k : = 2, G (t, x, y, z) : = (- x \sin Ω t + y \cos Ω t, z)$ of Holonomic-constraint models of the force branch: constraint data, the constrained equation, virtual displacements and the scleronomic/rheonomic distinction, and adopt the ideal-reaction law of Adopted ideal-reaction law for holonomic constraints: the d'Alembert condition, its scope and its limits. Both components of $G$ have length dimension $ℓ$ , and $[Ω] = τ^{- 1}$ .

Let $r_{0} > 0$ be a length and $u_{0} \in R$ the initial radial speed, with $[r_{0}] = ℓ$ and $[u_{0}] = ℓ τ^{- 1}$ . The initial data are $t_{0} : = 0, x_{0} : = (r_{0}, 0, 0), v_{0} : = (u_{0}, Ω r_{0}, 0) .$ Then the constrained model with these data has the unique maximal constrained motion $r (t) : = A e^{Ω t} + B e^{- Ω t}, A : = \frac{r_{0} + u_{0} / Ω}{2}, B : = \frac{r_{0} - u_{0} / Ω}{2}, x (t) : = r (t) (\cos Ω t, \sin Ω t, 0),$ defined for all $t \in R$ , with multiplier, reaction and reaction power $λ (t) = (2 m Ω r^{'} (t), m g), R (t) = 2 m Ω r^{'} (t) (- \sin Ω t, \cos Ω t, 0) + m g e_{3}, R (t) \cdot x^{'} (t) = 2 m Ω^{2} r (t) r^{'} (t),$ kinetic energy $K (t) = \frac{1}{2} m (r^{'} (t)^{2} + Ω^{2} r (t)^{2})$ and mechanical energy $E (t) = K (t) + m g z (t) = K (t)$ satisfying $E^{'} (t) = R (t) \cdot x^{'} (t) = - λ (t) \cdot G_{t} (t, x (t)) = 2 m Ω^{2} r (t) r^{'} (t)$ ; the constraint is rheonomic, and the scleronomic conservation clause does not apply. On the explicit model data $m = 1 k g, Ω = 2 s^{- 1}, r_{0} = 1 m, u_{0} = 0 m s^{- 1}, g = 10 m s^{- 2}$ one has $r (t) = (e^{2 t} + e^{- 2 t}) / 2 m$ , $E (t) = e^{4 t} + e^{- 4 t} J$ and $E^{'} (t) = 4 (e^{4 t} - e^{- 4 t}) W$ ; at $t = \frac{1}{2} s$ , $E = (e^{2} + e^{- 2}) J \approx 7.524391 J$ and $E^{'} = 4 (e^{2} - e^{- 2}) W \approx 29.014883 W$ , so the mechanical energy has strictly increased from its initial value $E (0) = 2 J$ by the work of the ideal reaction. All values are model values under the declared idealizations, not measurements.

Facts & Assumptions

Given: The constants $m, g, Ω, r_{0} > 0$ , the scalar initial radial speed $u_{0} \in R$ , the vector initial velocity $v_{0} = (u_{0}, Ω r_{0}, 0)$ , the model data of the Example, the datum $(O, 2, G)$ , and the curve $x (t) = r (t) (\cos Ω t, \sin Ω t, 0)$ with $r$ as displayed.

[F1]

The force branch and the mass operator: $F : I_{0} \times Q \times R^{3} \to R^{3}$ is the constant map $F (t, x, v) = (0, 0, - m g)$ , hence continuous, state-Lipschitz and of class $C^{1}$ ; the mass operator is $M = m I_{3}$ , symmetric positive definite (Adopted force model: force maps, the equation of motion, additive composition of force contributions and frame covariance, Configuration domain of $N$ labeled particles: open admissible sets, regular holonomic constraints and the mass operator).

[F2]

The holonomic-constraint branch (Holonomic-constraint models of the force branch: constraint data, the constrained equation, virtual displacements and the scleronomic/rheonomic distinction): $G$ is of class $C^{2}$ with $D_{x} G$ of rank $k$ on $Σ$ ; virtual displacements are $\ker D_{x} G (t, x)$ ; the datum is scleronomic exactly when there is $N \subseteq R^{3 N}$ with $Σ = {(t, x) \in O : x \in N}$ , equivalently when $(t, x) \in Σ$ and $(t^{'}, x) \in O$ always imply $(t^{'}, x) \in Σ$ , and then $G_{t} = 0$ on $Σ$ ; a constrained motion satisfies $M x^{''} = F + R$ with a continuous $R$ .

[F3]

The ideal-reaction law and the balance theorem (Adopted ideal-reaction law for holonomic constraints: the d'Alembert condition, its scope and its limits, Ideal holonomic constraints determine the reaction: multiplier form, explicit acceleration, unique constrained motions and the reaction-power identity): along an ideal motion $R = D_{x} G^{T} λ$ with the unique continuous multiplier; with $C = D_{x} G M^{- 1} D_{x} G^{T}$ and $Λ$ of that theorem, the multiplier of a constrained motion is $Λ (t, x, x^{'})$ and the constrained motions with consistent data are precisely the solutions of the resulting first-order system, which has a unique maximal solution through each consistent datum.

[F4]

The rheonomic-power theorem (Reaction work and mechanical-energy balance for ideal holonomic constraints: vanishing power for scleronomic constraints and the rheonomic work term): $R \cdot x^{'} = - λ \cdot G_{t}$ , and for a potential presentation $F_{i} = - \nabla_{x_{i}} U + d_{i}$ , $E^{'} = \partial_{t} U + \sum_{i} ⟨ d_{i}, w_{i} ⟩ - λ \cdot G_{t}$ .

[F5]

Trigonometric and exponential calculus: the derivatives of sine and cosine, the identity $\sin^{2} + \cos^{2} = 1$ , the derivative of the exponential, the chain rule, the algebra of derivatives, and the elementary antiderivative facts used for the explicit solution (Sine and cosine defined by their real power series, The derivatives of sine and cosine are cosine and minus sine, Parity and the Pythagorean identity for sine and cosine, The real exponential function and the number $e$ by a power series, The exponential function is smooth and $(\exp)^{'} = \exp$ , 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 derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral).

[F6]

Kinetic and mechanical energy of a one-label curve family and the potential presentation $U (t, x, y, z) = m g z$ , $d \equiv 0$ (Total mass, total momentum, centre of mass, angular momentum, torque, kinetic energy, power and work of a particle model in an inertial frame clauses (b),(d), Potential presentations of a force model, potential and mechanical energy, closed versus exact force fields, local potentials and equipotential level sets clauses (a),(b)); the Euclidean pairing (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ); intervals and constants (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length, 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).

Verification

technique · direct; verify the constraint, the consistency of the data and the equation of motion on the explicit curve, then identify the multiplier, the reaction power and the energy balance, and evaluate the finite model data

1.1F1F2F5algebra

The datum is a regular holonomic-constraint datum with $k = 2 = 3 N - 1$ : $G$ is smooth, and its Jacobian is the constant-rank matrix $D_{x} G (t, x, y, z) = (\begin{array}{ccc} - \sin Ω t & \cos Ω t & 0 \\ 0 & 0 & 1 \end{array});$ the two rows are independent for every $t$ because a combination $a (- \sin Ω t, \cos Ω t, 0) + b (0, 0, 1) = (0, 0, 0)$ has $b = 0$ from the third entry and then $a = 0$ from the first two entries, since $(- \sin Ω t, \cos Ω t) \neq (0, 0)$ by [F5]. The locus is $Σ = {(t, r \cos Ω t, r \sin Ω t, 0) : t, r \in R}$ , nonempty and contained in $I_{0} \times Q$ , and the virtual displacements at $(t, x)$ are the one-dimensional space $R (\cos Ω t, \sin Ω t, 0)$ because $δ \in \ker D_{x} G$ means $δ_{z} = 0$ and $- δ_{x} \sin Ω t + δ_{y} \cos Ω t = 0$ . Finally the datum is not scleronomic: $(0, (1, 0, 0)) \in Σ$ because $G (0, 1, 0, 0) = (0, 0)$ , while for $t_{1} : = π / (2 Ω)$ one has $G_{1} (t_{1}, 1, 0, 0) = - \sin (π / 2) = - 1 \neq 0$ , so $(t_{1}, (1, 0, 0)) \in O = R \times R^{3}$ but $(t_{1}, (1, 0, 0)) \notin Σ$ ; by the membership form of [F2] the datum is rheonomic.

1.2F2givenalgebra

Consistency of the data: $G (0, x_{0}) = (0, 0)$ and, with the declared vector $v_{0} = (u_{0}, Ω r_{0}, 0)$ , $G_{t} (0, x_{0}) + D_{x} G (0, x_{0}) v_{0} = (- Ω r_{0}, 0) + (Ω r_{0}, 0) = (0, 0) .$ Thus $(0, x_{0}, v_{0})$ is consistent.

2.1F1F2F3F5step 1.1algebra

The curve $x$ is a constrained motion with the stated multiplier: for $r (t) = A e^{Ω t} + B e^{- Ω t}$ one has $r^{''} = Ω^{2} r$ by [F5], and the displayed $x$ is $C^{\infty}$ with $x^{'} = r^{'} (\cos Ω t, \sin Ω t, 0) + r Ω (- \sin Ω t, \cos Ω t, 0), x^{''} = (r^{''} - Ω^{2} r) (\cos Ω t, \sin Ω t, 0) + 2 Ω r^{'} (- \sin Ω t, \cos Ω t, 0) = 2 Ω r^{'} (- \sin Ω t, \cos Ω t, 0) .$ Moreover $G (t, x (t)) = (- r \cos Ω t \sin Ω t + r \sin Ω t \cos Ω t, 0) = (0, 0)$ , and $G_{t} (t, x (t)) + D_{x} G (t, x (t)) x^{'} (t) = (- Ω r, 0) + (r Ω, 0) = (0, 0)$ , so $x$ is a constrained curve family with permitted velocity. With $λ (t) : = (2 m Ω r^{'} (t), m g)$ , the reaction $R : = D_{x} G^{T} λ$ is $2 m Ω r^{'} (- \sin Ω t, \cos Ω t, 0) + m g e_{3}$ , and $F + D_{x} G^{T} λ = (0, 0, - m g) + 2 m Ω r^{'} (- \sin Ω t, \cos Ω t, 0) + (0, 0, m g) = m (2 Ω r^{'} (- \sin Ω t, \cos Ω t, 0)) = m x^{''} = M x^{''}$ ; since $R = D_{x} G^{T} λ$ annihilates $\ker D_{x} G$ by [F3], the reaction is ideal and $x$ is a constrained motion of the model with reaction $R$ .

3.1F1F3step 1.1step 1.2step 2.1algebra

The multiplier of step 2.1 is the multiplier $Λ$ of the balance theorem and the motion is the unique maximal one: here $C = D_{x} G M^{- 1} D_{x} G^{T} = (1 / m) I_{2}$ because the two rows of $D_{x} G$ are orthonormal, $D_{x} G M^{- 1} F = (1 / m) (0, - m g) = (0, - g)$ , $G_{t t} = (- Ω^{2} G_{1}, 0) = (0, 0)$ along the motion, $2 G_{t q} [x^{'}] = (- 2 Ω (\cos Ω t x_{1}^{'} + \sin Ω t x_{2}^{'}), 0) = (- 2 Ω r^{'}, 0)$ and $G_{q q} [x^{'}, x^{'}] = 0$ ; hence $Λ = - C^{- 1} [(0, - g) + 0 + (- 2 Ω r^{'}, 0) + 0] = (2 m Ω r^{'}, m g) = λ$ , so by [F3] clause 1 the multiplier of the motion is exactly $λ$ . Here $O^{'} = O = I_{0} \times Q$ , $G$ is smooth with rank $2$ throughout $O$ by step 1.1, and $F$ is $C^{1}$ by [F1], so all hypotheses of [F3] hold. The data of step 1.2 are consistent, the curve solves its first-order system, and a solution defined on all of $R$ is the maximal solution through its datum by uniqueness.

4.1F4F5F6step 1.1step 3.1algebra

Reaction power and energy balance: on the motion, $e_{3} \cdot x^{'} = 0$ and $(- \sin Ω t, \cos Ω t, 0) \cdot x^{'} = r Ω$ , so $R \cdot x^{'} = 2 m Ω r^{'} \cdot r Ω = 2 m Ω^{2} r r^{'}$ , and $G_{t} (t, x (t)) = (- Ω r, 0)$ gives $- λ \cdot G_{t} = - (2 m Ω r^{'}) (- Ω r) = 2 m Ω^{2} r r^{'}$ , in agreement with [F4] clause 1. Since $F = - \nabla U$ for $U (t, x, y, z) = m g z$ with residual forces zero and $\partial_{t} U = 0$ , [F4] clause 2 gives $E^{'} = \partial_{t} U - λ \cdot G_{t} = 2 m Ω^{2} r r^{'}$ . Independently $K^{'} = m (r^{'} r^{''} + Ω^{2} r r^{'}) = m (Ω^{2} r r^{'} + Ω^{2} r r^{'}) = 2 m Ω^{2} r r^{'}$ by [F5], and $z \equiv 0$ , so $E^{'} = K^{'} = R \cdot x^{'}$ . Because the datum is rheonomic (step 1.1), clause 3 of [F4] is not available and the mechanical energy is not asserted constant.

5.1F5F6step 4.1algebra

Finite model data: with $m = 1$ , $Ω = 2$ , $r_{0} = 1$ and $u_{0} = 0$ one has $A = B = \frac{1}{2}$ , so $r (t) = (e^{2 t} + e^{- 2 t}) / 2$ , $r^{'} (t) = (e^{2 t} - e^{- 2 t})$ , $K (t) = \frac{1}{2} (r^{' 2} + 4 r^{2}) = e^{4 t} + e^{- 4 t}$ and $E (t) = K (t) J$ because $z (t) = 0$ ; then $E^{'} (t) = 4 (e^{4 t} - e^{- 4 t}) W$ , while the reaction power at the same time is $2 m Ω^{2} r r^{'} = 8 r (t) r^{'} (t) = \frac{1}{2} \cdot 8 (e^{2 t} + e^{- 2 t}) (e^{2 t} - e^{- 2 t}) = 4 (e^{4 t} - e^{- 4 t})$ , and the two agree. At $t = \frac{1}{2} s$ the values are $E = (e^{2} + e^{- 2}) \approx 7.524391 J$ , $E^{'} = 4 (e^{2} - e^{- 2}) \approx 29.014883 W > 0$ , and $E (0) = 2 J$ ; the energy has increased by the work of the ideal reaction.

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

Clauses (1)-(4) of the Example are proved: the datum is regular and rheonomic, the data are consistent, the displayed curve is the unique maximal constrained motion with the stated multiplier and reaction, the reaction power is $2 m Ω^{2} r r^{'}$ , the mechanical-energy balance holds with the rheonomic term and no other contribution, and the finite model data exhibit a strict energy increase. The construction is an idealization of a bead threaded on a smooth rigid wire whose rotation is prescribed: friction, wire flexibility, driving details and the ability of the wire to supply the computed reaction are not modelled, and the numbers are model values, not measurements of any apparatus.

A bead on a uniformly rotating straight wire: the rheonomic ideal constraint, its reaction, and the work it performs

Example

Facts & Assumptions

Verification

Depends on

Dependency tree · 2 levels

Sources