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.
Constant forcing: free fall and the approach to terminal velocity under linear drag
Example
Let , and consider the two constant-forcing models with time domain (the half-line solution in (ii) is the restriction of its global solution) (The damped driven oscillator model: second-order equation, phase-plane system and characteristic data).
- (i) Uniform force: with data , . The unique solution is .
- (ii) Linear drag: , , , that is , with data . The unique solution on is , and its velocity increases to the limiting value .
Facts & Assumptions
Given: The parameters and the data of the two lines; the forced oscillator theorem applies in both since and the forcing is constant, hence continuous.
For , , and continuous , the unique solution of with data at is , where is the homogeneous solution with the data and is the homogeneous kernel with , ; for one has , and for , one has (The forced oscillator with : unique global solution and the convolution (Green's function) formula, The degenerate and repulsive oscillator: solutions for k=0 and the explicit growing solution for k<0). [given]
For the homogeneous solutions are when and when , with , respectively , (The degenerate and repulsive oscillator: solutions for k=0 and the explicit growing solution for k<0). [given]
for real , and sums and scalar multiples are differentiated termwise. [thm-derivative-of-exponential, thm-algebra-of-derivatives]
Verification
Line (i): here , so [L1] gives and by [L2]; hence because .
Line (ii): here , , and ; by [L1], , and the datum gives by [L2]. Hence
Velocity: by [L3], , so and as because ; moreover , so , confirming both lines satisfy their equations with the prescribed data.
Depends on
The forced oscillator with : unique global solution and the convolution (Green's function) formula
The degenerate and repulsive oscillator: solutions for k=0 and the explicit growing solution for k<0
The damped driven oscillator model: second-order equation, phase-plane system and characteristic data
The exponential function is smooth and
Sums, scalar multiples, products and quotients: , , , and when
Dependency tree · 2 levels
Sources
- K. Likharev, Essential Graduate Physics, Classical Mechanics (complete 252-page volume), Chapter 5 Section 5.1, Eq. (5.13) and Chapter 2 Section 2.4 (linear drag and terminal velocity in one-dimensional motion), printed pages 3 and 2-4 of the respective chapters
- I. Stewart, Advanced Classical Mechanics (MIT 8.09 Fall 2014, complete course text), Chapter 7 Section 7.1: the damped oscillator equation and its damping parameter, printed pages 146-148