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.

Cylindrical coordinates for one label: the kinetic metric m diag(1, r^2, 1) and the coordinate form of the model's equation

Physical scope

A worked check of the coordinate-covariance theorem on cylindrical coordinates for one labelled particle of mass m in a declared potential presentation: the map covers the open region off the z-axis periodically and supplies local coordinates there, but is not a global chart of all configuration space; the substituted Lagrangian has kinetic metric m diag(1, r^2, 1), the coordinate Euler-Lagrange equations are exactly the Cartesian equation written in the cylindrical frame, and the Cartesian stationary curves correspond to coordinate lifts. The radial and axial coordinates have length dimension, the angle is dimensionless, and no measurement is reported.

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 a global potential presentation $F (t, x, v) = - \nabla U (t, x)$ with $C^{2}$ potential $U : I_{0} \times Q \to R$ 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); the mechanical Lagrangian is $L (t, x, v) = \frac{1}{2} m ∣ v ∣_{2}^{2} - U (t, x)$ (The action functional of a force model with a potential presentation: the mechanical Lagrangian, its chart instance and its dimensions). Let $Ω : = {(r, θ, z) \in R^{3} : r > 0}$ and define the cylindrical coordinate map $X (r, θ, z) : = (r \cos θ, r \sin θ, z), X : Ω ⟶ Q,$ with substituted Lagrangian and kinetic metric $\tilde{L} (t, r, θ, z, \dot{r}, \dot{θ}, \dot{z}) = \frac{1}{2} m ({\dot{r}}^{2} + r^{2} {\dot{θ}}^{2} + {\dot{z}}^{2}) - \tilde{U} (t, r, θ, z), \tilde{U} (t, r, θ, z) : = U (t, X (r, θ, z)),$ $G (r, θ, z) = D X (r, θ, z)^{T} (m I_{3}) D X (r, θ, z) = m (\begin{array}{ccc} 1 & 0 & 0 \\ 0 & r^{2} & 0 \\ 0 & 0 & 1 \end{array}) .$

Under Dimensions and SI unit conventions of the non-relativistic classical mechanics framework, $[m] = μ$ , $[r] = [z] = ℓ$ , $[t] = τ$ and $[θ] = 1$ (dimensionless angle); $[\dot{r}] = [\dot{z}] = ℓ τ^{- 1}$ , $[\dot{θ}] = τ^{- 1}$ , and $[U] = μ ℓ^{2} τ^{- 2}$ . The configuration image is $Q_{c y l} : = {(x, y, z) \in R^{3} : x^{2} + y^{2} > 0}$ , which omits the $z$ -axis.

Then:

$X$ is a $C^{\infty}$ map with everywhere invertible Jacobian, hence a local diffeomorphism at every point of $Ω$ , so the covariance theorem applies to it; its image is $Q_{c y l}$ , it is periodic in $θ$ , and it is not a global chart of $Q$ . The coordinate equations are interpreted on these local charts or along a chosen coordinate lift.
the Euler-Lagrange equations of $\tilde{L}$ are exactly $m (\ddot{r} - r {\dot{θ}}^{2}) = - \partial_{r} \tilde{U}, m (r^{2} \ddot{θ} + 2 r \dot{r} \dot{θ}) = - \partial_{θ} \tilde{U}, m \ddot{z} = - \partial_{z} \tilde{U},$ which are the coordinate components of $m x^{''} = - \nabla U (t, x)$ along $x = X (r, θ, z)$ ;
consequently, for $a < b$ and a $C^{2}$ curve $(r, θ, z) : [a, b] \to Ω$ with $x : = X \circ (r, θ, z)$ , the coordinate curve is stationary for the substituted action if and only if the Cartesian curve $x$ satisfies the model's equation of motion on $[a, b]$ .

Facts & Assumptions

Given: The model data of the Example, the map $X$ and a $C^{2}$ curve $q (t) = (r (t), θ (t), z (t))$ with values in $Ω$ and $x : = X \circ q$ .

[F1]

Regularity and invertibility ( $C^{k}$ Euclidean maps and diffeomorphisms, The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case, Invertible Euclidean linear maps, The derivatives of sine and cosine are cosine and minus sine, The principle of mathematical induction, A function differentiable at $c$ is continuous at $c$ , 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}$ ): repeated differentiation cycles through $\pm \sin$ and $\pm \cos$ ; induction and their continuity show these functions, and therefore the coordinate functions of $X$ , are $C^{\infty}$ . The Jacobian is $D X (r, θ, z) = (\begin{array}{ccc} \cos θ & - r \sin θ & 0 \\ \sin θ & r \cos θ & 0 \\ 0 & 0 & 1 \end{array}), \det D X (r, θ, z) = r > 0,$ so $D X$ is invertible on $Ω$ ; and $D X^{T} (m I_{3}) D X$ is the displayed diagonal matrix because its columns are orthogonal with squared norms $1, r^{2}, 1$ by $\sin^{2} + \cos^{2} = 1$ (Parity and the Pythagorean identity for sine and cosine).

[F2]

The covariance theorem (Time-dependent coordinate maps transform the potential-part equation into the substituted Euler-Lagrange equation): for this coordinate map the Euler-Lagrange expression of $\tilde{L}$ along $q$ satisfies $E_{\tilde{L}} (q) = D X^{T} E_{L} (x)$ , and the vanishing of the substituted Euler-Lagrange equation is equivalent to the Cartesian curve solving $m x^{''} (t) = - \nabla U (t, x (t))$ on $[a, b]$ (The stationary-action criterion and the potential-part Euler-Lagrange equation for the Cartesian equivalence).

[F3]

Chain rule for the coordinate description (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 derivatives of sine and cosine are cosine and minus sine, The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length): differentiating $x (t) = X (q (t))$ twice gives $x^{'} = \dot{r} e_{r} + r \dot{θ} e_{θ} + \dot{z} e_{3}, x^{''} = (\ddot{r} - r {\dot{θ}}^{2}) e_{r} + (r \ddot{θ} + 2 \dot{r} \dot{θ}) e_{θ} + \ddot{z} e_{3},$ where $e_{r} : = (\cos θ, \sin θ, 0)$ , $e_{θ} : = (- \sin θ, \cos θ, 0)$ , $e_{3} : = (0, 0, 1)$ are the displayed orthonormal basis vectors; and $\nabla U (t, x) = \partial_{r} \tilde{U} e_{r} + \frac{1}{r} \partial_{θ} \tilde{U} e_{θ} + \partial_{z} \tilde{U} e_{3}$ along $x$ .

[F4]

The trigonometric parameterization needed for the global image and periodicity (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, Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ , 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 $\sin θ \geq 0$ on this interval. Thus, for $u, v \in R$ with $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 then give $\sin θ_{0} = ∣ v ∣$ . Taking $θ = θ_{0}$ when $v \geq 0$ and $θ = - θ_{0}$ when $v < 0$ gives $(\cos θ, \sin θ) = (u, v)$ . The period theorem gives period $2 π$ for sine and cosine.

Verification

technique · direct; compute the Jacobian, the kinetic metric and the Euler-Lagrange equations of the substituted Lagrangian, and identify them with the Cartesian equation in the orthonormal cylindrical frame

1.1F1F4algebra

Clause 1: the displayed Jacobian and its determinant $r > 0$ are computed from the derivatives of sine and cosine, so $D X (r, θ, z)$ is invertible for every $(r, θ, z) \in Ω$ and $X$ has the invertibility hypothesis of the covariance theorem. By The Euclidean inverse function theorem and A local inverse of a $C^{k}$ regular map is $C^{k}$ , its restriction near any point is a smooth diffeomorphism onto an open part of its image; the inverse is a local cylindrical coordinate chart, and these local images show $X (Ω)$ is open. The image is contained in $Q_{c y l}$ because $(r \cos θ)^{2} + (r \sin θ)^{2} = r^{2} > 0$ . Conversely, for $(a, b, c) \in Q_{c y l}$ put $ρ : = \sqrt{a^{2} + b^{2}} > 0$ , $u : = a / ρ$ and $v : = b / ρ$ . Then $u^{2} + v^{2} = 1$ , so [F4] supplies $θ$ with $\cos θ = u$ and $\sin θ = v$ , giving $X (ρ, θ, c) = (a, b, c)$ . Thus $X (Ω) = Q_{c y l}$ . By [F4], $X (r, θ + 2 π, z) = X (r, θ, z)$ with distinct inputs, so $X$ is not injective and is not a global chart of $Q$ . The kinetic metric is computed by matrix multiplication: the columns of $D X$ are $e_{r}$ , $r e_{θ}$ , $e_{3}$ , an orthogonal triple of norms $1$ , $r$ , $1$ , so $D X^{T} (m I_{3}) D X = m d i a g (1, r^{2}, 1)$ as displayed.

2.1F1step 1.1algebra

Substituted Lagrangian: from clause (b) of the generalized-coordinate construction, $\tilde{L} = L \circ (t, X, D X v)$ equals $\frac{1}{2} m ({\dot{r}}^{2} + r^{2} {\dot{θ}}^{2} + {\dot{z}}^{2}) - \tilde{U}$ , matching the computed kinetic metric.

3.1F2step 2.1algebra

Euler-Lagrange equations: with $\partial \tilde{L} / \partial \dot{r} = m \dot{r}$ , $\partial \tilde{L} / \partial r = m r {\dot{θ}}^{2} - \partial_{r} \tilde{U}$ , $\partial \tilde{L} / \partial \dot{θ} = m r^{2} \dot{θ}$ , $\partial \tilde{L} / \partial θ = - \partial_{θ} \tilde{U}$ , $\partial \tilde{L} / \partial \dot{z} = m \dot{z}$ and $\partial \tilde{L} / \partial z = - \partial_{z} \tilde{U}$ , the equations $\frac{d}{d t} \partial_{\dot{q}} \tilde{L} - \partial_{q} \tilde{L} = 0$ read $m \ddot{r} - m r {\dot{θ}}^{2} + \partial_{r} \tilde{U} = 0, m r^{2} \ddot{θ} + 2 m r \dot{r} \dot{θ} + \partial_{θ} \tilde{U} = 0, m \ddot{z} + \partial_{z} \tilde{U} = 0,$ which are the displayed coordinate equations.

4.1F3step 3.1algebra

Cartesian identification: by [F3], $m x^{''} = - \nabla U (t, x)$ is equivalent, in the orthonormal frame $(e_{r}, e_{θ}, e_{3})$ , to the three scalar equations $m (\ddot{r} - r {\dot{θ}}^{2}) = - \partial_{r} \tilde{U}$ , $m (r \ddot{θ} + 2 \dot{r} \dot{θ}) = - \frac{1}{r} \partial_{θ} \tilde{U}$ , and $m \ddot{z} = - \partial_{z} \tilde{U}$ ; the second equation of step 3.1 is this one multiplied by $r$ . Hence the coordinate Euler-Lagrange equations are exactly the Cartesian equation written in the cylindrical frame.

5.1F2step 3.1step 4.1∎

Clause 3: regard the time-independent map as $\hat{X} : R \times Ω \to Q$ , $\hat{X} (t, q) : = X (q)$ . Then its substituted domain is $\tilde{O} = R \times Ω \times R^{3}$ , which is a time-dependent Lagrangian chart over $[a, b] \times Ω$ because $Ω$ is open and nonempty. By clause 2 of [F2], stationarity of $q$ for the substituted action is equivalent to stationarity of $x$ for $S$ ; by clause 1 of [F2] and step 4.1, the latter is equivalent to the Cartesian equation along $x = X \circ q$ .

Remarks

The example displays the two ingredients of the generalized-coordinate construction: the kinetic metric is the Jacobian-transpose multiple of the mass operator, and the coordinate equations carry the centripetal and Coriolis terms of the Cartesian acceleration exactly as computed by the chain rule. No new dynamical content is added by the change of coordinates.
For a $C^{2}$ curve with $z \equiv z_{0}$ satisfying the first two equations, the third equation holds exactly when $\partial_{z} \tilde{U} (t, r (t), θ (t), z_{0}) = 0$ throughout its interval, because $\ddot{z} = 0$ . Under this condition the plane-polar equations describe a motion of the declared three-dimensional model in that plane. The displayed angular Euler-Lagrange equation divided by $r > 0$ is $m (2 \dot{r} \dot{θ} + r \ddot{θ}) = - \frac{1}{r} \partial_{θ} \tilde{U}$ .

Cylindrical coordinates for one label: the kinetic metric m diag(1, r^2, 1) and the coordinate form of the model's equation

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources