Antiderivatives: the representative polynomial antiderivative, the constant family and checking candidates

Goal and scope

For f=[3,−4,6] (f(x)=3−4x+6x²): prove from the definition the derivative formula for polynomials of degree at most four; build the representative antiderivative F0=[0,3,−2,2] and verify F0'=f; prove that F0+C is an antiderivative for every real C and that, among polynomials with at most five coefficients, every antiderivative is F0+C; check the candidates G=[7,3,−2,2] (accept), H=[0,3,−4,2] (reject) and K=[0,3,−3,8/3] (reject although it matches at two test points); evaluate F0(2)+C with C=−5; and explain why an antiderivative is not an inverse function.

Works only inside the MKO's polynomial model on all of ℝ: the concrete input f has at most four integer coefficients and exercise candidates such as G,H,K have at most five rational coefficients in ascending lists; the general family F0+C and its coefficient proof allow real C and real polynomial coefficients. 'Differ only by a constant' is proved by coefficients within the polynomial model only; the version for general differentiable functions on an interval needs the mean value theorem and is not proved here. It does not change the canonical MKO or its English edition.

Givens and symbols

• distributive
• power_laws
• abs_rules
• order_basics
• frac_rules
• numeric_evaluation

• G1 — Polynomials are ascending lists on all of ℝ (an interval); trailing zeros are normalized.
• G2 — f=[3,−4,6].
• G3 — Candidates G=[7,3,−2,2], H=[0,3,−4,2], K=[0,3,−3,8/3]; evaluation data x=2, C=−5.

• [a_0,a_1,a_2,a_3] — an ascending coefficient list
• F_0 — the representative antiderivative with constant term 0
• F_0+C — the constant family of antiderivatives
• D,\ R,\ M — the main term, remainder and remainder bound of the quotient

Rules and sources

• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• power_laws · prerequisite — Integer exponent laws (base nonzero, or exponents positive integers): a^m·a^n=a^{m+n}, (a^m)^n=a^{mn}, (ab)^n=a^n b^n, a^0=1.
• 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.
• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• frac_rules · prerequisite — Fraction rules (all denominators nonzero): a/c+b/c=(a+b)/c; (a/b)(c/d)=(ac)/(bd); (a/b)/(c/d)=(ad)/(bc) (also needing c≠0); a/b=(ak)/(bk) for k≠0.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• 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.
• 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.
• square_nonneg · prerequisite — Squares are nonnegative: for every real u, u²≥0, and u²=0 ⇔ u=0.
• 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.
• forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements.
• subset_def · prerequisite — Subset: A⊆B means every element of A is an element of B, i.e. ∀x (x∈A⇒x∈B).
• mko_antideriv · cited — F is an antiderivative of f on an interval when F is differentiable there and F'=f. For the polynomial defined on all of ℝ, f(x)=Σa_k x^k, choose F0(x)=Σa_k x^(k+1)/(k+1) with constant term zero; F0+C is also an antiderivative. Within the polynomial model, identical derivative coefficients force identical positive-degree coefficients, leaving only the constant term free. · mko-antiderivative
• mko_derivative_def · cited — For f:ℝ→ℝ, the derivative at x is lim_(h→0,h≠0)(f(x+h)−f(x))/h when this finite two-sided limit exists. · mko-derivative
• poly_coeff_identity · prerequisite — Two real polynomials that take the same value at every real x have the same normalized coefficient lists (a nonzero polynomial has only finitely many roots).
• L_poly_deriv4 · lemma — For p(x)=c0+c1x+c2x²+c3x³+c4x⁴ with real coefficients and every real x: p is differentiable at x and p'(x)=c1+2c2x+3c3x²+4c4x³; that is, [c0,c1,c2,c3,c4] has derivative list [c1,2c2,3c3,4c4].
• L_same_deriv · lemma — If P=[p0,p1,p2,p3,p4] satisfies P'=f on ℝ, then p1=3, p2=−2, p3=2, p4=0, that is P=F0+p0.

Main derivation

F\ \text{antiderivative of}\ f\ \text{on}\ \mathbb{R}

F\ \text{differentiable on}\ \mathbb{R}\ \land\ \forall x\in\mathbb{R}:\ F'(x)=f(x)

f=[3,-4,6]

f(x)=3-4x+6x^2

p=[c_0,c_1,c_2,c_3,c_4]

p'=[c_1,2c_2,3c_3,4c_4]\ \text{on}\ \mathbb{R}

a_k\ \mapsto\ \tfrac{a_k}{k+1}\ \text{as the coefficient of}\ x^{k+1}

F_0=[0,\ \tfrac31,\ \tfrac{-4}{2},\ \tfrac63]=[0,3,-2,2]

F_0=[0,3,-2,2]

F_0'=[3,\ 2\cdot(-2),\ 3\cdot 2]=[3,-4,6]=f;\ F_0\ \text{is an antiderivative}

F_0+C=[C,3,-2,2],\ C\in\mathbb{R}

(F_0+C)'=[3,-4,6]=f\ \text{for every}\ C

G=[7,3,-2,2]

G=F_0+7,\ G'=f:\ \text{accept}

H=[0,3,-4,2]

H'=[3,-8,6]\neq[3,-4,6]=f:\ \text{reject}

P=[p_0,p_1,p_2,p_3,p_4],\ P'=f\ \text{on}\ \mathbb{R}

P=F_0+p_0

F_0(2)+C,\ C=-5

(3\cdot 2-2\cdot 2^2+2\cdot 2^3)+(-5)=14-5=9

K=[0,3,-3,\tfrac83]

K'=[3,-6,8];\ K'(0)=f(0),\ K'(1)=f(1),\ K'(2)=23\neq 19=f(2):\ \text{reject}

5x^0,\ 0

5x^0=5\ (\text{also at}\ x=0)\ \to\ [0,5];\ 0\ \to\ [0]

p(x)=2x

\text{antiderivative}\ x^2;\ \text{inverse}\ y\mapsto\tfrac y2;\ 1/p'=\tfrac12:\ \text{three different objects}

\text{S05, S06, S09}

\{P:\ P'=f,\ P\ \text{at most five coefficients}\}=\{F_0+C:\ C\in\mathbb{R}\}

Substeps and lemmas

\frac{p(x+h)-p(x)}{h}\ (h\neq 0)

D+hR,\ D=c_1+2c_2x+3c_3x^2+4c_4x^3,\ R=c_2+c_3(3x+h)+c_4(6x^2+4xh+h^2)

0<|h|\le 1

|R|\le M=|c_2|+|c_3|(3|x|+1)+|c_4|(6x^2+4|x|+1)

\varepsilon>0,\ \delta=\min\left(1,\tfrac{\varepsilon}{M+1}\right)

0<|h|<\delta\Rightarrow|(D+hR)-D|\le|h|M<\varepsilon;\ p'(x)=D

P'(x)=f(x)\ \forall x

[p_1,2p_2,3p_3,4p_4]=[3,-4,6,0]

kp_k=a_{k-1}\ (k=1,2,3,4)

p_1=3,\ p_2=-2,\ p_3=2,\ p_4=0;\ P=[p_0,3,-2,2]=F_0+p_0

Reverse audits

• S14 · sufficient_goal_reduction · S06, S09, set_extensionality — Goal G: the two sets are equal. Sufficient condition H: inclusion both ways; H⇒G by extensionality. The two inclusions are proved forwards in S06 and S09.
• S13 · premise_audit · S03, S01 — Different values at one input show the two functions differ.
• S12 · premise_audit · S03, mko_antideriv — Follows the convention of MKO assumption a2; the derivative is checked by the lemma.
• S11 · premise_audit · S03, quantifier_negation — Two matching test points cannot prove an identity; one disagreeing coefficient or point suffices to reject.
• S10 · inverse_equivalence · numeric_evaluation — Exact evaluation.
• S09.2 · premise_audit · S09.1, frac_rules, mul_inverse_nonzero — There is no equation at position k=0 (the constant term), so p0 is unconstrained.
• S09.1 · premise_audit · S03, poly_coeff_identity — Passing from identical polynomial functions to equal coefficients uses poly_coeff_identity; checking only two points as in S11 is not enough to establish the identity here.
• S09 · premise_audit · L_same_deriv — The conclusion is limited to the polynomial model; the interval version for general differentiable functions is not claimed.
• S08 · premise_audit · S03, quantifier_negation — One point of disagreement refutes H'=f.
• S07 · premise_audit · S06 — Compare the nonconstant coefficients of G and F0 one by one.
• S06 · premise_audit · S03, S05, forall_intro — This step proves only that every F0+C is an antiderivative; that there are no others is proved in S09.
• S05 · sufficient_goal_reduction · S01, S03, S04 — Goal G: F0 is an antiderivative. Sufficient condition H: F0 is differentiable with derivative list equal to the list of f; H⇒G by the definition. H is proved forwards coefficient by coefficient from the lemma, without finite test points.
• S04 · premise_audit · S02, mko_antideriv — This step only builds the candidate by the formula; whether it is an antiderivative is verified in S05.
• S03.3 · premise_audit · S03.1, S03.2, mko_derivative_def, forall_intro — M+1 avoids division by 0 when M=0.
• S03.2 · premise_audit · abs_rules, order_basics — Only an upper bound; |h|≤1 is ensured by δ≤1 in S03.3.
• S03.1 · inverse_equivalence · distributive, frac_rules — Identities plus division by h≠0, valid both ways.
• S03 · premise_audit · L_poly_deriv4, mko_derivative_def — The lemma covers degree at most four; candidates have at most five coefficients, exactly within range.
• S02 · inverse_equivalence · def_unfold — Reading back gives the original list.
• S01 · premise_audit · G1, mko_antideriv — This step only states the definition.

Error controls and negative controls

Do not drop the constant family

One misconception the MKO lists is dropping the constant family. F0 is only the chosen representative; all antiderivatives are F0+C (S06, S14). C disappears under differentiation but matters in evaluation: F0(2)+C is 9 for C=−5, not 14 (S10).

Finite test points cannot replace a polynomial identity

Another misconception is replacing F'=f by a few equal test points. K' and f agree at x=0 and 1 because their difference 2x(x−1) vanishes there; but at x=2, 23≠19 (S11). Acceptance must compare derivative lists coefficient by coefficient (S09.1 explains why coefficient comparison matches the functional identity).

An antiderivative is not an inverse function

A third misconception is treating an antiderivative as an inverse function. For p(x)=2x the antiderivative is x², the inverse is y/2, and the reciprocal of the derivative is 1/2, three different objects (S13). The definition of an antiderivative involves only F'=f (S01).

• F0 is the only antiderivative of f → reject — F0+7=G is one too (S07); all antiderivatives are F0+C.
• K'(0)=f(0) and K'(1)=f(1), so K is an antiderivative → reject — K'(2)=23≠19=f(2); K'=[3,−6,8]≠[3,−4,6].
• Differentiation removes C, so F0(2)+C=14 when C=−5 → reject — Evaluation keeps C: 14+(−5)=9.
• The antiderivative of 2x is its inverse function x/2 → reject — (x/2)'=1/2≠2x; the antiderivatives are x²+C.
• 5x^0 is 0^0 at x=0, so its antiderivative is undefined at 0 → reject — The polynomial convention is x^0=1, including at x=0; 5x^0 is the constant 5, with antiderivative 5x defined everywhere.

Result and limitations

The representative antiderivative of f=[3,−4,6] is F0=[0,3,−2,2]=3x−2x²+2x³, with F0'=f. For every real C, F0+C is an antiderivative; among polynomials with at most five coefficients, the antiderivatives are exactly F0+C. G=[7,3,−2,2]=F0+7 is accepted; H is rejected because H'=[3,−8,6]; K′ matches f at x=0 and 1, but K'=[3,−6,8]≠f, so it is rejected. F0(2)+C equals 9 for C=−5. An antiderivative is neither an inverse function nor a reciprocal of the derivative.

• For general differentiable functions on an interval, 'two antiderivatives differ by a constant' needs the mean value theorem; this guide proves it only by coefficients inside the polynomial model and does not extend it to general functions or disconnected domains.
• poly_coeff_identity (polynomials equal everywhere have equal coefficients) is a premise of this guide and is not proved here.

Verification and source binding

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 0a7ad7b92f3eb8cf9c92f59c031efe93847f4df94d0f2541c2d6a9ae98227411
• original source SHA-256: 2ed700aa9d9c5a319e9f4d0ebcba193c2e7bdf4f88f31d9da27c9e22df7547ef
• Lean: NOT_RUN · independent AI: NOT_MEASURED

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