PropositionStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

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.

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

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources