Alphabeta Math

1 · Prerequisites

2 · Summary

The companion page to cm-math-verification records explicit finite checks of its results. Everything here is mathematics: the examples carry domain: mathematics, depend only on the mathematical items of the parent page and on mathematical suppliers, and make no physical or empirical claim. No measurement, simulation or numerical integration is involved; the displayed values and bounds are exact expressions, including square roots, multiples of $π$ , polynomials in the stated parameters, and exponential expressions.

An explicit saddle of the oscillator action at $T = 2 π$ : the two variations $\sin (t / 2)$ and $\sin (3 t / 2)$ evaluates the oscillator second variation at $ω = 1$ , $T = 2 π$ for the variations $\sin (t / 2)$ and $\sin (3 t / 2)$ : the values $- 3 π / 4$ and $5 π / 4$ and the exact action values $- 3 π ε^{2} / 8 < 0 < 5 π ε^{2} / 8$ exhibit the saddle of the stationary zero curve, with the defining integrals also evaluated directly as a check.

Two distinct oscillator solutions with the same zero endpoints at $T = π$ , and their common action value exhibits the two distinct solutions $\sin t$ and $2 \sin t$ of $x^{''} + x = 0$ with the same zero endpoints at $T = π$ , and shows that every member $A \sin t$ of the one-dimensional solution family has the same action value $0$ .

Parallel-axis theorem checked on two equal point masses on the third axis computes, for $ν = m δ_{r e_{3}} + m δ_{- r e_{3}}$ , both the inertia matrix $d i a g (2 m r^{2}, 2 m r^{2}, 0)$ about the origin and the inertia tensor $d i a g (2 m (r^{2} + c^{2}), 2 m (r^{2} + c^{2}), 0)$ about $c e_{3}$ , twice: once from the definition and once through the parallel-axis identity of Parallel-axis theorem: the inertia tensor about a displaced point of a centred mass distribution.

Two-mass spring eigenmodes at explicit parameters: eigenrelations, a mode solution, and the zero-frequency case checks the eigenrelations $K u_{+} = u_{+}$ , $K u_{-} = 7 u_{-}$ of the two-mass system at $k = 1$ , $c = 3$ , verifies the mode solution $\cos (t) u_{+} + \cos (\sqrt{7} t) u_{-}$ by differentiation, and exhibits the unbounded affine motion $(1 + t) u_{+}$ of the degenerate case $k = 0$ , $c = 1$ .

The pendulum linearisation bound at $g = l = 1$ : exact error bound for the data $δ = 1 / 100$ , $T = 1$ instantiates the pendulum bound at $g = l = 1$ , $r = 1 / 2$ , $δ = 1 / 100$ , $T = 1$ : the smallness condition $δ e^{L T} < r$ follows from $2 < e < 3$ , and the error is bounded by $(e^{2 t} - e^{t}) / (12 \cdot 10^{4})$ on $[0, 1]$ , with the pointwise remainder checks $∣ \sin θ - θ ∣ \leq 1 / 48$ and $∣ \sin θ ∣ \leq 1 / 2$ on the ball.

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

None yet.

5 · Examples, experiments and counterexamples

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

An explicit saddle of the oscillator action at $T = 2 π$ : the two variations $\sin (t / 2)$ and $\sin (3 t / 2)$

Example

Fix $ω = 1$ and $T = 2 π$ in the chart $L (q, v) = \frac{1}{2} (v^{2} - q^{2})$ on $O = R \times R \times R$ over $[0, 2 π] \times R$ (A time-dependent Lagrangian chart, its action functional and its fixed-endpoint first variations), and consider the variations

$η_{1} (t) = \sin \frac{t}{2}, η_{3} (t) = \sin \frac{3 t}{2}$

of the zero curve $q_{0} \equiv 0$ . The proposition Second variation of the oscillator action on a finite interval: both signs for $T > π / ω$ and the value at $T = π / ω$ gives

$δ^{2} S (q_{0}) [η_{1}, η_{1}] = - \frac{3 π}{4} < 0, δ^{2} S (q_{0}) [η_{3}, η_{3}] = \frac{5 π}{4} > 0,$

and with the exact identity $S (ε η) = \frac{ε^{2}}{2} δ^{2} S (q_{0}) [η, η]$ of that proposition,

$S (ε η_{1}) = - \frac{3 π ε^{2}}{8} < 0 < \frac{5 π ε^{2}}{8} = S (ε η_{3}) (ε \neq 0) .$

Thus at the duration $T = 2 π > π = π / ω$ the stationary zero curve has variations that decrease and variations that increase the action arbitrarily close to it: it is a saddle, and neither a local minimiser nor a local maximiser. Every number below is exact; no measurement or numerical integration is involved.

Facts & Assumptions

Given: The chart $L (q, v) = \frac{1}{2} (v^{2} - q^{2})$ over $[0, 2 π] \times R$ , the zero curve $q_{0}$ , the variations $η_{1}, η_{3}$ , and the action $S$ and second variation $δ^{2} S$ 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]

Second variation values and exact action (Second variation of the oscillator action on a finite interval: both signs for $T > π / ω$ and the value at $T = π / ω$ , The second variation of a time-dependent action: twice differentiability of the fixed-endpoint family and the Hessian integral formula): for this chart with parameters $ω = 1$ , $T = 2 π$ one has $δ^{2} S (q_{0}) [η_{n}, η_{n}] = \frac{T}{2} ((n π / T)^{2} - ω^{2})$ for the variations $η_{n} (t) = \sin (n π t / T)$ , and $S (ε η_{n}) = \frac{ε^{2}}{2} δ^{2} S (q_{0}) [η_{n}, η_{n}]$ for every real $ε$ .

[L2]

Trigonometric integral 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 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$ , 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, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length): the double-angle formulas give $\cos^{2} u = \frac{1}{2} (1 + \cos 2 u)$ and $\sin^{2} u = \frac{1}{2} (1 - \cos 2 u)$ ; $\sin$ and $\cos$ are continuous, hence integrable on $[0, 2 π]$ ; the fundamental theorem evaluates the integrals below; and $\sin 0 = \sin π = \sin 2 π = \sin 3 π = 0$ .

Verification

Proof technique: direct; substitute $T = 2 π$ , $ω = 1$ into the proposition and evaluate the defining integrals independently.

1.1givenL2algebra

The variations: $η_{1}$ and $η_{3}$ are $C^{\infty}$ on $R$ with $η_{1} (0) = η_{1} (2 π) = 0$ and $η_{3} (0) = η_{3} (2 π) = 0$ by [L2], so both are variations of $q_{0}$ ; their derivatives are $η_{1}^{'} (t) = \frac{1}{2} \cos \frac{t}{2}$ and $η_{3}^{'} (t) = \frac{3}{2} \cos \frac{3 t}{2}$ .

2.1step 1.1givenL1algebra

Second variations: substituting $T = 2 π$ and $ω = 1$ into [L1] gives $δ^{2} S (q_{0}) [η_{n}, η_{n}] = π (n^{2} / 4 - 1)$ , hence $δ^{2} S (q_{0}) [η_{1}, η_{1}] = π (1 / 4 - 1) = - \frac{3 π}{4}$ and $δ^{2} S (q_{0}) [η_{3}, η_{3}] = π (9 / 4 - 1) = \frac{5 π}{4}$ .

3.1step 2.1L2algebra

Independent integral check: by [L2], $\int_{0}^{2 π} η_{1}^{'} (t)^{2} d t = \frac{1}{4} \int_{0}^{2 π} \frac{1 + \cos t}{2} d t = \frac{1}{4} \cdot π, \int_{0}^{2 π} η_{1} (t)^{2} d t = \int_{0}^{2 π} \frac{1 - \cos t}{2} d t = π,$ so $δ^{2} S (q_{0}) [η_{1}, η_{1}] = π / 4 - π = - \frac{3 π}{4}$ ; and with $η_{3}^{'} (t)^{2} = \frac{9}{4} \cos^{2} \frac{3 t}{2}$ the same computation gives $\int_{0}^{2 π} η_{3}^{' 2} = \frac{9}{4} \cdot π$ and $\int_{0}^{2 π} η_{3}^{2} = π$ , so $δ^{2} S (q_{0}) [η_{3}, η_{3}] = \frac{9 π}{4} - π = \frac{5 π}{4}$ , in agreement with step 2.1.

4.1step 2.1step 3.1L1algebra∎

Action values and saddle: by the exact identity in [L1], $S (ε η_{1}) = \frac{ε^{2}}{2} \cdot (- \frac{3 π}{4}) = - \frac{3 π ε^{2}}{8} < 0$ and $S (ε η_{3}) = \frac{5 π ε^{2}}{8} > 0$ for every $ε \neq 0$ , while $S (q_{0}) = 0$ ; since both families tend to $q_{0}$ as $ε \to 0$ , the stationary zero curve is neither a local minimiser nor a local maximiser, as claimed.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

Two distinct oscillator solutions with the same zero endpoints at $T = π$ , and their common action value

Example

Take $m = 1$ , $k = 1$ , hence $ω = 1$ , and $T = π$ in The undamped oscillator: Dirichlet non-uniqueness at $T = n π / ω$ despite unique initial-value solutions, and consider the two curves

$x_{1} (t) = \sin t, x_{2} (t) = 2 \sin t (t \in [0, π]) .$

Both are $C^{\infty}$ solutions of $x^{''} + x = 0$ on $[0, π]$ with $x (0) = x (π) = 0$ , and they are distinct; they have different initial velocities $1$ and $2$ . On the chart $L (q, v) = \frac{1}{2} (v^{2} - q^{2})$ over $[0, π] \times R$ (A time-dependent Lagrangian chart, its action functional and its fixed-endpoint first variations) both are stationary curves of the action, and their action values agree:

$S (x_{1}) = S (x_{2}) = 0.$

This is the concrete $T = π$ case of the non-uniqueness in The undamped oscillator: Dirichlet non-uniqueness at $T = n π / ω$ despite unique initial-value solutions and of the signed-action checks of An explicit saddle of the oscillator action at $T = 2 π$ : the two variations $\sin (t / 2)$ and $\sin (3 t / 2)$ ; all numbers are exact.

Facts & Assumptions

Given: The model $x^{''} + x = 0$ on $[0, π]$ , its curves $x_{1} (t) = \sin t$ and $x_{2} (t) = 2 \sin t$ , and the chart $L (q, v) = \frac{1}{2} (v^{2} - q^{2})$ with its action $S$ .

[L1]

The non-uniqueness proposition (The undamped oscillator: Dirichlet non-uniqueness at $T = n π / ω$ despite unique initial-value solutions): for $m = k = 1$ and $T = π = n π / ω$ with $n = 1$ , the set of $C^{2}$ solutions of $x^{''} + x = 0$ on $[0, π]$ with $x (0) = x (π) = 0$ is exactly ${A \sin t : A \in R}$ , and each such curve is a stationary curve of the action of the chart $L (q, v) = \frac{1}{2} (v^{2} - q^{2})$ (Stationarity of the time-dependent action is equivalent to the vanishing of the Euler-Lagrange expression, A time-dependent Lagrangian chart, its action functional and its fixed-endpoint first variations).

[L2]

Trigonometric calculus and integrals (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)$ , 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$ , 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, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length): $\sin$ and $\cos$ are differentiable with $\sin^{'} = \cos$ , $\cos^{'} = - \sin$ , the zeros of $\sin$ are the integer multiples of $π$ and in particular $\sin 0 = \sin π = 0$ ; the double-angle formula gives $\cos^{2} t - \sin^{2} t = \cos 2 t$ ; the fundamental theorem evaluates $\int_{0}^{π} \cos 2 t d t = \frac{1}{2} [\sin 2 t]_{0}^{π} = 0$ because $\sin 2 π = 0$ ; and continuous integrands on $[0, π]$ are integrable.

Verification

Proof technique: direct; verify the two solutions and their endpoint data, note their distinctness, and evaluate the action along the family.

1.1givenL2algebra

The two solutions: by [L2], $x_{1}^{''} = - \sin t = - x_{1}$ and $x_{2}^{''} = - 2 \sin t = - x_{2}$ , so both curves solve $x^{''} + x = 0$ on $[0, π]$ ; and $x_{1} (0) = x_{1} (π) = 0$ , $x_{2} (0) = x_{2} (π) = 0$ by the zero set of $\sin$ .

2.1step 1.1givenL2algebra

Distinctness with equal boundary data: $x_{2} - x_{1} = \sin t \neq 0$ (at $t = π / 2$ the value is $1$ ), so the solutions are distinct, while both take the value $0$ at $0$ and at $π$ ; their initial velocities are $x_{1}^{'} (0) = 1$ and $x_{2}^{'} (0) = 2$ , so they are different initial-value solutions, in accordance with the initial-value uniqueness clause of [L1].

3.1step 1.1step 2.1L1L2algebra

Action along the family: for $A \in R$ , using $L (A \sin t, A \cos t) = \frac{A^{2}}{2} (\cos^{2} t - \sin^{2} t)$ and linearity of the integral, $S (A \sin) = \frac{A^{2}}{2} \int_{0}^{π} (\cos^{2} t - \sin^{2} t) d t = \frac{A^{2}}{2} \int_{0}^{π} \cos 2 t d t = \frac{A^{2}}{4} [\sin 2 t]_{0}^{π} = 0$ by [L2]; in particular $S (x_{1}) = S (x_{2}) = 0$ .

4.1step 1.1step 2.1step 3.1L1∎

Reading: by [L1] the curves $x_{1}, x_{2}$ are stationary for the action of the chart and share the endpoint data $(0, 0)$ ; they are distinct and have the same action value $0$ , exhibiting in one explicit computation the failure of uniqueness of the fixed-endpoint problem at $T = π$ , with no claim about any other duration.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

Parallel-axis theorem checked on two equal point masses on the third axis

Example

Let $m > 0$ , $r > 0$ , and let

$ν : = m δ_{r e_{3}} + m δ_{- r e_{3}}$

be the weighted sum of the two Dirac measures at $\pm r e_{3}$ (The Dirac set function at a point, Nonnegative scalar multiples and countable weighted sums of measures are measures), a bounded finite Borel measure and hence a mass distribution of total mass $2 m$ (Mass distributions on $R^{3}$ : total mass, first moment and inertia matrix). Assume the Axiom of Countable Choice ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )), used only to make the displayed integrals finite (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}$ ). Then:

$ν$ is centred, $μ (ν) = m r e_{3} + m (- r e_{3}) = 0$ , and its inertia matrix about the origin is $I (ν) = d i a g (2 m r^{2}, 2 m r^{2}, 0)$ ;
the inertia tensor about $a = c e_{3}$ , computed directly from the definition, is $I_{ν} (c e_{3}) = d i a g (2 m (r^{2} + c^{2}), 2 m (r^{2} + c^{2}), 0)$ , and the parallel-axis identity of Parallel-axis theorem: the inertia tensor about a displaced point of a centred mass distribution, $I_{ν} (a) = I (ν) + 2 m (∥ a ∥_{2}^{2} I_{3} - a a^{T})$ , reproduces exactly this value.

All entries are exact polynomial expressions in $m, r, c$ ; no measurement is involved.

Facts & Assumptions

Given: The parameters $m > 0$ , $r > 0$ , a real $c$ , the measure $ν = m δ_{r e_{3}} + m δ_{- r e_{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}$ .

[L1]

The measure and its integrals (The Dirac set function at a point, A Dirac set function is a probability measure, Nonnegative scalar multiples and countable weighted sums of measures are measures, Nonnegative scalar multiples and countable weighted sums of measures): $ν (E) = m δ_{r e_{3}} (E) + m δ_{- r e_{3}} (E)$ for every Borel set $E$ , so $ν$ is a measure with $ν (R^{3}) = 2 m$ and $ν ({r e_{3}}) = ν ({- r e_{3}}) = m$ ; for every real measurable $f$ bounded on the two-point support one has $\int f d ν = m f (r e_{3}) + m f (- r e_{3})$ (The nonnegative Lebesgue integral, The integral of a nonnegative simple function, Integral over a measurable subset, Integrable real and complex functions, and their integrals, Monotonicity and nonnegative homogeneity of the nonnegative integral, The Lebesgue integral is linear on $L^{1} (μ)$ ).

[L2]

The two inertia objects (Mass distributions on $R^{3}$ : total mass, first moment and inertia matrix, The inertia tensor of a finite bounded Borel measure about any point of $R^{3}$ ): $I (ν)_{j k} = \int (∥ ρ ∥_{2}^{2} δ_{j k} - ρ_{j} ρ_{k}) d ν$ and $I_{ν} (a)_{j k} = \int (∥ ρ - a ∥_{2}^{2} δ_{j k} - (ρ_{j} - a_{j}) (ρ_{k} - a_{k})) d ν$ ; all entries are finite real numbers under ${A C}_{ω}$ (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}$ ).

[L3]

The parallel-axis theorem (Parallel-axis theorem: the inertia tensor about a displaced point of a centred mass distribution): for a centred mass distribution of total mass $m_{t o t}$ one has $I_{ν} (a) = I (ν) + m_{t o t} (∥ a ∥_{2}^{2} I_{3} - a a^{T})$ .

[L4]

Matrix data (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, Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes, Laws of finite sums and finite products): for $ρ = \pm r e_{3}$ one has $ρ ρ^{T} = r^{2} e_{3} e_{3}^{T}$ and $∥ ρ ∥_{2}^{2} = r^{2}$ ; for $a = c e_{3}$ and $ρ = r e_{3}$ one has $ρ - a = (r - c) e_{3}$ while for $ρ = - r e_{3}$ one has $ρ - a = - (r + c) e_{3}$ ; and $I_{3} - e_{3} e_{3}^{T} = d i a g (1, 1, 0)$ .

Verification

Proof technique: direct; evaluate the two atomic integrals and compare the two sides of the parallel-axis identity.

1.1givenL1L2algebra

Centredness and total mass: by the atomic formula of [L1], $μ (ν) = m \cdot r e_{3} + m \cdot (- r e_{3}) = 0$ and $ν (R^{3}) = 2 m$ , so $ν$ is a centred mass distribution of total mass $2 m$ and [L3] applies.

2.1step 1.1L1L2L4algebra

Inertia about the origin: by [L1], [L2] and [L4], $I (ν) = m (r^{2} I_{3} - r^{2} e_{3} e_{3}^{T}) + m (r^{2} I_{3} - r^{2} e_{3} e_{3}^{T}) = 2 m r^{2} (I_{3} - e_{3} e_{3}^{T}) = d i a g (2 m r^{2}, 2 m r^{2}, 0) .$

2.2step 1.1L1L2L4algebra

Inertia about $c e_{3}$ , computed directly: for $ρ = r e_{3}$ the shifted integrand is $(r - c)^{2} (I_{3} - e_{3} e_{3}^{T})$ and for $ρ = - r e_{3}$ it is $(r + c)^{2} (I_{3} - e_{3} e_{3}^{T})$ , so by [L1], [L2] and [L4], $I_{ν} (c e_{3}) = m ((r - c)^{2} + (r + c)^{2}) (I_{3} - e_{3} e_{3}^{T}) = 2 m (r^{2} + c^{2}) (I_{3} - e_{3} e_{3}^{T}) = d i a g (2 m (r^{2} + c^{2}), 2 m (r^{2} + c^{2}), 0) .$

3.1step 1.1step 2.1step 2.2L3L4algebra∎

The theorem side: by [L3] with $m_{t o t} = 2 m$ and $a = c e_{3}$ , $I_{ν} (c e_{3}) = I (ν) + 2 m (c^{2} I_{3} - c^{2} e_{3} e_{3}^{T})$ , which by step 2.1 and [L4] equals $2 m (r^{2} + c^{2}) (I_{3} - e_{3} e_{3}^{T})$ , in exact agreement with the direct computation of step 2.2: the parallel-axis identity holds at this data.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

Two-mass spring eigenmodes at explicit parameters: eigenrelations, a mode solution, and the zero-frequency case

Example

Take $m = 1$ , $k = 1$ , $c = 3$ in Two equal masses with two outer springs and a coupling spring: eigenmodes, decoupling and the explicit normal frequencies, so that $K = (\begin{array}{cc} 4 & - 3 \\ - 3 & 4 \end{array})$ and $u_{\pm} = \frac{1}{\sqrt{2}} (1, \pm 1)^{T}$ ; the proposition gives $K u_{+} = u_{+}$ and $K u_{-} = 7 u_{-}$ , hence squared frequencies $k / m = 1$ and $(k + 2 c) / m = 7$ . The curve

$x (t) = \cos (t) u_{+} + \cos (\sqrt{7} t) u_{-}$

solves $x^{''} = - K x$ with $x (0) = (\sqrt{2}, 0)$ and $x^{'} (0) = 0$ . In the degenerate case $k = 0$ , $c = 1$ one has $K = (\begin{array}{cc} 1 & - 1 \\ - 1 & 1 \end{array})$ and $K u_{+} = 0$ , so $x (t) = (1 + t) u_{+}$ solves $x^{''} = - K x$ and is unbounded on $[0, \infty)$ : the zero-frequency mode is affine, not oscillatory. All entries are exact; no numerical integration or measurement is involved.

Facts & Assumptions

Given: The parameters of the two cases, the matrix $K$ and vectors $u_{\pm}$ of each case, and the system $x^{''} = - K x$ of Two equal masses with two outer springs and a coupling spring: eigenmodes, decoupling and the explicit normal frequencies with $m = 1$ .

[L1]

The proposition (Two equal masses with two outer springs and a coupling spring: eigenmodes, decoupling and the explicit normal frequencies): for $m > 0$ , $k \geq 0$ , $c \geq 0$ one has $K u_{+} = k u_{+}$ and $K u_{-} = (k + 2 c) u_{-}$ , the system $m x^{''} = - K x$ is equivalent to the two scalar oscillator equations $m y_{+}^{''} + k y_{+} = 0$ , $m y_{-}^{''} + (k + 2 c) y_{-} = 0$ via $x = y_{+} u_{+} + y_{-} u_{-}$ , and for $k = 0$ the family $x (t) = (A + B t) u_{+}$ consists of solutions with $K u_{+} = 0$ (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 for the scalar solution families).

[L2]

Matrix and derivative 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 Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , 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 chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ , The derivatives of sine and cosine are cosine and minus sine, Sine and cosine defined by their real power series, 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): matrix-vector multiplication is the displayed sum; $\frac{d}{d t} \cos t = - \sin t$ and $\frac{d}{d t} \cos (\sqrt{7} t) = - \sqrt{7} \sin (\sqrt{7} t)$ , so $\frac{d^{2}}{d t^{2}} \cos (\sqrt{7} t) = - 7 \cos (\sqrt{7} t)$ by the chain rule; and $∥ (A + B t) u_{+} ∥_{2} = ∣ A + B t ∣$ because $u_{+}$ is a unit vector.

Verification

Proof technique: direct; multiply the two explicit matrices into the displayed vectors and substitute the resulting eigenrelations into the two solutions.

1.1givenL1L2algebra

Eigenrelations in the first case: direct multiplication gives $K u_{+} = \frac{1}{\sqrt{2}} (\begin{array}{c} 4 - 3 \\ - 3 + 4 \end{array}) = \frac{1}{\sqrt{2}} (\begin{array}{c} 1 \\ 1 \end{array}) = u_{+}, K u_{-} = \frac{1}{\sqrt{2}} (\begin{array}{c} 4 + 3 \\ - 3 - 4 \end{array}) = \frac{7}{\sqrt{2}} (\begin{array}{c} 1 \\ - 1 \end{array}) = 7 u_{-},$ so $k = 1$ and $k + 2 c = 7$ are the eigenvalues and the squared frequencies are $1$ and $7$ ; the second case has $K u_{+} = \frac{1}{\sqrt{2}} (1 - 1, - 1 + 1)^{T} = 0$ .

2.1step 1.1givenL2algebra

The mode solution: with $x (t) = \cos (t) u_{+} + \cos (\sqrt{7} t) u_{-}$ one has $x^{''} (t) = - \cos (t) u_{+} - 7 \cos (\sqrt{7} t) u_{-} = - (\cos (t) K u_{+} + \cos (\sqrt{7} t) K u_{-}) = - K x (t)$ by step 1.1 and [L2], so $x^{''} = - K x$ ; also $x (0) = u_{+} + u_{-} = (\sqrt{2}, 0)$ and $x^{'} (0) = 0$ because both sine factors vanish at $0$ .

3.1step 1.1givenL1L2algebra∎

The zero-frequency case: for $k = 0$ , $c = 1$ and $x (t) = (1 + t) u_{+}$ one has $x^{''} = 0$ and $- K x = - (1 + t) K u_{+} = 0$ by step 1.1, so $x$ solves the system; moreover $∥ x (t) ∥_{2} = 1 + t$ tends to $+ \infty$ , so the motion is unbounded and affine rather than oscillatory, as clause 4 of [L1] predicts.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

The pendulum linearisation bound at $g = l = 1$ : exact error bound for the data $δ = 1 / 100$ , $T = 1$

Example

Take $g = l = 1$ in The pendulum field near the downward equilibrium: bounded force derivative, cubic remainder and the finite-time small-angle error bound, so that $ω = 1$ , $F (θ, v) = (v, - \sin θ)$ , $A = (\begin{array}{cc} 0 & 1 \\ - 1 & 0 \end{array})$ , $L = 1$ and $∥ A ∥ = 1$ . Choose the ball radius $r = 1 / 2$ , the datum $z_{0} = (δ, 0)$ with $δ = 1 / 100$ , and the horizon $T = 1$ . Then $δ e^{L T} = e / 100 < 3 / 100 < 1 / 2 = r$ because $2 < e < 3$ (The elementary numerical bound $2 < e < 3$ ), so the proposition applies and gives

$∥ z (t) - y (t) ∥_{2} \leq \frac{1}{12 \cdot 10^{4}} (e^{2 t} - e^{t}) (0 \leq t \leq 1),$

where $y (t) = δ (\cos t, - \sin t)$ solves $y^{'} = A y$ , $y (0) = z_{0}$ ; at $t = 1$ the bound reads $(e^{2} - e) / (12 \cdot 10^{4})$ and is at most $e^{3} / (12 \cdot 10^{4})$ . The remainder checks at $∥ z ∥_{2} \leq r$ are: $∣ \sin θ - θ ∣ \leq ∣ θ ∣^{3} / 6 \leq 1 / 48$ , and $∣ \sin θ ∣ \leq ∣ θ ∣ \leq r = 1 / 2$ . All constants are exact; the single inequality $e < 3$ is the only numerical input.

Facts & Assumptions

Given: The parameters $g = l = 1$ , the field $F (θ, v) = (v, - \sin θ)$ , the matrix $A$ , the constants $r = 1 / 2$ , $δ = 1 / 100$ , $T = 1$ , and the solution $y (t) = δ (\cos t, - \sin t)$ of the linear problem.

[L1]

The proposition (The pendulum field near the downward equilibrium: bounded force derivative, cubic remainder and the finite-time small-angle error bound): for this field, $∥ F (z) - A z ∥_{2} = ∣ \sin θ - θ ∣ \leq ∣ θ ∣^{3} / 6 \leq r ∥ z ∥_{2}^{2} / 6$ and $∥ F (z) ∥_{2} \leq L ∥ z ∥_{2}$ with $L = 1$ and $∥ A ∥ = 1$ on $∥ z ∥_{2} \leq r$ ; for $δ e^{L T} < r$ the estimate $∥ z (t) - y (t) ∥_{2} \leq (ω^{2} r / 6) δ^{2} \int_{0}^{t} e^{∥ A ∥ (t - s)} e^{2 L s} d s$ holds on $[0, T]$ (Finite-time linearization error bound: quadratic remainder, exponential growth bound and the variation-of-constants estimate).

[L2]

Exponential and trigonometric calculus (The exponential function is smooth and $(\exp)^{'} = \exp$ , The real exponential function and the number $e$ by a power series, The elementary numerical bound $2 < e < 3$ , The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$ , 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)$ , 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, A uniform derivative bound gives a uniform Taylor remainder bound, 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 chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ): $2 < e < 3$ ; $e^{t}$ is its own derivative, and $e^{u + v} = e^{u} e^{v}$ for real $u, v$ . For fixed $t > 0$ , $G (s) = e^{t + s}$ has derivative $G^{'} (s) = e^{t + s}$ on $[0, t]$ ; this derivative is continuous, hence integrable, so the fundamental theorem gives $\int_{0}^{t} e^{t + s} d s = e^{2 t} - e^{t}$ . At $t = 0$ the integral and expression both vanish. $\sin$ and $\cos$ have range $[- 1, 1]$ and $\sin 0 = 0$ ; and the Taylor bound gives $∣ \sin θ - θ ∣ \leq ∣ θ ∣^{3} / 6$ .

[L3]

Norm data (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , The operator norm as the least bound and as the unit-sphere or unit-ball supremum, The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral, 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, Open ball, closed ball and sphere in a metric space): use the one-based component labels $w_{j} : = w (j - 1)$ for $w \in R^{2}$ , $j \in {1, 2}$ . Then $∥ (w_{1}, w_{2}) ∥_{2}^{2} = w_{1}^{2} + w_{2}^{2}$ ; $y_{1} (t) = δ \cos t$ and $y_{2} (t) = - δ \sin t$ satisfy $y_{1}^{'} = y_{2}$ and $y_{2}^{'} = - y_{1}$ .

Verification

Proof technique: direct; instantiate the proposition at the stated constants, verify the smallness condition with $e < 3$ , evaluate the integral with the fundamental theorem, and check the pointwise remainder bounds.

1.1givenL1L2algebra

Smallness condition: $L = 1$ and $δ = 1 / 100$ give $δ e^{L T} = e / 100$ , and $e < 3$ gives $e / 100 < 3 / 100 < 1 / 2 = r$ , so the datum lies in the range of the proposition with $T = 1$ .

1.2givenL1L2algebra

Pointwise bounds at this data: on $∥ z ∥_{2} \leq 1 / 2$ one has $∣ θ ∣^{3} / 6 \leq (1 / 2) ∥ z ∥_{2}^{2} / 6 = ∥ z ∥_{2}^{2} / 12$ and $∣ \sin θ ∣ \leq ∣ θ ∣ \leq 1 / 2$ , so the two hypotheses of [L1] hold with $C = 1 / 12$ and $L = 1$ ; at $z = (1 / 2, 0)$ this reads $∣ \sin (1 / 2) - 1 / 2 ∣ \leq 1 / 48$ .

2.1step 1.1step 1.2L1L2algebra

The error bound: by [L1] with $ω = 1$ , $r = 1 / 2$ , $δ = 1 / 100$ , $L = ∥ A ∥ = 1$ , $∥ z (t) - y (t) ∥_{2} \leq \frac{1}{12} \cdot \frac{1}{10^{4}} \int_{0}^{t} e^{t - s} e^{2 s} d s = \frac{e^{2 t} - e^{t}}{12 \cdot 10^{4}}$ for $0 \leq t \leq 1$ . By [L2], $e^{t - s} e^{2 s} = e^{t + s}$ and $\int_{0}^{t} e^{t + s} d s = e^{2 t} - e^{t}$ , including $t = 0$ . This evaluates the upper bound, not the actual nonlinear error.

3.1step 2.1L1L3algebra∎

Reading at $t = 1$ : the bound becomes $(e^{2} - e) / (12 \cdot 10^{4}) < e^{3} / (12 \cdot 10^{4})$ , a finite quantity of order $δ^{2} = 10^{- 4}$ , and $y_{1} (t) = δ \cos t$ satisfies $∣ z_{1} (t) - y_{1} (t) ∣ \leq ∥ z (t) - y (t) ∥_{2}$ by [L3]; the estimate is restricted to $[0, 1]$ and asserts nothing about the nonlinear pendulum beyond it.

Cm Math Verification — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

5 · Examples, experiments and counterexamples

An explicit saddle of the oscillator action at $T = 2 π$ : the two variations $\sin (t / 2)$ and $\sin (3 t / 2)$

Example

Facts & Assumptions

Verification

Two distinct oscillator solutions with the same zero endpoints at $T = π$ , and their common action value

Example

Facts & Assumptions

Verification

Parallel-axis theorem checked on two equal point masses on the third axis

Example

Facts & Assumptions

Verification

Two-mass spring eigenmodes at explicit parameters: eigenrelations, a mode solution, and the zero-frequency case

Example

Facts & Assumptions

Verification

The pendulum linearisation bound at $g = l = 1$ : exact error bound for the data $δ = 1 / 100$ , $T = 1$

Example

Facts & Assumptions

Verification

Sources

Cm Math Verification — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

5 · Examples, experiments and counterexamples

An explicit saddle of the oscillator action at T=2πT=2π: the two variations sin⁡(t/2)sin(t/2) and sin⁡(3t/2)sin(3t/2)

Example

Facts & Assumptions

Verification

Two distinct oscillator solutions with the same zero endpoints at T=πT=π, and their common action value

Example

Facts & Assumptions

Verification

Parallel-axis theorem checked on two equal point masses on the third axis

Example

Facts & Assumptions

Verification

Two-mass spring eigenmodes at explicit parameters: eigenrelations, a mode solution, and the zero-frequency case

Example

Facts & Assumptions

Verification

The pendulum linearisation bound at g=l=1g=l=1: exact error bound for the data δ=1/100δ=1/100, T=1T=1

Example

Facts & Assumptions

Verification

Sources

An explicit saddle of the oscillator action at $T = 2 π$ : the two variations $\sin (t / 2)$ and $\sin (3 t / 2)$

Two distinct oscillator solutions with the same zero endpoints at $T = π$ , and their common action value

The pendulum linearisation bound at $g = l = 1$ : exact error bound for the data $δ = 1 / 100$ , $T = 1$