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

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-antiderivative/)

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-antiderivative-01 · production-20261019-adopted-96



## 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

S01 · definitionBefore

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

After

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

Conditions: none

Rule: mko_antideriv · Uses: G1

Leaf basis: mko_antideriv + def_unfold

By the MKO: an antiderivative F must be differentiable on the interval (here all of ℝ), with derivative equal to f everywhere. This is a condition about derivatives and has nothing to do with inverse functions or reciprocals of derivatives.



S02 · equivalentBefore

f=[3,-4,6]

After

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

Conditions: none

Rule: def_unfold · Uses: G2, G1

Leaf basis: def_unfold

Ascending reading: constant 3, coefficient −4 of x, coefficient 6 of x².



S03 · impliesBefore

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

After

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

Conditions: none

Rule: L_poly_deriv4 · Uses: mko_derivative_def

Leaf basis: mko_derivative_def + distributive + abs_rules + order_basics

By Lemma L_poly_deriv4, a polynomial of degree at most four is differentiable everywhere with derivative list [c1,2c2,3c3,4c4]; the constant c0 does not appear in it. The lemma is proved from the definition in S03.1 to S03.3. Every polynomial differentiated here has degree at most four.



S04 · definitionBefore

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

After

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

Conditions: none

Rule: mko_antideriv · Uses: S02, mko_antideriv

Leaf basis: mko_antideriv + frac_rules + numeric_evaluation

By the MKO's representative formula, the coefficient a_k of x^k becomes the coefficient a_k/(k+1) of x^(k+1), with constant term 0. 3/1=3, −4/2=−2, 6/3=2 (N4, N5), so F0=3x−2x²+2x³. Coefficients are written as reduced fractions with positive denominators.



S05 · impliesBefore

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

After

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

Conditions: none

Rule: L_poly_deriv4 · Uses: S03, S04, S02, S01

Leaf basis: L_poly_deriv4 + mko_antideriv + numeric_evaluation

By the lemma, F0 is differentiable everywhere with derivative list [3,−4,6], that is 3−4x+6x²=f(x) at every x (N6 is a polynomial identity). By S01, F0 is an antiderivative of f on ℝ.



S06 · impliesBefore

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

After

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

Conditions: none

Rule: L_poly_deriv4 · Uses: S03, S05

Leaf basis: L_poly_deriv4 + forall_intro

The list of F0+C differs only in the constant term; the lemma's derivative list does not contain c0, so the derivative is still [3,−4,6]=f. As C is arbitrary, generalization gives that the whole family F0+C consists of antiderivatives. Giving one antiderivative F0 differs from giving all of them.



S07 · impliesBefore

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

After

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

Conditions: none

Rule: L_poly_deriv4 · Uses: G3, S06

Leaf basis: L_poly_deriv4 + forall_elim

G differs from F0 only in the constant term (7 versus 0), so G=F0+7; by S06 with C=7, G'=f, and G is accepted. A candidate's constant term does not affect acceptance.



S08 · impliesBefore

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

After

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

Conditions: none

Rule: L_poly_deriv4 · Uses: G3, S03, S02

Leaf basis: L_poly_deriv4 + quantifier_negation + numeric_evaluation

By the lemma, H'=[3,2·(−4),3·2]=[3,−8,6]. The coefficient at index 1 (counting from 0) is −8≠−4, so H'−f=−4x, not the zero polynomial; for example at x=1, H'(1)=1 and f(1)=5 (N7, N8). H is rejected.



S09 · impliesBefore

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

After

P=F_0+p_0

Conditions: none

Rule: L_same_deriv · Uses: S03, S04

Leaf basis: poly_coeff_identity + frac_rules + mul_inverse_nonzero

By Lemma L_same_deriv, among polynomials with at most five coefficients, every antiderivative differs from F0 only in the constant term. This is the MKO's 'identical derivative coefficients force identical positive-degree coefficients'. The lemma is proved in S09.1 and S09.2.



S10 · equivalentBefore

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

After

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

Conditions: none

Rule: numeric_evaluation · Uses: S04, G3

Leaf basis: numeric_evaluation

F0(2)=6−8+16=14 (N9), and adding C=−5 gives 9 (N10). Differentiation removes C, but evaluation does not: both C and x are genuine inputs and C may not be dropped just because the derivative does not contain it.



S11 · impliesBefore

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

After

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

Conditions: none

Rule: L_poly_deriv4 · Uses: G3, S03, S02

Leaf basis: L_poly_deriv4 + quantifier_negation + numeric_evaluation

By the lemma, K'=[3,2·(−3),3·(8/3)]=[3,−6,8]. K'−f=2x²−2x=2x(x−1) (N14), which vanishes at x=0 and x=1, so sampling only those points would mislead (N11, N12); but it is not the zero polynomial, and at x=2, K'(2)=23 while f(2)=19 (N13). Comparing coefficients (−6≠−4) rejects K directly.



S12 · impliesBefore

5x^0,\ 0

After

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

Conditions: none

Rule: mko_antideriv · Uses: S03, mko_antideriv

Leaf basis: mko_antideriv + L_poly_deriv4 + power_laws

Monomial boundary: in polynomials x^0 is always 1, including at x=0, so 5x^0 is the constant 5 and its representative antiderivative is 5x, that is [0,5] (derivative [5] by the lemma). With coefficient c=0 the function is zero, and its representative antiderivative is normalized to [0], without meaningless higher zero terms; its family of antiderivatives is all constants.



S13 · impliesBefore

p(x)=2x

After

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

Conditions: none

Rule: mko_antideriv · Uses: S03, S01

Leaf basis: mko_antideriv + L_poly_deriv4 + quantifier_negation

For p(x)=2x: an antiderivative is x² ([0,0,1], whose derivative is [0,2]=p by the lemma); the inverse function is y↦y/2; the reciprocal of the derivative is 1/2. At input 4, x² gives 16 while the inverse gives 2 (N15). The three are entirely different: an antiderivative is neither an inverse function nor a reciprocal of the derivative.



S14 · impliesBefore

\text{S05, S06, S09}

After

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

Conditions: none

Rule: set_extensionality · Uses: S05, S06, S09

Leaf basis: set_extensionality + subset_def

S06 gives ⊇ (every F0+C is an antiderivative) and S09 gives ⊆ (every such P is F0+p0). By set extensionality the sets are equal: in the polynomial model, the antiderivatives of f are exactly the constant family F0+C.







## Substeps and lemmas

S03.1 · equivalentBefore

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

After

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)

Conditions: h\neq 0

Rule: distributive · Uses: distributive, power_laws, frac_rules

Leaf basis: distributive + power_laws + frac_rules + mul_inverse_nonzero

Expand power by power: (x+h)²−x²=h(2x+h), (x+h)³−x³=h(3x²+h(3x+h)), (x+h)⁴−x⁴=h(4x³+h(6x²+4xh+h²)) (N1, N2, N3). Multiplying by the coefficients and adding, with c0 cancelling, gives p(x+h)−p(x)=h(D+hR); for h≠0 divide by h.



S03.2 · impliesBefore

0<|h|\le 1

After

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

Conditions: |h|\le 1

Rule: abs_rules · Uses: S03.1, abs_rules

Leaf basis: abs_rules + order_basics + square_nonneg

Triangle inequality and |uv|=|u||v|, then |h|≤1 and h²≤1: |3x+h|≤3|x|+1 and |6x²+4xh+h²|≤6x²+4|x|+1. M depends only on x and the coefficients.



S03.3 · impliesBefore

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

After

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

Conditions: M+1>0

Rule: mko_derivative_def · Uses: S03.1, S03.2, mko_derivative_def

Leaf basis: mko_derivative_def + forall_intro + order_basics + abs_rules

If 0<|h|<δ then |h|<1 and S03.2 applies: |hR|≤|h|M≤|h|(M+1)<δ(M+1)≤ε. As ε is arbitrary, the definition gives p'(x)=D. As x is arbitrary, p is differentiable everywhere. S03.1 to S03.3 prove Lemma L_poly_deriv4.



S09.1 · impliesBefore

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

After

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

Conditions: none

Rule: poly_coeff_identity · Uses: S03, S02, poly_coeff_identity

Leaf basis: poly_coeff_identity + def_unfold

By S03, P' has list [p1,2p2,3p3,4p4]; f padded with a trailing zero is [3,−4,6,0] (the same polynomial). They agree at every x, so by poly_coeff_identity the coefficients agree term by term.



S09.2 · impliesBefore

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

After

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

Conditions: k\neq 0

Rule: frac_rules · Uses: S09.1, frac_rules

Leaf basis: frac_rules + mul_inverse_nonzero + numeric_evaluation

k=1, 2, 3, 4 are all nonzero, so we may divide: p1=3/1=3, p2=−4/2=−2, p3=6/3=2, p4=0/4=0. So the nonconstant coefficients of P are exactly those of F0, P=F0+p0, and the constant p0 is free. S09.1 and S09.2 prove Lemma L_same_deriv.







## 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 familyOne 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 identityAnother 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 functionA 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)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-antiderivative-01.json)