ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-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.

Five worked initial value problems for the homogeneous oscillator across the discriminant, degenerate and repulsive cases

Example

In each line, $m = 1$ and the initial datum $(x_{0}, v_{0})$ is prescribed for the homogeneous model with time domain $I = R$ and zero forcing, $x^{''} + c x^{'} + k x = 0$ (The damped driven oscillator model: second-order equation, phase-plane system and characteristic data). The solution is read off from the classification theorem and the degenerate-case proposition, and its initial values are checked explicitly.

(i) $k = 4$ , $c = 0$ , $(x_{0}, v_{0}) = (1, 0)$ : the solution is $x (t) = \cos (2 t)$ .
(ii) $k = 1$ , $c = 2$ , $(x_{0}, v_{0}) = (1, 0)$ : the solution is $x (t) = (1 + t) e^{- t}$ .
(iii) $k = 1$ , $c = 3$ , $(x_{0}, v_{0}) = (1, 0)$ : with $λ_{\pm} = (- 3 \pm \sqrt{5}) / 2$ the solution is $x (t) = (- λ_{-} e^{λ_{+} t} + λ_{+} e^{λ_{-} t}) / \sqrt{5}$ .
(iv) $k = 0$ , $c = 2$ , $(x_{0}, v_{0}) = (0, 1)$ : the solution is $x (t) = \frac{1}{2} (1 - e^{- 2 t})$ .
(v) $k = - 1$ , $c = 0$ , $(x_{0}, v_{0}) = (1, 0)$ : the solution is $x (t) = \frac{1}{2} (e^{t} + e^{- t})$ , which is unbounded on $[0, \infty)$ .

Facts & Assumptions

Given: The homogeneous model of The damped driven oscillator model: second-order equation, phase-plane system and characteristic data with $m = 1$ and the parameters of the five lines.

[L1]

For $k > 0$ the solutions are classified by the sign of $Δ = c^{2} - 4 m k$ as in The homogeneous damped oscillator: solution classification by the discriminant and uniqueness for initial data: distinct real roots in case 1, a double root $λ = - c / (2 m)$ in case 2, and the family $e^{- γ t} (A \cos ω t + B \sin ω t)$ with $γ = c / (2 m)$ , $ω = \sqrt{k / m - γ^{2}}$ in case 3; clause 4 gives the coefficient formulas $A = (v_{0} - λ_{-} x_{0}) / (λ_{+} - λ_{-})$ , $B = (λ_{+} x_{0} - v_{0}) / (λ_{+} - λ_{-})$ in case 1; $A = x_{0}$ , $B = v_{0} - λ x_{0}$ in case 2; $A = x_{0}$ , $B = (v_{0} + γ x_{0}) / ω$ in case 3. [given]

[L2]

For $k \leq 0$ the solutions are those of The degenerate and repulsive oscillator: solutions for k=0 and the explicit growing solution for k<0: for $k = 0$ , $c > 0$ they are $A + B e^{- c t / m}$ with $A = x_{0} + v_{0} m / c$ , $B = - v_{0} m / c$ ; for $k < 0$ they are $A e^{λ_{+} t} + B e^{λ_{-} t}$ with $λ_{\pm} = (- c \pm \sqrt{c^{2} - 4 m k}) / (2 m)$ , $λ_{-} < 0 < λ_{+}$ , and $e^{λ_{+} t} \to + \infty$ . [given]

[L3]

$(\cos t)^{'} = - \sin t$ , $(\sin t)^{'} = \cos t$ , and $(e^{μ t})^{'} = μ e^{μ t}$ for real $μ$ . [thm-sine-and-cosine-derivatives, thm-derivative-of-exponential]

Verification

technique · direct; compute the discriminant and coefficients in each line and check the initial data

1.1givenL1L3algebra

Line (i): $Δ = 0 - 16 < 0$ and $γ = 0$ , $ω = \sqrt{4} = 2$ , so by [L1] case 3 the solution is $A \cos 2 t + B \sin 2 t$ with $A = x_{0} = 1$ , $B = (v_{0} + γ x_{0}) / ω = 0$ ; by [L3] the candidate $\cos (2 t)$ has value $1$ and derivative $- 2 \sin (2 t)$ vanishing at $0$ , so it is the solution.

1.2givenL1L3algebra

Line (ii): $Δ = 4 - 4 = 0$ , so the double root is $λ = - 1$ and the family is $(A + B t) e^{- t}$ with $A = x_{0} = 1$ , $B = v_{0} - λ x_{0} = 1$ ; the candidate $(1 + t) e^{- t}$ has the value $1$ and derivative $e^{- t} - (1 + t) e^{- t} = - t e^{- t}$ equal to $0$ at $t = 0$ , matching $(x_{0}, v_{0}) = (1, 0)$ .

1.3givenL1algebra

Line (iii): $Δ = 5 > 0$ and $λ_{\pm} = (- 3 \pm \sqrt{5}) / 2$ with $λ_{+} - λ_{-} = \sqrt{5}$ and $λ_{+} + λ_{-} = - 3$ ; the coefficients of [L1] case 1 are $A = (v_{0} - λ_{-} x_{0}) / \sqrt{5} = - λ_{-} / \sqrt{5}$ and $B = (λ_{+} x_{0} - v_{0}) / \sqrt{5} = λ_{+} / \sqrt{5}$ , so the solution is $x (t) = A e^{λ_{+} t} + B e^{λ_{-} t} = (- λ_{-} e^{λ_{+} t} + λ_{+} e^{λ_{-} t}) / \sqrt{5}$ . Then $x (0) = (λ_{+} - λ_{-}) / \sqrt{5} = 1$ and $x^{'} (0) = λ_{+} A + λ_{-} B = (- λ_{+} λ_{-} + λ_{-} λ_{+}) / \sqrt{5} = 0$ , matching $(x_{0}, v_{0}) = (1, 0)$ .

1.4givenL2L3algebra

Line (iv): $k = 0$ , $c = 2 > 0$ , and [L2] gives $x (t) = A + B e^{- 2 t}$ with $A = 0 + 1 / 2 = 1 / 2$ , $B = - 1 / 2$ , that is $x (t) = \frac{1}{2} (1 - e^{- 2 t})$ ; its derivative is $e^{- 2 t}$ by [L3], so $x (0) = 0$ and $x^{'} (0) = 1$ .

2.1givenL2L3algebra∎

Line (v): $k = - 1 < 0$ and $λ_{\pm} = \pm 1$ by [L2]; the solution with data $(1, 0)$ is $\frac{1}{2} e^{t} + \frac{1}{2} e^{- t}$ (the coefficients $A = B = 1 / 2$ solve $A + B = 1$ , $A - B = 0$ ), and it is unbounded on $[0, \infty)$ because $e^{t} \to + \infty$ , in accordance with [L2].

Five worked initial value problems for the homogeneous oscillator across the discriminant, degenerate and repulsive cases

Example

Facts & Assumptions

Verification

Depends on

Dependency tree · 2 levels

Sources