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 linear triatomic chain: the translation zero mode, the antisymmetric stretch and the symmetric stretch, with the corrected frequency comparison

Physical scope

A worked instance of the coupled quadratic model: a linear chain of three labels with masses m, m_c, m joined by identical nearest-neighbour springs of stiffness k, modelled by the quadratic stiffness matrix k[[1,-1,0],[-1,2,-1],[0,-1,1]], with its three modal patterns (translation at zero modal stiffness, antisymmetric stretch at sqrt(k/m) and symmetric stretch at sqrt((k/m)(1+2m/m_c))), the general motion, the affine translation zero mode and the corrected frequency ordering omega_3>omega_2. The parameters are model data with declared units; the example asserts no measured molecular frequency and no empirical identification of the chain with a real molecule.

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.

Global-time, growth and boundedness claims below refer to the unique maximal extension of the autonomous free equation on $R$ ; local motions remain its restrictions. Values at $0$ in coefficient formulas are evaluated on that extension when the original interval omits $0$ .

Consider three particle labels constrained to a line, with coordinates $x_{1}, x_{2}, x_{3}$ in metres and masses $m, m_{c}, m > 0$ read in kilograms (Dimensions and SI unit conventions of the non-relativistic classical mechanics framework); the outer labels have mass $m$ and the middle label mass $m_{c}$ . Adjacent labels interact through identical springs of stiffness $k > 0$ in kilograms per second squared, and the potential is approximated by its quadratic part $U = \frac{k}{2} ((x_{1} - x_{2})^{2} + (x_{2} - x_{3})^{2})$ about the equilibrium. The model is the coupled quadratic model of The coupled quadratic oscillator model: mass metric, stiffness, generalized force, modal vocabulary and the small-oscillation model at a mechanical equilibrium with $n = 3$ , $q = (x_{1}, x_{2}, x_{3})$ ,

$M = diag (m, m_{c}, m), K = k (\begin{array}{ccc} 1 & - 1 & 0 \\ - 1 & 2 & - 1 \\ 0 & - 1 & 1 \end{array}) .$

Then:

$M$ is symmetric positive definite and $K$ is symmetric with $\ker K = span {(1, 1, 1)}$ ;
the modal data are as follows, with $M$ -orthonormal modal vectors: (a) $λ_{1} = 0$ with $u_{1} = (1, 1, 1) / \sqrt{2 m + m_{c}}$ : the translation mode, in which the three labels move together; (b) $λ_{2} = k / m$ with $u_{2} = (1, 0, - 1) / \sqrt{2 m}$ : the antisymmetric stretch, in which the outer labels move oppositely and the middle label is at rest; (c) $λ_{3} = \frac{k}{m} (1 + \frac{2 m}{m_{c}})$ with $u_{3} = (1, - 2 m / m_{c}, 1) / \sqrt{2 m (1 + 2 m / m_{c})}$ : the symmetric stretch, in which the outer labels move together and the middle label moves oppositely;
every motion is $q (t) = (a + b t) u_{1} + (A \cos (ω_{2} t) + B \sin (ω_{2} t)) u_{2} + (C \cos (ω_{3} t) + D \sin (ω_{3} t)) u_{3}$ with $ω_{2} = \sqrt{k / m}$ and $ω_{3} = \sqrt{\frac{k}{m} (1 + \frac{2 m}{m_{c}})}$ , and the pure-zero-mode motions are exactly the affine curves $q (t) = (a + b t) u_{1}$ ; for $b \neq 0$ they are unbounded on $[0, \infty)$ ;
$ω_{3} > ω_{2}$ for all $m, m_{c} > 0$ : in this model the symmetric stretch is the stiffer vibration.

Facts & Assumptions

Given: The data $m, m_{c}, k > 0$ , the matrices $M, K$ of the Example, the vectors $u_{1}, u_{2}, u_{3}$ and the numbers $λ_{1}, λ_{2}, λ_{3}$ .

[F1]

Model dictionary (The coupled quadratic oscillator model: mass metric, stiffness, generalized force, modal vocabulary and the small-oscillation model at a mechanical equilibrium): the data $(M, K, 0)$ declare a free coupled quadratic model with three degrees of freedom, kinetic energy $\frac{1}{2} \sum_{i} m_{i} x_{i}^{' 2}$ and potential energy $\frac{1}{2} q^{T} K q$ ; the modal vocabulary is that of clause (e).

[F2]

Free-mode theory (The free coupled quadratic model: global existence, the complete modal classification, mode energies, intrinsic degenerate mode subspaces, boundedness and the unstable direction clauses 2, 4 and 5): every free motion is a modal superposition with oscillatory, affine or exponential families according to the sign of $λ_{i}$ ; the pure- $λ$ motions are the solutions of $q^{''} + λ q = 0$ with values in the intrinsic subspace $N_{λ}$ , which for $λ = 0$ are the affine curves in $N_{0} = \ker K$ ; an affine component with nonzero slope is unbounded on $[0, \infty)$ .

[F3]

Two-mode check (Two equal masses with two outer springs and a coupling spring: eigenmodes, decoupling and the explicit normal frequencies): the two-label symmetric case with outer stiffness $k$ and coupling $c$ has frequencies $\sqrt{k / m}$ and $\sqrt{(k + 2 c) / m}$ ; it is the $2 \times 2$ instance of the same eigenproblem and is used below only as a consistency check on the antisymmetric sector.

[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}$ ): matrix-vector products and $M$ -inner products are computed componentwise; the products displayed in the Verification are direct computations.

[F5]

Scalar oscillator calculus: for $λ_{i} > 0$ , The homogeneous damped oscillator: solution classification by the discriminant and uniqueness for initial data with scalar mass $1$ , damping $0$ and stiffness $λ_{i}$ gives exactly $z_{i} (t) = A_{i} \cos (\sqrt{λ_{i}} t) + B_{i} \sin (\sqrt{λ_{i}} t)$ . Its hypothesis $k > 0$ excludes the zero-stiffness case; the affine family for $λ_{i} = 0$ is supplied by [F2]. The chain rule The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ governs differentiation of composites, and $C^{k}$ Euclidean maps and diffeomorphisms supplies the $C^{2}$ regularity convention.

Verification

technique · direct; verify the three eigenpairs by explicit matrix multiplication and read the motion statement from the free-mode theorem

1.1F1F4algebra

Kernel and positivity: $q^{T} K q = k ((x_{1} - x_{2})^{2} + (x_{2} - x_{3})^{2}) \geq 0$ with equality if and only if $x_{1} = x_{2} = x_{3}$ , so $K$ is symmetric non-negative with the stated kernel; $M$ is diagonal with positive entries.

1.2F1F4algebra

Eigenpairs: multiplying, $K u_{1} = 0, K u_{2} = k (1, 0, - 1) / \sqrt{2 m} = \frac{k}{m} M u_{2}, K u_{3} = k (1 + \frac{2 m}{m_{c}}) (1, - 2, 1) / \sqrt{2 m (1 + 2 m / m_{c})} = \frac{k}{m} (1 + \frac{2 m}{m_{c}}) M u_{3},$ using $M u_{3} = m (1, - 2, 1) / \sqrt{2 m (1 + 2 m / m_{c})}$ . Direct products give $u_{1}^{T} M u_{1} = (2 m + m_{c}) / (2 m + m_{c}) = 1$ , $u_{2}^{T} M u_{2} = 2 m / (2 m) = 1$ , and $u_{3}^{T} M u_{3} = (2 m + 4 m^{2} / m_{c}) / (2 m (1 + 2 m / m_{c})) = 1$ ; the three mixed numerators are $m - m = 0$ , $m - 2 m + m = 0$ , and $m - m = 0$ , respectively, so the modal vectors are $M$ -orthonormal. This proves clauses 1 and 2.

2.1F3step 1.2

Consistency check: on the antisymmetric sector $x_{1} = - x_{3}$ , $x_{2} = 0$ , the displayed equations give $m x_{1}^{''} = - k x_{1}$ and $m x_{3}^{''} = - k x_{3}$ , with the middle equation identically zero. Thus the frequency is $\sqrt{k / m}$ . Equivalently, this is the two-label model of [F3] with outer stiffness $k$ and zero coupling, whose two equal frequencies are $\sqrt{k / m}$ ; no spurious coupling term is used.

2.2F2F5step 1.2

Motions: since $λ_{1} = 0 < λ_{2} < λ_{3}$ , [F2] gives that every motion is the displayed superposition with the affine family for $λ_{1}$ and oscillatory families for $λ_{2}, λ_{3}$ ; the pure-zero-mode motions form the affine curves in $N_{0} = \ker K = span {u_{1}}$ , i.e. $q (t) = (a + b t) u_{1}$ , which are unbounded on $[0, \infty)$ for $b \neq 0$ because $∣ a + b t ∣ \to \infty$ . This is clause 3.

2.3step 1.2algebra

Frequency ordering: $ω_{3}^{2} / ω_{2}^{2} = 1 + 2 m / m_{c} > 1$ , so $ω_{3} > ω_{2}$ for every $m_{c} > 0$ ; this is clause 4.

3.1step 1.2step 2.2step 2.3given∎

Clauses 1-4 are verified on the explicit data. The comparison in clause 4 is read off the eigenvalues computed from the displayed matrices; the cited treatment's sentence comparing the two frequencies is not used, because with the matrices it displays the computed eigenvalues give the opposite ordering, and the discrepancy is recorded as a source error in the reader record for that treatment. All parameters are model data; no molecular frequency, force constant or apparatus behaviour is asserted.

Remarks

The zero mode is the centre-of-mass motion. $u_{1}$ moves all three labels together; the quadratic potential is blind to it, and the model has no restoring force in that direction. This is the exact mechanism of a translation mode: a linearization about a non-isolated minimum (the equilibrium manifold here is the line $x_{1} = x_{2} = x_{3}$ ) acquires a zero modal stiffness. If the physical chain is confined, or an external restoring force acts on the centre of mass, the data change (an additional stiffness term appears) and the zero mode disappears.
What the example does not establish. The quadratic potential is the second-order truncation of the real interatomic potential; the example computes the normal modes of the truncated model and asserts nothing about the accuracy of that truncation, the anharmonic behaviour at larger amplitudes, or the vibrational spectrum of any real molecule.

A linear triatomic chain: the translation zero mode, the antisymmetric stretch and the symmetric stretch, with the corrected frequency comparison

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources