Initial-value problem: auditing four polynomial candidates

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

\text{initial-value problem}

y''(x)=6x\ (x\in\mathbb{R}),\ y(0)=1,\ y'(0)=2

y\ \text{solves the IVP}

(E)\ \forall x\in\mathbb{R}:\ R_y(x)=0\ \land\ (I_1)\ y(0)=1\ \land\ (I_2)\ y'(0)=2

y_A=x^3+2x+1

y_A'=3x^2+2,\ y_A''=6x

R_{y_A}(x)=y_A''(x)-6x

R_{y_A}(x)=6x-6x=0\ \ \forall x\in\mathbb{R}

y_A(0),\ y_A'(0)

y_A(0)=1,\ y_A'(0)=2

(E),\ (I_1),\ (I_2)\ \text{for}\ y_A

y_A\ \text{solves the IVP on}\ \mathbb{R}

y_B=x^3+1

R_{y_B}\equiv 0,\ y_B(0)=1,\ y_B'(0)=0\neq 2

y_A,\ y_B\ \text{both satisfy}\ (E),\ (I_1)

y_A(1)=4\neq 2=y_B(1)

y_C=x^2+2x+1

y_C(0)=1,\ y_C'(0)=2,\ R_{y_C}(0)=2\neq 0

y_D=3x^5-15x^4+21x^3+2x+1

y_D'=15x^4-60x^3+63x^2+2,\ y_D''=60x^3-180x^2+126x

R_{y_D}(x)=y_D''(x)-6x

R_{y_D}(x)=60x^3-180x^2+120x=60x(x-1)(x-2)

x\in\{0,1,2\}

R_{y_D}(0)=R_{y_D}(1)=R_{y_D}(2)=0,\ y_D(0)=1,\ y_D'(0)=2

R_{y_D}(3)

60\cdot 3\cdot 2\cdot 1=360\neq 0\ \Rightarrow\ y_D\ \text{not a solution}

y_A,\ y_B,\ y_C,\ y_D

\text{only}\ y_A\ \text{solves the IVP among the four candidates}

Substeps and lemmas

(x^3+2x+1)'

3x^2+2

(3x^2+2)'

6x

(3x^5-15x^4+21x^3+2x+1)'

15x^4-60x^3+63x^2+2

(15x^4-60x^3+63x^2+2)'

60x^3-180x^2+126x

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 equation

The 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 interval

The 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 values

y_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)