Ordinary differential equation: finding the order and checking the candidates y=x² and y=x²+x

Goal and scope

On the interval I=ℝ consider the ordinary differential equation y″−2y′+y=x²−4x+2. (1) Determine its order; (2) check that y₁(x)=x² is a solution on all of ℝ (its residual is identically zero); (3) prove that y₂(x)=x²+x has residual x−2, which vanishes only at x=2, so it is not a solution on ℝ; (4) check the initial values y(0)=0, y′(0)=0 and, citing the existence and uniqueness theorem for second-order linear equations with its hypotheses, conclude that y₁ is the unique solution of this initial value problem; (5) show that without initial values the solution is not unique.

The main checks are limited to integer-coefficient polynomial candidates and exact residuals (MKO assumption a2); residuals are simplified symbolically, so conclusions hold at every point of the interval, not just at sampled points. Uniqueness is not inferred from the equation itself but from a cited theorem with explicit hypotheses (citation_verified), which this guide does not prove. y₃=x²+eˣ is used only to show that without initial values the solution is not unique. General existence theory and the classification of nonlinear equations are not treated; the canonical MKO and its English edition are not changed.

Givens and symbols

• func_limit_def
• distributive
• eq_replace
• forall_intro
• quantifier_negation

• G1 — Interval I=ℝ; the unknown y is a twice differentiable real-valued function on ℝ; equation E: for every x∈I, y″(x)−2y′(x)+y(x)=x²−4x+2.
• G2 — Candidates: y₁(x)=x² and y₂(x)=x²+x (integer-coefficient polynomials); also y₃(x)=x²+eˣ, used only in S13 and S14 to show non-uniqueness.
• G3 — Initial conditions: y(0)=0 and y′(0)=0.
• G4 — Residual: for a candidate u, r_u(x)=u″(x)−2u′(x)+u(x)−(x²−4x+2). u is a solution of E on I exactly when r_u(x)=0 for every x∈I.

• I=\mathbb{R} — the interval on which the equation is posed
• y',\ y'' — first and second derivatives of the unknown function
• r_u(x) — residual of the candidate u at x: left side minus right side
• y_1,\ y_2,\ y_3 — the three candidate functions
• p,\ q,\ g — coefficients and right side of the standard form y''+py'+qy=g

Rules and sources

• func_limit_def · prerequisite — Limit of a function: lim_{x→a} f(x)=L means that for every ε>0 there is δ>0 such that |f(x)−L|<ε for every domain point x with 0<|x−a|<δ (a must be a limit point of the domain).
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w).
• add_comm · prerequisite — Commutativity of addition: u+v=v+u.
• add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
• mul_inverse_nonzero · prerequisite — Inverse of a nonzero number: in ℚ, ℝ or ℂ, if u≠0 there is 1/u with u·(1/u)=1, and v/u means v·(1/u). 0 has no inverse, so v/0 is undefined.
• abs_rules · prerequisite — Absolute value (reals): |u|=u if u≥0 and |u|=−u if u<0; |u|≥0; |uv|=|u||v|; triangle inequality |u+v|≤|u|+|v|; |u|<r ⇔ −r<u<r.
• mul_one · prerequisite — Multiplicative identity: 1·u=u.
• mul_assoc · prerequisite — Associativity of multiplication: (uv)w=u(vw).
• neg_mul · prerequisite — Signs and multiplication: (−u)v=−(uv) and (−u)(−v)=uv.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• mul_zero · prerequisite — Multiplying by zero: u·0=0. Reason: u·0=u·(0+0)=u·0+u·0; subtracting u·0 from both sides gives 0=u·0.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_ode_def · cited — On a specified interval, an ordinary differential equation relates an unknown single-variable function y and its finite-order derivatives. Its order is the highest derivative order occurring in the equation. A zero substitution residual checks only whether a given candidate satisfies the relation over the specified domain. · mko-ordinary-differential-equation
• mko_ode_check · cited — Checking a candidate means recomputing y, y′, y″ and so on and substituting into the same equation; a zero residual at one point is usually not enough to prove a solution on the whole interval. Initial values can screen candidates, but existence and uniqueness need extra hypotheses such as continuity or a Lipschitz condition, together with the corresponding theorem. · mko-ordinary-differential-equation
• deriv_rules · prerequisite — Differentiation rules on ℝ: the derivative of a constant is 0; (x)′=1; (u+v)′=u′+v′; (cu)′=cu′ for a constant c; (eˣ)′=eˣ.
• poly_exp_continuous · prerequisite — Constant functions and polynomial functions are continuous at every point of ℝ.
• thm_linear_ivp · cited — Let p, q and g be continuous on an open interval I containing x₀. Then for any real numbers Y₀ and Y₁ the initial value problem y″+p(x)y′+q(x)y=g(x), y(x₀)=Y₀, y′(x₀)=Y₁ has exactly one solution, and this solution exists throughout I. · William F. Trench, Elementary Differential Equations with Boundary Value Problems, Section 5.3, Theorem 5.3.1
• L_deriv_square · lemma — For every real x, the function x↦x² is differentiable at x and (x²)′=2x.

Main derivation

y''-2y'+y=x^2-4x+2\ \text{on }I=\mathbb{R}

F(x,y,y',y'')=y''-2y'+y-(x^2-4x+2)=0

F(x,y,y',y'')=0

\text{order}=2

y_1(x)=x^2

y_1'(x)=2x

y_1'(x)=2x

y_1''(x)=2

y_1''(x)-2y_1'(x)+y_1(x)

2-2(2x)+x^2

2-2(2x)+x^2

x^2-4x+2

r_{y_1}(x)=(x^2-4x+2)-(x^2-4x+2)

\forall x\in\mathbb{R}:\ r_{y_1}(x)=0

y_2(x)=x^2+x

y_2'(x)=2x+1,\ \ y_2''(x)=2

r_{y_2}(x)=2-2(2x+1)+(x^2+x)-(x^2-4x+2)

r_{y_2}(x)=x-2

r_{y_2}(x)=x-2

r_{y_2}(2)=0,\ r_{y_2}(0)=-2\neq 0\ \Rightarrow\ y_2\ \text{not a solution on }\mathbb{R}

y_1(0),\ y_1'(0)

y_1(0)=0,\ y_1'(0)=0

y''+p\,y'+q\,y=g,\ p=-2,\ q=1,\ g=x^2-4x+2,\ y(0)=0,\ y'(0)=0

y_1\ \text{is the unique solution of the IVP on }\mathbb{R}

y_3(x)=x^2+e^x

y_3'(x)=2x+e^x,\ \ y_3''(x)=2+e^x

r_{y_3}(x)=(2+e^x)-2(2x+e^x)+(x^2+e^x)-(x^2-4x+2)

r_{y_3}(x)=0\ \forall x,\ \ y_3(0)=1\neq 0

\text{proved facts about }E

\text{order }2;\ y_1\ \text{solves};\ y_2\ \text{does not};\ y_1\ \text{unique for the IVP};\ E\ \text{alone not unique}

Substeps and lemmas

(x+h)^2-x^2

h(2x+h)

\frac{(x+h)^2-x^2}{h}=2x+h\ (h\neq 0)

\lim_{h\to 0}\frac{(x+h)^2-x^2}{h}=2x

2-2(2x+1)+(x^2+x)

x^2-3x

(x^2-3x)-(x^2-4x+2)

x-2

Reverse audits

• S15 · sufficient_goal_reduction · S02, S07, S10, S12, S14, and_intro_elim — Goal G: the five determinations in the goal. Sufficient condition H: S02, S07, S10, S12 and S14 (H⇒G by conjunction introduction). H is derived forwards from the givens and the cited theorem, without using G as a premise; the theorem behind uniqueness is marked citation_verified.
• S14 · premise_audit · S13, G4, distributive, add_inverse — It needs the coefficients to cancel term by term; this shows that solutions of E are not unique, which does not contradict S12, whose uniqueness holds only after the initial values are added.
• S13 · premise_audit · deriv_rules, L_deriv_square — Only differentiation rules are used; y₃ is not a polynomial and lies outside the MKO exercise class, so it is used for illustration only.
• S12 · premise_audit · thm_linear_ivp, poly_exp_continuous, S07, S11 — The theorem needs: a linear equation with leading coefficient 1, p, q, g continuous on an open interval containing x₀, and two initial values; all four are checked. The theorem itself is not proved here (citation_verified). No such conclusion is claimed for nonlinear equations.
• S11 · premise_audit · S03, numeric_evaluation — This is evaluation at x=0; satisfying the initial values does not by itself make y₁ the only solution; uniqueness comes from the theorem in S12.
• S10 · premise_audit · S09, quantifier_negation, numeric_evaluation — Negating the universal statement needs one counterexample, x=0; the fact r_{y₂}(2)=0 gives no support to y₂ being a solution.
• S09.2 · inverse_equivalence · neg_mul, add_inverse — Distributing the minus sign and additive inverses, valid both ways for all x.
• S09.1 · inverse_equivalence · distributive, add_inverse — Distributivity and collecting like terms, valid both ways for all x.
• S09 · inverse_equivalence · distributive, add_inverse — Each move is a polynomial identity valid for all x (N3), so the step holds both ways.
• S08 · premise_audit · L_deriv_square, deriv_rules — Each derivative must be recomputed rather than copied from y₁; the candidates differ by the term +x, so y₂′ gains 1.
• S07 · premise_audit · S06, G4, forall_intro — Generalization is allowed because S03 to S06 hold for arbitrary x. The conclusion is only that y₁ is a solution, not that it is the only one (see S12 to S14).
• S06 · inverse_equivalence · mul_assoc, add_comm — Only associativity and commutativity are used; the step holds both ways.
• S05 · inverse_equivalence · eq_replace, S03, S04 — Replacement of equals, valid both ways: the two expressions denote the same number at every x.
• S04 · premise_audit · S03, deriv_rules — Only differentiation rules are used; y₁′ is differentiable on all of ℝ, so y₁″ is defined everywhere.
• S03.2 · premise_audit · S03.1, func_limit_def, mul_inverse_nonzero — Dividing by h needs h≠0; the limit definition only looks at h with 0<|h|<δ, so h=0 is never substituted.
• S03.1 · inverse_equivalence · distributive, add_inverse — Expanding h(2x+h) gives 2xh+h², and adding back x² gives (x+h)²; the two expressions are equal for all x and h.
• S03 · premise_audit · L_deriv_square — It depends on the lemma; no converse is claimed (functions with derivative 2x are not only x², they may differ by a constant).
• S02 · premise_audit · S01, mko_ode_def — It needs the coefficient of y″ to be nonzero; with coefficient 0, y″ would not really occur and the order would drop.
• S01 · premise_audit · G1, G4, mko_ode_def — This step only rewrites and names and derives no new fact; moving a term across is an equivalence.

Error controls and negative controls

Success at one point is not a solution on an interval

One misconception named by the MKO: substituting y₂=x²+x at x=2 gives residual 0, but at x=0 the residual is −2. A solution needs a zero residual at every point of the interval; for polynomial candidates the safe method is to simplify the residual to a polynomial, as in S07 and S09, and see whether it is the zero polynomial.

Determine the order from the highest derivative that actually occurs

The order is not the number of terms on the left (3), nor the degree of a candidate (the 2 of x² is a coincidence). If a higher derivative has coefficient 0, as in 0·y‴+y″=1, then y‴ does not really occur and the equation has order 2. Trying the candidate x⁵ would not change the order of the equation either.

Existence and uniqueness need a theorem and its hypotheses

Another misconception named by the MKO is to claim directly from an equation and initial values that a unique solution exists. The theorem used in S12 requires a linear equation with coefficients continuous on an open interval containing x₀. Without the hypotheses the conclusion can fail: the nonlinear equation y′=3y^(2/3) with y(0)=0 has both y=0 and y=x³ as solutions (the right side is not Lipschitz near y=0).

• r_{y₂}(2)=0, so y₂=x²+x solves the equation on ℝ → reject — r_{y₂}(0)=−2≠0; the residual x−2 vanishes only at x=2 (S10).
• The left side has three terms, so the equation has order 3 → reject — The order is that of the highest derivative actually occurring, here y″, so the order is 2 (S02).
• Every first-order equation with one initial value has exactly one solution → reject — y′=3y^(2/3) with y(0)=0 has the two solutions y=0 and y=x³; uniqueness needs hypotheses such as a Lipschitz condition.
• The equation by itself determines the solution y=x² → reject — y₃=x²+eˣ also satisfies the equation (S14); initial values are needed to single out y₁.

Result and limitations

y″−2y′+y=x²−4x+2 is a second-order ordinary differential equation. The residual of y₁=x² vanishes identically on ℝ, so it is a solution; the residual of y₂=x²+x is x−2, zero only at x=2, so it is not a solution on ℝ. y₁ satisfies y(0)=0 and y′(0)=0, and by the existence and uniqueness theorem for second-order linear equations (continuous coefficients, citation_verified) it is the unique solution of this initial value problem; without initial values y₃=x²+eˣ is also a solution, so the equation alone does not determine a unique solution.

• This revision supports thm_linear_ivp with the checked Theorem 5.3.1 in Section 5.3 of Trench's Elementary Differential Equations with Boundary Value Problems. The original Boyce–DiPrima edition and number are retained as provenance, not claimed to have been inspected. The theorem is not reproved here.
• The nonlinear example y′=3y^(2/3) appears only in an error control and a negative control as an illustration, without a step-by-step derivation.

Verification and source binding

7 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: b3522cf0b2e691223792ec73da6938700017174c9b8f5f44531a26e1e9437318
• original source SHA-256: b3522cf0b2e691223792ec73da6938700017174c9b8f5f44531a26e1e9437318
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)