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 harmonic model on explicit data: the sinusoid, its least period, the conserved energy and the phase ellipse checked at $m = 1$ , $k = 4$

Physical scope

A worked check of the harmonic model at the declared data m=1 kg, k=4 N/m, datum (0, 0 m, 1 m/s): the displayed sinusoid is the unique maximal motion, its amplitude and phase, least period, frequency, conserved energy and phase ellipse are computed from the general theorem, and the energy identity is verified directly. The item asserts no measured value and no claim that a real oscillator realizes the model.

Example

Declare the harmonic model of The harmonic (linear restoring) model: a declared linear force law with parameter $k > 0$ with the data $m = 1 k g, k = 4 N / m = 4 k g / s^{2},$ time window $R$ and configuration domain $R$ , and the datum at $t_{0} = 0$ $x_{0} = 0 m, v_{0} = 1 m / s .$ The claim checked below is that the curve $x_{p h y s} (t_{p h y s}) = \frac{1}{2} \sin (2 t_{p h y s} / (1 s)) m (t_{p h y s} \in R)$ is the unique maximal motion of the model with this datum, that its least positive period is $π$ seconds, that its energy is the constant $\frac{1}{2}$ joule, and that its phase curve is the ellipse $4 x^{2} + v^{2} = 1$ in the numerical SI phase coordinates $x : = x_{p h y s} / (1 m)$ and $v : = v_{p h y s} / (1 m / s)$ of The phase plane of a one-dimensional model: phase curves, the energy function and its level sets, and turning points. All coefficient calculations below use these numerical coordinates and $t : = t_{p h y s} / (1 s)$ ; equivalently the physical ellipse is $4 (x_{p h y s} / (1 m))^{2} + (v_{p h y s} / (1 m / s))^{2} = 1$ .

Verification

Proof technique: direct; read the general theorem at the declared data, compute the coefficients, and verify the displayed identities by differentiation and substitution.

Given: The harmonic model with $m = 1$ kg, $k = 4$ kg/s $^{2}$ , the datum $(0, 0, 1)$ , and the curve $x (t) = \frac{1}{2} \sin (2 t)$ .

[L1] Model and general theory (The harmonic (linear restoring) model: a declared linear force law with parameter $k > 0$ , The motions of the harmonic model are the sinusoids $A \cos (ω (t - t_{0})) + B \sin (ω (t - t_{0}))$ : amplitude and phase, the least period, the conserved energy $k R^{2} / 2$ and the elliptical phase curves, Existence, uniqueness and conservation of energy for a one-dimensional conservative model: phase curves lie in energy level sets and the velocity is determined by the position and energy up to sign): the model has $F (x) = - 4 x$ , energy $E = \frac{1}{2} v^{2} + 2 x^{2}$ , undamped frequency $ω = \sqrt{k / m}$ , and every motion has the form $A \cos (ω (t - t_{0})) + B \sin (ω (t - t_{0}))$ with $A = x (t_{0})$ , $B = x^{'} (t_{0}) / ω$ , amplitude $R = \sqrt{A^{2} + B^{2}}$ , conserved energy $\frac{1}{2} k R^{2}$ , least period $2 π / ω$ if $R > 0$ , and phase curve contained in, and filling, the ellipse $x^{2} / R^{2} + v^{2} / (ω^{2} R^{2}) = 1$ .

[L2] Values and derivatives (The derivatives of sine and cosine are cosine and minus sine, 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)$ , 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$ , Parity and the Pythagorean identity for sine and cosine, Quarter-turn values and shifts by pi/2 and pi, The zero sets of sine and cosine and the least positive common period 2 pi): $(\sin (2 t))^{'} = 2 \cos (2 t)$ , $(\cos (2 t))^{'} = - 2 \sin (2 t)$ , $\sin^{2} + \cos^{2} = 1$ , $\sin (π / 2) = 1$ , $\cos (π / 2) = 0$ , and $\cos (u + 2 π) = \cos u$ , $\sin (u + 2 π) = \sin u$ for all $u$ .

[L3] Dimensions are read by Dimensions and SI unit conventions of the non-relativistic classical mechanics framework: $[k] = μ τ^{- 2}$ , $[m] = μ$ , so $[k / m] = τ^{- 2}$ .

1.1givenL1L3algebra

The frequency is $ω = \sqrt{k / m} = \sqrt{4} s^{- 1} = 2 s^{- 1}$ by [L1] and [L3], and $A = x_{0} = 0$ , $B = v_{0} / ω = \frac{1}{2}$ m. By clause 1 of The motions of the harmonic model are the sinusoids $A \cos (ω (t - t_{0})) + B \sin (ω (t - t_{0}))$ : amplitude and phase, the least period, the conserved energy $k R^{2} / 2$ and the elliptical phase curves the curve $x (t) = \frac{1}{2} \sin (2 t)$ is the unique maximal motion with the declared datum, defined on $R$ .

2.1step 1.1L1L2algebra

Amplitude and phase: $R = \sqrt{0^{2} + (1 / 2)^{2}} = \frac{1}{2}$ m; taking $φ = π / 2$ gives $\cos φ = 0 = A / R$ and $\sin φ = 1 = B / R$ by [L2], so clause 2 of The motions of the harmonic model are the sinusoids $A \cos (ω (t - t_{0})) + B \sin (ω (t - t_{0}))$ : amplitude and phase, the least period, the conserved energy $k R^{2} / 2$ and the elliptical phase curves gives $x (t) = \frac{1}{2} \cos (2 t - π / 2) = \frac{1}{2} \sin (2 t)$ , the displayed curve.

2.2step 1.1L1L2algebra

Period and frequency: $R > 0$ , so by clause 3 of The motions of the harmonic model are the sinusoids $A \cos (ω (t - t_{0})) + B \sin (ω (t - t_{0}))$ : amplitude and phase, the least period, the conserved energy $k R^{2} / 2$ and the elliptical phase curves the least positive period is $2 π / ω = π$ s, and the frequency is $1 / π$ cycles per second; indeed $\sin (2 (t + π)) = \sin (2 t + 2 π) = \sin (2 t)$ by [L2].

2.3step 1.1L1L2algebra

Energy: by clause 4 of The motions of the harmonic model are the sinusoids $A \cos (ω (t - t_{0})) + B \sin (ω (t - t_{0}))$ : amplitude and phase, the least period, the conserved energy $k R^{2} / 2$ and the elliptical phase curves, $E = \frac{1}{2} k R^{2} = \frac{1}{2} \cdot 4 \cdot \frac{1}{4} = \frac{1}{2}$ J, constant in $t$ . Directly, with $x^{'} (t) = \cos (2 t)$ by [L2], $E (x (t), x^{'} (t)) = \frac{1}{2} \cos^{2} (2 t) + 2 \cdot \frac{1}{4} \sin^{2} (2 t) = \frac{1}{2} (\cos^{2} (2 t) + \sin^{2} (2 t)) = \frac{1}{2},$ using [L1] and the Pythagorean identity of [L2].

3.1step 2.1L1L2algebra∎

Phase ellipse: with $R^{2} = \frac{1}{4}$ and $ω^{2} R^{2} = 1$ , the ellipse of clause 4 is $4 x^{2} + v^{2} = 1$ ; the phase curve $(\frac{1}{2} \sin (2 t), \cos (2 t))$ satisfies $4 \cdot \frac{1}{4} \sin^{2} (2 t) + \cos^{2} (2 t) = 1$ by [L2], and by clause 4 of The motions of the harmonic model are the sinusoids $A \cos (ω (t - t_{0})) + B \sin (ω (t - t_{0}))$ : amplitude and phase, the least period, the conserved energy $k R^{2} / 2$ and the elliptical phase curves it fills the ellipse; the amplitude $\frac{1}{2}$ m is attained at $t = π / 4 + n π / 2$ , $n \in Z$ , where $\cos (2 t - π / 2) = \pm 1$ .

Remarks

What the check exhibits. The data produce the motion $\frac{1}{2} \sin (2 t)$ with exact period $π$ s, energy $\frac{1}{2}$ J and phase ellipse $4 x^{2} + v^{2} = 1$ ; the check exercises clause 1-4 of The motions of the harmonic model are the sinusoids $A \cos (ω (t - t_{0})) + B \sin (ω (t - t_{0}))$ : amplitude and phase, the least period, the conserved energy $k R^{2} / 2$ and the elliptical phase curves and the conservation and level-set statements of Existence, uniqueness and conservation of energy for a one-dimensional conservative model: phase curves lie in energy level sets and the velocity is determined by the position and energy up to sign on one motion.
Scope. The values $m = 1$ kg and $k = 4$ N/m are declared data of this computation; no measured value is asserted, and no real spring is claimed to obey the linear law in any regime.

A harmonic model on explicit data: the sinusoid, its least period, the conserved energy and the phase ellipse checked at $m = 1$ , $k = 4$

Example

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources

A harmonic model on explicit data: the sinusoid, its least period, the conserved energy and the phase ellipse checked at m=1m=1, k=4k=4

Example

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources

A harmonic model on explicit data: the sinusoid, its least period, the conserved energy and the phase ellipse checked at $m = 1$ , $k = 4$