# Initial-value problem: auditing four polynomial candidates [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-initial-value-problem/) This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented. derivation-mko-initial-value-problem-01 · production-20261019-adopted-96 ## Goal and scope Initial-value problem: y''(x)=6x on ℝ with y(0)=1 and y'(0)=2. Audit the four integer-coefficient polynomial candidates y_A=x³+2x+1, y_B=x³+1, y_C=x²+2x+1 and y_D=3x⁵−15x⁴+21x³+2x+1 one by one: check the equation residual and the two initial values separately, decide which candidate solves this initial-value problem, and explain why checking only the initial data, only one initial value, or the residual only on a finite grid is not enough. Works inside the MKO's scope: integer-coefficient polynomial candidates, explicit initial values and a specified finite residual grid (assumption a1). The residual of candidate y_A is computed symbolically with the derivative rules for polynomials and is therefore zero on all of ℝ; y_D shows the limits of a finite-grid check. The guide does not claim uniqueness, find a general solution or discuss maximal intervals of existence (assumption a2), and does not change the canonical MKO or its English edition. ## Givens and symbols - distributive - eq_replace - numeric_evaluation - and_intro_elim - quantifier_negation - forall_elim - G1 — Initial-value problem: an unknown function y:ℝ→ℝ satisfies the second-order ordinary differential equation y''(x)=6x (for every x∈ℝ) together with the initial data y(0)=1 and y'(0)=2 (x0=0, y0=1, v0=2). - G2 — Candidates (integer-coefficient polynomials on ℝ): y_A=x³+2x+1, y_B=x³+1, y_C=x²+2x+1, y_D=3x⁵−15x⁴+21x³+2x+1. - G3 — The residual is R_y(x)=y''(x)−6x; the finite residual grid specified for candidate y_D is {0,1,2}. - y_A,\ y_B,\ y_C,\ y_D — the four polynomial candidates - R_y(x)=y''(x)-6x — the equation residual of a candidate y - (E) — the equation requirement: R_y(x)=0 for every x∈ℝ - (I_1),\ (I_2) — the initial-condition requirements: y(0)=1 and y'(0)=2 - \{0,1,2\} — the finite residual grid specified for y_D ## Rules and sources - 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. - numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable. - and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q. - quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x). - forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds. - 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_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v). - 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. - de_morgan_logic · prerequisite — De Morgan's laws for logic: ¬(P∧Q) ⇔ ¬P∨¬Q and ¬(P∨Q) ⇔ ¬P∧¬Q. - exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x). - add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w). - zero_product · prerequisite — Zero-product property: in ℤ, ℚ, ℝ, ℂ (or any integral domain), uv=0 ⇔ u=0 or v=0. - case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility. - mko_ivp · cited — An initial-value problem consists of an ordinary differential equation and initial data for the same unknown function at a specified point. A first-order problem commonly gives y(x0)=y0; a second-order problem typically needs y(x0)=y0 and y'(x0)=v0. A candidate solution must satisfy both the equation and the initial data. · mko-initial-value-problem - mko_ode_residual · 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 - poly_deriv · prerequisite — Derivatives of polynomials: polynomials are differentiable everywhere on ℝ; (x^k)'=k x^(k−1) for k≥1, the derivative of a constant is 0, and (f+g)'=f'+g', (cf)'=cf'. ## Main derivation S01 · definitionBefore \text{initial-value problem} After y''(x)=6x\ (x\in\mathbb{R}),\ y(0)=1,\ y'(0)=2 Conditions: none Rule: mko_ivp · Uses: G1, mko_ivp Leaf basis: mko_ivp + def_intro By the MKO, an initial-value problem consists of an equation and initial data for the same unknown function at a specified point. Here the equation is of second order (the highest derivative is y''), so two initial data are given: y(0)=1 and y'(0)=2. Both are requirements on the same function y at the same point x0=0. S02 · equivalentBefore y\ \text{solves the IVP} After (E)\ \forall x\in\mathbb{R}:\ R_y(x)=0\ \land\ (I_1)\ y(0)=1\ \land\ (I_2)\ y'(0)=2 Conditions: none Rule: def_unfold · Uses: S01, G3, mko_ode_residual Leaf basis: def_unfold + and_intro_elim Unfold 'solves the initial-value problem': a candidate must meet three requirements at once: the equation requirement (E), that the residual R_y(x)=y''(x)−6x vanishes on all of ℝ, and the two initial-condition requirements (I1) and (I2). They form a conjunction, and failure of any one means the candidate does not solve this initial-value problem. S03 · equivalentBefore y_A=x^3+2x+1 After y_A'=3x^2+2,\ y_A''=6x Conditions: none Rule: poly_deriv · Uses: G2, poly_deriv Leaf basis: poly_deriv Differentiate y_A term by term with the derivative rules for polynomials, in two sub-steps for the first and second derivatives. S04 · equivalentBefore R_{y_A}(x)=y_A''(x)-6x After R_{y_A}(x)=6x-6x=0\ \ \forall x\in\mathbb{R} Conditions: none Rule: eq_replace · Uses: S03, S02 Leaf basis: eq_replace + add_inverse + forall_intro Substitute y_A''=6x: R_{y_A}(x)=6x−6x=0. This is an algebraic identity valid for every real x, not the result of sampling some points, so the equation requirement (E) holds on all of ℝ. S05 · equivalentBefore y_A(0),\ y_A'(0) After y_A(0)=1,\ y_A'(0)=2 Conditions: none Rule: numeric_evaluation · Uses: G2, S03 Leaf basis: numeric_evaluation + forall_elim Substitute x=0: y_A(0)=0+0+1=1 and y_A'(0)=3·0+2=2. Both initial-condition requirements (I1) and (I2) hold. Note that y_A'(0) uses the derivative y_A', not y_A itself. S06 · impliesBefore (E),\ (I_1),\ (I_2)\ \text{for}\ y_A After y_A\ \text{solves the IVP on}\ \mathbb{R} Conditions: none Rule: and_intro_elim · Uses: S02, S04, S05 Leaf basis: and_intro_elim + def_unfold All three requirements are proved (S04, S05), so by S02 y_A solves this initial-value problem on ℝ. This also shows the problem has at least one solution; uniqueness is not claimed. S07 · impliesBefore y_B=x^3+1 After R_{y_B}\equiv 0,\ y_B(0)=1,\ y_B'(0)=0\neq 2 Conditions: none Rule: poly_deriv · Uses: G2, poly_deriv, S02 Leaf basis: poly_deriv + de_morgan_logic + numeric_evaluation y_B'=3x² and y_B''=6x, so R_{y_B}(x)=6x−6x=0 for every x and (E) holds; y_B(0)=1, so (I1) holds; but y_B'(0)=3·0=0≠2, so (I2) fails. By S02, y_B satisfies the equation but does not solve this initial-value problem. S08 · impliesBefore y_A,\ y_B\ \text{both satisfy}\ (E),\ (I_1) After y_A(1)=4\neq 2=y_B(1) Conditions: none Rule: numeric_evaluation · Uses: S04, S05, S07 Leaf basis: numeric_evaluation + exists_intro y_A and y_B both satisfy the equation and y(0)=1, but y_A(1)=1+2+1=4 and y_B(1)=1+1=2, so they are different functions. Hence y(0)=1 alone does not single out a solution; the second datum y'(0)=2 is what excludes y_B. This is why the MKO says a second-order problem typically needs both y(x0) and y'(x0). S09 · impliesBefore y_C=x^2+2x+1 After y_C(0)=1,\ y_C'(0)=2,\ R_{y_C}(0)=2\neq 0 Conditions: none Rule: quantifier_negation · Uses: G2, poly_deriv, S02 Leaf basis: quantifier_negation + poly_deriv + numeric_evaluation y_C'=2x+2 and y_C''=2. Initial data: y_C(0)=1 and y_C'(0)=2, both hold. But R_{y_C}(x)=2−6x, and at x=0, R_{y_C}(0)=2≠0. To negate 'R(x)=0 for every x' one x with R(x)≠0 is enough, so (E) fails and y_C is not a solution. Someone who checks only the initial data would wrongly accept y_C. S10 · equivalentBefore y_D=3x^5-15x^4+21x^3+2x+1 After y_D'=15x^4-60x^3+63x^2+2,\ y_D''=60x^3-180x^2+126x Conditions: none Rule: poly_deriv · Uses: G2, poly_deriv Leaf basis: poly_deriv + numeric_evaluation Differentiate y_D term by term, computing the first and second derivatives in two sub-steps; the coefficient products are checked exactly in N2 to N7. S11 · equivalentBefore R_{y_D}(x)=y_D''(x)-6x After R_{y_D}(x)=60x^3-180x^2+120x=60x(x-1)(x-2) Conditions: none Rule: distributive · Uses: S10, G3 Leaf basis: distributive + add_assoc + numeric_evaluation R_{y_D}(x)=60x³−180x²+126x−6x=60x³−180x²+120x. Factor out the common factor: 60x(x²−3x+2), and x²−3x+2=(x−1)(x−2). So R_{y_D}(x)=60x(x−1)(x−2); N9 checks this as a polynomial identity. S12 · impliesBefore x\in\{0,1,2\} After R_{y_D}(0)=R_{y_D}(1)=R_{y_D}(2)=0,\ y_D(0)=1,\ y_D'(0)=2 Conditions: none Rule: zero_product · Uses: S11, G2, G3, S10 Leaf basis: zero_product + numeric_evaluation On the specified grid one factor of 60x(x−1)(x−2) is zero, so the residual is 0 at all three points (N10). Initial data: y_D(0)=1 (only the constant term remains) and y_D'(0)=2 (only the constant term 2 remains). y_D passes this finite-grid-plus-initial-data audit. S13 · impliesBefore R_{y_D}(3) After 60\cdot 3\cdot 2\cdot 1=360\neq 0\ \Rightarrow\ y_D\ \text{not a solution} Conditions: none Rule: quantifier_negation · Uses: S11, S12, S02 Leaf basis: quantifier_negation + numeric_evaluation Take x=3 outside the grid: R_{y_D}(3)=60·3·2·1=360≠0. So 'R(x)=0 for every x' fails, (E) fails and y_D does not solve this initial-value problem, even though it passed the finite audit of S12. This is the MKO's warning: a zero residual at finitely many points is not an identity on the whole interval. S14 · impliesBefore y_A,\ y_B,\ y_C,\ y_D After \text{only}\ y_A\ \text{solves the IVP among the four candidates} Conditions: none Rule: case_analysis · Uses: S06, S07, S09, S13 Leaf basis: case_analysis + and_intro_elim Each of the four candidates is decided: y_A meets all three requirements (S06); y_B fails at y'(0) (S07); y_C fails the equation (S09); y_D passes only the finite grid and fails the equation at x=3 (S13). The conclusion covers these four candidates only: y_A is a solution and the others are not. ## Substeps and lemmas S03.1 · equivalentBefore (x^3+2x+1)' After 3x^2+2 Conditions: none Rule: poly_deriv · Uses: G2, poly_deriv Leaf basis: poly_deriv + numeric_evaluation The derivative of a sum is the sum of the derivatives: (x³)'=3x², (2x)'=2·(x)'=2 and (1)'=0, so y_A'=3x²+2. Cross-check: y_A(x+h)−y_A(x)=h(3x²+2)+3xh²+h³ (N1, a polynomial identity); dividing by h and letting h→0 gives 3x²+2. S03.2 · equivalentBefore (3x^2+2)' After 6x Conditions: none Rule: poly_deriv · Uses: S03.1, poly_deriv Leaf basis: poly_deriv Differentiate once more: (3x²)'=3·2x=6x and (2)'=0, so y_A''=6x. S10.1 · equivalentBefore (3x^5-15x^4+21x^3+2x+1)' After 15x^4-60x^3+63x^2+2 Conditions: none Rule: poly_deriv · Uses: G2, poly_deriv Leaf basis: poly_deriv + numeric_evaluation (3x⁵)'=5·3x⁴=15x⁴, (−15x⁴)'=−4·15x³=−60x³, (21x³)'=3·21x²=63x², (2x)'=2 and (1)'=0. S10.2 · equivalentBefore (15x^4-60x^3+63x^2+2)' After 60x^3-180x^2+126x Conditions: none Rule: poly_deriv · Uses: S10.1, poly_deriv Leaf basis: poly_deriv + numeric_evaluation (15x⁴)'=4·15x³=60x³, (−60x³)'=−3·60x²=−180x², (63x²)'=2·63x=126x and (2)'=0. ## Reverse audits - S14 · sufficient_goal_reduction · S06, S07, S09, S13 — Goal G: the verdict on the four candidates. Sufficient condition H: the four separate verdicts S06, S07, S09 and S13, which cover every candidate; H⇒G by proof by cases. H is derived forwards from the derivative rules and exact substitution; G is never used as a premise. - S13 · premise_audit · S11, quantifier_negation, S02 — One witness point x=3 suffices to negate the universal statement (N11). - S12 · premise_audit · S11, zero_product, numeric_evaluation — These are facts at finitely many points; no converse is claimed, that is, (E) on ℝ is not inferred from these three points (S13 proves it fails). - S11 · inverse_equivalence · distributive, numeric_evaluation — Backwards, expanding 60x(x−1)(x−2) returns 60x³−180x²+120x; they are the same polynomial (N9 checks the cubic identity on the grid 0 to 3). - S10.2 · inverse_equivalence · poly_deriv — As in S10.1; the coefficient products are N5, N6 and N7. - S10.1 · inverse_equivalence · poly_deriv — Term-by-term application of the rules; the coefficient products are N2, N3 and N4. - S10 · inverse_equivalence · poly_deriv — Derivatives are unique, so both sides name the same function. - S09 · premise_audit · quantifier_negation, poly_deriv, S02 — ¬∀x P(x) ⇔ ∃x ¬P(x); the witness x=0 is explicit and checked exactly (N8). - S08 · premise_audit · S04, S05, S07, numeric_evaluation — One concrete counterexample (two different functions) suffices to show that one datum is not enough; it is not claimed that two data always guarantee uniqueness, which needs a separate argument. - S07 · premise_audit · poly_deriv, S02, numeric_evaluation — Negating a conjunction needs only one failing part, here (I2); it is not claimed that y_B is bad in any other sense, since it does solve the equation. - S06 · premise_audit · S02, S04, S05, and_intro_elim — The conjunction needs all three parts; no uniqueness is claimed: finding one solution does not exclude others. - S05 · inverse_equivalence · numeric_evaluation — Exact substitution; both sides have the same value. - S04 · inverse_equivalence · eq_replace, add_inverse — Equal expressions are substituted and u−u=0 is used; both sides agree for every x. - S03.2 · inverse_equivalence · poly_deriv — As in S03.1, a direct application of the rules. - S03.1 · inverse_equivalence · poly_deriv — Each term is a direct application of the rules, and the resulting function is unique. - S03 · inverse_equivalence · poly_deriv — A derivative is a uniquely determined function, so both sides name the same function; N1 cross-checks the first derivative through a difference-quotient identity. - S02 · inverse_equivalence · def_unfold, and_intro_elim — This unfolds the definition and holds both ways: all three requirements together make a solution, and a solution meets all three. - S01 · premise_audit · G1, mko_ivp — This step only states the problem and derives no new fact; writing initial data does not by itself guarantee a solution or a unique one (MKO, first paragraph). ## Error controls and negative controls Checking the initial data but not the equationThe first mistake named by the MKO. y_C satisfies y(0)=1 and y'(0)=2, but y_C''=2 and the residual 2−6x is already 2 at x=0 (S09). The equation requirement and the initial-condition requirements must be checked separately, and failure of either rules the candidate out. Zero residual on a finite grid does not establish a solution on the whole intervalThe second mistake named by the MKO. The residual 60x(x−1)(x−2) of y_D vanishes on the whole grid {0,1,2} and the initial values match, but R(3)=360 (S12, S13). Finite sampling can refute (by finding a nonzero point) but cannot by itself prove a residual is identically zero; for y_A, the residual is shown to vanish for all x by the algebraic identity 6x−6x=0. A second-order problem needs two initial valuesy_A and y_B both satisfy y''=6x and y(0)=1, yet they are different functions (S08). Checking only y(0) would wrongly accept y_B; y'(0)=2 is the necessary second datum. When checking y'(0), substitute into the derivative y', not into y itself. - y_C(0)=1 and y_C'(0)=2, so y_C solves this initial-value problem → reject — R_{y_C}(x)=2−6x and R_{y_C}(0)=2≠0, so the equation fails. - y_D has zero residual at 0, 1 and 2 and correct initial values, so y_D is a solution → reject — R_{y_D}(3)=60·3·2·1=360≠0. - y_B satisfies y''=6x and y(0)=1, so it solves this initial-value problem → reject — y_B'(0)=0≠2, so the second initial value fails. - Finding one candidate that meets the equation and the initial data proves that the solution is unique → reject — One solution existing does not exclude others; with only y(0)=1, y_A and y_B are two different solutions. Uniqueness needs a separate argument, which this guide does not give. ## Result and limitations Of the four candidates, only y_A=x³+2x+1 solves the initial-value problem y''=6x, y(0)=1, y'(0)=2 on ℝ: its residual is identically zero and both initial values hold. y_B=x³+1 satisfies the equation and y(0)=1 but y_B'(0)=0; y_C=x²+2x+1 satisfies both initial values but R(0)=2; y_D has zero residual on the grid {0,1,2} and correct initial values, but R(3)=360. Uniqueness is not claimed. - This guide does not prove that the solution of this initial-value problem is unique. One possible route: the difference w of two solutions satisfies w''=0, w(0)=0 and w'(0)=0, and then 'a function with zero derivative on an interval is constant' (a corollary of the mean value theorem) applies; that needs a citation of the theorem, which is not done here. - N1 and N9 are grid checks of polynomial identities (with a stated degree bound per variable), and N10 is a finite check at three points only; the conclusions do not depend on them, they are cross-checks. ## Verification and source binding 14 declared checks for this guide; only the listed expressions are covered. - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: 9ab9d67dde3d67d0467dfdb56a74490ed9fc771c9c18aba72aa959ee7d220859 - original source SHA-256: 9ab9d67dde3d67d0467dfdb56a74490ed9fc771c9c18aba72aa959ee7d220859 - Lean: NOT_RUN · independent AI: NOT_MEASURED [Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-initial-value-problem-01.json)