Pipeline-generated

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.

Cm Math Verification

1 · Prerequisites

2 · Summary

The verification layer of the non-relativistic classical mechanics collection, all of it mathematics: the second variation of a time-dependent action and its oscillator saddle, the non-uniqueness of the zero-endpoint Dirichlet problem, the measure-theoretic parallel-axis theorem, the explicit normal modes of two coupled oscillators, and the finite-time small-angle error bound for the pendulum. Every item carries domain: mathematics and depends only on mathematical suppliers; nothing here asserts that a physical system is described by these models, that any unit convention holds, or that any parameter is measured. The classical-mechanics readings belong to the consuming physics pages, which add their own postulates and empirical qualifications.

Second variation of an action. The fixed-endpoint second variation of a time-dependent action at a curve defines the fixed-endpoint family $q + ε η$ and the second derivative $δ^{2} S (q) [η, η]$ ; The second variation of a time-dependent action: twice differentiability of the fixed-endpoint family and the Hessian integral formula proves that the family is twice differentiable and identifies the second derivative with the integral of the Hessian quadratic form of the Lagrangian along the family, so the definition is a well-defined real number. Both items sit over the chart and first-variation conventions of A time-dependent Lagrangian chart, its action functional and its fixed-endpoint first variations and The first variation of a time-dependent action on a finite interval: admissibility, the integral formula and continuity of the Euler-Lagrange coefficient.

The oscillator saddle and Dirichlet endpoint degeneracy. Second variation of the oscillator action on a finite interval: both signs for $T > π / ω$ and the value at $T = π / ω$ computes $δ^{2} S (q_{0}) [η_{n}, η_{n}] = \frac{T}{2} ((n π / T)^{2} - ω^{2})$ for the variations $η_{n} = \sin (n π t / T)$ of the zero curve of $L = \frac{1}{2} (v^{2} - ω^{2} q^{2})$ and shows that for $T > π / ω$ both signs occur among arbitrarily small variations, so the stationary zero curve is neither a local minimiser nor a local maximiser, while at $T = π / ω$ the second-variation value in direction $η_{1}$ is zero. More generally, The undamped oscillator: Dirichlet non-uniqueness at $T = n π / ω$ despite unique initial-value solutions proves that the Dirichlet problem with zero endpoints has nonzero solutions exactly for $T = n π / ω$ with an integer $n \geq 1$ ; in each such case its solution space is ${A \sin (ω t) : A \in R}$ , although every initial-value problem is uniquely solvable.

Parallel-axis theorem. The inertia tensor of a finite bounded Borel measure about any point of $R^{3}$ extends the measure-theoretic inertia matrix of Mass distributions on $R^{3}$ : total mass, first moment and inertia matrix to an arbitrary reference point, Finiteness and a uniform bound for the entries of the inertia tensor about an arbitrary point proves the entries finite with an explicit uniform bound under ${A C}_{ω}$ , and Parallel-axis theorem: the inertia tensor about a displaced point of a centred mass distribution proves the centred identity $I_{ν} (a) = I (ν) + m (∥ a ∥_{2}^{2} I_{3} - a a^{T})$ , so that the translation behaviour that the parent definition left open is settled for centred mass distributions.

Two coupled oscillators. Two equal masses with two outer springs and a coupling spring: eigenmodes, decoupling and the explicit normal frequencies treats $K = (\begin{array}{cc} k + c & - c \\ - c & k + c \end{array})$ : it identifies the orthonormal eigenvectors $u_{\pm}$ with eigenvalues $k$ and $k + 2 c$ , proves the decoupling bijection onto two scalar oscillator equations and exhibits the exact solution family with squared frequencies $k / m$ and $(k + 2 c) / m$ , together with the affine zero-frequency mode in the degenerate case $k = 0$ .

The pendulum bound. The pendulum field near the downward equilibrium: bounded force derivative, cubic remainder and the finite-time small-angle error bound verifies the hypotheses of the finite-time linearisation theorem for the field $F (θ, v) = (v, - ω^{2} \sin θ)$ : the cubic remainder $∣ \sin θ - θ ∣ \leq ∣ θ ∣^{3} / 6$ , the Lipschitz constant and the operator norm, and then instantiates the order- $δ^{2}$ error bound on $[0, T]$ under $δ e^{L T} < r$ . The scope sentence of that proposition and the page remark Scope and limits of the verification items on this page record that the estimate is conditional, finite-time and makes no exact-harmonicity claim about the nonlinear pendulum.

The companion page cm-math-verification-examples records explicit finite checks of these results: the two-sided saddle values at $T = 2 π$ , the $T = π$ non-uniqueness with its common action value, the parallel-axis identity on two point masses, the two-mass eigenrelations at concrete parameters, and the pendulum error expression with its exact constants.

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

DefinitionDefinition: AI-adaptedProof: Not applicableprecheck passOpen item page →

The fixed-endpoint second variation of a time-dependent action at a curve

Definition

Let $n \geq 1$ , let $a < b$ be reals, let $U \subseteq R^{n}$ be open and nonempty, and let $(O, L)$ be a time-dependent Lagrangian chart over $[a, b] \times U$ in the sense of A time-dependent Lagrangian chart, its action functional and its fixed-endpoint first variations: $O \subseteq R \times R^{n} \times R^{n}$ is open with

$[a, b] \times U \times R^{n} \subseteq O,$

and $L : O \to R$ is of class $C^{2}$ . Recall from that definition that a $C^{2}$ curve $q : [a, b] \to U$ is the restriction to $[a, b]$ of a $C^{2}$ map on an open interval, that a variation of $q$ is such a map $η : [a, b] \to R^{n}$ with

$η (a) = η (b) = 0,$

and that the action of a $C^{2}$ curve is

$S (q) : = \int_{a}^{b} L (t, q (t), q^{'} (t)) d t .$

The fixed-endpoint family. Let $q : [a, b] \to U$ be a $C^{2}$ curve and let $η$ be a variation of $q$ . For $ε \in R$ put

$q_{ε} (t) : = q (t) + ε η (t) (t \in [a, b]) .$

By clause 1 of The first variation of a time-dependent action on a finite interval: admissibility, the integral formula and continuity of the Euler-Lagrange coefficient there is $ε_{0} > 0$ such that $q_{ε}$ is a $C^{2}$ admissible curve with values in $U$ for every $ε \in (- ε_{0}, ε_{0})$ , so that the action $S (q_{ε})$ is defined for those $ε$ .

The second variation. The second variation of $S$ at $q$ in the direction $η$ is the second derivative at $ε = 0$ of the function $ε \mapsto S (q + ε η)$ :

$δ^{2} S (q) [η, η] : = \frac{d^{2}}{d ε^{2}} ∣_{ε = 0} S (q + ε η) .$

This is a well-defined real number under the present hypotheses: the map $ε \mapsto S (q + ε η)$ is twice differentiable at $0$ , with the explicit integral formula, by The second variation of a time-dependent action: twice differentiability of the fixed-endpoint family and the Hessian integral formula ↗, which depends on this definition only for the notation $δ^{2} S (q) [η, η]$ . The value is a single real number determined by the pair $(q, η)$ and does not depend on the choice of the $C^{2}$ extensions of $q$ and $η$ , since the values of $q_{ε}$ and $q_{ε}^{'}$ on $[a, b]$ are those of any such extension and the derivative on $[a, b]$ is extension-independent (A time-dependent Lagrangian chart, its action functional and its fixed-endpoint first variations).

Scope. The definition introduces the one-parameter family and its second derivative at $ε = 0$ , nothing else. It asserts nothing about minimising or maximising $S$ , nothing about the sign of $δ^{2} S$ , and no physical interpretation of $L$ ; stationarity of a curve is the separate first-order condition recorded in A time-dependent Lagrangian chart, its action functional and its fixed-endpoint first variations, and no equivalence with the vanishing of an Euler-Lagrange expression is used at this point.

Remarks

Normalisation. The symbol $δ^{2} S (q) [η, η]$ denotes the second derivative itself, not one half of it. The companion propositions of this page use exactly this normalisation when they compute second-variation values for the oscillator Lagrangian.
First and second variation together. The first variation $δ S (q) [η] = \frac{d}{d ε} ∣_{0} S (q + ε η)$ of A time-dependent Lagrangian chart, its action functional and its fixed-endpoint first variations and the second variation defined here are the two fixed-endpoint derivatives of the family $q + ε η$ . For a stationary $q$ the first one vanishes and $δ^{2} S (q) [η, η]$ is the leading second-order quantity computed by The second variation of a time-dependent action: twice differentiability of the fixed-endpoint family and the Hessian integral formula ↗.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passOpen item page →

The second variation of a time-dependent action: twice differentiability of the fixed-endpoint family and the Hessian integral formula

Statement

Let $(O, L)$ be a time-dependent Lagrangian chart over $[a, b] \times U$ in the sense of A time-dependent Lagrangian chart, its action functional and its fixed-endpoint first variations (so $L$ is $C^{2}$ and $[a, b] \times U \times R^{n} \subseteq O$ ), let $q : [a, b] \to U$ be a $C^{2}$ curve and let $η$ be a variation of $q$ (a $C^{2}$ map with $η (a) = η (b) = 0$ ). Write $ψ (ε, t) : = (t, q (t) + ε η (t), q^{'} (t) + ε η^{'} (t))$ and, for $∣ ε ∣ < ε_{0}$ with $ε_{0}$ as in clause 1 below,

$H (ε, t) : = \sum_{j, k = 1}^{n} [\frac{\partial^{2} L}{\partial q_{j} \partial q_{k}} (ψ (ε, t)) η_{j} (t) η_{k} (t) + 2 \frac{\partial^{2} L}{\partial q_{j} \partial v_{k}} (ψ (ε, t)) η_{j} (t) η_{k}^{'} (t) + \frac{\partial^{2} L}{\partial v_{j} \partial v_{k}} (ψ (ε, t)) η_{j}^{'} (t) η_{k}^{'} (t)] .$

Then:

there is $ε_{0} > 0$ such that for every $ε \in (- ε_{0}, ε_{0})$ the curve $q + ε η$ is a $C^{2}$ admissible curve with values in $U$ , and the map $ε \mapsto S (q + ε η)$ is of class $C^{2}$ on $(- ε_{0}, ε_{0})$ ;
for every $ε \in (- ε_{0}, ε_{0})$ ,

$\frac{d^{2}}{d ε^{2}} S (q + ε η) = \int_{a}^{b} H (ε, t) d t;$

in particular the second variation of The fixed-endpoint second variation of a time-dependent action at a curve is

$δ^{2} S (q) [η, η] = \int_{a}^{b} H (0, t) d t,$

the formula of clause 2 with every second partial of $L$ evaluated at $(t, q (t), q^{'} (t))$ .

Facts & Assumptions

Given: The chart data $(O, L)$ , a $C^{2}$ curve $q : [a, b] \to U$ , a variation $η$ , the map $ψ (ε, t) = (t, q (t) + ε η (t), q^{'} (t) + ε η^{'} (t))$ , and the action $S$ and second variation of A time-dependent Lagrangian chart, its action functional and its fixed-endpoint first variations and The fixed-endpoint second variation of a time-dependent action at a curve.

[L1]

Admissibility: there is $ε_{0} > 0$ such that for $∣ ε ∣ < ε_{0}$ the curve $q + ε η$ is a $C^{2}$ admissible curve with values in $U$ , hence $ψ$ maps $(- ε_{0}, ε_{0}) \times [a, b]$ into $O$ because $[a, b] \times U \times R^{n} \subseteq O$ (The first variation of a time-dependent action on a finite interval: admissibility, the integral formula and continuity of the Euler-Lagrange coefficient, clause 1).

[L2]

Differentiation under the integral sign on a compact rectangle (Leibniz's rule on a compact rectangle: an interior parameter derivative with a continuous extension may be passed through a Riemann integral): if $g, h : [α, β] \times [a, b] \to R$ are continuous and for each fixed $t$ the map $ε \mapsto g (ε, t)$ is differentiable on $(α, β)$ with derivative $h (ε, t)$ , then $ε \mapsto \int_{a}^{b} g (ε, t) d t$ is differentiable on $(α, β)$ with derivative $\int_{a}^{b} h (ε, t) d t$ .

[L3]

Chain rule and smoothness of the gradients (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ , If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative, The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder, $C^{k}$ Euclidean maps and diffeomorphisms, $C^{k}$ maps and multi-index derivative notation in Euclidean space, The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case, Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ , 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): because $L$ is $C^{2}$ on the open set $O$ , its gradient maps $L_{q} : O \to R^{n}$ and $L_{v} : O \to R^{n}$ are $C^{1}$ . For fixed $t$ the curve $ε \mapsto ψ (ε, t)$ is affine in $ε$ , with $ε$ -derivative the constant vector $(0, η (t), η^{'} (t))$ ; hence for $∣ ε ∣ < ε_{0}$ the chain rule gives the $ε$ -derivatives

$\frac{\partial}{\partial ε} [L (ψ)] = L_{q} (ψ) \cdot η (t) + L_{v} (ψ) \cdot η^{'} (t),$

$\frac{\partial}{\partial ε} [L_{q} (ψ)]_{j} = \sum_{k} \frac{\partial^{2} L}{\partial q_{j} \partial q_{k}} (ψ) η_{k} (t) + \sum_{k} \frac{\partial^{2} L}{\partial q_{j} \partial v_{k}} (ψ) η_{k}^{'} (t),$

$\frac{\partial}{\partial ε} [L_{v} (ψ)]_{j} = \sum_{k} \frac{\partial^{2} L}{\partial v_{j} \partial q_{k}} (ψ) η_{k} (t) + \sum_{k} \frac{\partial^{2} L}{\partial v_{j} \partial v_{k}} (ψ) η_{k}^{'} (t),$

and each displayed expression is continuous on every rectangle $[- δ, δ] \times [a, b]$ with $0 < δ < ε_{0}$ , the compositions of the continuous second partials with the continuous map $ψ$ and the continuous functions $η, η^{'}$ being continuous.

[L4]

Clairaut-Schwarz (Clairaut--Schwarz theorem for continuous second partial derivatives): the second partials of the $C^{2}$ function $L$ commute on $O$ , so $\partial^{2} L / \partial v_{j} \partial q_{k} = \partial^{2} L / \partial q_{k} \partial v_{j}$ there.

[L5]

Integrals (The lower and upper Darboux integrals of a bounded $f$ on $[a, b]$ as $\sup_{P} L (f, P)$ and $\inf_{P} U (f, P)$ , Darboux integrability as their equality, and the notation $\int_{a}^{b} f$ , A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion, Integrable functions on $[a, b]$ form a set closed under sums and scalar multiples, and $\int_{a}^{b} (λ f + μ g) = λ \int_{a}^{b} f + μ \int_{a}^{b} g$ , Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length, The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral, Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point, Absolute value in an ordered field): a continuous real function on the compact interval $[a, b]$ is Darboux integrable, and the integral of a finite sum of integrable functions with real coefficients is the corresponding sum of integrals.

[L6]

Uniform continuity and uniform integral errors (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line, Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous, Integrable functions on $[a, b]$ form a set closed under sums and scalar multiples, and $\int_{a}^{b} (λ f + μ g) = λ \int_{a}^{b} f + μ \int_{a}^{b} g$ , If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ , If $f, g$ are integrable on $[a, b]$ then so are $∣ f ∣$ , $f^{2}$ , $f g$ , $\max (f, g)$ and $\min (f, g)$ , and $∣ \int_{a}^{b} f ∣ \leq \int_{a}^{b} ∣ f ∣$ ): the closed bounded rectangle $R = [- δ, δ] \times [a, b]$ is compact, a continuous real function on a compact metric space is uniformly continuous; and if $u, v$ are integrable on $[a, b]$ with $∣ u (t) - v (t) ∣ \leq η$ for every $t \in [a, b]$ and some $η \geq 0$ , then $u - v$ and $∣ u - v ∣$ are integrable and $∣ \int_{a}^{b} u - \int_{a}^{b} v ∣ = ∣ \int_{a}^{b} (u - v) ∣ \leq \int_{a}^{b} ∣ u - v ∣ \leq η (b - a),$ by linearity of the integral, the triangle inequality for the integral and the two-sided bound of monotonicity.

Proof

Proof technique: direct; apply differentiation under the integral sign twice on a compact rectangle, the first derivative being the first-variation integrand and the second being the Hessian quadratic form of $L$ along the family.

1.1givenL1L3

Fix $0 < δ < ε_{0}$ with $ε_{0}$ from [L1], put $R : = [- δ, δ] \times [a, b]$ , and define $g (ε, t) : = L (ψ (ε, t))$ on $R$ . By [L1] the values of $ψ$ on $R$ lie in $O$ , so $g$ is defined and continuous on $R$ ; by [L3] the $ε$ -partial $g_{1} (ε, t) = L_{q} (ψ) \cdot η (t) + L_{v} (ψ) \cdot η^{'} (t)$ exists on $R$ and is continuous there.

2.1L2L5step 1.1

By [L2] applied to the continuous pair $(g, g_{1})$ on $R$ , the map $F (ε) : = S (q + ε η) = \int_{a}^{b} g (ε, t) d t$ is differentiable on $(- δ, δ)$ with derivative $F^{'} (ε) = \int_{a}^{b} g_{1} (ε, t) d t$ .

2.2L2L3L5step 1.1

By [L3] the $ε$ -partial of $g_{1}$ exists on $R$ and equals the four-term sum $g_{2} (ε, t) = [L_{q q} (ψ) η \cdot η + L_{q v} (ψ) η^{'} \cdot η] + [L_{v q} (ψ) η \cdot η^{'} + L_{v v} (ψ) η^{'} \cdot η^{'}],$ written with the block matrices $L_{q q}, L_{q v}, L_{v q}, L_{v v}$ of second partials evaluated at $ψ = ψ (ε, t)$ ; it is continuous on $R$ . Applying [L2] to the pair $(g_{1}, g_{2})$ shows that $ε \mapsto \int_{a}^{b} g_{1} (ε, t) d t$ is differentiable on $(- δ, δ)$ with derivative $\int_{a}^{b} g_{2} (ε, t) d t$ . Hence $F$ is twice differentiable on $(- δ, δ)$ with $F^{''} (ε) = \int_{a}^{b} g_{2} (ε, t) d t$ , and since every $0 < δ < ε_{0}$ is allowed, clause 2 holds for every $ε \in (- ε_{0}, ε_{0})$ once $g_{2}$ is rewritten in the symmetric form $H$ .

3.1L6L5step 2.2

Continuity of the second derivative: the function $g_{2}$ is continuous on the compact rectangle $R$ , so [L6] makes it uniformly continuous. Given $\tilde{ε} > 0$ choose $γ > 0$ such that $∣ g_{2} (ε, t) - g_{2} (ε^{'}, t) ∣ < \tilde{ε} / (b - a)$ for every $t \in [a, b]$ whenever $ε, ε^{'} \in (- δ, δ)$ satisfy $∣ ε - ε^{'} ∣ < γ$ . Then for such $ε, ε^{'}$ , linearity of the integral and [L6] give $∣ F^{''} (ε) - F^{''} (ε^{'}) ∣ = ∣ \int_{a}^{b} (g_{2} (ε, t) - g_{2} (ε^{'}, t)) d t ∣ \leq \frac{\tilde{ε}}{b - a} (b - a) = \tilde{ε},$ so $F^{''}$ is continuous on $(- δ, δ)$ ; since every $0 < δ < ε_{0}$ is allowed, $ε \mapsto S (q + ε η)$ is of class $C^{2}$ on $(- ε_{0}, ε_{0})$ , which is clause 1.

4.1L4step 2.2given∎

Symmetrisation: by [L4], for all $j, k$ one has $(L_{v q} (ψ))_{j k} = \partial^{2} L / \partial v_{j} \partial q_{k} (ψ) = \partial^{2} L / \partial q_{k} \partial v_{j} (ψ) = (L_{q v} (ψ))_{k j}$ , so $η^{'} \cdot L_{v q} (ψ) η = η \cdot L_{q v} (ψ) η^{'}$ after relabelling the summation indices; therefore $g_{2} = H$ and clauses 2 and 3 follow, the latter by the definition of $δ^{2} S (q) [η, η]$ and evaluation at $ε = 0$ .

Remarks

The statement is deliberately integral: the second derivative of the family is identified with the integral of the Hessian form, and no pointwise second-order Taylor hypothesis on $L$ beyond $C^{2}$ is used.
Both differentiations are instances of the same compact-rectangle theorem, the first with the first-variation integrand of The first variation of a time-dependent action on a finite interval: admissibility, the integral formula and continuity of the Euler-Lagrange coefficient and the second with its $ε$ -derivative; no second-order chain rule is needed, because the family is affine in $ε$ and the second derivative of $L \circ ψ$ is obtained by applying the ordinary chain rule to the $C^{1}$ maps $L_{q}$ and $L_{v}$ .

PropositionStatement: AI-adaptedProof: AI-adaptedprecheck passOpen item page →

Second variation of the oscillator action on a finite interval: both signs for $T > π / ω$ and the value at $T = π / ω$

Statement

Let $ω > 0$ and $T > 0$ , let $U : = R$ , and consider the time-dependent Lagrangian chart over $[0, T] \times U$ with $O : = R \times R \times R$ and $L (q, v) : = \frac{1}{2} (v^{2} - ω^{2} q^{2})$ (A time-dependent Lagrangian chart, its action functional and its fixed-endpoint first variations). Write $S$ for its action and $δ^{2} S$ for the second variation of The fixed-endpoint second variation of a time-dependent action at a curve. Then:

the zero curve $q_{0} \equiv 0$ is a $C^{2}$ admissible curve and is stationary for $S$ ;
for every integer $n \geq 1$ the map $η_{n} (t) : = \sin (n π t / T)$ is a variation of $q_{0}$ , and

$δ^{2} S (q_{0}) [η_{n}, η_{n}] = \frac{T}{2} ((\frac{n π}{T})^{2} - ω^{2});$

moreover $S (ε η_{n}) = \frac{ε^{2}}{2} δ^{2} S (q_{0}) [η_{n}, η_{n}]$ for every real $ε$ ; 3. if $T > π / ω$ , then $δ^{2} S (q_{0}) [η_{1}, η_{1}] < 0$ and $δ^{2} S (q_{0}) [η_{n}, η_{n}] > 0$ for every integer $n > ω T / π$ . Consequently, for every real $δ_{0} > 0$ there exist variations $η$ of $q_{0}$ with $\sup_{t \in [0, T]} (∣ η (t) ∣ + ∣ η^{'} (t) ∣ + ∣ η^{''} (t) ∣) < δ_{0}$ and $S (η) < 0$ , and variations with the same bound and $S (η) > 0$ ; hence the zero curve is neither a local minimiser nor a local maximiser of $S$ , in the sense that every neighbourhood of $q_{0}$ for the supremum distance $\sup_{[0, T]} (∣ q - q_{0} ∣ + ∣ q^{'} - q_{0}^{'} ∣ + ∣ q^{''} - q_{0}^{''} ∣)$ contains curves whose action is below $S (q_{0})$ and curves whose action is above $S (q_{0})$ ; 4. if $T = π / ω$ , then $δ^{2} S (q_{0}) [η_{1}, η_{1}] = 0$ , while $δ^{2} S (q_{0}) [η_{n}, η_{n}] > 0$ for every integer $n \geq 2$ .

Facts & Assumptions

Given: The parameters $ω > 0$ and $T > 0$ , the chart data $(O, L)$ above, the zero curve $q_{0} \equiv 0$ , the action $S$ , the second variation $δ^{2} S$ , and the maps $η_{n} (t) = \sin (n π t / T)$ for integers $n \geq 1$ .

[F1]

Chart and stationarity (A time-dependent Lagrangian chart, its action functional and its fixed-endpoint first variations, Stationarity of the time-dependent action is equivalent to the vanishing of the Euler-Lagrange expression): the Euler-Lagrange expression of this chart along a $C^{2}$ curve $q$ is $E (q) (t) = - ω^{2} q (t) - q^{''} (t)$ , and $q$ is stationary for $S$ if and only if $E (q) = 0$ on $[0, T]$ .

[F2]

Second variation formula (The second variation of a time-dependent action: twice differentiability of the fixed-endpoint family and the Hessian integral formula, The fixed-endpoint second variation of a time-dependent action at a curve): for every $C^{2}$ curve $q$ on $[0, T]$ and every variation $η$ , $δ^{2} S (q) [η, η] = \int_{0}^{T} (η^{'} (t)^{2} - ω^{2} η (t)^{2}) d t,$ because the second partials of $L$ are the constants $\partial^{2} L / \partial q^{2} = - ω^{2}$ , $\partial^{2} L / \partial q \partial v = 0$ and $\partial^{2} L / \partial v^{2} = 1$ .

[F3]

Trigonometric data (The derivatives of sine and cosine are cosine and minus sine, Sine and cosine defined by their real power series, The addition formulas for sine and cosine, Parity and the Pythagorean identity for sine and cosine, The zero sets of sine and cosine and the least positive common period 2 pi, The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ): $\sin$ and $\cos$ are differentiable with $\sin^{'} = \cos$ and $\cos^{'} = - \sin$ , and $\sin 0 = 0$ ; for every real $u$ the addition formulas and the Pythagorean identity give $\cos^{2} u = \frac{1}{2} (1 + \cos 2 u)$ and $\sin^{2} u = \frac{1}{2} (1 - \cos 2 u)$ ; the zero set of $\sin$ is exactly $π Z$ . Hence for every integer $n \geq 1$ the map $η_{n} (t) = \sin (n π t / T)$ is $C^{2}$ on an open interval containing $[0, T]$ , with $η_{n}^{'} (t) = (n π / T) \cos (n π t / T)$ and $η_{n} (0) = η_{n} (T) = \sin (n π) = 0$ .

[F4]

Integration (The lower and upper Darboux integrals of a bounded $f$ on $[a, b]$ as $\sup_{P} L (f, P)$ and $\inf_{P} U (f, P)$ , Darboux integrability as their equality, and the notation $\int_{a}^{b} f$ , A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion, The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ , Integrable functions on $[a, b]$ form a set closed under sums and scalar multiples, and $\int_{a}^{b} (λ f + μ g) = λ \int_{a}^{b} f + μ \int_{a}^{b} g$ , Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length): continuous real functions on $[0, T]$ are Darboux integrable; if $G$ is differentiable with derivative $G^{'}$ and $G^{'}$ is integrable then $\int_{0}^{T} G^{'} = G (T) - G (0)$ ; and the integral of a finite linear combination of integrable functions is the corresponding combination of integrals.

[F5]

Archimedean property (Every complete ordered field is Archimedean): for every real $x$ there is a natural number $n$ with $x < n$ .

Proof

Proof technique: direct; compute the second variation of the oscillator family with elementary trigonometric integrals, obtain the exact action along the family, and read off the two signs and the degenerate case. [given]

1.1givenF1F4algebra

Stationarity of the zero curve: $q_{0}$ is a $C^{2}$ admissible curve with values in $U = R$ , and $E (q_{0}) (t) = - ω^{2} \cdot 0 - 0 = 0$ for every $t$ , so $q_{0}$ is stationary by [F1]; also $S (q_{0}) = \int_{0}^{T} 0 d t = 0$ by [F4].

1.2givenF2F3

Variation and second variation: for every integer $n \geq 1$ , $η_{n}$ is a variation of $q_{0}$ by [F3], so [F2] and [F3] give $δ^{2} S (q_{0}) [η_{n}, η_{n}] = \int_{0}^{T} ((\frac{n π}{T})^{2} \cos^{2} (\frac{n π t}{T}) - ω^{2} \sin^{2} (\frac{n π t}{T})) d t .$

2.1step 1.2F3F4algebra

Evaluation of the integrals: by [F3] and [F4], $\int_{0}^{T} \cos^{2} (\frac{n π t}{T}) d t = \frac{1}{2} \int_{0}^{T} (1 + \cos \frac{2 n π t}{T}) d t = \frac{T + 0}{2} = \frac{T}{2},$ and likewise $\int_{0}^{T} \sin^{2} (n π t / T) d t = T / 2$ , because the FTC gives $\int_{0}^{T} \cos (2 n π t / T) d t = \frac{T}{2 n π} [\sin (2 n π t / T)]_{0}^{T} = \frac{T}{2 n π} (\sin (2 n π) - \sin 0) = 0$ by the vanishing of $\sin$ at integer multiples of $π$ from [F3]. Substituting into step 1.2 gives the second-variation value of clause 2.

3.1step 1.2step 2.1F4algebra

Exact action along the family: since $L$ is homogeneous of degree two in $(q, v)$ , for every real $ε$ the integrand of $S (ε η_{n})$ is $L (ε η_{n}, ε η_{n}^{'}) = ε^{2} L (η_{n}, η_{n}^{'})$ ; by linearity of the integral [F4] and step 1.2, $S (ε η_{n}) = ε^{2} S (η_{n}) = \frac{ε^{2}}{2} δ^{2} S (q_{0}) [η_{n}, η_{n}]$ , which is the exact identity of clause 2.

4.1step 1.1step 2.1step 3.1F3F5algebra

Signs for $T > π / ω$ : if $T > π / ω$ , then $π / T < ω$ , so clause 2 gives $δ^{2} S (q_{0}) [η_{1}, η_{1}] < 0$ ; by [F5] choose an integer $n$ with $n > ω T / π$ , so $(n π / T)^{2} > ω^{2}$ and $δ^{2} S (q_{0}) [η_{n}, η_{n}] > 0$ . For any real $δ_{0} > 0$ pick $ε > 0$ with $ε (1 + n π / T + (n π / T)^{2}) < δ_{0}$ ; then $∣ η_{n} ∣ \leq 1$ , $∣ η_{n}^{'} ∣ \leq n π / T$ and $∣ η_{n}^{''} ∣ \leq (n π / T)^{2}$ by [F3], so the variations $ε η_{1}$ and $ε η_{n}$ satisfy the displayed supremum bound, while step 3.1 gives $S (ε η_{1}) = \frac{ε^{2}}{2} δ^{2} S (q_{0}) [η_{1}, η_{1}] < 0$ and $S (ε η_{n}) > 0$ ; with $S (q_{0}) = 0$ from step 1.1, the zero curve is neither a local minimiser nor a local maximiser.

5.1step 2.1algebra∎

The degenerate case: if $T = π / ω$ , substitution into clause 2 gives $δ^{2} S (q_{0}) [η_{1}, η_{1}] = \frac{T}{2} (ω^{2} - ω^{2}) = 0$ , while for every integer $n \geq 2$ the value is $\frac{T}{2} (n^{2} ω^{2} - ω^{2}) > 0$ .

Remarks

The computation is a finite-time statement about the action functional on $[0, T]$ with fixed endpoints. For every $T > π / ω$ it shows that the zero stationary curve is neither a local minimum nor a local maximum; nothing here asserts anything about the physical least-action principle, and the results are mathematical properties of the model A time-dependent Lagrangian chart, its action functional and its fixed-endpoint first variations.
The bound $n > ω T / π$ is the quantisation of the statement that a sufficiently high-frequency sine variation has positive second variation; at $T = π / ω$ the displayed second-variation value in direction $η_{1}$ is zero, consistent with the endpoint non-uniqueness of The undamped oscillator: Dirichlet non-uniqueness at $T = n π / ω$ despite unique initial-value solutions.

PropositionStatement: AI-adaptedProof: AI-adaptedprecheck passOpen item page →

The undamped oscillator: Dirichlet non-uniqueness at $T = n π / ω$ despite unique initial-value solutions

Statement

Let $m > 0$ and $k > 0$ , put $ω : = (k / m)^{1 / 2} > 0$ (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ), and let $T > 0$ . Consider the undamped homogeneous oscillator equation

$m x^{''} (t) + k x (t) = 0$

of The damped driven oscillator model: second-order equation, phase-plane system and characteristic data with time domain $I = R$ and zero forcing, and its solutions on intervals with nonempty interior. The Dirichlet curves below are restrictions to $[0, T]$ of its global solutions. Then:

for every real $A$ the function $x_{A} (t) : = A \sin (ω t)$ is a $C^{2}$ (indeed $C^{\infty}$ ) solution on $R$ with $x_{A} (0) = 0$ and $x_{A} (T) = A \sin (ω T)$ ; moreover $x_{A} (T) = 0$ if and only if $A = 0$ or $ω T \in π Z$ (The zero sets of sine and cosine and the least positive common period 2 pi);
if $T = n π / ω$ for some integer $n \geq 1$ , then the set of $C^{2}$ solutions of the Dirichlet problem on $[0, T]$ ,

$m x^{''} + k x = 0, x (0) = x (T) = 0,$

is exactly ${x_{A} : A \in R}$ ; this set is a one-dimensional real vector space, so the boundary-value problem has infinitely many distinct solutions with the same endpoint data $(0, 0)$ , one for each initial velocity $A ω$ ; 3. by contrast, for every $(x_{0}, v_{0}) \in R^{2}$ the initial-value problem $m x^{''} + k x = 0$ , $x (0) = x_{0}$ , $x^{'} (0) = v_{0}$ , has exactly one solution on $R$ , namely $x (t) = x_{0} \cos (ω t) + (v_{0} / ω) \sin (ω t)$ (The homogeneous damped oscillator: solution classification by the discriminant and uniqueness for initial data, clauses 3 and 4 with $c = 0$ ); uniqueness for the initial-value problem therefore does not imply uniqueness for the boundary-value problem; 4. for the chart with $O = R \times R \times R$ and $L (q, v) = \frac{1}{2} (v^{2} - ω^{2} q^{2})$ over $[0, T] \times R$ (A time-dependent Lagrangian chart, its action functional and its fixed-endpoint first variations), each $x_{A}$ is a stationary curve of the action; and if $T = n π / ω$ , the stationary curves on $[0, T]$ satisfying the endpoint conditions $x (0) = x (T) = 0$ are exactly the curves $x_{A}$ , so the fixed-endpoint problem with zero data has infinitely many stationary curves (Stationarity of the time-dependent action is equivalent to the vanishing of the Euler-Lagrange expression).

Facts & Assumptions

Given: The parameters $m > 0$ , $k > 0$ , $T > 0$ , the number $ω = (k / m)^{1 / 2}$ , the oscillator model of The damped driven oscillator model: second-order equation, phase-plane system and characteristic data, the curves $x_{A} (t) = A \sin (ω t)$ , and the chart of clause 4.

[F1]

Classification and uniqueness (The homogeneous damped oscillator: solution classification by the discriminant and uniqueness for initial data, The damped driven oscillator model: second-order equation, phase-plane system and characteristic data): for the parameters $(m, c, k) = (m, 0, k)$ one has $Δ = - 4 m k < 0$ , $γ = 0$ and $ω_{c l} : = \sqrt{4 m k - c^{2}} / (2 m) = \sqrt{k / m} = ω$ , so clause 3 states that $x : J \to R$ on an interval $J$ with nonempty interior is a solution if and only if $x (t) = A \cos (ω t) + B \sin (ω t)$ for some $A, B \in R$ ; and clause 4 states that for every $(x_{0}, v_{0}) \in R^{2}$ there is exactly one solution $x : R \to R$ with $x (0) = x_{0}$ , $x^{'} (0) = v_{0}$ .

[F2]

Trigonometric data (The derivatives of sine and cosine are cosine and minus sine, Sine and cosine defined by their real power series, The zero sets of sine and cosine and the least positive common period 2 pi, The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ , 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$ and $\cos$ are differentiable with $\sin^{'} = \cos$ , $\cos^{'} = - \sin$ and $\sin 0 = 0$ ; the zero set of $\sin$ is exactly $π Z$ ; the chain rule gives $\frac{d}{d t} \sin (ω t) = ω \cos (ω t)$ and $\frac{d^{2}}{d t^{2}} \sin (ω t) = - ω^{2} \sin (ω t)$ .

[F3]

Chart and stationarity (A time-dependent Lagrangian chart, its action functional and its fixed-endpoint first variations, Stationarity of the time-dependent action is equivalent to the vanishing of the Euler-Lagrange expression): the Euler-Lagrange expression along a $C^{2}$ curve $q$ is $E (q) = - ω^{2} q - q^{''}$ , and $q$ is stationary for the action $S$ of this chart if and only if $E (q) = 0$ on $[0, T]$ .

[F4]

Square root (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ): $ω = (k / m)^{1 / 2}$ satisfies $ω > 0$ and $ω^{2} = k / m$ , and the interval convention is Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length.

Proof

Proof technique: direct; verify the explicit family, determine its endpoint values from the zero set of the sine, classify the Dirichlet solutions through the oscillator classification theorem, and identify the stationary curves through the Euler-Lagrange expression. [given]

1.1givenF2F4algebra

The family $x_{A} (t) = A \sin (ω t)$ : by [F2] the curve is $C^{\infty}$ with $x_{A}^{''} (t) = - A ω^{2} \sin (ω t)$ , so $m x_{A}^{''} (t) + k x_{A} (t) = (- m ω^{2} + k) A \sin (ω t) = 0$ by $ω^{2} = k / m$ from [F4]; also $x_{A} (0) = 0$ and $x_{A} (T) = A \sin (ω T)$ .

2.1step 1.1F2algebra

Endpoint vanishing: by the zero-set statement of [F2], $\sin (ω T) = 0$ is equivalent to $ω T \in π Z$ , so $x_{A} (T) = 0$ holds exactly when $A = 0$ or $ω T \in π Z$ .

2.2step 1.1F1F2algebra

Classification of the Dirichlet solutions: assume $T = n π / ω$ with an integer $n \geq 1$ and let $x$ be a $C^{2}$ solution of $m x^{''} + k x = 0$ on $[0, T]$ with $x (0) = x (T) = 0$ . By clause 3 of [F1] there are $A, B \in R$ with $x (t) = A \cos (ω t) + B \sin (ω t)$ for $t \in [0, T]$ ; the condition $x (0) = 0$ gives $A = 0$ , and then $x (T) = B \sin (n π) = 0$ holds automatically by [F2], so $x = x_{B}$ . Conversely every $x_{B}$ is a solution by step 1.1 and satisfies $x_{B} (T) = B \sin (n π) = 0$ . Hence the solution set of the Dirichlet problem is exactly ${B \sin (ω t) : B \in R} = {x_{A} : A \in R}$ , which is a linear subspace containing the nonzero function $\sin (ω t)$ and is therefore one-dimensional.

3.1step 2.2F1F2algebra

Initial-value uniqueness and contrast: by clause 4 of [F1] the initial-value problem with data $(x_{0}, v_{0})$ has exactly one solution on $R$ , with the displayed trigonometric form; for $A \neq A^{'}$ the solutions $x_{A}$ and $x_{A^{'}}$ of the boundary-value problem are distinct (they differ at $t = π / (2 ω)$ , which lies in $[0, T]$ because $T \geq π / ω$ , and $\sin (π / 2) \neq 0$ by the zero-set statement of [F2]) although they share the endpoint data $(0, 0)$ and differ in initial velocity $A ω \neq A^{'} ω$ ; this is the announced contrast between the two problems.

4.1step 1.1step 2.2F3∎

Stationary curves: by [F3] and step 1.1, $E (x_{A}) = - ω^{2} x_{A} - x_{A}^{''} = 0$ on $[0, T]$ , so every $x_{A}$ is stationary for the action; if $T = n π / ω$ , a stationary curve on $[0, T]$ with $x (0) = x (T) = 0$ is a $C^{2}$ solution of $m x^{''} + k x = 0$ with those endpoint values by [F3], hence is one of the $x_{A}$ by step 2.2. This proves clause 4.

Remarks

At $T = π / ω$ the second-variation value in direction $η_{1} = \sin (ω t)$ of Second variation of the oscillator action on a finite interval: both signs for $T > π / ω$ and the value at $T = π / ω$ is zero and the Dirichlet solution space is one-dimensional. More generally, its nonzero solutions occur exactly when $T = n π / ω$ for an integer $n \geq 1$ , as clauses 1-2 show. The computations here are mathematical statements about the model; no physical forcing or measured period is asserted.
The one-parameter family ${x_{A}}$ is not an artefact of dropping a hypothesis: it persists as the full solution set of the Dirichlet problem, and it is a legitimate underdetermined boundary-value problem, in contrast with the exactly solvable initial-value problem.

DefinitionDefinition: AI-adaptedProof: Not applicableprecheck passOpen item page →

The inertia tensor of a finite bounded Borel measure about any point of $R^{3}$

Definition

Let $B (R^{3})$ be the Borel sigma-algebra of $R^{3}$ (The Borel sigma-algebra of a topological space), let $ν$ be a measure on the measurable space $(R^{3}, B (R^{3}))$ (Measures on sigma-algebras, Measure spaces) that is finite and bounded: $ν (R^{3}) < + \infty$ and $ν (R^{3} ∖ {\overline{B}}_{R} (0)) = 0$ for some real $R > 0$ (Open ball, closed ball and sphere in a metric space). Put $m : = ν (R^{3}) \in [0, + \infty)$ ; nonnegativity follows from the definition of measure Measures on sigma-algebras. If $m > 0$ , then $ν$ is a mass distribution in the sense of Mass distributions on $R^{3}$ : total mass, first moment and inertia matrix. If $m = 0$ , then for every Borel set $E \subseteq R^{3}$ one has $0 \leq ν (E) \leq ν (R^{3}) = 0$ , so $ν$ is the zero measure. Integrals against $ν$ are Lebesgue integrals as in Integral over a measurable subset and Integrable real and complex functions, and their integrals, defined componentwise for vector- and matrix-valued integrands. When $m > 0$ , recall that the inertia matrix of $ν$ is

$I (ν) = \int (∥ ρ ∥_{2}^{2} I_{3} - ρ ρ^{T}) d ν (ρ) \in M_{3} (R),$

with $I_{3}$ the identity matrix and entrywise integrals $I (ν)_{j k} = \int (∥ ρ ∥_{2}^{2} δ_{j k} - ρ_{j} ρ_{k}) d ν$ , where $∥ \cdot ∥_{2}$ and the matrix conventions are those of The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , The vector space $M_{m \times n} (F) : = F^{m \times n}$ of $m$ by $n$ matrices over a field, with entrywise operations and Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes.

Shifted integrand and inertia tensor about a point. For $a \in R^{3}$ define the component functions

$G_{a} (ρ)_{j k} : = ∥ ρ - a ∥_{2}^{2} δ_{j k} - (ρ_{j} - a_{j}) (ρ_{k} - a_{k}) (j, k \in {1, 2, 3}),$

equivalently the matrix-valued function $G_{a} (ρ) = ∥ ρ - a ∥_{2}^{2} I_{3} - (ρ - a) (ρ - a)^{T}$ , and define the inertia tensor of $ν$ about $a$ $I_{ν} (a) \in M_{3} (R)$ by its entries

$I_{ν} (a)_{j k} : = \int G_{a} (ρ)_{j k} d ν (ρ) .$

Under the Axiom of Countable Choice ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )) each entry is a finite real number; this is the content of Finiteness and a uniform bound for the entries of the inertia tensor about an arbitrary point ↗, which depends on this definition only for its notation. For $a = 0$ the shifted integrand is the parent integrand $∥ ρ ∥_{2}^{2} I_{3} - ρ ρ^{T}$ . Thus $I_{ν} (0) = I (ν)$ when $m > 0$ ; if $m = 0$ , the parent definition does not define $I (ν)$ , while the shifted integral remains defined and equals the zero matrix $0_{3 \times 3}$ for every $a$ .

Scope. The definition names a mathematical function $a \mapsto I_{ν} (a)$ from $R^{3}$ to $M_{3} (R)$ determined by any finite bounded Borel measure $ν$ and its coordinate origin. For the zero measure this function is identically $0_{3 \times 3}$ . No physical body, unit system or measured mass is asserted. No translation identity for nonzero $a$ is asserted here; the centred, positive-total-mass case is proved separately on this page.

Remarks

The measure need not be atomless. Points, curves, surfaces and volumes are all admissible: $ν$ is an arbitrary bounded finite Borel measure, so finite sums of Dirac measures, lines and surface measures embedded in $R^{3}$ and absolutely continuous volume measures are all special cases, exactly as in Mass distributions on $R^{3}$ : total mass, first moment and inertia matrix.
Translation of the point, not of the measure. The point $a$ only shifts the reference point at which the second moments are computed; the measure and its coordinate representation are unchanged, and $μ (ν)$ is not assumed to vanish unless a consumer states it.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passOpen item page →

Finiteness and a uniform bound for the entries of the inertia tensor about an arbitrary point

Statement

Assume the Axiom of Countable Choice ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $ν$ be a measure on $(R^{3}, B (R^{3}))$ that is finite and bounded: $ν (R^{3}) < + \infty$ and $ν (R^{3} ∖ {\overline{B}}_{R} (0)) = 0$ for some real $R > 0$ (Open ball, closed ball and sphere in a metric space), and let $a \in R^{3}$ . With the shifted integrands $G_{a} (ρ)_{j k} = ∥ ρ - a ∥_{2}^{2} δ_{j k} - (ρ_{j} - a_{j}) (ρ_{k} - a_{k})$ of The inertia tensor of a finite bounded Borel measure about any point of $R^{3}$ (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ for the norm), then:

for all $j, k$ the function $G_{a} (\cdot)_{j k} : R^{3} \to R$ is Borel measurable and $ν$ -integrable (Borel measurable and Lebesgue measurable functions on $R^{n}$ );
each entry $I_{ν} (a)_{j k}$ is a finite real number and

$∣ I_{ν} (a)_{j k} ∣ \leq 2 (R + ∥ a ∥_{2})^{2} ν (R^{3}) .$

Facts & Assumptions

Given: A finite bounded Borel measure $ν$ on $R^{3}$ with $ν (R^{3} ∖ {\overline{B}}_{R} (0)) = 0$ , and a point $a \in R^{3}$ .

[L1]

Under ${A C}_{ω}$ every continuous map $R^{3} \to R$ is Borel measurable (Continuous functions on Euclidean spaces are Borel measurable, Borel measurable and Lebesgue measurable functions on $R^{n}$ ), and sums, scalar multiples and pointwise products of measurable real-valued functions are measurable (Arithmetic and lattice operations preserve measurability whenever they are defined).

[L2]

Estimates on the ball: for $ρ \in {\overline{B}}_{R} (0)$ one has $∥ ρ ∥_{2} \leq R$ and therefore $∥ ρ - a ∥_{2} \leq ∥ ρ ∥_{2} + ∥ a ∥_{2} \leq R + ∥ a ∥_{2}$ by the triangle inequality for the Euclidean norm (The inner-product norm is definite, homogeneous, and satisfies the triangle inequality, The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ); and for each index $j$ one has $(ρ_{j} - a_{j})^{2} \leq \sum_{l} (ρ_{l} - a_{l})^{2} = ∥ ρ - a ∥_{2}^{2}$ , because each term of a finite sum of nonnegative reals is at most the sum (Laws of finite sums and finite products, clause 4, The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

[L3]

The elementary inequality $2 u v \leq u^{2} + v^{2}$ for reals $u, v$ follows from $(u - v)^{2} \geq 0$ by squaring rules (Squares of nonzero elements are positive, Absolute value in an ordered field).

[L4]

Nonnegative integrals: the constant function with value $c \geq 0$ has $\int c d ν = c ν (R^{3})$ via the simple-function integral; the nonnegative integral is monotone and homogeneous for nonnegative scalars (The nonnegative Lebesgue integral, The integral of a nonnegative simple function, Monotonicity and nonnegative homogeneity of the nonnegative integral).

[L5]

A real measurable function $f$ with $\int ∣ f ∣ d ν < + \infty$ is $ν$ -integrable, and then $∣ \int f d ν ∣ \leq \int ∣ f ∣ d ν$ (Integrable real and complex functions, and their integrals, The modulus of an integral is bounded by the integral of the modulus, Integral over a measurable subset).

[L6]

Indefinite integrals and null sets (The indefinite integral of a nonnegative measurable function is a measure, A nonnegative integral over a null set vanishes, Integral over a measurable subset): for every nonnegative measurable $f$ the set function $A \mapsto \int_{A} f d ν$ is a measure, so $\int_{A \cup B} f d ν = \int_{A} f d ν + \int_{B} f d ν$ for disjoint measurable $A, B$ ; and if $A$ is $ν$ -null then $\int_{A} f d ν = 0$ .

Proof

Proof technique: direct; prove measurability, bound the shifted integrand pointwise on the support ball by a constant, and integrate the constant.

1.1givenL1L2

Measurability: the coordinate maps $ρ \mapsto ρ_{j}$ , the identity maps $ρ \mapsto a_{j}$ , and $ρ \mapsto ∥ ρ - a ∥_{2}^{2} = \sum_{l} (ρ_{l} - a_{l})^{2}$ are continuous, hence Borel measurable by [L1]; sums and products of these measurable functions are measurable by [L1], so each $G_{a} (\cdot)_{j k} = ∥ ρ - a ∥_{2}^{2} δ_{j k} - (ρ_{j} - a_{j}) (ρ_{k} - a_{k})$ is Borel measurable.

1.2givenL2L3algebra

Pointwise bound on the support ball: for $ρ \in {\overline{B}}_{R} (0)$ , by [L2] and [L3], $∣ G_{a} (ρ)_{j k} ∣ \leq ∥ ρ - a ∥_{2}^{2} + ∣ ρ_{j} - a_{j} ∣ ∣ ρ_{k} - a_{k} ∣ \leq ∥ ρ - a ∥_{2}^{2} + \frac{1}{2} ((ρ_{j} - a_{j})^{2} + (ρ_{k} - a_{k})^{2}) \leq 2 ∥ ρ - a ∥_{2}^{2} \leq 2 (R + ∥ a ∥_{2})^{2} .$

2.1step 1.1step 1.2givenL4L5L6algebra∎

Integrability and the bound: the function $∣ G_{a} (\cdot)_{j k} ∣$ is nonnegative and measurable by step 1.1, so [L6] applied to the disjoint measurable sets ${\overline{B}}_{R} (0)$ and $N : = R^{3} ∖ {\overline{B}}_{R} (0)$ , the latter $ν$ -null, gives $\int ∣ G_{a} (\cdot)_{j k} ∣ d ν = \int_{{\overline{B}}_{R} (0)} ∣ G_{a} (\cdot)_{j k} ∣ d ν + \int_{N} ∣ G_{a} (\cdot)_{j k} ∣ d ν = \int_{{\overline{B}}_{R} (0)} ∣ G_{a} (\cdot)_{j k} ∣ d ν$ . On ${\overline{B}}_{R} (0)$ the integrand is bounded by the constant $M : = 2 (R + ∥ a ∥_{2})^{2}$ by step 1.2, so monotonicity in [L4] applied to the pointwise inequality $∣ G_{a} (\cdot)_{j k} ∣ χ_{{\overline{B}}_{R} (0)} \leq M χ_{{\overline{B}}_{R} (0)} \leq M$ , and the constant-value formula, give $\int ∣ G_{a} (\cdot)_{j k} ∣ d ν \leq \int M d ν = M ν (R^{3}) < + \infty$ . By step 1.1 and [L5] the function $G_{a} (\cdot)_{j k}$ is $ν$ -integrable, its integral $I_{ν} (a)_{j k}$ is a finite real number, and $∣ I_{ν} (a)_{j k} ∣ = ∣ \int G_{a} (\cdot)_{j k} d ν ∣ \leq \int ∣ G_{a} (\cdot)_{j k} ∣ d ν \leq 2 (R + ∥ a ∥_{2})^{2} ν (R^{3})$ .

Remarks

The bound is uniform in the shape of the measure: it uses only the support radius $R$ , the shift $∥ a ∥_{2}$ and the total mass $ν (R^{3})$ , not the detailed distribution. For $a = 0$ it reproduces the bound $2 R^{2} ν (R^{3})$ of the shifted integrand computed at the origin.
The Axiom of Countable Choice is used exactly once, in [L1], to obtain the Borel measurability of the continuous integrands; every later consumer of this finiteness statement carries the assumption explicitly.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passOpen item page →

Parallel-axis theorem: the inertia tensor about a displaced point of a centred mass distribution

Statement

Assume the Axiom of Countable Choice ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )), used only to make the displayed integrals finite. Let $ν$ be a mass distribution on $R^{3}$ with total mass $m = ν (R^{3}) \in (0, + \infty)$ that is centred, that is, $μ (ν) = \int ρ d ν (ρ) = 0 \in R^{3}$ (Mass distributions on $R^{3}$ : total mass, first moment and inertia matrix), and let $I (ν)$ be its inertia matrix. Then for every $a \in R^{3}$ the inertia tensor of $ν$ about $a$ (The inertia tensor of a finite bounded Borel measure about any point of $R^{3}$ ) satisfies

$I_{ν} (a) = I (ν) + m (∥ a ∥_{2}^{2} I_{3} - a a^{T}),$

where $∥ \cdot ∥_{2}$ is the Euclidean norm, $I_{3}$ the identity matrix and $a a^{T}$ the matrix product of The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , The vector space $M_{m \times n} (F) : = F^{m \times n}$ of $m$ by $n$ matrices over a field, with entrywise operations and Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes. Entrywise,

$I_{ν} (a)_{j k} = I (ν)_{j k} + m (∥ a ∥_{2}^{2} δ_{j k} - a_{j} a_{k}) (j, k \in {1, 2, 3}) .$

Facts & Assumptions

Given: A centred mass distribution $ν$ with total mass $m$ , a point $a \in R^{3}$ , and the notation of Mass distributions on $R^{3}$ : total mass, first moment and inertia matrix and The inertia tensor of a finite bounded Borel measure about any point of $R^{3}$ : the first moment $μ (ν)$ , the inertia matrix $I (ν)$ with $I (ν)_{j k} = \int (∥ ρ ∥_{2}^{2} δ_{j k} - ρ_{j} ρ_{k}) d ν$ , and the inertia tensor $I_{ν} (a)$ with $I_{ν} (a)_{j k} = \int (∥ ρ - a ∥_{2}^{2} δ_{j k} - (ρ_{j} - a_{j}) (ρ_{k} - a_{k})) d ν$ .

[L1]

Finiteness and integrability (Finiteness and a uniform bound for the entries of the inertia tensor about an arbitrary point, Finiteness of the moments of a bounded finite Borel measure on $R^{3}$ , Mass distributions on $R^{3}$ : total mass, first moment and inertia matrix): the functions $ρ \mapsto ρ_{j}$ , $ρ \mapsto ρ_{j} ρ_{k}$ , and the shifted polynomials $∥ ρ - a ∥_{2}^{2} δ_{j k} - (ρ_{j} - a_{j}) (ρ_{k} - a_{k})$ are $ν$ -integrable; the entries $I_{ν} (a)_{j k}$ , $I (ν)_{j k}$ and $μ (ν)_{j}$ are finite real numbers.

[L2]

Linearity of the Lebesgue integral on $L^{1}$ (The Lebesgue integral is linear on $L^{1} (μ)$ , Integrable real and complex functions, and their integrals, Integral over a measurable subset): for real $α, β$ and integrable real functions $f, g$ , the combination $α f + β g$ is integrable and $\int (α f + β g) d ν = α \int f d ν + β \int g d ν$ .

[L3]

Centredness and total mass (Mass distributions on $R^{3}$ : total mass, first moment and inertia matrix, The nonnegative Lebesgue integral, The integral of a nonnegative simple function): $\int ρ_{j} d ν = μ (ν)_{j} = 0$ for each $j$ , and the constant function $1$ has $\int 1 d ν = ν (R^{3}) = m$ .

[L4]

Component algebra (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes): for all $ρ, a \in R^{3}$ and all $j, k$ , $∥ ρ - a ∥_{2}^{2} = ∥ ρ ∥_{2}^{2} - 2 ⟨ ρ, a ⟩ + ∥ a ∥_{2}^{2}, (ρ_{j} - a_{j}) (ρ_{k} - a_{k}) = ρ_{j} ρ_{k} - ρ_{j} a_{k} - a_{j} ρ_{k} + a_{j} a_{k},$ and $⟨ ρ, a ⟩ = \sum_{l} a_{l} ρ_{l}$ .

Proof

Proof technique: direct; expand the shifted integrand into the parent integrand plus constants and linear terms, and integrate termwise, the linear terms vanishing by centredness.

1.1givenL4algebra

Expansion of the integrand: for every $ρ \in R^{3}$ and all $j, k$ , [L4] gives $∥ ρ - a ∥_{2}^{2} δ_{j k} - (ρ_{j} - a_{j}) (ρ_{k} - a_{k}) = [∥ ρ ∥_{2}^{2} δ_{j k} - ρ_{j} ρ_{k}] + [∥ a ∥_{2}^{2} δ_{j k} - a_{j} a_{k}] + [- 2 ⟨ ρ, a ⟩ δ_{j k} + ρ_{j} a_{k} + a_{j} ρ_{k}] .$

2.1step 1.1givenL1L2

Integrability of the pieces: the first bracket is integrable by [L1]; the second bracket is a constant function and hence integrable because $ν (R^{3}) < + \infty$ ; the functions $ρ \mapsto ρ_{j}$ are integrable by [L1], so the third bracket is a finite real linear combination of integrable functions and is integrable by [L2].

3.1step 1.1step 2.1L1L2L3algebra

Termwise integration: applying [L2] to the decomposition of step 1.1 and using the defining integrals of [L1] and the values of [L3], $I_{ν} (a)_{j k} = I (ν)_{j k} + m (∥ a ∥_{2}^{2} δ_{j k} - a_{j} a_{k}) - 2 δ_{j k} \sum_{l} a_{l} μ (ν)_{l} + a_{k} μ (ν)_{j} + a_{j} μ (ν)_{k},$ and every term of the last group vanishes because $μ (ν) = 0$ .

4.1step 3.1L4algebra∎

Conclusion in matrix form: reading the entrywise identity of step 3.1 as a matrix identity gives $I_{ν} (a) = I (ν) + m (∥ a ∥_{2}^{2} I_{3} - a a^{T})$ , which is the statement.

Remarks

Centredness is exactly what is used. The proof shows that for a general mass distribution the same expansion leaves the additional terms $- 2 (⟨ a, μ (ν) ⟩) δ_{j k} + a_{k} μ (ν)_{j} + a_{j} μ (ν)_{k}$ ; the centred case is the classical parallel-axis form, and the theorem asserts nothing about the non-centred case beyond this displayed expansion.
Shape independence. The derivation uses only the finiteness of the first and second moments and the vanishing of the first moment, so the conclusion covers positive-total-mass point, line, surface and volume distributions alike: $ν$ is an arbitrary bounded finite Borel measure of positive total mass, as in Mass distributions on $R^{3}$ : total mass, first moment and inertia matrix.

PropositionStatement: AI-adaptedProof: AI-adaptedprecheck passOpen item page →

Two equal masses with two outer springs and a coupling spring: eigenmodes, decoupling and the explicit normal frequencies

Statement

Let $m > 0$ , $k \geq 0$ and $c \geq 0$ , and put

$K : = (\begin{array}{cc} k + c & - c \\ - c & k + c \end{array}), u_{+} : = \frac{1}{\sqrt{2}} (\begin{array}{c} 1 \\ 1 \end{array}), u_{-} : = \frac{1}{\sqrt{2}} (\begin{array}{c} 1 \\ - 1 \end{array}),$

and $ω_{+} : = (k / m)^{1 / 2}$ , $ω_{-} : = ((k + 2 c) / m)^{1 / 2}$ (nonnegative square roots, Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ). Consider the linear system

$m x^{''} (t) = - K x (t)$

for $C^{2}$ curves $x : J \to R^{2}$ on intervals $J \subseteq R$ with nonempty interior (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length, The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral). The vector equation and its scalar mode equations are autonomous equations with time domain $R$ ; a solution on $J$ is their restriction to that solution interval. Every such local solution extends uniquely to the displayed global family. Global growth claims below refer to that extension. Then:

$K u_{+} = k u_{+}$ and $K u_{-} = (k + 2 c) u_{-}$ ; the vectors $u_{+}, u_{-}$ are orthonormal, and every $x \in R^{2}$ satisfies $x = ⟨ u_{+}, x ⟩ u_{+} + ⟨ u_{-}, x ⟩ u_{-}$ (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ );
$x$ is a solution if and only if there are solutions $y_{+}, y_{-} : J \to R$ of the scalar equations

$m y_{+}^{''} + k y_{+} = 0, m y_{-}^{''} + (k + 2 c) y_{-} = 0$

of The damped driven oscillator model: second-order equation, phase-plane system and characteristic data with $x = y_{+} u_{+} + y_{-} u_{-}$ ; the pair $(y_{+}, y_{-})$ is unique and is given by $y_{\pm} = ⟨ u_{\pm}, x ⟩$ ; 3. consequently, for $k > 0$ the solutions are exactly the curves

$x (t) = (A_{+} \cos (ω_{+} t) + B_{+} \sin (ω_{+} t)) u_{+} + (A_{-} \cos (ω_{-} t) + B_{-} \sin (ω_{-} t)) u_{-} (A_{\pm}, B_{\pm} \in R),$

that is, the system is a superposition of an in-phase normal mode with squared frequency $k / m$ and an anti-phase normal mode with squared frequency $(k + 2 c) / m$ (The homogeneous damped oscillator: solution classification by the discriminant and uniqueness for initial data); 4. if $k = 0$ and $c \geq 0$ , then $K u_{+} = 0$ , and the curves $x (t) = (A + B t) u_{+}$ ( $A, B \in R$ ) are solutions; for $B \neq 0$ each such curve has a global extension unbounded on $[0, \infty)$ , so the zero-frequency mode is affine rather than oscillatory. The bijection of clause 2 remains valid with the scalar equations $m y_{+}^{''} = 0$ and $m y_{-}^{''} + 2 c y_{-} = 0$ , and for $c > 0$ the $u_{-}$ -component is the trigonometric family with $ω_{-} = (2 c / m)^{1 / 2}$ (The homogeneous damped oscillator: solution classification by the discriminant and uniqueness for initial data); if $c = 0$ , it is affine as well (The degenerate and repulsive oscillator: solutions for k=0 and the explicit growing solution for k<0).

Facts & Assumptions

Given: The parameters $m > 0$ , $k \geq 0$ , $c \geq 0$ , the matrix $K$ and vectors $u_{\pm}$ , and the system $m x^{''} = - K x$ on intervals $J$ with nonempty interior.

[F1]

Matrix and vector data (Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes, The vector space $M_{m \times n} (F) : = F^{m \times n}$ of $m$ by $n$ matrices over a field, with entrywise operations, The transpose $A^{T}$ of a matrix, The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ): $K$ is symmetric, $K_{12} = K_{21} = - c$ ; the Euclidean inner product of $R^{2}$ is the componentwise sum $⟨ u, v ⟩ = u_{1} v_{1} + u_{2} v_{2}$ ; and $⟨ u_{+}, u_{+} ⟩ = ⟨ u_{-}, u_{-} ⟩ = 1$ , $⟨ u_{+}, u_{-} ⟩ = 0$ .

[F2]

Scalar equations and their solutions (The damped driven oscillator model: second-order equation, phase-plane system and characteristic data, The homogeneous damped oscillator: solution classification by the discriminant and uniqueness for initial data, The degenerate and repulsive oscillator: solutions for k=0 and the explicit growing solution for k<0, Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ , The addition formulas for sine and cosine): for $μ > 0$ , put $ω = (μ / m)^{1 / 2}$ . For any scalar solution $y : J \to R$ of $m y^{''} + μ y = 0$ , choose $t_{0} \in J$ , put $J_{0} : = {s \in R : t_{0} + s \in J}$ and define $\tilde{y} (s) : = y (t_{0} + s)$ for $s \in J_{0}$ . Then $0 \in J_{0}$ , $J_{0}$ has nonempty interior, and autonomy gives $m {\tilde{y}}^{''} + μ \tilde{y} = 0$ on $J_{0}$ . The homogeneous-oscillator classification applies there, so $\tilde{y} (s) = \tilde{A} \cos (ω s) + \tilde{B} \sin (ω s)$ . The addition formulas then give $y (t) = A \cos (ω t) + B \sin (ω t)$ on $J$ , where $A = \tilde{A} \cos (ω t_{0}) - \tilde{B} \sin (ω t_{0})$ and $B = \tilde{A} \sin (ω t_{0}) + \tilde{B} \cos (ω t_{0})$ . Conversely these unshifted families solve the scalar equation on every interval. For the zero-stiffness equation $m y^{''} = 0$ , the same translation and the degenerate oscillator classification give $\tilde{y} (s) = \tilde{A} + \tilde{B} s$ ; restoring the constants gives $y (t) = A + B t$ with $A = \tilde{A} - \tilde{B} t_{0}$ and $B = \tilde{B}$ , and every such affine function solves the equation.

[F3]

Vector-valued calculus (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral, 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, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length): derivatives of $R^{2}$ -valued curves are computed componentwise; for a $C^{2}$ curve $x$ and a constant $u \in R^{2}$ the real function $t \mapsto ⟨ u, x (t) ⟩$ is $C^{2}$ with first derivative $⟨ u, x^{'} (t) ⟩$ and second derivative $⟨ u, x^{''} (t) ⟩$ ; and if $y_{+}, y_{-}$ are $C^{2}$ real functions then $t \mapsto y_{+} (t) u_{+} + y_{-} (t) u_{-}$ is a $C^{2}$ curve with second derivative $y_{+}^{''} u_{+} + y_{-}^{''} u_{-}$ .

Proof

Proof technique: direct; verify the eigenrelations by matrix multiplication, decouple the system in the orthonormal eigenbasis, and read the scalar solution families off the classification theorem.

1.1givenF1algebra

Eigenrelations and expansion: direct multiplication gives $K u_{+} = \frac{1}{\sqrt{2}} (\begin{array}{c} (k + c) - c \\ - c + (k + c) \end{array}) = \frac{k}{\sqrt{2}} (\begin{array}{c} 1 \\ 1 \end{array}) = k u_{+}, K u_{-} = \frac{1}{\sqrt{2}} (\begin{array}{c} (k + c) + c \\ - c - (k + c) \end{array}) = (k + 2 c) u_{-},$ and $⟨ u_{+}, u_{-} ⟩ = \frac{1}{2} (1 - 1) = 0$ , $⟨ u_{\pm}, u_{\pm} ⟩ = \frac{1}{2} (1 + 1) = 1$ ; also $⟨ u_{+}, x ⟩ = \frac{1}{\sqrt{2}} (x_{1} + x_{2})$ and $⟨ u_{-}, x ⟩ = \frac{1}{\sqrt{2}} (x_{1} - x_{2})$ , so $⟨ u_{+}, x ⟩ u_{+} + ⟨ u_{-}, x ⟩ u_{-} = x$ for every $x$ , and $K$ is symmetric since $K_{12} = K_{21} = - c$ .

2.1givenstep 1.1F3algebra

From a solution to scalar solutions: let $x : J \to R^{2}$ be a $C^{2}$ solution of $m x^{''} = - K x$ and set $y_{\pm} (t) : = ⟨ u_{\pm}, x (t) ⟩$ . By [F3] the functions $y_{\pm}$ are $C^{2}$ and $m y_{\pm}^{''} = m ⟨ u_{\pm}, x^{''} ⟩ = - ⟨ u_{\pm}, K x ⟩$ ; since $K$ is symmetric, $⟨ u_{\pm}, K x ⟩ = u_{\pm}^{T} K x = (K u_{\pm})^{T} x = ⟨ K u_{\pm}, x ⟩$ , and step 1.1 gives $K u_{+} = k u_{+}$ , $K u_{-} = (k + 2 c) u_{-}$ ; hence $m y_{+}^{''} + k y_{+} = 0$ and $m y_{-}^{''} + (k + 2 c) y_{-} = 0$ on $J$ .

2.2givenstep 1.1F3algebra

From scalar solutions to a solution: conversely, let $y_{+}, y_{-} : J \to R$ be $C^{2}$ solutions of the two scalar equations and put $x : = y_{+} u_{+} + y_{-} u_{-}$ . By [F3] the curve $x$ is $C^{2}$ and $m x^{''} = m y_{+}^{''} u_{+} + m y_{-}^{''} u_{-} = - k y_{+} u_{+} - (k + 2 c) y_{-} u_{-} = - (y_{+} K u_{+} + y_{-} K u_{-}) = - K x$ by step 1.1, so $x$ solves the system.

3.1step 1.1step 2.1step 2.2

Bijection: the two constructions are mutually inverse. If $x$ is a solution, then the pair $y_{\pm} = ⟨ u_{\pm}, x ⟩$ of step 2.1 reconstructs $x$ by the expansion identity of step 1.1; if $(y_{+}, y_{-})$ is a pair of scalar solutions, then the coordinates of $x = y_{+} u_{+} + y_{-} u_{-}$ are $⟨ u_{\pm}, x ⟩ = ⟨ u_{\pm}, u_{+} ⟩ y_{+} + ⟨ u_{\pm}, u_{-} ⟩ y_{-} = y_{\pm}$ by the orthonormality of step 1.1. Hence clause 2 holds, including uniqueness of the pair.

4.1step 3.1F2algebra

Frequencies on an arbitrary interval: assume $k > 0$ and choose $t_{0} \in J$ . For scalar components $y_{\pm}$ from clause 2, the translated functions ${\tilde{y}}_{\pm} (s) : = y_{\pm} (t_{0} + s)$ are defined on $J - t_{0}$ , which contains $0$ and has nonempty interior, and solve the same autonomous scalar equations. Apply [F2] to obtain the trigonometric families in $s$ with frequencies $ω_{+} = (k / m)^{1 / 2}$ and $ω_{-} = ((k + 2 c) / m)^{1 / 2}$ . The addition formulas in [F2] restore constants $A_{\pm}, B_{\pm}$ and give $y_{\pm} (t) = A_{\pm} \cos (ω_{\pm} t) + B_{\pm} \sin (ω_{\pm} t)$ on $J$ . Conversely each displayed scalar family solves its equation on $J$ ; the bijection of step 3.1 therefore gives exactly the vector solutions in clause 3, with the $u_{+}$ -mode (both coordinates equal) in phase and the $u_{-}$ -mode (opposite coordinates) anti-phase.

5.1step 1.1step 3.1F2algebra∎

Degenerate case on an arbitrary interval: let $k = 0$ , $c \geq 0$ , and choose $t_{0} \in J$ . Step 1.1 gives $K u_{+} = 0$ , so for $x (t) = (A + B t) u_{+}$ one has $m x^{''} = 0$ and $- K x = - (A + B t) K u_{+} = 0$ : the family consists of solutions. The same formula defines $x$ on all of $R$ , and if $B \neq 0$ its global extension has $∥ x (t) ∥_{2} = ∣ A + B t ∣$ unbounded on $[0, \infty)$ . The translations ${\tilde{y}}_{\pm} (s) : = y_{\pm} (t_{0} + s)$ of the scalar components are defined on $J - t_{0}$ and satisfy $m {\tilde{y}}_{+}^{''} = 0$ , $m {\tilde{y}}_{-}^{''} + 2 c {\tilde{y}}_{-} = 0$ . By [F2], ${\tilde{y}}_{+}$ is affine, and restoring constants gives $y_{+} (t) = A + B t$ ; if $c = 0$ the same affine classification applies to ${\tilde{y}}_{-}$ , while if $c > 0$ the homogeneous-oscillator classification gives the trigonometric family for ${\tilde{y}}_{-}$ and the addition formulas restore its constants to the stated family with $ω_{-} = (2 c / m)^{1 / 2}$ . The bijection of step 3.1 remains valid and establishes clause 4. In both stiffness cases the scalar classifications give a unique global extension of each component, and the inverse modal transform gives the unique global vector extension claimed in the statement.

Remarks

The system is the Euler-Lagrange equation of the Lagrangian $\frac{1}{2} m ({\dot{x}}_{1}^{2} + {\dot{x}}_{2}^{2}) - \frac{1}{2} k (x_{1}^{2} + x_{2}^{2}) - \frac{1}{2} c (x_{1} - x_{2})^{2}$ for two equal masses attached to fixed walls by equal springs of stiffness $k$ and coupled by a middle spring of stiffness $c$ ; the proposition states the mathematics of that model only, and no physical identification of $m, k, c$ is asserted.
The $k = 0$ clause is the zero-frequency caution: a vanishing eigenvalue produces affine rather than oscillatory motion, so no nonzero frequency can be read off from the eigenrelation $K u_{+} = k u_{+}$ in that case.

PropositionStatement: AI-adaptedProof: AI-adaptedprecheck passOpen item page →

The pendulum field near the downward equilibrium: bounded force derivative, cubic remainder and the finite-time small-angle error bound

Statement

Let $g > 0$ and $l > 0$ , put $ω : = (g / l)^{1 / 2} > 0$ (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ), and define the field

$F : R^{2} \to R^{2}, F (θ, v) : = (v, - ω^{2} \sin θ),$

so that $z^{'} = F (z)$ for $z = (θ, v)$ is the first-order form of the pendulum equation $θ^{''} = - ω^{2} \sin θ$ (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral for the componentwise first-order reduction). Put

$A : = (\begin{array}{cc} 0 & 1 \\ - ω^{2} & 0 \end{array}), L : = \max {1, ω^{2}} .$

Then:

$F$ is of class $C^{\infty}$ (in particular continuous and locally Lipschitz in the state variable), $F (0) = 0$ , $A = D F (0)$ is the total derivative of $F$ at the origin, and for every $r > 0$ and every $z = (θ, v)$ with $∥ z ∥_{2} \leq r$ (Open ball, closed ball and sphere in a metric space for the ball, The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ for the norm)

$∥ F (z) - A z ∥_{2} = ω^{2} ∣ \sin θ - θ ∣ \leq \frac{ω^{2}}{6} ∣ θ ∣^{3} \leq \frac{ω^{2} r}{6} ∥ z ∥_{2}^{2}, ∥ F (z) ∥_{2} \leq L ∥ z ∥_{2};$

moreover $F$ is globally Lipschitz in the state variable with constant $L$ (Lipschitz map, $α$ -Hölder map for rational $0 < α \leq 1$ , and contraction), and the operator norm of $A$ for the Euclidean norm is $∥ A ∥ = L$ (The operator norm as the least bound and as the unit-sphere or unit-ball supremum); 2. let $z_{0} \in R^{2}$ with $δ : = ∥ z_{0} ∥_{2} > 0$ , let $T > 0$ and $r > 0$ satisfy $δ e^{L T} < r$ , and let $y : R \to R^{2}$ be the solution of the linear initial value problem $y^{'} = A y$ , $y (0) = z_{0}$ (Variation of constants for $z^{'} = A z + b (t)$ via the matrix exponential). Then the maximal solution $z$ of $z^{'} = F (z)$ , $z (0) = z_{0}$ , is defined on $[0, T]$ with $∥ z (t) ∥_{2} \leq δ e^{L t}$ for $t \in [0, T]$ , and for every $t \in [0, T]$

$∥ z (t) - y (t) ∥_{2} \leq \frac{ω^{2} r}{6} δ^{2} \int_{0}^{t} e^{∥ A ∥ (t - s)} e^{2 L s} d s \leq \frac{ω^{2} r}{6} δ^{2} t e^{(∥ A ∥ + 2 L) t}$

(Finite-time linearization error bound: quadratic remainder, exponential growth bound and the variation-of-constants estimate); 3. the linear system $y^{'} = A y$ is the linearised pendulum: writing $y = (y_{1}, y_{2})$ one has $y_{1}^{''} = - ω^{2} y_{1}$ and $y_{2} = y_{1}^{'}$ , and the first components satisfy $∣ z_{1} (t) - y_{1} (t) ∣ \leq ∥ z (t) - y (t) ∥_{2}$ with the bounds of clause 2. The estimate is a finite-time statement of order $δ^{2}$ : it neither states nor implies that the nonlinear pendulum is exactly harmonic, and it makes no claim beyond $[0, T]$ .

Facts & Assumptions

Given: The parameters $g > 0$ , $l > 0$ , the number $ω = (g / l)^{1 / 2}$ , the field $F (θ, v) = (v, - ω^{2} \sin θ)$ , the matrix $A$ and the constant $L = \max {1, ω^{2}}$ .

[F1]

The linearisation theorem (Finite-time linearization error bound: quadratic remainder, exponential growth bound and the variation-of-constants estimate): if $F : U \to R^{n}$ is continuous and locally Lipschitz in the state variable on an open $U ∋ 0$ , and $r > 0$ , $C \geq 0$ , $L \geq 0$ , $A \in M_{n} (R)$ satisfy $\overline{B} (0, r) \subseteq U$ , $∥ F (z) - A z ∥_{2} \leq C ∥ z ∥_{2}^{2}$ , $∥ F (z) ∥_{2} \leq L ∥ z ∥_{2}$ for $∥ z ∥_{2} \leq r$ , then for every datum with $δ : = ∥ z_{0} ∥_{2} > 0$ and every $T > 0$ with $δ e^{L T} < r$ the maximal solution $z$ of $z^{'} = F (z)$ , $z (0) = z_{0}$ is defined on $[0, T]$ , satisfies $∥ z (t) ∥_{2} \leq δ e^{L t}$ , and with the solution $y$ of $y^{'} = A y$ , $y (0) = z_{0}$ obeys the two displayed bounds with $∥ A ∥$ the operator norm.

[F2]

Trigonometric calculus (The derivatives of sine and cosine are cosine and minus sine, Sine and cosine defined by their real power series, Signs, monotonicity intervals, and ranges of sine and cosine, 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)$ , A uniform derivative bound gives a uniform Taylor remainder bound, The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ): $\sin$ and $\cos$ are differentiable with $\sin^{'} = \cos$ , $\cos^{'} = - \sin$ , $\sin 0 = 0$ ; both have range $[- 1, 1]$ ; for all reals $θ, θ^{'}$ the mean value theorem gives $∣ \sin θ - \sin θ^{'} ∣ \leq ∣ θ - θ^{'} ∣$ and $∣ \sin θ ∣ \leq ∣ θ ∣$ ; and the Taylor remainder bound with $n = 2$ and $M = 1$ gives $∣ \sin θ - θ ∣ \leq ∣ θ ∣^{3} / 6$ for every real $θ$ .

[F3]

Total derivative (The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case, If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative, The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder, $C^{k}$ Euclidean maps and diffeomorphisms): the partial derivatives of $F$ are $\partial F_{1} / \partial θ = 0$ , $\partial F_{1} / \partial v = 1$ , $\partial F_{2} / \partial θ = - ω^{2} \cos θ$ , $\partial F_{2} / \partial v = 0$ , all continuous, so $F$ is $C^{1}$ with $D F (θ, v) = (\begin{array}{cc} 0 & 1 \\ - ω^{2} \cos θ & 0 \end{array})$ ; a $C^{1}$ map is continuous and locally Lipschitz in the state variable (Lipschitz map, $α$ -Hölder map for rational $0 < α \leq 1$ , and contraction, The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ).

[F4]

Norms (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , Real and complex inner product spaces, with the inner product linear in the first argument, The operator norm as the least bound and as the unit-sphere or unit-ball supremum, Open ball, closed ball and sphere in a metric space): for $z = (θ, v)$ , $∥ z ∥_{2}^{2} = θ^{2} + v^{2}$ , $∥ A z ∥_{2}^{2} = ω^{4} θ^{2} + v^{2}$ , $∥ F (z) ∥_{2}^{2} = v^{2} + ω^{4} \sin^{2} θ$ and $∥ F (z) - A z ∥_{2}^{2} = ω^{4} (\sin θ - θ)^{2}$ ; the operator norm of $A$ is the supremum of $∥ A z ∥_{2}$ over $∥ z ∥_{2} \leq 1$ .

[F5]

Linear systems (Variation of constants for $z^{'} = A z + b (t)$ via the matrix exponential, The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral, 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, Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes): for every datum there is exactly one solution of $y^{'} = A y$ on $R$ ; the equation $y^{'} = A y$ is the pair $y_{1}^{'} = y_{2}$ , $y_{2}^{'} = - ω^{2} y_{1}$ .

Proof

Proof technique: direct; compute the derivative of the pendulum field, bound the quadratic remainder by the cubic sine estimate, identify the Lipschitz and operator norms, and instantiate the linearisation theorem.

1.1givenF2F3algebra

Derivative and regularity: by [F3], $F$ is $C^{1}$ with $D F (θ, v) = (\begin{array}{cc} 0 & 1 \\ - ω^{2} \cos θ & 0 \end{array})$ ; since $\sin$ and $\cos$ are $C^{\infty}$ the field is in fact $C^{\infty}$ . Also $F (0, 0) = (0, - ω^{2} \sin 0) = (0, 0)$ and $A = D F (0, 0) = (\begin{array}{cc} 0 & 1 \\ - ω^{2} & 0 \end{array})$ .

1.2givenF2F4algebra

Remainder and growth bounds: for $∥ z ∥_{2} \leq r$ , [F2] gives $∥ F (z) - A z ∥_{2} = ω^{2} ∣ \sin θ - θ ∣ \leq \frac{ω^{2}}{6} ∣ θ ∣^{3}$ , and $∣ θ ∣^{3} \leq r θ^{2} \leq r (θ^{2} + v^{2}) = r ∥ z ∥_{2}^{2}$ ; moreover $∥ F (z) ∥_{2}^{2} = v^{2} + ω^{4} \sin^{2} θ \leq v^{2} + ω^{4} θ^{2} \leq L^{2} (θ^{2} + v^{2})$ because $L = \max {1, ω^{2}}$ , so $∥ F (z) ∥_{2} \leq L ∥ z ∥_{2}$ .

2.1step 1.2F2F4algebra

Lipschitz constant and operator norm: for $z = (θ, v)$ and $z^{'} = (θ^{'}, v^{'})$ , $∥ F (z) - F (z^{'}) ∥_{2}^{2} = (v - v^{'})^{2} + ω^{4} (\sin θ - \sin θ^{'})^{2} \leq (v - v^{'})^{2} + ω^{4} (θ - θ^{'})^{2} \leq L^{2} ∥ z - z^{'} ∥_{2}^{2}$ by [F2] and $L = \max {1, ω^{2}}$ , so $L$ is a global Lipschitz constant for $F$ ; and $∥ A z ∥_{2}^{2} = ω^{4} θ^{2} + v^{2} \leq L^{2} ∥ z ∥_{2}^{2}$ with equality at $e_{1}$ if $ω^{2} \geq 1$ and at $e_{2}$ if $1 \geq ω^{2}$ , so the operator norm is $∥ A ∥ = L$ .

3.1step 1.1step 1.2step 2.1F1given

Instantiation of the linearisation theorem: take $n = 2$ , $U = R^{2}$ , the field $F$ of clause 1, the matrix $A$ , the constants $L$ and $C : = ω^{2} r / 6$ , and the datum $z_{0}$ with $δ = ∥ z_{0} ∥_{2} > 0$ and $δ e^{L T} < r$ . Steps 1.1, 1.2 and 2.1 verify every hypothesis of [F1], so the maximal solution $z$ of $z^{'} = F (z)$ , $z (0) = z_{0}$ is defined on $[0, T]$ , $∥ z (t) ∥_{2} \leq δ e^{L t}$ there, and the two integral bounds of [F1] hold with the displayed $C$ and $∥ A ∥ = L$ ; this is clause 2.

4.1step 3.1F4F5algebra∎

Linearised equation and scope: by [F5] the system $y^{'} = A y$ reads $y_{1}^{'} = y_{2}$ , $y_{2}^{'} = - ω^{2} y_{1}$ , hence $y_{1}^{''} = - ω^{2} y_{1}$ , the exactly harmonic linearised pendulum; and $∣ z_{1} (t) - y_{1} (t) ∣ \leq ∥ z (t) - y (t) ∥_{2}$ because $∥ (w_{1}, w_{2}) ∥_{2}^{2} = w_{1}^{2} + w_{2}^{2}$ . The bounds of clause 2 are finite-time and of order $δ^{2}$ ; no identification of the nonlinear solution with the harmonic one beyond this estimate is claimed.

Remarks

The constant $ω^{2} r / 6$ is exactly the quadratic-remainder constant obtained from the cubic bound $∣ \sin θ - θ ∣ \leq ∣ θ ∣^{3} / 6$ on the ball of radius $r$ : the remainder is cubic in the angle and quadratic in the state norm, which is what the linearisation theorem of Finite-time linearization error bound: quadratic remainder, exponential growth bound and the variation-of-constants estimate requires.
The scope sentence of clause 3 is part of the claim: the estimate is a conditional consequence of the explicit model $θ^{''} = - ω^{2} \sin θ$ and its stated smallness hypotheses, and it is not a statement about any measured pendulum.

RemarkRemark: AI-adaptedProof: Not applicableOpen item page →

Scope and limits of the verification items on this page

Scope of the verification items

Every item on this page is mathematics: the oscillator, the two-mass spring system, the pendulum field and the mass distributions are mathematical objects with explicit parameters, and no item asserts a physical law, a unit convention or a measured value. The following limits belong to the claims and must be carried by any consumer.

The second-variation sign results are finite-time statements about the action. The definition The fixed-endpoint second variation of a time-dependent action at a curve and the formula of The second variation of a time-dependent action: twice differentiability of the fixed-endpoint family and the Hessian integral formula concern the fixed-endpoint family $q + ε η$ of a $C^{2}$ Lagrangian chart on a compact interval and produce one real number per pair $(q, η)$ . The saddle computation of Second variation of the oscillator action on a finite interval: both signs for $T > π / ω$ and the value at $T = π / ω$ is a statement about the action functional of the quadratic Lagrangian on $[0, T]$ ; it does not assert that any physical motion extremises a physical action, and it does not contradict any minimum principle, because stationarity and minimisation are distinct conditions (the scope note of Tong, Section 2.1). For $T > π / ω$ both signs occur; the quantitative statement is exactly the one displayed, with the variations $η_{n} = \sin (n π t / T)$ and the exact identity $S (ε η_{n}) = \frac{ε^{2}}{2} δ^{2} S (q_{0}) [η_{n}, η_{n}]$ .
Endpoint degeneracy at $T = π / ω$ is not a failure of the model. At this value the displayed second-variation value in direction $η_{1}$ is zero and the Dirichlet problem of The undamped oscillator: Dirichlet non-uniqueness at $T = n π / ω$ despite unique initial-value solutions has the one-dimensional solution space ${A \sin (ω t)}$ , while initial-value problems remain uniquely solvable. More generally, the Dirichlet problem is non-unique exactly at $T = n π / ω$ for positive integers $n$ . This non-uniqueness is an underdetermination of a boundary-value problem, not a contradiction between the differential equation and its solutions. At $T = π / ω$ , the item also computes positive second-variation values in directions $η_{n}$ for $n \geq 2$ ; it makes no claim about all remaining directions or about overall extremality at this duration.
The parallel-axis theorem is the centred positive-mass case. Parallel-axis theorem: the inertia tensor about a displaced point of a centred mass distribution assumes $μ (ν) = 0$ , that is, coordinates whose origin is the centre of mass, together with finite second moments, which for a bounded finite Borel measure are proved in Finiteness and a uniform bound for the entries of the inertia tensor about an arbitrary point and in the finiteness lemma of Mass distributions on $R^{3}$ : total mass, first moment and inertia matrix. The theorem covers point, line, surface and volume measures, but only the centred identity $I_{ν} (a) = I (ν) + m (∥ a ∥_{2}^{2} I_{3} - a a^{T})$ ; for a non-centred distribution the additional first-moment terms displayed in the proof of that theorem are present, and no physical assertion about any body is made.
The coupled-oscillator proposition is an exact statement about a linear system. Two equal masses with two outer springs and a coupling spring: eigenmodes, decoupling and the explicit normal frequencies identifies the eigenmodes of the constant matrix $K = (\begin{array}{cc} k + c & - c \\ - c & k + c \end{array})$ and proves the decoupling bijection; it claims exactness for all times for the linear system with the stated parameter ranges. The degenerate case $k = 0$ produces affine motion of the in-phase mode and is reported as such; no oscillatory frequency is attached to a vanishing eigenvalue.
The pendulum bound is finite-time, conditional and of order $δ^{2}$ . The pendulum field near the downward equilibrium: bounded force derivative, cubic remainder and the finite-time small-angle error bound is a conditional consequence of the explicit field $F (θ, v) = (v, - ω^{2} \sin θ)$ , the smallness condition $δ e^{L T} < r$ and the cubic remainder $∣ \sin θ - θ ∣ \leq ∣ θ ∣^{3} / 6$ . It is not an assertion that the nonlinear pendulum is exactly harmonic, not a global or long-time statement, and not a report about any measured pendulum; the exactly harmonic system is the linearised equation $y_{1}^{''} = - ω^{2} y_{1}$ alone.

5 · Examples, experiments and counterexamples

None yet.

Cm Math Verification

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

The fixed-endpoint second variation of a time-dependent action at a curve

Definition

Remarks

The second variation of a time-dependent action: twice differentiability of the fixed-endpoint family and the Hessian integral formula

Statement

Facts & Assumptions

Proof

Remarks

Second variation of the oscillator action on a finite interval: both signs for T>π/ωT>π/ω and the value at T=π/ωT=π/ω

Statement

Facts & Assumptions

Proof

Remarks

The undamped oscillator: Dirichlet non-uniqueness at T=nπ/ωT=nπ/ω despite unique initial-value solutions

Statement

Facts & Assumptions

Proof

Remarks

The inertia tensor of a finite bounded Borel measure about any point of R3R3

Definition

Remarks

Finiteness and a uniform bound for the entries of the inertia tensor about an arbitrary point

Statement

Facts & Assumptions

Proof

Remarks

Parallel-axis theorem: the inertia tensor about a displaced point of a centred mass distribution

Statement

Facts & Assumptions

Proof

Remarks

Two equal masses with two outer springs and a coupling spring: eigenmodes, decoupling and the explicit normal frequencies

Statement

Facts & Assumptions

Proof

Remarks

The pendulum field near the downward equilibrium: bounded force derivative, cubic remainder and the finite-time small-angle error bound

Statement

Facts & Assumptions

Proof

Remarks

Scope and limits of the verification items on this page

Scope of the verification items

5 · Examples, experiments and counterexamples

Sources

Second variation of the oscillator action on a finite interval: both signs for $T > π / ω$ and the value at $T = π / ω$

The undamped oscillator: Dirichlet non-uniqueness at $T = n π / ω$ despite unique initial-value solutions

The inertia tensor of a finite bounded Borel measure about any point of $R^{3}$