The derivative: a quadratic's derivative from the difference-quotient limit, and no derivative at a corner

Goal and scope

For f(t)=3t²−2t+5: first simplify the difference quotient for h≠0, (f(1+h)−f(1))/h=4+3h, then prove f'(1)=4 by ε-δ; derive the general formulas: the quotient is 2a2x+a1+a2h and the derivative 2a2x+a1; explain why the finite-step quotient 4.3 at h=1/10 is not the derivative, and the affine boundary a2=0; finally prove that g(t)=|t−2| has no derivative at t=2 (not 0), while its derivative is 1 for t>2.

Stays inside the MKO: full real domain, polynomials of degree at most two (a2=0 allowed), and the corner of |t−c|. General differentiation rules, higher-degree polynomials and other functions are not treated. It does not change the canonical MKO or its English edition.

Givens and symbols

• distributive
• frac_rules
• abs_rules
• order_basics
• func_limit_def
• numeric_evaluation

• G1 — Functions ℝ→ℝ on the full real domain; a finite step h must be nonzero.
• G2 — f(t)=3t²−2t+5 (a2=3, a1=−2, a0=5); find the derivative at x=1.
• G3 — For comparison: the finite step h=1/10; the affine e(t)=−2t+5 (a2=0); the corner function g(t)=|t−2|.

• Q(h)=\frac{f(x+h)-f(x)}{h} — the difference quotient at step h≠0
• f'(x) — the finite two-sided limit of Q(h) as h→0 with h≠0
• a_2,a_1,a_0 — the coefficients of f(t)=a2t²+a1t+a0
• g(t)=|t-2| — the function with a corner at t=2

Rules and sources

• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• 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.
• 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.
• 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).
• 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.
• 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.
• add_comm · prerequisite — Commutativity of addition: u+v=v+u.
• add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w).
• 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.
• add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
• add_zero · prerequisite — Additive identity: u+0=u.
• 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.
• 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.
• exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
• 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.
• 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.
• contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
• exists_elim · prerequisite — ∃-elimination: from ∃x∈D, P(x) we may name some element a with P(a) by a fresh name; reasoning with a is allowed as long as the final conclusion does not mention a.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• mko_derivative · 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. For f(t)=a2t²+a1t+a0 (a2=0 allowed) the derivative is 2a2x+a1 and the finite quotient is that value plus a2h; for |t−c| the derivative is 1 above c and −1 below c, and at c it does not exist rather than being 0. · mko-derivative
• L_diff_quot · lemma — For f(t)=a2t²+a1t+a0, a real x and h≠0: (f(x+h)−f(x))/h=2a2x+a1+a2h.
• L_lin_limit · lemma — For reals A and B: every ε>0 admits δ>0 with |(A+Bh)−A|<ε whenever 0<|h|<δ; that is, A+Bh→A as h→0.

Main derivation

f'(x)

f'(x)=D\iff\forall\varepsilon>0\ \exists\delta>0\ \forall h:\ 0<|h|<\delta\Rightarrow\left|\frac{f(x+h)-f(x)}{h}-D\right|<\varepsilon

f(1)

3\cdot 1^2-2\cdot 1+5=6

f(1+h)

3(1+h)^2-2(1+h)+5=6+4h+3h^2

f(1+h)-f(1)

4h+3h^2

\frac{4h+3h^2}{h}\ (h\neq 0)

4+3h

\varepsilon>0\ \text{arbitrary},\ \delta=\tfrac{\varepsilon}{3}

0<|h|<\delta\Rightarrow|(4+3h)-4|=3|h|<\varepsilon;\ f'(1)=4

\frac{f(x+h)-f(x)}{h},\ f(t)=a_2t^2+a_1t+a_0,\ h\neq 0

2a_2x+a_1+a_2h

\lim_{h\to 0,\,h\neq 0}(2a_2x+a_1+a_2h)

f'(x)=2a_2x+a_1\ \text{for every real}\ x

h=\tfrac{1}{10}

Q(\tfrac{1}{10})=4+\tfrac{3}{10}=\tfrac{43}{10}\neq 4=f'(1)

e(t)=-2t+5\ (a_2=0)

\frac{e(x+h)-e(x)}{h}=-2\ (h\neq 0),\ e'(x)=-2

g(t)=|t-2|,\ t=2

\frac{g(2+h)-g(2)}{h}=\frac{|h|-0}{h}=\frac{|h|}{h}\ (h\neq 0)

\frac{|h|}{h}

1\ (h>0),\quad -1\ (h<0)

g'(2)=D\ \text{(assumed)},\ \varepsilon=\tfrac12,\ h=\pm\tfrac{\delta}{2}

|1-D|<\tfrac12,\ |-1-D|<\tfrac12\Rightarrow 2\le|1-D|+|D+1|<1:\ \text{contradiction}

t_0>2,\ 0<|h|<t_0-2

\frac{g(t_0+h)-g(t_0)}{h}=\frac{(t_0+h-2)-(t_0-2)}{h}=1;\ g'(t_0)=1

\text{a totalized API returning}\ 0\ \text{at}\ t=2

g'(2)\ \text{does not exist};\ 0\ \text{is not a limit of}\ Q

Substeps and lemmas

f(x+h)-f(x)

a_2(2xh+h^2)+a_1h=h(2a_2x+a_1+a_2h)

\frac{h(2a_2x+a_1+a_2h)}{h}

2a_2x+a_1+a_2h

B=0

|(A+0\cdot h)-A|=0<\varepsilon\ \text{for every}\ h

B\neq 0,\ \delta=\tfrac{\varepsilon}{|B|}

0<|h|<\delta\Rightarrow|Bh|=|B||h|<|B|\delta=\varepsilon

Reverse audits

• S15 · premise_audit · S12, S13, quantifier_negation — It follows directly from the values in S12 and the non-existence in S13.
• S14 · premise_audit · abs_rules, S01 — h must be small enough not to cross 2; this shows non-existence happens only at the corner itself.
• S13 · premise_audit · S01, S12, abs_rules, contradiction — The contradiction refutes only the existence of the two-sided limit; the one-sided derivatives 1 and −1 still exist.
• S12 · premise_audit · abs_rules, case_analysis — The cases are exhaustive; h=0 is not considered.
• S11 · inverse_equivalence · eq_replace, abs_rules — Replacement of equals, valid both ways.
• S10 · premise_audit · S07, S08, L_diff_quot — A direct substitution into the general formulas; no claim that finite quotients equal derivatives in general.
• S09 · premise_audit · S05, S06, numeric_evaluation — N4 and N5 can be recomputed; the step does not claim that any finite quotient equals the derivative.
• S08.2 · premise_audit · abs_rules, order_basics — Dividing by |B| needs B≠0, hence the case split.
• S08.1 · premise_audit · mul_zero — Only ε>0 is needed.
• S08 · premise_audit · S01, S07, L_lin_limit — The two cases cover every a2, including a2=0.
• S07.2 · inverse_equivalence · frac_rules, mul_inverse_nonzero — It needs h≠0; at h=0 the two sides cannot be compared.
• S07.1 · inverse_equivalence · distributive, power_laws — An identity, valid both ways.
• S07 · inverse_equivalence · L_diff_quot — The lemma gives equality of the two expressions for h≠0, valid both ways.
• S06 · sufficient_goal_reduction · S01, S05, forall_intro — Goal G: f'(1)=4. Sufficient condition H: for arbitrary ε, δ=ε/3 works; H⇒G by the definition. H is proved forwards from S05, without assuming G and without substituting h=0.
• S05 · inverse_equivalence · frac_rules, distributive — Backward, multiply by h/h, which needs h≠0; G1 guarantees this.
• S04 · inverse_equivalence · eq_replace, add_inverse — Replacement of equals, valid both ways.
• S03 · inverse_equivalence · distributive, power_laws — An identity for every h, valid both ways.
• S02 · inverse_equivalence · numeric_evaluation — Exact evaluation; both sides name the same number.
• S01 · premise_audit · G1, mko_derivative, func_limit_def — This step only unfolds the definition.

Error controls and negative controls

Distinguish a finite difference quotient from the derivative

One misconception the MKO lists is calling a finite difference quotient the derivative. The quotient at h=1/10 is 4.3 while the derivative is 4, a difference of a2h=0.3 (S09). For the affine e, finite quotients equal the derivative only because a2=0 (S10); this cannot be promoted to a general rule.

Do not substitute h=0 into the quotient

Another misconception is setting h=0 and computing anyway. The original quotient at h=0 is 0/0, undefined. The correct order is: simplify for h≠0 first (S05, S07.2), then take the limit as h→0 (S06, S08). That the simplified 4+3h has value 4 at h=0, equal to the limit, is guaranteed by the ε-δ argument of S06, not by substituting into the original quotient.

Do not assign zero at the corner

The left and right quotients of |t−2| at 2 are −1 and 1, so the two-sided limit does not exist (S13). Neither their average 0 nor the default 0 of a totalized API may pose as the derivative (S15).

• (f(1.1)−f(1))/0.1=4.3, so f'(1)=4.3 → reject — That is a finite quotient; the derivative is the limit 4 (S06, S09).
• Find the derivative by setting h=0 in (f(1+h)−f(1))/h → reject — At h=0 it is 0/0, undefined; a finite step must be nonzero.
• The one-sided derivatives −1 and 1 of |t−2| at 2 average to 0, so g'(2)=0 → reject — The two-sided limit does not exist (S13); |Q(h)−0|=1 for every h≠0.
• With a2=0, f is not a function of this model → reject — The MKO allows a2=0 (degree at most two); e(t)=−2t+5 has derivative −2 (S10).
• |t−2| has no derivative at any point → reject — Its derivative is 1 for t>2 and −1 for t<2 (S14); only at t=2 does it fail to exist.

Result and limitations

For h≠0 the quotient of f(t)=3t²−2t+5 at 1 is 4+3h, and f'(1)=4 (with δ=ε/3). In general a polynomial of degree at most two has quotient 2a2x+a1+a2h and derivative 2a2x+a1; the finite quotient 4.3 at h=1/10 is not the derivative, and only the affine case a2=0 makes finite quotients equal the derivative. g(t)=|t−2| has right quotient 1 and left quotient −1 at 2, so g'(2) does not exist (it is not 0); g'=1 for t>2 and g'=−1 for t<2.

• This guide treats only polynomials of degree at most two and |t−c|; general differentiation rules belong to mko-derivative-rules.

Verification and source binding

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

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

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