ExampleConstruction: AI-adaptedVerification: AI-adapted

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 ideal pendulum on declared data: strict minimum and Lyapunov stability at the downward equilibrium, negative Hessian and instability at the upward equilibrium, the exact linearised eigenvalues and oscillation frequency, and failure of attraction

Physical scope

A declared-data check of the page's energy-stability theorem on the ideal planar pendulum: with mass 1 kg, length 1 m and g=9.81 m s^-2 in the angle chart, the downward equilibrium is a strict minimum, hence Lyapunov stable but not attracting, with purely imaginary linearised eigenvalues and a positive angular oscillation frequency; the upward equilibrium has a strictly negative Hessian, hence is unstable, with real linearised eigenvalues. All data are declared model data; no measurement and no empirical comparison is made.

Example

Declared model data. Take one label on the real line as the angle chart of the ideal planar pendulum: the chart domain is $Ω : = R$ , the configuration coordinate is the angle $q$ (radians, identified modulo $2 π$ at the end), the kinetic metric is the constant matrix $M : = m ℓ^{2}$ with $m : = 1 k g$ , $ℓ : = 1 m$ , and the potential is $U (q) : = m g ℓ (1 - \cos q), g : = 9.81 m s^{- 2}, m g ℓ = 9.81 J .$ This is the mechanical chart datum of The mechanical first-order field, Lagrangian and energy of a configuration-dependent kinetic metric in a chart with $Ω = R$ , $M$ constant and $U$ of class $C^{\infty}$ . Its equations are $m ℓ^{2} \ddot{q} = - m g ℓ \sin q$ , equivalently $\ddot{q} = - (g / ℓ) \sin q$ .

Assertions to check. (i) $q = 0$ and $q = π$ are mechanical equilibria; (ii) at $q = 0$ the potential is a strict local minimum and Energy stability and instability of the mechanical model at an equilibrium: the strict minimum is Lyapunov stable, a negative Hessian eigenvalue gives linear instability, a negative definite potential Hessian gives nonlinear instability, and exact energy conservation rules out attraction clause 1 makes $(0, 0)$ Lyapunov stable, while the linearised eigenvalues are $\pm i \sqrt{g / ℓ} = \pm i 3 \sqrt{109} / 10 s^{- 1}$ (so the angular oscillation frequency is $3 \sqrt{109} / 10 s^{- 1}$ ) and the equilibrium is not asymptotically stable; (iii) at $q = π$ the Hessian is $- m g ℓ < 0$ and clause 3 makes $(π, 0)$ unstable, with linearised eigenvalues $\pm 3 \sqrt{109} / 10 s^{- 1}$ .

Facts & Assumptions

Given: the declared chart data $M = 1 k g m^{2}$ , $U (q) = 9.81 (1 - \cos q) J$ on $Ω = R$ and the two equilibria $q = 0$ , $q = π$ .

[L1]

The energy-stability theorem (Energy stability and instability of the mechanical model at an equilibrium: the strict minimum is Lyapunov stable, a negative Hessian eigenvalue gives linear instability, a negative definite potential Hessian gives nonlinear instability, and exact energy conservation rules out attraction): under the chart hypotheses, a strict local minimum of $U$ makes $(q_{0}, 0)$ Lyapunov stable; a negative Hessian eigenvalue gives an unbounded solution $e^{κ t} (w, κ w)$ of the associated vector equation $Y^{'} = D G (q_{0}, 0) Y$ , the action on an initial deviation of the normalized matrix equation (linear instability); a negative definite Hessian $D^{2} U (q_{0})$ makes the equilibrium unstable; and exact energy conservation prevents asymptotic stability whenever states of different energy accumulate at the equilibrium.

[L2]

Trigonometric facts: $(\sin)^{'} = \cos$ , $(\cos)^{'} = - \sin$ , $\sin 0 = 0$ and $\cos 0 = 1$ (The derivatives of sine and cosine are cosine and minus sine); $\sin π = 0$ , $\cos π = - 1$ and the half-turn shifts are those of Quarter-turn values and shifts by pi/2 and pi. Both functions are $2 π$ -periodic, and $\sin q = 0$ exactly when $q \in π Z$ (The zero sets of sine and cosine and the least positive common period 2 pi). Cosine is strictly decreasing on $[2 j π, (2 j + 1) π]$ and strictly increasing on $[(2 j + 1) π, (2 j + 2) π]$ for every integer $j$ (Signs, monotonicity intervals, and ranges of sine and cosine); with its value $1$ at $- 2 π, 0, 2 π$ , these inequalities give $\cos q < 1$ whenever $0 < ∣ q ∣ < 2 π$ .

Verification

technique · direct

1.1givenL2algebra

Equilibria and second derivative: by [L2], $U^{'} (q) = m g ℓ \sin q$ and $U^{''} (q) = m g ℓ \cos q$ ; hence $U^{'} (0) = U^{'} (π) = 0$ , so $q = 0$ and $q = π$ are mechanical equilibria (The mechanical first-order field, Lagrangian and energy of a configuration-dependent kinetic metric in a chart), with $U^{''} (0) = m g ℓ = 981 / 100 J > 0$ and $U^{''} (π) = - m g ℓ < 0$ .

2.1step 1.1givenL1L2algebra

Downward equilibrium: $U (q) - U (0) = m g ℓ (1 - \cos q) > 0$ for $0 < ∣ q ∣ < 2 π$ , because $\cos q < 1$ there; thus $q = 0$ is a strict local minimum (take $r_{0} : = π$ ), and [L1] first clause gives Lyapunov stability of $(0, 0)$ in the chart. Since $g / ℓ = 981 / 100 s^{- 2}$ , the linearised first-order matrix is $A_{0} = (\begin{array}{cc} 0 & 1 \\ - g / ℓ & 0 \end{array})$ , whose characteristic polynomial is $λ^{2} + g / ℓ$ and whose eigenvalues are $\pm i \sqrt{g / ℓ} = \pm i 3 \sqrt{109} / 10 s^{- 1}$ . The coefficient $ω : = \sqrt{g / ℓ}$ in $\ddot{η} + ω^{2} η = 0$ is the angular oscillation frequency of this linearised model, so the equilibrium is not hyperbolic and no exponential conclusion follows.

2.2step 1.1givenL1algebra

Upward equilibrium: $U^{''} (π) = - 981 / 100 J < 0$ , and since $n = 1$ the Hessian is negative definite at $q = π$ ; [L1] third clause therefore makes $(π, 0)$ unstable. The linearised first-order matrix is $A_{π} = (\begin{array}{cc} 0 & 1 \\ g / ℓ & 0 \end{array})$ , with characteristic polynomial $λ^{2} - g / ℓ$ and real eigenvalues $\pm \sqrt{g / ℓ} = \pm 3 \sqrt{109} / 10 s^{- 1}$ , one positive, matching the linear-instability statement of [L1] second clause.

3.1step 2.1givenL1algebra

Failure of attraction: for every $0 < ε < π$ the datum $z_{0} : = (ε, 0)$ has energy $E (z_{0}) = m g ℓ (1 - \cos ε) > 0 = E (0, 0)$ , so letting $ε ↓ 0$ supplies states of different energy accumulating at the equilibrium; by [L1] fourth clause (and the strict-minimum clause of step 2.1) $(0, 0)$ is Lyapunov stable but not asymptotically stable. In particular no datum of positive energy can converge to $(0, 0)$ , because the energy is conserved.

4.1step 2.1step 2.2givenalgebra∎

All quantities above are declared model data substituted into the chart formulas; $M$ has dimension $k g m^{2}$ , the potential and the energies share the dimension $J = k g m^{2} s^{- 2}$ , and the frequencies have dimension $s^{- 1}$ (Dimensions and SI unit conventions of the non-relativistic classical mechanics framework). No pendulum, material or measurement is involved.

Remarks

Periodic identification. The chart coordinate $q$ is the lift of the circle angle; the potential is $2 π$ -periodic and the equation is invariant under $q \mapsto q + 2 π$ , so the equilibria at $q = 2 π k$ (stable) and $q = π + 2 π k$ (unstable) are the same physical configurations as those checked. The two equilibria are the only mechanical equilibria, by step 1.1 and the zero set of the sine.
What the check does not show. The check verifies the hypotheses of Energy stability and instability of the mechanical model at an equilibrium: the strict minimum is Lyapunov stable, a negative Hessian eigenvalue gives linear instability, a negative definite potential Hessian gives nonlinear instability, and exact energy conservation rules out attraction on declared data; it does not produce a basin of attraction, a decay rate (none exists at the stable equilibrium) or any statement about the pendulum as an apparatus.

The ideal pendulum on declared data: strict minimum and Lyapunov stability at the downward equilibrium, negative Hessian and instability at the upward equilibrium, the exact linearised eigenvalues and oscillation frequency, and failure of attraction

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources