LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generated

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.

Solutions of $v^{''} + ω^{2} v = 0$ are exactly the functions $A \cos (ω (t - t_{0})) + B \sin (ω (t - t_{0}))$

Statement

Let $ω > 0$ , let $I \subseteq R$ be an interval with at least two points (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length), let $t_{0} \in I$ , and let $v : I \to R$ be twice differentiable with

$v^{''} (t) + ω^{2} v (t) = 0 (t \in I) .$

Here twice differentiable means that $v$ and $v' : I \to R$ are differentiable at every point of $I$ in the domain-relative sense of 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; $v'' = (v')'$ , with one-sided limits at included endpoints.

Then there are reals $A, B$ with

$v (t) = A \cos (ω (t - t_{0})) + B \sin (ω (t - t_{0})) (t \in I) .$

Conversely, for all reals $A, B$ the function $t \mapsto A \cos (ω (t - t_{0})) + B \sin (ω (t - t_{0}))$ is twice differentiable on $R$ and satisfies $v^{''} + ω^{2} v = 0$ there.

Facts & Assumptions

Given: A real $ω > 0$ , an interval $I \subseteq R$ with at least two points, a point $t_{0} \in I$ , and a twice differentiable $v : I \to R$ with $v^{''} + ω^{2} v = 0$ on $I$ .

[L1]

Sine and cosine are differentiable with $(\sin u)^{'} = \cos u$ and $(\cos u)^{'} = - \sin u$ ; the chain rule differentiates the compositions $t \mapsto \cos (ω (t - t_{0}))$ , $t \mapsto \sin (ω (t - t_{0}))$ with derivatives $- ω \sin (ω (t - t_{0}))$ and $ω \cos (ω (t - t_{0}))$ (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)$ ).

[L2]

Sums, products and constant multiples of differentiable functions are differentiable with the usual rules (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$ ).

[L3]

A function continuous on $I$ whose derivative vanishes at every interior point of $I$ is constant on $I$ (A function continuous on an interval $I$ whose derivative vanishes at every interior point of $I$ is constant on $I$ ; consequently two such functions with the same derivative differ by a constant).

[L4]

$\sin^{2} + \cos^{2} = 1$ identically (Parity and the Pythagorean identity for sine and cosine).

Proof

technique · direct

1.1givenL1L2construct

Write $φ (t) : = ω (t - t_{0})$ and define $w : = v \cos φ - \frac{v^{'}}{ω} \sin φ, z : = v \sin φ + \frac{v^{'}}{ω} \cos φ$ on $I$ . Every factor is differentiable (including $v'$ , by the twice differentiable hypothesis), so $w$ and $z$ are differentiable by [L2].

1.2givenL1L2algebra

Differentiating and using $v^{''} = - ω^{2} v$ : $w^{'} = v^{'} \cos φ - ω v \sin φ - \frac{v^{''}}{ω} \sin φ - v^{'} \cos φ = - \frac{ω^{2} v + v^{''}}{ω} \sin φ = 0,$ and likewise $z^{'} = v^{'} \sin φ + ω v \cos φ + \frac{v^{''}}{ω} \cos φ - v^{'} \sin φ = \frac{ω^{2} v + v^{''}}{ω} \cos φ = 0$ on $I$ .

2.1step 1.1step 1.2L3

By [L3] and step 1.2 there are reals $A, B$ with $w = A$ and $z = B$ on $I$ .

3.1step 1.1step 2.1L4algebra

Multiplying out and using [L4], $w \cos φ + z \sin φ = v (\cos^{2} φ + \sin^{2} φ) = v$ on $I$ ; hence $v = A \cos φ + B \sin φ$ , which is the asserted representation.

4.1L1L2algebra∎

Conversely, if $u (t) : = A \cos (ω (t - t_{0})) + B \sin (ω (t - t_{0}))$ , then [L1] and [L2] give $u^{'} = - ω A \sin φ + ω B \cos φ$ and $u^{''} = - ω^{2} A \cos φ - ω^{2} B \sin φ = - ω^{2} u$ on $I$ , so $u^{''} + ω^{2} u = 0$ .

Solutions of $v^{''} + ω^{2} v = 0$ are exactly the functions $A \cos (ω (t - t_{0})) + B \sin (ω (t - t_{0}))$

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

Solutions of v′′+ω2v=0v′′+ω2v=0 are exactly the functions Acos⁡(ω(t−t0))+Bsin⁡(ω(t−t0))Acos(ω(t−t0​))+Bsin(ω(t−t0​))

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

Solutions of $v^{''} + ω^{2} v = 0$ are exactly the functions $A \cos (ω (t - t_{0})) + B \sin (ω (t - t_{0}))$