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

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

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



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

S01 · definitionBefore

f'(x)

After

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

Conditions: h\neq 0

Rule: mko_derivative · Uses: G1, func_limit_def

Leaf basis: mko_derivative + func_limit_def + def_unfold

By the MKO, the derivative is the finite two-sided limit of the difference quotient as h→0 with h≠0. The quotient itself is defined only for h≠0; the derivative is a limit, not the quotient at some finite step. If the limit does not exist, neither does the derivative.



S02 · equivalentBefore

f(1)

After

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

Conditions: none

Rule: numeric_evaluation · Uses: G2

Leaf basis: numeric_evaluation

The centre value f(1)=3−2+5=6 (N3). It is the amount subtracted in the numerator of the quotient.



S03 · equivalentBefore

f(1+h)

After

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

Conditions: none

Rule: distributive · Uses: G2, distributive

Leaf basis: distributive + power_laws + add_comm + add_assoc

(1+h)²=1+2h+h², so 3(1+h)²=3+6h+3h²; −2(1+h)=−2−2h; adding, 3+6h+3h²−2−2h+5=6+4h+3h² (N1 checks this as a polynomial identity).



S04 · equivalentBefore

f(1+h)-f(1)

After

4h+3h^2

Conditions: none

Rule: eq_replace · Uses: S02, S03

Leaf basis: eq_replace + add_inverse + add_zero

Substitute S03 and S02: (6+4h+3h²)−6=4h+3h².



S05 · equivalentBefore

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

After

4+3h

Conditions: h\neq 0

Rule: frac_rules · Uses: S04, frac_rules

Leaf basis: frac_rules + distributive + mul_inverse_nonzero

The numerator is 4h+3h²=h(4+3h); for h≠0 cancel h to get 4+3h. At h=0 the quotient is 0/0, undefined; so h=0 may not be substituted into the original quotient; one simplifies for h≠0 first and then examines the limit.



S06 · impliesBefore

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

After

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

Conditions: \varepsilon>0

Rule: forall_intro · Uses: S01, S05

Leaf basis: forall_intro + exists_intro + abs_rules + order_basics

Take an arbitrary ε>0 and let δ=ε/3. If 0<|h|<δ, then by S05 |Q(h)−4|=|3h|=3|h|<3δ=ε. As ε is arbitrary, S01 gives f'(1)=4.



S07 · equivalentBefore

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

After

2a_2x+a_1+a_2h

Conditions: h\neq 0

Rule: L_diff_quot · Uses: G2

Leaf basis: distributive + frac_rules + mul_inverse_nonzero

Generalize: by Lemma L_diff_quot, the difference quotient of any polynomial of degree at most two at any x is 2a2x+a1+a2h. With a2=3, a1=−2, x=1 this is 6−2+3h=4+3h, agreeing with S05 (N6). The lemma is proved in S07.1 and S07.2.



S08 · impliesBefore

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

After

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

Conditions: none

Rule: L_lin_limit · Uses: S01, S07

Leaf basis: forall_intro + order_basics + abs_rules

With A=2a2x+a1 and B=a2, Lemma L_lin_limit gives that the quotient tends to 2a2x+a1 as h→0; by S01 this is f'(x). As x is arbitrary, the formula holds for every real x. The lemma is proved in S08.1 and S08.2 for B=0 and B≠0.



S09 · impliesBefore

h=\tfrac{1}{10}

After

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

Conditions: none

Rule: numeric_evaluation · Uses: S05, S06, G3

Leaf basis: numeric_evaluation + frac_rules

The quotient at the finite step h=1/10 is 4+3/10=43/10 (N4, computed directly from f(1.1) and f(1)), differing from the derivative 4 by a2h=3/10. A finite quotient is only an average rate; the derivative is the limit as h→0. The two agree only when a2h=0 (see S10).



S10 · impliesBefore

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

After

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

Conditions: h\neq 0

Rule: L_diff_quot · Uses: S07, S08, G3

Leaf basis: L_diff_quot + L_lin_limit + mul_zero

MKO assumption a2 allows a2=0 (degree at most two, not necessarily a genuine quadratic). By S07 the quotient with a2=0, a1=−2 is −2+0·h=−2 for every h≠0 (N11); by S08, e'(x)=−2. Here every finite quotient equals the derivative only because a2h=0; this does not extend to a2≠0 (S09). A constant, a2=a1=0, has derivative 0, also a legitimate low-degree boundary.



S11 · equivalentBefore

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

After

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

Conditions: h\neq 0

Rule: eq_replace · Uses: G3, abs_rules

Leaf basis: eq_replace + abs_rules

g(2)=|0|=0 and g(2+h)=|h|, so the quotient is |h|/h, defined for h≠0.



S12 · case_splitBefore

\frac{|h|}{h}

After

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

Conditions: h\neq 0

Rule: abs_rules · Uses: S11, abs_rules

Leaf basis: abs_rules + case_analysis + frac_rules

For h>0, |h|=h and the quotient is h/h=1; for h<0, |h|=−h and the quotient is −h/h=−1 (N9, N10). The two cases cover every h≠0. The right derivative is 1 and the left derivative −1.



S13 · impliesBefore

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

After

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

Conditions: none

Rule: contradiction · Uses: S01, S12

Leaf basis: contradiction + exists_elim + abs_rules + order_basics

By contradiction: suppose g'(2)=D exists. For ε=1/2 obtain δ>0 and take h=δ/2 and h=−δ/2, both with 0<|h|<δ. By S12, |1−D|<1/2 and |−1−D|<1/2. Triangle inequality: 2=|1−(−1)|≤|1−D|+|D−(−1)|<1/2+1/2=1, a contradiction. So g has no derivative at 2.



S14 · impliesBefore

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

After

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

Conditions: t_0>2

Rule: abs_rules · Uses: G3, S01

Leaf basis: abs_rules + order_basics + frac_rules

For t0>2, if |h|<t0−2 then t0+h>2, both absolute values equal their arguments, the numerator is h (N12), and the quotient is exactly 1. So with δ=t0−2 the error is 0 for every ε, and g'(t0)=1. Likewise for t0<2, g(t)=2−t near t0, so g'(t0)=−1.



S15 · impliesBefore

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

After

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

Conditions: none

Rule: quantifier_negation · Uses: S12, S13

Leaf basis: quantifier_negation + abs_rules

Some formal libraries make the derivative a total function and fill the default 0 where none exists. But 0 is not a limit of the quotient: |Q(h)−0|=1 for every h≠0, so ε=1/2 already fails. The answer of this entry is therefore 'g'(2) does not exist', not 0; a default value is a bookkeeping convention, not the existence of a derivative.







## Substeps and lemmas

S07.1 · equivalentBefore

f(x+h)-f(x)

After

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

Conditions: none

Rule: distributive · Uses: distributive, power_laws

Leaf basis: distributive + power_laws + add_inverse

(x+h)²−x²=2xh+h², a1(x+h)−a1x=a1h, and a0 cancels; factoring out h gives h(2a2x+a1+a2h) (N2 checks this as a polynomial identity in five variables).



S07.2 · equivalentBefore

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

After

2a_2x+a_1+a_2h

Conditions: h\neq 0

Rule: frac_rules · Uses: S07.1, frac_rules

Leaf basis: frac_rules + mul_inverse_nonzero

h≠0, so cancel h. S07.1 and S07.2 together prove Lemma L_diff_quot.



S08.1 · impliesBefore

B=0

After

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

Conditions: B=0

Rule: mul_zero · Uses: mul_zero

Leaf basis: mul_zero + add_zero + order_basics

If B=0 then A+Bh=A for every h; the error is 0<ε, so any δ>0 works.



S08.2 · impliesBefore

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

After

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

Conditions: |B|>0

Rule: order_basics · Uses: abs_rules, order_basics

Leaf basis: abs_rules + order_basics + mul_inverse_nonzero

If B≠0 then |B|>0; let δ=ε/|B|>0. If 0<|h|<δ, multiplying by the positive |B| gives |B||h|<ε. S08.1 and S08.2 together prove Lemma L_lin_limit.







## 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 derivativeOne 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 quotientAnother 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 cornerThe 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)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-derivative-01.json)