ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck pass

How statement and proof provenance work

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

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

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

A drive along the in-phase pattern of the two-mass chain: resonance exactly at that mode's frequency and a bounded steady response off resonance

Physical scope

A worked instance of the forced coupled quadratic model: the two equal-mass chain of the companion example with a prescribed generalized force J(t)=F cos(Omega t) u_+ along the in-phase pattern (a sinusoidal drive for Omega>0 and a constant-force specialization for Omega=0), the modal force components (F/m,0), the unbounded resonance at Omega = sqrt(k/m) with the explicit linearly growing modal motion, the bounded steady response of amplitude |F|/(2c) at Omega = sqrt((k+2c)/m), and the boundedness of every motion for Omega^2 not equal to k/m. The force is prescribed external data; no back-reaction, measured response or empirical value is asserted.

Example

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

Adopt the two-mass chain of Two coupled masses on a line: the in-phase and anti-phase normal modes, their frequencies, mode-energies and the zero-stiffness translation mode: mass metric $M = m I_{2}$ , stiffness $K = (\begin{array}{cc} k + c & - c \\ - c & k + c \end{array})$ with $m > 0$ , $k > 0$ , $c > 0$ , and modal vectors $u_{\pm} = (1, \pm 1) / \sqrt{2 m}$ with modal stiffnesses $λ_{+} = k / m$ , $λ_{-} = (k + 2 c) / m$ and frequencies $ω_{+} = \sqrt{k / m}$ , $ω_{-} = \sqrt{(k + 2 c) / m}$ . Choose a real drive coefficient $F \neq 0$ . In the physical equation $J = F u_{+} \cos (Ω t)$ its unit is ${k g}^{3 / 2} m s^{- 2}$ , since $u_{+}$ has unit ${k g}^{- 1 / 2}$ and $J$ is a force. Thus $F / m$ is a modal force amplitude with unit $a_{*} / s^{2}$ , and $∣ F ∣ / (2 c)$ below is a modal coordinate amplitude with unit $a_{*}$ ; multiplying by $u_{+}$ gives each particle's displacement amplitude. Choose a frequency $Ω \geq 0$ and prescribe $J (t) = F \cos (Ω t) u_{+} .$ For $Ω > 0$ this is the sinusoidal drive of The sinusoidally driven oscillator model: a prescribed external force $f_{0} \cos (Ω t)$ added to the damped oscillator; for $Ω = 0$ it is the constant force allowed by clause (b) of The coupled quadratic oscillator model: mass metric, stiffness, generalized force, modal vocabulary and the small-oscillation model at a mechanical equilibrium. In either case it is prescribed external data, so the model is the forced coupled quadratic model $M q^{''} + K q = J$ . The all-time claims below concern maximal motions on $R$ ; local solutions are their restrictions. Then:

the modal force components of $J (t) = J_{0} \cos (Ω t)$ with $J_{0} = F u_{+}$ are $ψ_{0} = O^{T} M^{- 1 / 2} J_{0} = (F / m, 0)$ : the drive excites the in-phase modal coordinate alone, with modal amplitude $F / m$ , and leaves the relative coordinate unforced;
if $Ω = ω_{+} = \sqrt{k / m}$ , then $q^{p} (t) = \frac{F}{2 m ω_{+}} t \sin (ω_{+} t) u_{+}$ is a motion of the model, of in-phase pattern, with linearly growing amplitude $∣ F ∣ t / (2 m ω_{+})$ , and every motion of the model is unbounded on $[0, \infty)$ ;
if $Ω^{2} \neq k / m$ then every motion of the model is bounded on $[0, \infty)$ ; in particular at $Ω = ω_{-} = \sqrt{(k + 2 c) / m}$ — the frequency of the unforced relative mode — the drive is non-resonant and the steady modal response has amplitude $\frac{∣ F ∣ / m}{∣ k / m - (k + 2 c) / m ∣} = \frac{∣ F ∣}{2 c};$
the resonance condition is exactly that the drive frequency equal the frequency of a mode whose modal force component does not vanish: here the in-phase mode at $ω_{+}$ , not the relative mode at $ω_{-}$ .

Facts & Assumptions

Given: The data $m, k, c > 0$ of the chain, the modal vectors $u_{\pm}$ and modal stiffnesses $λ_{\pm}$ , the modal data $O$ , $M^{1 / 2}$ with $e_{\pm} = (1, \pm 1) / \sqrt{2}$ , real $F \neq 0$ and $Ω \geq 0$ .

[F1]

Chain data and modes (Two coupled masses on a line: the in-phase and anti-phase normal modes, their frequencies, mode-energies and the zero-stiffness translation mode clauses 1, 2 and 4): $M = m I_{2}$ , $K$ as displayed, $O = [e_{+} e_{-}]$ , $u_{\pm} = M^{- 1 / 2} e_{\pm}$ , $K u_{\pm} = λ_{\pm} M u_{\pm}$ with the displayed $λ_{\pm}$ , and $K$ is positive definite.

[F2]

Forced modal response (The forced coupled quadratic model: modal responses, resonance, and boundedness for positive definite stiffness off resonance clauses 1-3): the unique motion with a datum has the modal convolution form with $ψ = O^{T} M^{- 1 / 2} J$ ; for $J (t) = J_{0} \cos (Ω t)$ the modal force is $ψ (t) = ψ_{0} \cos (Ω t)$ with $ψ_{0} = O^{T} M^{- 1 / 2} J_{0}$ ; the sinusoidal particular functions of clauses 2(a)-(c) hold; every motion is $q^{p} + q^{h}$ with $q^{h}$ free; in the resonant cases (some $ψ_{0, i} \neq 0$ with $λ_{i} > 0$ , $Ω^{2} = λ_{i}$ , or $λ_{i} = 0$ , $Ω = 0$ ) every motion is unbounded on $[0, \infty)$ ; and for positive definite $K$ with no resonant index of nonzero modal force, every motion is bounded.

[F3]

Prescribed generalized force (The coupled quadratic oscillator model: mass metric, stiffness, generalized force, modal vocabulary and the small-oscillation model at a mechanical equilibrium clause (b)): $J$ is continuous prescribed model data. For $Ω > 0$ the cosine term has the restricted sinusoidal-drive status of The sinusoidally driven oscillator model: a prescribed external force $f_{0} \cos (Ω t)$ added to the damped oscillator clause (ii); for $Ω = 0$ it is the constant-force specialization of the general $J$ data. In both cases it depends on time alone and has no modelled back-reaction.

[F4]

Direct linear algebra (Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes, The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ): $M^{- 1 / 2} = \frac{1}{\sqrt{m}} I_{2}$ , $J_{0} = F (1, 1) / \sqrt{2 m}$ , $e_{+}^{T} (1, 1) = \sqrt{2}$ , $e_{-}^{T} (1, 1) = 0$ ; the products below are direct computations. The particular motions displayed are differentiated by the chain rule (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ).

Verification

technique · direct; compute the modal force, instantiate the resonant and non-resonant cases of the forced modal theorem, and evaluate the steady amplitude

1.1F1F4algebra

Modal force: with $J_{0} = F u_{+} = F (1, 1) / \sqrt{2 m}$ , $ψ_{0} = O^{T} M^{- 1 / 2} J_{0} = \frac{F}{\sqrt{m}} (\begin{array}{c} e_{+}^{T} \\ e_{-}^{T} \end{array}) \frac{(1, 1)}{\sqrt{2 m}} = \frac{F}{m} (\begin{array}{c} 1 \\ 0 \end{array}),$ because $e_{+}^{T} (1, 1) = \sqrt{2}$ and $e_{-}^{T} (1, 1) = 0$ . This is clause 1.

2.1F1F2F4step 1.1algebra

Resonant case: for $Ω = ω_{+}$ , $λ_{+} = Ω^{2}$ and $ψ_{0, +} = F / m \neq 0$ ; by [F2] clause 2(b) the function $z_{+}^{p} (t) = \frac{F}{m} \frac{t \sin (ω_{+} t)}{2 ω_{+}}$ solves the in-phase modal equation and $q^{p} = M^{- 1 / 2} O z^{p} = \frac{F}{2 m ω_{+}} t \sin (ω_{+} t) u_{+}$ is a motion of the model, with the stated linearly growing amplitude; and by [F2] clause 3(a) every motion of the model is unbounded on $[0, \infty)$ . This is clause 2.

2.2F1F2F4step 1.1algebra

Non-resonant case: if $Ω^{2} \neq k / m = λ_{+}$ , then the only index with $ψ_{0, i} \neq 0$ is $i = +$ (since $ψ_{0, -} = 0$ ), and it is not resonant; $K$ is positive definite by [F1], so [F2] clause 3(b) gives that every motion is bounded on $[0, \infty)$ . At $Ω = ω_{-}$ the steady in-phase response of [F2] clause 2(a) has amplitude $∣ ψ_{0, +} ∣ / ∣ λ_{+} - Ω^{2} ∣ = \frac{∣ F ∣}{m} / \frac{2 c}{m} = ∣ F ∣ / (2 c)$ , and the relative mode has zero modal force. This is clause 3.

3.1F2step 1.1step 2.1step 2.2

Resonance reading: by [F2] the resonant frequencies are exactly the frequencies of the modal directions with nonzero modal force component; here $ψ_{0}$ is supported on the in-phase direction alone, so the resonance is at $ω_{+}$ and the equally available frequency $ω_{-}$ of the relative mode does not produce resonance for this drive. This is clause 4.

4.1F3step 1.1step 2.1step 2.2step 3.1∎

Clauses 1-4 are verified on the explicit data under the prescribed drive [F3]; no damping, back-reaction, measured response or apparatus detail is asserted, and the parameters are model data.

Remarks

The unbounded motion is a mode-shaped oscillation. The resonant motion of clause 2 keeps the in-phase pattern $u_{+}$ fixed and grows linearly in amplitude; it is not a runaway in an arbitrary direction, and the prescribed particular response has zero relative coordinate. An arbitrary motion can additionally contain the bounded homogeneous relative oscillation of the free model.
Why the amplitude at $Ω = ω_{-}$ grows as $c \to 0^{+}$ . $∣ F ∣ / (2 c)$ is the steady amplitude at the relative-mode frequency; as the coupling tends to zero the two frequencies merge ( $ω_{-} \to ω_{+}$ ) and the drive approaches resonance, so the bounded steady amplitude grows without bound. This is the limiting consistency of clauses 2 and 3 and not an assertion about any particular apparatus.

A drive along the in-phase pattern of the two-mass chain: resonance exactly at that mode's frequency and a bounded steady response off resonance

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources