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.

The planar pendulum by constraint elimination: kinetic metric, Lagrange equation and the ideal reaction recovered

Physical scope

A worked check of the constraint-elimination theorem on the planar pendulum model: one particle of mass m constrained without friction to a circle of radius l in the plane z=0 under a uniform downward field; the periodic angle map from R is a surjective immersion onto the circle, and multiple angle representatives are allowed. It gives kinetic metric m l^2, substituted potential -m g l cos(theta), the pendulum equation theta-double-dot = -(g/l) sin(theta), and the reaction as the transpose constraint-Jacobian multiple with its two component multipliers. The constraint components have dimensions length squared and length, so their multipliers have different dimensions. All quantities are model values of the declared idealization.

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 (t, (x, y, z), v) : = (0, - m g, 0)$ with constant $g > 0$ : the global potential model of potential $U (x, y, z) = m g y$ and no residual forces (Potential presentations of a force model, potential and mechanical energy, closed versus exact force fields, local potentials and equipotential level sets). Under Dimensions and SI unit conventions of the non-relativistic classical mechanics framework, $[m] = μ$ , $[x] = [y] = [z] = [l] = ℓ$ , $[t] = τ$ , $[g] = ℓ τ^{- 2}$ , and $[U] = μ ℓ^{2} τ^{- 2}$ ; the angle $θ$ is dimensionless. Fix $l > 0$ and constrain the label to the circle of radius $l$ in the plane $z = 0$ by the regular holonomic-constraint datum of Holonomic-constraint models of the force branch: constraint data, the constrained equation, virtual displacements and the scleronomic/rheonomic distinction $O : = R \times R^{3}, k : = 2, g_{c} (x, y, z) : = (x^{2} + y^{2} - l^{2}, z),$ and adopt the ideal-reaction law of Adopted ideal-reaction law for holonomic constraints: the d'Alembert condition, its scope and its limits. The locus is the time-independent set $C = {(x, y, z) : x^{2} + y^{2} = l^{2}, z = 0}$ , so the datum is scleronomic, and the map $X : R ⟶ Q, X (θ) : = (l \sin θ, - l \cos θ, 0)$ is a surjective immersion of the constrained configurations in the sense of Generalized-coordinate maps of the model, the substituted Lagrangian, the kinetic metric and generalized forces. It is periodic and not one-to-one; the definition and reduction theorem allow these multiple angle representatives.

Then, with $r = 3 N - k = 1$ , kinetic metric $G (θ) = m l^{2}$ , substituted potential $\tilde{U} (θ) = - m g l \cos θ$ and substituted Lagrangian $\tilde{L} (θ, \dot{θ}) = \frac{1}{2} m l^{2} {\dot{θ}}^{2} + m g l \cos θ,$ the following hold:

for every interval $J \subseteq I_{0} = R$ with nonempty interior and every $C^{2}$ curve $θ : J \to R$ with $x : = X \circ θ$ , the curve $θ$ solves the Lagrange equation $Λ (\tilde{L}) (θ) = 0$ , i.e. $m l^{2} θ^{''} + m g l \sin θ = 0,$ if and only if $x$ is a constrained motion with ideal reaction;
when this holds, the reaction is $R (t) = D_{x} g_{c} (x (t))^{T} (\begin{array}{c} λ_{1} (t) \\ λ_{2} (t) \end{array}) = - m (l θ^{'} (t)^{2} + g \cos θ (t)) (\sin θ (t), - \cos θ (t), 0),$ where $λ_{1} (t) = - \frac{m}{2 l} (l θ^{'} (t)^{2} + g \cos θ (t))$ and $λ_{2} (t) = 0$ ; the multipliers have dimensions $[λ_{1}] = μ τ^{- 2}$ and $[λ_{2}] = μ ℓ τ^{- 2}$ , so the reaction has force dimension, annihilates the virtual displacements, and has a unique multiplier;
in particular the reduced pendulum equation $θ^{''} = - (g / l) \sin θ$ is exactly the Lagrange equation of $\tilde{L}$ , and every $C^{2}$ solution of it on such an interval $J$ , with $x = X \circ θ$ , is an ideal constrained motion of the model.

Facts & Assumptions

Given: The model data of the Example, the datum $(O, 2, g_{c})$ , the surjective immersion $X$ , a $C^{2}$ curve $θ : J \to R$ with $x = X \circ θ$ , and the constants $m, l, g > 0$ with the declared dimensions.

[F1]

The reduction theorem (Ideal scleronomic holonomic constraints: the substituted Lagrange equations are equivalent to the constrained model equation): for a scleronomic regular holonomic datum with a global-coverage parametrization $X (Ω) = C \cap Q$ and a potential presentation $(U, d)$ , a $C^{2}$ coordinate curve solves the Lagrange equations of $\tilde{L}$ with residual generalized force if and only if $x = X \circ θ$ is a constrained motion with ideal reaction; injectivity of $X$ is unnecessary, the virtual displacements at $x$ equal $D X (θ) (R)$ , and the reaction is unique with a unique multiplier vector.

[F2]

The datum and its locus (Holonomic-constraint models of the force branch: constraint data, the constrained equation, virtual displacements and the scleronomic/rheonomic distinction, Adopted ideal-reaction law for holonomic constraints: the d'Alembert condition, its scope and its limits, For an $m \times n$ matrix $A$ , $rank (A) + \dim N (A) = n$ , Submersions and immersions between Euclidean open sets, The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case): $g_{c}$ is smooth with $D_{x} g_{c} (x, y, z) = (\begin{array}{ccc} 2 x & 2 y & 0 \\ 0 & 0 & 1 \end{array})$ of rank $2$ on $C$ (the last row is independent; on $x^{2} + y^{2} = l^{2}$ not both $2 x, 2 y$ vanish), its component dimensions are $ℓ^{2}$ and $ℓ$ , the locus is nonempty and time-independent, and the virtual displacements at $X (θ)$ are $\ker D_{x} g_{c} = R (\cos θ, \sin θ, 0)$ .

[F3]

The parametrization and its derivatives (Generalized-coordinate maps of the model, the substituted Lagrangian, the kinetic metric and generalized forces, The derivatives of sine and cosine are cosine and minus sine, Sine and cosine defined by their real power series, A function differentiable at $c$ is continuous at $c$ , The principle of mathematical induction, 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$ , Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes, The transpose $A^{T}$ of a matrix, 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): repeated differentiation cycles through $\pm \sin$ and $\pm \cos$ ; induction shows all iterated derivatives of $X$ exist and are continuous, so $X$ is $C^{\infty}$ . Also $D X (θ) = (l \cos θ, l \sin θ, 0)$ , $G (θ) = D X (θ)^{T} (m I_{3}) D X (θ) = m l^{2}$ , and $\tilde{U} (θ) = U (X (θ)) = - m g l \cos θ$ ; the displayed vectors $e_{θ} = (\cos θ, \sin θ, 0)$ and $e_{r} = (\sin θ, - \cos θ, 0) = X (θ) / l$ are orthonormal.

[F4]

The angle coverage and period (The derivatives of sine and cosine are cosine and minus sine, A function differentiable at $c$ is continuous at $c$ , 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)$ , Pi is the first positive zero of sine, Quarter-turn values and shifts by pi/2 and pi, Parity and the Pythagorean identity for sine and cosine, The zero sets of sine and cosine and the least positive common period 2 pi, Squares of nonzero elements are positive, Absolute value in an ordered field): cosine is continuous on $[0, π]$ , with $\cos 0 = 1$ and $\cos π = - 1$ , and sine is nonnegative there. For $u^{2} + v^{2} = 1$ , $v^{2} \geq 0$ gives $u^{2} \leq 1$ , hence $u \in [- 1, 1]$ ; the intermediate value theorem gives $θ_{0} \in [0, π]$ with $\cos θ_{0} = u$ . The Pythagorean identity and sine's sign give $\sin θ_{0} = ∣ v ∣$ ; use $θ = θ_{0}$ for $v \geq 0$ and $θ = - θ_{0}$ for $v < 0$ , with parity, to obtain $(\cos θ, \sin θ) = (u, v)$ . Sine and cosine have period $2 π$ .

Verification

technique · direct; verify the hypotheses of the reduction theorem on the pendulum datum, compute the substituted Lagrangian and its Lagrange equation, and evaluate the reaction and multiplier

1.1F2F3F4givenalgebra

Hypotheses of the reduction theorem: $g_{c}$ is smooth and $D_{x} g_{c}$ has rank $2$ on $C$ by [F2], so $(O, 2, g_{c})$ is a regular holonomic-constraint datum with nonempty locus, and it is scleronomic with $C = {(x, y, z) : x^{2} + y^{2} = l^{2}, z = 0}$ . The map $X$ is $C^{3}$ by [F3], with $D X (θ) = (l \cos θ, l \sin θ, 0)$ injective for all $θ$ because its norm is $l > 0$ . For any $(x, y, 0) \in C$ , put $u = - y / l$ and $v = x / l$ ; then $u^{2} + v^{2} = 1$ , so [F4] gives $θ$ with $\sin θ = v$ and $\cos θ = u$ , hence $X (θ) = (x, y, 0)$ . Conversely every $X (θ)$ lies in $C$ by the Pythagorean identity, so $X (R) = C \cap Q$ . The period statement in [F4] gives $X (θ + 2 π) = X (θ)$ with distinct inputs, so the map is periodic and not one-to-one. Moreover $(t, X (θ)) \in O$ for all $t, θ$ . Thus $X$ is a global-coverage parametrization with repeated angle representatives allowed, and $r = 3 N - k = 1$ ; the presentation $(U, d) = (m g y, 0)$ has no residual forces.

1.2F3algebra

Substituted Lagrangian and Lagrange equation: by [F3], $G (θ) = m l^{2}$ and $\tilde{U} (θ) = - m g l \cos θ$ , so $\tilde{L} = \frac{1}{2} m l^{2} {\dot{θ}}^{2} + m g l \cos θ$ and $Λ (\tilde{L}) (θ) = \frac{d}{d t} (m l^{2} θ^{'}) - \frac{\partial \tilde{L}}{\partial θ} = m l^{2} θ^{''} + m g l \sin θ .$ The Lagrange equation $Λ (\tilde{L}) (θ) = 0$ is therefore $m l^{2} θ^{''} + m g l \sin θ = 0$ , equivalent to $θ^{''} = - (g / l) \sin θ$ because $m l^{2} > 0$ .

2.1F1F2step 1.2algebra

Equivalence and reaction: since $d \equiv 0$ , the residual generalized force vanishes, and by [F1] the equation of step 1.2 holds along $θ$ if and only if $x = X \circ θ$ is a constrained motion with ideal reaction. In that case $R = m x^{''} - F$ and, differentiating $x$ twice, $x^{''} = l (- θ^{' 2} \sin θ + θ^{''} \cos θ, θ^{' 2} \cos θ + θ^{''} \sin θ, 0);$ substituting $θ^{''} = - (g / l) \sin θ$ and $F = (0, - m g, 0)$ gives $R = - m (l θ^{' 2} + g \cos θ) (\sin θ, - \cos θ, 0)$ . Since $D_{x} g_{c} (x)^{T} (λ_{1}, λ_{2}) = 2 λ_{1} (x, y, 0) + (0, 0, λ_{2})$ and $(x, y, z) = X (θ)$ , this equals $D_{x} g_{c} (x)^{T} (λ_{1}, 0)$ with $λ_{1} = - \frac{m}{2 l} (l θ^{' 2} + g \cos θ)$ , as stated. The reaction is normal to $\ker D_{x} g_{c}$ from [F2], so it annihilates the virtual displacements; [F1] supplies uniqueness of the multiplier vector.

3.1step 1.1step 1.2step 2.1∎

Clauses 1-3 are verified: the datum and parametrization satisfy the hypotheses of the reduction theorem; the Lagrange equation of $\tilde{L}$ is the reduced pendulum equation; and the reaction is the normal multiple with the displayed multiplier. All quantities are model values under the declared idealizations (frictionless circular track, rigid radius, uniform downward field), not measurements.

Remarks

The multiplier and reaction computed here agree with the multiplier-balance account of the preceding page on the same idealized apparatus; the present verification shows that the same motion is obtained by eliminating the constraint in the Lagrangian rather than by solving for the multiplier. Neither route adds an empirical claim.

The planar pendulum by constraint elimination: kinetic metric, Lagrange equation and the ideal reaction recovered

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources