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 equal-arm double pendulum in the linear approximation: the slow same-side mode, the fast opposite-side mode and the bounded modal motions

Physical scope

A worked instance of the coupled quadratic model: the two-angle small-oscillation data M = m l^2 [[2,1],[1,1]], K = m g l diag(2,1) attributed to the linearisation of an equal-mass equal-length planar double pendulum, with its two modal data (the slower same-side mode of frequency sqrt((g/l)(2-sqrt2)) and the faster opposite-side mode of frequency sqrt((g/l)(2+sqrt2))), the general bounded modal motion and the pure-mode data. The example verifies the quadratic model on the declared matrices; it does not derive the pendulum Lagrangians, does not control the error of the linear approximation at finite amplitude and asserts no measured period.

Example

The algebra below uses the fixed-unit numerical convention of The coupled quadratic oscillator model: mass metric, stiffness, generalized force, modal vocabulary and the small-oscillation model at a mechanical equilibrium, with coordinate units radians, time unit $1 s$ and energy unit $1 J$ . Physical model parameters are given their stated units; in matrix products, initial-vector identities and coefficient formulas their numerical coefficients in these fixed units are used. Modal amplitudes have common unit $a_{*} = (1 J)^{1 / 2} (1 s)$ ; the $j$ -th component of a mass-normalized modal vector has unit $s_{j} / a_{*}$ . Modal oscillatory and hyperbolic coefficients have unit $a_{*}$ , and zero-mode slopes have unit $a_{*} / (1 s)$ . Physical coordinates and energies are reconstructed with the coordinate units and $1 J$ , respectively. In particular a numerical single-mode datum $q (0) = u_{i}$ means a modal amplitude of one in this common amplitude unit.

Global-time, growth and boundedness claims below refer to the unique maximal extension of the autonomous free equation on $R$ ; local motions remain its restrictions. Values at $0$ in coefficient formulas are evaluated on that extension when the original interval omits $0$ .

Let a planar double pendulum consist of two equal particle labels of mass $m > 0$ connected by two equal massless rods of length $l > 0$ , pivoted at a fixed point; let $θ_{1}, θ_{2}$ be the angles of the rods from the downward vertical, read in radians (dimensionless under the angle convention of Dimensions and SI unit conventions of the non-relativistic classical mechanics framework), and let $g > 0$ be the uniform gravitational acceleration of the model. In the linear approximation about the downward equilibrium of the cited treatment, the small-oscillation data are the coupled quadratic model of The coupled quadratic oscillator model: mass metric, stiffness, generalized force, modal vocabulary and the small-oscillation model at a mechanical equilibrium with $n = 2$ ,

$M = m l^{2} (\begin{array}{cc} 2 & 1 \\ 1 & 1 \end{array}), K = m g l (\begin{array}{cc} 2 & 0 \\ 0 & 1 \end{array}), J \equiv 0.$

Write $γ_{s} : = 2 - \sqrt{2}$ , $γ_{f} : = 2 + \sqrt{2}$ . Then:

$M$ is symmetric positive definite (with $M^{1 / 2}$ its unique positive definite square root) and $K$ is symmetric positive definite, so the model is oscillatory with both modal stiffnesses positive;
the modal data are $λ_{s} = \frac{g}{l} γ_{s} with w_{s} = (\begin{array}{c} 1 \\ \sqrt{2} \end{array}), λ_{f} = \frac{g}{l} γ_{f} with w_{f} = (\begin{array}{c} 1 \\ - \sqrt{2} \end{array}),$ that is $K w_{s} = λ_{s} M w_{s}$ and $K w_{f} = λ_{f} M w_{f}$ ; the $M$ -orthonormal modal vectors are $u_{s} = w_{s} / \sqrt{2 m l^{2} γ_{f}}$ and $u_{f} = w_{f} / \sqrt{2 m l^{2} γ_{s}}$ ;
the mode frequencies are $ω_{s} = \sqrt{\frac{g}{l} (2 - \sqrt{2})} < ω_{f} = \sqrt{\frac{g}{l} (2 + \sqrt{2})},$ and every motion is bounded on $R$ and has the form $q (t) = (A \cos (ω_{s} t) + B \sin (ω_{s} t)) u_{s} + (C \cos (ω_{f} t) + D \sin (ω_{f} t)) u_{f};$
in the slow mode $u_{s}$ the two angles have the same sign ( $θ_{2} = \sqrt{2} θ_{1}$ ) and in the fast mode $u_{f}$ they have opposite signs ( $θ_{2} = - \sqrt{2} θ_{1}$ ); the datum $q (0) = u_{s}$ , $q^{'} (0) = 0$ excites exactly the slow mode and the datum $q (0) = u_{f}$ , $q^{'} (0) = 0$ exactly the fast mode.

Facts & Assumptions

Given: The parameters $m, l, g > 0$ , the matrices $M, K$ of the Example, the vectors $w_{s}, w_{f}$ and the numbers $γ_{s}, γ_{f}$ .

[F1]

Model dictionary (The coupled quadratic oscillator model: mass metric, stiffness, generalized force, modal vocabulary and the small-oscillation model at a mechanical equilibrium): the data $(M, K, 0)$ declare a free coupled quadratic model with two degrees of freedom, kinetic energy $\frac{1}{2} q^{' T} M q^{'}$ , potential energy $\frac{1}{2} q^{T} K q$ and the modal vocabulary of clause (e).

[F2]

Free-mode theory (The free coupled quadratic model: global existence, the complete modal classification, mode energies, intrinsic degenerate mode subspaces, boundedness and the unstable direction clauses 1, 2, 4 and 5): every free motion is the modal superposition of that theorem; positive definite stiffness gives positive modal stiffnesses and bounded motions; the pure- $λ$ motions are the solutions of $q^{''} + λ q = 0$ with values in the intrinsic subspace $N_{λ}$ .

[F3]

Direct linear algebra (Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes, The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ): $M$ -inner products, matrix products and positive definiteness are checked by the displayed quadratic forms and products. The existence of the positive definite square root is supplied by [F1], not by these arithmetic definitions.

[F4]

Scalar oscillator calculus (The homogeneous damped oscillator: solution classification by the discriminant and uniqueness for initial data, The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ , $C^{k}$ Euclidean maps and diffeomorphisms): for $λ > 0$ the scalar equation $z^{''} + λ z = 0$ has exactly the family $A \cos (ω t) + B \sin (ω t)$ with $ω = \sqrt{λ}$ .

Verification

Proof technique: direct; check positive definiteness, verify the two eigenpairs by explicit multiplication, and read the motion and boundedness statements from the free-mode theorem.

1.1F1F3algebra

Positive definiteness: $M$ is symmetric and, for $w = (x, y) \neq 0$ , $w^{T} M w = m l^{2} (2 x^{2} + 2 x y + y^{2}) = m l^{2} (x^{2} + (x + y)^{2}) > 0$ , since both squares can vanish only when $x = y = 0$ . Likewise $w^{T} K w = m g l (2 x^{2} + y^{2}) > 0$ , so $K$ is symmetric positive definite; hence both modal stiffnesses are positive and the model is oscillatory.

1.2F1F3algebra

Eigenpairs: multiplying, $K w_{s} = m g l (\begin{array}{c} 2 \\ \sqrt{2} \end{array}), M w_{s} = m l^{2} (\begin{array}{c} 2 + \sqrt{2} \\ 1 + \sqrt{2} \end{array}),$ and $2 / (2 + \sqrt{2}) = \sqrt{2} / (1 + \sqrt{2}) = 2 - \sqrt{2}$ , so $K w_{s} = \frac{g}{l} (2 - \sqrt{2}) M w_{s}$ ; similarly $K w_{f} = m g l (\begin{array}{c} 2 \\ - \sqrt{2} \end{array}), M w_{f} = m l^{2} (\begin{array}{c} 2 - \sqrt{2} \\ 1 - \sqrt{2} \end{array}),$ and $2 / (2 - \sqrt{2}) = - \sqrt{2} / (1 - \sqrt{2}) = 2 + \sqrt{2}$ , so $K w_{f} = \frac{g}{l} (2 + \sqrt{2}) M w_{f}$ . The normalizations give $u_{s}^{T} M u_{s} = u_{f}^{T} M u_{f} = 1$ and $u_{s}^{T} M u_{f} = 0$ , because $w_{s}^{T} M w_{s} = 2 m l^{2} γ_{f}$ , $w_{f}^{T} M w_{f} = 2 m l^{2} γ_{s}$ and $w_{s}^{T} M w_{f} = m l^{2} (2 - 2) = 0$ ; this proves clauses 1 and 2.

2.1F2F4step 1.2

Motions: by [F2] with $λ_{s}, λ_{f} > 0$ every motion is the displayed two-frequency superposition, with coefficients bijective onto the data, and it is bounded on $R$ because both modal families are bounded; the frequencies are $\sqrt{λ_{s}}$ and $\sqrt{λ_{f}}$ by [F4]. This is clause 3.

2.2F2step 1.2algebra

Mode patterns and pure-mode data: reading the coordinates of $w_{s} = (1, \sqrt{2})$ and $w_{f} = (1, - \sqrt{2})$ gives $θ_{2} = \sqrt{2} θ_{1}$ in the slow mode and $θ_{2} = - \sqrt{2} θ_{1}$ in the fast mode; the data $q (0) = u_{s}$ , $q^{'} (0) = 0$ correspond to $A = 1$ , $B = C = D = 0$ , hence to $q (t) = \cos (ω_{s} t) u_{s}$ , and analogously for $u_{f}$ . This is clause 4.

2.3step 1.2algebra

Frequency comparison: $γ_{f} - γ_{s} = 2 \sqrt{2} > 0$ gives $ω_{f} > ω_{s}$ : the mode in which the rods swing in opposite directions is the faster one, consistent with the cited treatment's conclusion.

3.1givenstep 1.1step 2.1step 2.2∎

Clauses 1-4 are verified on the declared matrices, which are the small-oscillation data attributed to the double pendulum in the cited linearization. The verification does not derive those matrices from the pendulum Lagrangian, makes no claim about the accuracy of the linear approximation at finite angle, and asserts no measured period; the gravitational acceleration $g$ is a model parameter.

Remarks

Why the slow mode is the same-side mode. The potential energy $\frac{1}{2} q^{T} K q = m g l (θ_{1}^{2} + \frac{1}{2} θ_{2}^{2})$ penalizes $θ_{1}$ more strongly than $θ_{2}$ , while the kinetic metric couples the two angles; the resulting slow direction is the one in which both rods move together and the fast direction the one in which they move oppositely. The computation above verifies the frequencies and patterns; the physical reading is the interpretation of the model data.
The linear model is not the pendulum. The matrices are the coefficients of the second-order Taylor expansion of the full Lagrangian in displacement and velocity at the downward rest point: $M$ is the zeroth-order value of the kinetic metric at that equilibrium, whereas $K$ is the Hessian of the potential. Derivatives of the kinetic metric multiply terms of total degree at least three in displacement and velocity, so they do not enter this quadratic Lagrangian. The exact pendulum is not a quadratic model, and the finite-time accuracy of the linear approximation is controlled only by Finite-time error control for the small-oscillation approximation: the quadratic remainder of the mechanical field and the variation-of-constants bound on small data, not by this example.

The equal-arm double pendulum in the linear approximation: the slow same-side mode, the fast opposite-side mode and the bounded modal motions

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources