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 pendulum angle chart: stability, linearized equation, finite-time bound and quadratic-energy check

Physical scope

A worked check of the adopted ideal pendulum angle-chart equation m l^2 theta-ddot = -m g l sin(theta): its scalar potential and strict minimum, Lyapunov stability from the mathematical chart theorem, the linearized angular equation with frequency sqrt(g/l), the finite-time small-angle error bound at g=l=1, and the failure of the quadratic energy of the linearized angular equation to be conserved along exact motions. The item asserts no measured value, no period formula for finite amplitudes and no derivation of the effective equation from the constrained system.

Example

Adopt the ideal planar pendulum angle-chart equation as an effective physical model, using the mathematical constant-metric chart of The mechanical first-order field, Lagrangian and energy of a configuration-dependent kinetic metric in a chart. This angular chart model is not an instance of the one-dimensional translational model class of The one-dimensional force models: data, motions, phase system, potential presentation, energy and equilibria: $θ$ is a dimensionless angle and its generalized inertia has dimension mass times length squared. The chart data are configuration domain $R$ , coordinate $θ$ (the angle from the downward vertical, in radians), effective mass parameter $m_{e f} : = m l^{2} > 0, force law F (θ) : = - m g l \sin θ,$ and constants $m, l, g > 0$ of dimensions mass, length and length per time squared (Dimensions and SI unit conventions of the non-relativistic classical mechanics framework). The force $F$ is a generalized torque. Its equation of motion is $m l^{2} θ^{''} = - m g l \sin θ, equivalently θ^{''} = - \frac{g}{l} \sin θ,$ the recorded source's point-pendulum equation (Eq. (1.18) there) expressed with the effective inertia $m_{e f} = m l^{2}$ and generalized torque $F = - m g l \sin θ$ . The potential $U = - m g l \cos θ$ is an energy-valued scalar function of the dimensionless angle. The stability and linearization calculations use the autonomous scalar equation as a mathematical chart system with constant coefficient $M = m_{e f}$ . All phase norms mean the Euclidean norm of the numerical pair $(θ, (1 s) θ^{'})$ ; the normalized time variable used in the finite-time estimate is $s = t_{p h y s} / (1 s)$ . The claims checked below are:

the generalized torque is $- U^{'} (θ)$ for $U (θ) = - m g l \cos θ$ , and $θ = 0$ is a strict local minimum;
the hanging rest point $(θ, θ^{'}) = (0, 0)$ is Lyapunov stable, and the linearised angular equation is $m_{e f} θ^{''} + m g l θ = 0$ with frequency $ω = \sqrt{g / l}$ ;
at $g = 1 m / s^{2}$ , $l = 1 m$ , use $s = t_{p h y s} / (1 s)$ and $z = (θ, d θ / d s)$ . For every initial phase vector $z_{0}$ with $∥ z_{0} ∥_{2} = δ = 1 / 100$ , radius $r = 1 / 2$ and normalized horizon $T = 1$ , write $t$ for the numerical time $s$ in the bound. Then the difference between the exact motion and the harmonic motion with the same datum obeys $∥ z (t) - y (t) ∥_{2} \leq \frac{t e^{3 t}}{12 \cdot 10^{4}} (0 \leq t \leq 1), ∥ z (1) - y (1) ∥_{2} \leq \frac{e^{3}}{12 \cdot 10^{4}} \approx 1.67 \cdot 10^{- 4},$ the source-supported bound of The pendulum field near the downward equilibrium: bounded force derivative, cubic remainder and the finite-time small-angle error bound;
the quadratic energy of the linearised angular equation, $E_{q u a d} : = \frac{1}{2} m_{e f} θ^{' 2} + \frac{1}{2} m g l θ^{2}$ , is not conserved along exact motions, with $\frac{d}{d t} [\frac{1}{2} m_{e f} θ^{' 2} + \frac{1}{2} m g l θ^{2}] = m g l θ^{'} (θ - \sin θ),$ which is positive at the phase point $(θ, θ^{'}) = (π / 2, 1 s^{- 1})$ .

Verification

Proof technique: direct; verify the angular potential and strict minimum, apply the mathematical chart stability and linearisation results, transport the source-supported small-angle bound with its numbers, and differentiate the quadratic energy of the linearised angular equation along an exact motion.

Given: The effective pendulum model with $m_{e f} = m l^{2}$ , $F = - m g l \sin θ$ , potential $U = - m g l \cos θ$ ; the constants $m, l, g > 0$ ; the phase point $(π / 2, 1)$ for the last claim.

[L1] Applicable mathematical chart results (The mechanical first-order field, Lagrangian and energy of a configuration-dependent kinetic metric in a chart, Energy is conserved along solutions of the mechanical system with a configuration-dependent kinetic metric, A strict local minimum of the potential gives a Lyapunov stable equilibrium of the mechanical system, by energy conservation, Linearisation of the mechanical system at an equilibrium: M(q_0) xi'' + D²U(q_0) xi = 0, and the small-oscillation quadratic model): with the constant positive kinetic coefficient $M = m l^{2}$ and $U = - m g l \cos θ$ , the chart equation is $M θ^{''} = - U^{'}$ and its conserved chart energy is $\frac{1}{2} M θ^{' 2} + U$ . A strict local minimum gives a Lyapunov-stable rest point. At a critical point the derivative linearization is $M ξ^{''} + U^{''} (θ_{*}) ξ = 0$ . These mathematical results apply to the declared angular chart system, whose coordinate and inertia are not a translational position and mass in kilograms.

[L2] Derivatives, continuity and values (The derivatives of sine and cosine are cosine and minus sine, A function differentiable at $c$ is continuous at $c$ , Quarter-turn values and shifts by pi/2 and pi, Signs, monotonicity intervals, and ranges of sine and cosine, The zero sets of sine and cosine and the least positive common period 2 pi, The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ , The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , 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 $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set): $(\sin θ)^{'} = \cos θ$ , $(\cos θ)^{'} = - \sin θ$ , so $U^{'} (θ) = m g l \sin θ$ and $U^{''} (θ) = m g l \cos θ$ ; since sine and cosine are differentiable on $R$ , they are continuous there by A function differentiable at $c$ is continuous at $c$ , and therefore the displayed first and second derivatives are continuous. Thus $U$ is $C^{2}$ in the one-variable sense that its derivatives through order two exist and are continuous. Also $\cos 0 = 1$ , $\sin (π / 2) = 1$ , cosine is strictly decreasing on $[0, π]$ and strictly increasing on $[- π, 0]$ , and the mean value theorem applies to continuous functions differentiable on the open interval; $\sin θ = 0$ exactly when $θ = n π$ for an integer $n$ .

[L3] The pendulum field near the downward equilibrium: bounded force derivative, cubic remainder and the finite-time small-angle error bound: for $g, l > 0$ , $ω^{2} = g / l$ and the field $F_{p} (θ, v) = (v, - ω^{2} \sin θ)$ of the pendulum ODE $θ^{''} = - ω^{2} \sin θ$ , one has $D F_{p} (0) = (\begin{array}{cc} 0 & 1 \\ - ω^{2} & 0 \end{array})$ , $∥ F_{p} (z) - D F_{p} (0) z ∥_{2} = ω^{2} ∣ \sin θ - θ ∣ \leq (ω^{2} / 6) ∣ θ ∣^{3}$ and $∥ F_{p} (z) ∥_{2} \leq L ∥ z ∥_{2}$ with $L = \max {1, ω^{2}}$ ; and if $δ e^{L T} < r$ , the maximal exact solution with $∥ z (0) ∥_{2} = δ$ and the linearised solution $y$ obey $∥ z (t) - y (t) ∥_{2} \leq \frac{ω^{2} r}{6} δ^{2} t e^{(∥ D F_{p} (0) ∥ + 2 L) t} (0 \leq t \leq T) .$

[L4] Exponentials (The exponential function is smooth and $(\exp)^{'} = \exp$ , The real exponential function and the number $e$ by a power series, The elementary numerical bound $2 < e < 3$ ): $e^{0} = 1$ , $2 < e < 3$ , so $e^{3} < 27$ ; and $e^{s}$ is strictly increasing.

1.1givenL1L2algebra

Angular potential. By [L2], $U^{'} (θ) = m g l \sin θ = - F (θ)$ ; the generalized torque is therefore the negative derivative of the declared energy-valued scalar potential $U (θ) = - m g l \cos θ$ . The equilibria are the zeros of $\sin θ$ , namely $θ = n π$ , $n \in Z$ ; and $θ = 0$ is a strict local minimum because $U (0) = - m g l$ and $U (θ) = - m g l \cos θ > - m g l$ for $0 < ∣ θ ∣ < π$ by [L2]. This is claim 1.

2.1step 1.1L1

Stability. By [L1] and step 1.1 the hanging rest point $(0, 0)$ is Lyapunov stable for the model's phase system, with the Euclidean phase norm of The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ and the balls of Open ball, closed ball and sphere in a metric space.

2.2step 1.1L1L4algebra

Linearisation and frequency: $U^{''} (θ) = m g l \cos θ$ , so $U^{''} (0) = m g l > 0$ ; by the linearisation clause of [L1] the linearised angular equation at $θ = 0$ is $m_{e f} ξ^{''} + m g l ξ = 0$ . Its angular frequency is $ω = \sqrt{U^{''} (0) / m_{e f}} = \sqrt{m g l / (m l^{2})} = \sqrt{g / l}$ by Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ . In the source's reading this is the small-oscillation frequency of the ideal pendulum model. This is claim 2.

3.1givenstep 2.2L3L4algebra

Small-angle bound at $g = l = 1$ . Here $ω^{2} = 1$ , $L = \max {1, 1} = 1$ , $∥ D F_{p} (0) ∥ = 1$ , and every explicitly quantified datum $z_{0}$ in claim 3 has $ω^{2} r / 6 = 1 / 12$ , $δ^{2} = 10^{- 4}$ . The hypothesis $δ e^{L T} < r$ reads $10^{- 2} e < 1 / 2$ , which holds since $e < 3 < 50$ by [L4]. By [L3] the exact solution and the linearised solution (which solves $θ^{''} = - θ$ , the numerical linearized chart equation with coefficient $ω^{2} = 1$ ) obey $∥ z (t) - y (t) ∥_{2} \leq \frac{1}{12} \cdot \frac{1}{10^{4}} \cdot t e^{3 t} = \frac{t e^{3 t}}{12 \cdot 10^{4}} (0 \leq t \leq 1),$ and at $t = 1$ this is at most $e^{3} / (12 \cdot 10^{4})$ , which is less than $27 / (12 \cdot 10^{4}) = \frac{9}{4} \cdot 10^{- 4}$ by [L4]. This is claim 3.

4.1givenstep 1.1L2algebra∎

The quadratic energy of the linearised angular equation is not conserved. Along a motion of the exact model, $\frac{d}{d t} E_{q u a d} = \frac{d}{d t} [\frac{1}{2} m_{e f} θ^{' 2} + \frac{1}{2} m g l θ^{2}] = m_{e f} θ^{'} θ^{''} + m g l θ θ^{'} = m g l θ^{'} (θ - \sin θ)$ by [L2] and the equation of motion $m_{e f} θ^{''} = - m g l \sin θ$ . At the phase point $(θ, θ^{'}) = (π / 2, 1 s^{- 1})$ the right side equals $m g l (1 s^{- 1}) (π / 2 - \sin (π / 2)) > 0$ . Indeed $\sin (π / 2) = 1 < π / 2$ : the mean value theorem applied to sine on $[0, π / 2]$ gives $1 = \cos ξ \cdot (π / 2)$ for some $ξ \in (0, π / 2)$ , with $\cos ξ < 1$ . Thus the quadratic energy changes along the exact pendulum motion, so the exact angular equation is not its linearised equation. This is claim 4.

Remarks

What the check exhibits. The exact pendulum angle-chart model has a stable hanging rest point and linearises to an angular oscillator equation at it. The difference between the exact and linearized angular motions is bounded only in the finite-time, small-amplitude sense of [L3], with the explicit numbers above. This is the page's instance of "exact versus small-angle model".
Scope and deferred modelling. The effective equation $θ^{''} = - (g / l) \sin θ$ is adopted here as the model's equation, with the recorded source support; its derivation from the constrained three-dimensional pendulum (ideal rod or string, constraint reactions, tangential balance) is a modelling step belonging to the constraints page, and no such derivation is claimed here. The finite-amplitude pendulum's period depends on its amplitude (through elliptic quadratures) and is outside this page's scope.

The pendulum angle chart: stability, linearized equation, finite-time bound and quadratic-energy check

Example

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources