CorollaryStatement: 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.

Forced quadratic system $M q^{''} + K q = φ (t)$ : decoupled forced modes and the convolution solution

Statement

Let $n \geq 1$ , let $M \in M_{n} (R)$ be symmetric positive definite, let $K \in M_{n} (R)$ be symmetric and non-negative, let $S : = M^{- 1 / 2} K M^{- 1 / 2} = O Λ O^{T}$ with $O$ orthogonal and $Λ = diag (λ_{1}, \dots, λ_{n})$ , $λ_{i} \geq 0$ (Decoupling of the constant-coefficient quadratic system $M q^{''} + K q = 0$ into normal modes, with the zero-mode and energy identities), let $I \subseteq R$ be an interval with nonempty interior (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length), let $φ : I \to R^{n}$ be continuous and let $t_{0} \in I$ . Put

$ψ (t) : = O^{T} M^{- 1 / 2} φ (t), ω_{i} : = \sqrt{λ_{i}} (λ_{i} > 0),$

and for a curve $q : I \to R^{n}$ whose first and second derivatives exist on $I$ (relative to $I$ at included endpoints) and whose second derivative is continuous on $I$ , put $z : = O^{T} M^{1 / 2} q$ . Then:

$q$ solves the forced quadratic system $M q^{''} + K q = φ$ on $I$ if and only if $z$ solves the decoupled forced system $z_{i}^{''} + λ_{i} z_{i} = ψ_{i} (1 \leq i \leq n)$ on $I$ .
For each $i$ , the unique solution $z_{i} : I \to R$ of the scalar equation in clause 1 with data $z_{i} (t_{0}) = ξ_{i}$ , $z_{i}^{'} (t_{0}) = η_{i}$ is $z_{i} (t) = ξ_{i} \cos (ω_{i} (t - t_{0})) + \frac{η_{i}}{ω_{i}} \sin (ω_{i} (t - t_{0})) + \frac{1}{ω_{i}} \int_{t_{0}}^{t} \sin (ω_{i} (t - s)) ψ_{i} (s) d s (λ_{i} > 0),$ $z_{i} (t) = ξ_{i} + η_{i} (t - t_{0}) + \int_{t_{0}}^{t} (t - s) ψ_{i} (s) d s (λ_{i} = 0) .$
Consequently, for every initial datum $(q (t_{0}), q^{'} (t_{0})) \in R^{2 n}$ there is exactly one solution $q : I \to R^{n}$ of $M q^{''} + K q = φ$ with that datum, and it is $q = M^{- 1 / 2} O z$ for the $z$ of clause 2.

Facts & Assumptions

Given: The symmetric positive definite $M$ , symmetric non-negative $K$ , the orthogonal diagonalisation $S = O Λ O^{T}$ , the interval $I$ , the continuous $φ : I \to R^{n}$ , the point $t_{0} \in I$ , and the transformed forcing $ψ = O^{T} M^{- 1 / 2} φ$ .

[F1]

The quadratic-mode theorem (Decoupling of the constant-coefficient quadratic system $M q^{''} + K q = 0$ into normal modes, with the zero-mode and energy identities) supplies the positive-definite square-root factors and an orthogonal diagonalisation $S = O Λ O^{T}$ with $λ_{i} \geq 0$ . Its scalar solution classification is stated only for intervals containing $0$ ; the present interval $I$ is arbitrary, so the proof below uses only this algebraic diagonalisation and verifies the forced scalar responses at the prescribed $t_{0}$ .

[F2]

The forced oscillator theorem (The forced oscillator with $k \geq 0$ : unique global solution and the convolution (Green's function) formula) applies on this arbitrary interval $I$ at the specified $t_{0}$ : with $m = 1$ , $c = 0$ , $k = λ_{i} \geq 0$ and continuous $ψ_{i}$ , it gives exactly one solution and its homogeneous-plus-convolution formula. The homogeneous classification (The homogeneous damped oscillator: solution classification by the discriminant and uniqueness for initial data) and degenerate proposition (The degenerate and repulsive oscillator: solutions for k=0 and the explicit growing solution for k<0) classify homogeneous solutions on every interval. For $λ_{i} > 0$ , translating an interval by $- t_{0}$ gives one containing $0$ , where the classification determines the homogeneous member from its data; for $λ_{i} = 0$ the proposition directly determines the affine member from its value and derivative at $t_{0}$ . Trigonometric derivatives and values at zero are $(\sin)^{'} = \cos$ , $(\cos)^{'} = - \sin$ , $\sin 0 = 0$ , and $\cos 0 = 1$ (The derivatives of sine and cosine are cosine and minus sine).

[F4]

The chain rule used below is The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ .

[F3]

$M^{1 / 2}$ , $M^{- 1 / 2}$ , $O$ and $O^{T} = O^{- 1}$ are the matrices of the modal theorem; $M^{- 1 / 2} M M^{- 1 / 2} = I_{n}$ and $O^{T} O = I_{n}$ . [given]

Proof

technique · direct; transport the forced system through the modal transformation and apply the scalar forced-oscillator theorem mode by mode

1.1F1F3algebra

Transport: differentiating $q = M^{- 1 / 2} O z$ twice gives $q^{''} = M^{- 1 / 2} O z^{''}$ , hence $M q^{''} + K q = M^{1 / 2} O (z^{''} + O^{T} M^{- 1 / 2} K M^{- 1 / 2} O z) = M^{1 / 2} O (z^{''} + Λ z)$ by the definition of $S$ and [F1], and $M^{1 / 2} O$ is invertible. Therefore $M q^{''} + K q = φ$ is equivalent to $z^{''} + Λ z = O^{T} M^{- 1 / 2} φ = ψ$ , which is the decoupled system of clause 1.

2.1step 1.1F2F4

The $i$ -th scalar equation is an oscillator equation with $m = 1$ , $c = 0$ , $k = λ_{i} \geq 0$ and continuous forcing $ψ_{i}$ ; by [F2] its unique solution on $I$ with data $(ξ_{i}, η_{i})$ at $t_{0}$ is the homogeneous solution with those data plus $\int_{t_{0}}^{t} g_{i} (t - s) ψ_{i} (s) d s$ . If $λ_{i} > 0$ , set $h_{i} (t) = ξ_{i} \cos (ω_{i} (t - t_{0})) + \frac{η_{i}}{ω_{i}} \sin (ω_{i} (t - t_{0}))$ . By the chain rule and trigonometric derivatives in [F2], $h_{i}^{''} + λ_{i} h_{i} = 0$ , $h_{i} (t_{0}) = ξ_{i}$ , and $h_{i}^{'} (t_{0}) = η_{i}$ ; translating any competing homogeneous solution to an interval containing $0$ and applying the classification in [F2] proves uniqueness. If $λ_{i} = 0$ , $h_{i} (t) = ξ_{i} + η_{i} (t - t_{0})$ directly solves the homogeneous equation with the required data and is the unique affine family member. Likewise $g_{i} (u) = \sin (ω_{i} u) / ω_{i}$ for $λ_{i} > 0$ and $g_{i} (u) = u$ for $λ_{i} = 0$ solve the homogeneous equation and have $g_{i} (0) = 0$ , $g_{i}^{'} (0) = 1$ ; the classified families give uniqueness of the kernel. Substitution in the forced theorem's formula gives exactly the two expressions in clause 2.

3.1step 1.1step 2.1F1F3∎

Clauses 1 and 2 exhibit $z$ as the unique solution of the decoupled forced system with prescribed data; since $q = M^{- 1 / 2} O z$ is a bijection with $(q (t_{0}), q^{'} (t_{0})) \mapsto (z (t_{0}), z^{'} (t_{0}))$ linear and invertible ( $q^{'} (t_{0}) = M^{- 1 / 2} O z^{'} (t_{0})$ ), clause 3 follows.

Forced quadratic system Mq′′+Kq=φ(t)Mq′′+Kq=φ(t): decoupled forced modes and the convolution solution

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

Forced quadratic system $M q^{''} + K q = φ (t)$ : decoupled forced modes and the convolution solution