# Average rate of change between distinct inputs: eligibility, swapping endpoints, the affine and quadratic formulas [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-rate-of-change/) 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-rate-of-change-01 · production-20261019-adopted-96 ## Goal and scope (1) For a specified function f with f(2)=7 and f(−4)=3: check eligibility, compute the average rate of change as a reduced fraction with positive denominator, and show that swapping both endpoints does not change it. (2) Prove that f(x)=mx+b has average rate m, and check it with ℓ(x)=−3x+7 between −2 and 4. (3) Prove that q(x)=a(x−h)²+k (a≠0) has average rate a(x₀+x₁−2h), check it with q(x)=−2(x−3)²+5 between 1 and 4, and use symmetric endpoints, a changed second endpoint and equal inputs to show that it is not a derivative and that 0 must not be assigned when the inputs coincide. Inside the MKO: both endpoints are permitted inputs of the same specified function with x₀≠x₁, integer endpoints and coefficients, answers as reduced fractions with positive denominators (a1, a2), and a≠0 in the quadratic slice (a3). The affine and quadratic formulas are proved by algebraic identities for all eligible endpoints. This guide neither defines nor computes derivatives; it only shows that the average rate is not a quantity of a single point; the canonical MKO and its English edition are not changed. ## Givens and symbols - frac_rules - distributive - mul_inverse_nonzero - neg_mul - numeric_evaluation - G1 — Definition (MKO): for two permitted inputs x₀≠x₁ of the same specified function f, the average rate is R=(f(x₁)−f(x₀))/(x₁−x₀). x₀=x₁ is ineligible and is not replaced by 0 or 0/0. In the representative fraction (b−a)/(d−c), a, b are the outputs y₀, y₁ and c, d the inputs x₀, x₁. - G2 — Direct two-point exercise: the specified function f is given only through f(2)=7 and f(−4)=3; take x₀=2, x₁=−4. - G3 — ℓ:ℝ→ℝ, ℓ(x)=−3x+7 (m=−3, b=7). - G4 — q:ℝ→ℝ, q(x)=−2(x−3)²+5 (a=−2≠0, h=3, k=5). - x_0,x_1 — the two input endpoints, x_0≠x_1 - y_0=f(x_0),\ y_1=f(x_1) — the corresponding outputs - R(f;x_0,x_1)=\frac{y_1-y_0}{x_1-x_0} — the average rate of change - \ell(x)=-3x+7 — the degree-one affine example - q(x)=-2(x-3)^2+5 — the quadratic example ## Rules and sources - 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. - distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu. - 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. - neg_mul · prerequisite — Signs and multiplication: (−u)v=−(uv) and (−u)(−v)=uv. - numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable. - 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. - add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v). - add_comm · prerequisite — Commutativity of addition: u+v=v+u. - mul_assoc · prerequisite — Associativity of multiplication: (uv)w=u(vw). - mul_one · prerequisite — Multiplicative identity: 1·u=u. - mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ). - quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x). - and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q. - mko_rate · cited — For two permitted inputs x0≠x1 of the same specified function f, with f(x0)=y0 and f(x1)=y1, the average rate of change is (y1−y0)/(x1−x0). Equal inputs fail this entry's eligibility condition; do not replace their quotient with zero or 0/0. For f(x)=mx+b on R it equals m. For q(x)=a(x−h)²+k with a≠0 it equals a(x0+x1−2h). This finite endpoint quotient is not a derivative. · mko-rate-of-change - diff_squares · prerequisite — Difference of squares: for all reals u, v, u²−v²=(u−v)(u+v) (expand the right side by distributivity). - L_swap · lemma — For x₀≠x₁: (y₀−y₁)/(x₀−x₁)=(y₁−y₀)/(x₁−x₀). - L_linear_rate · lemma — For f(x)=mx+b and x₀≠x₁: (f(x₁)−f(x₀))/(x₁−x₀)=m. - L_quad_rate · lemma — For q(x)=a(x−h)²+k and x₀≠x₁: (q(x₁)−q(x₀))/(x₁−x₀)=a(x₀+x₁−2h). ## Main derivation S01 · definitionBefore f(x_0)=y_0,\ f(x_1)=y_1 After R=\frac{y_1-y_0}{x_1-x_0}\ \ \text{only if}\ x_0\neq x_1 Conditions: x_0\neq x_1 Rule: mko_rate · Uses: G1, mko_rate Leaf basis: mko_rate + def_intro Define the average rate as in the MKO: the output difference divided by the input difference. There are two eligibility conditions: both endpoints are permitted inputs of the same specified function, and x₀≠x₁, so the denominator is nonzero. In the representative fraction (b−a)/(d−c), a, b are outputs and c, d inputs, not to be confused with the vertex-form a, h, k. S02 · impliesBefore x_0=2,\ x_1=-4 After x_1-x_0=-6\neq0 Conditions: none Rule: numeric_evaluation · Uses: S01, G2 Leaf basis: numeric_evaluation Both endpoints are inputs of the same f and −4−2=−6≠0, so the pair is eligible. A negative denominator does not violate eligibility; it only has to be made positive when simplifying. S03 · equivalentBefore R=\frac{3-7}{-4-2} After \frac{2}{3} Conditions: -6\neq0 Rule: frac_rules · Uses: S02, G2 Leaf basis: frac_rules + numeric_evaluation Using only the given outputs f(2)=7 and f(−4)=3 (MKO a1): R=(3−7)/(−4−2). Sub-steps S03.1 and S03.2 first get (−4)/(−6) and then reduce it to the fraction 2/3 with positive denominator. S04 · equivalentBefore \frac{y_0-y_1}{x_0-x_1}=\frac{7-3}{2-(-4)} After \frac{4}{6}=\frac{2}{3} Conditions: x_0\neq x_1 Rule: L_swap · Uses: S03 Leaf basis: frac_rules + neg_mul By Lemma L_swap, swapping both endpoints together (numerator and denominator both change sign) leaves the quotient unchanged: (7−3)/(2−(−4))=4/6=2/3, the same as S03. The proof is in S04.1. S05 · equivalentBefore \frac{(mx_1+b)-(mx_0+b)}{x_1-x_0} After m Conditions: x_0\neq x_1 Rule: L_linear_rate · Uses: S01 Leaf basis: distributive + mul_inverse_nonzero By Lemma L_linear_rate, an affine function has average rate equal to its slope m between any two different inputs. The proof is in S05.1 and S05.2; m=0 gives 0, the constant-function case. S06 · impliesBefore \ell(-2)=13,\ \ell(4)=-5 After \frac{-5-13}{4-(-2)}=\frac{-18}{6}=-3=m Conditions: 4\neq-2 Rule: L_linear_rate · Uses: S05, G3 Leaf basis: mko_rate + numeric_evaluation ℓ(−2)=−3·(−2)+7=13 and ℓ(4)=−3·4+7=−5. Direct computation gives (−5−13)/(4−(−2))=−18/6=−3, agreeing with m=−3 from S05. S07 · equivalentBefore \frac{q(x_1)-q(x_0)}{x_1-x_0} After a(x_0+x_1-2h) Conditions: x_0\neq x_1; a\neq0 Rule: L_quad_rate · Uses: S01 Leaf basis: distributive + diff_squares + mul_inverse_nonzero By Lemma L_quad_rate, the average rate of a quadratic is a(x₀+x₁−2h), depending on both endpoints. The proof is in S07.1 to S07.3: k cancels, the difference of squares factors, and x₁−x₀ cancels. S08 · impliesBefore q(1)=-3,\ q(4)=3 After \frac{3-(-3)}{4-1}=\frac{6}{3}=2 Conditions: 4\neq1 Rule: mko_rate · Uses: S01, G4 Leaf basis: mko_rate + numeric_evaluation q(1)=−2·(−2)²+5=−3 and q(4)=−2·1²+5=3. Direct computation: (3−(−3))/(4−1)=6/3=2. S09 · impliesBefore a(x_0+x_1-2h)\ \text{at}\ a=-2,\ h=3,\ x_0=1,\ x_1=4 After -2(1+4-6)=2 Conditions: none Rule: L_quad_rate · Uses: S07, S08 Leaf basis: numeric_evaluation Substitute into the formula: −2·(1+4−6)=−2·(−1)=2, agreeing with the direct computation in S08. S10 · impliesBefore x_0=1,\ x_1=5=2h-1 After R=-2(1+5-6)=0,\ \text{yet}\ q(3)=5\neq-3=q(1) Conditions: none Rule: L_quad_rate · Uses: S07, G4 Leaf basis: numeric_evaluation + quantifier_negation Symmetric endpoints 1 and 5 (mirror images about h=3): R=−2·0=0, and directly q(5)−q(1)=−3−(−3)=0. But q is not constant, for example q(3)=5≠−3. A zero average rate only says the two endpoint outputs are equal; it says nothing about what happens in between. S11 · impliesBefore x_0=1,\ x_1=2 After R=-2(1+2-6)=6\neq2 Conditions: none Rule: L_quad_rate · Uses: S07, S09 Leaf basis: numeric_evaluation + quantifier_negation Keep x₀=1 and change the second endpoint to 2: R=−2·(−3)=6; directly (q(2)−q(1))/(2−1)=(3−(−3))/1=6. This differs from the value 2 for x₁=4, so the average rate is not a quantity belonging to the single point x₀=1; it is a finite difference quotient between two endpoints, no limit is taken, and it may not be called a derivative. S12 · impliesBefore x_0=x_1=2 After x_1-x_0=0:\ \text{ineligible, no value assigned} Conditions: none Rule: mko_rate · Uses: S01, G4 Leaf basis: mko_rate + numeric_evaluation Equal inputs x₀=x₁=2: the denominator 2−2=0, so the pair is ineligible. The numerator q(2)−q(2)=0, so formally it is 0/0, which is not a number; by the MKO it is not replaced by 0 or 0/0, and this entry assigns no value to this pair. S13 · impliesBefore \text{S02 to S12} After R=\tfrac23;\ R_{\ell}=m=-3;\ R_q=a(x_0+x_1-2h),\ R_q(1,4)=2;\ x_0=x_1\ \text{ineligible} Conditions: none Rule: and_intro_elim · Uses: S03, S04, S05, S06, S07, S09, S10, S11, S12 Leaf basis: and_intro_elim Summary: the direct two-point rate is 2/3 and does not change when both endpoints are swapped; an affine function always has rate m; a quadratic has rate a(x₀+x₁−2h), equal to 2 between 1 and 4; symmetric endpoints can give 0 although the function is not constant; changing the second endpoint changes the result, so it is not a derivative; equal inputs get no value. ## Substeps and lemmas S03.1 · equivalentBefore \frac{3-7}{-4-2} After \frac{-4}{-6} Conditions: none Rule: numeric_evaluation · Uses: S02 Leaf basis: numeric_evaluation Numerator 3−7=−4, denominator −4−2=−6. S03.2 · equivalentBefore \frac{-4}{-6} After \frac{4}{6}=\frac{2}{3} Conditions: none Rule: frac_rules · Uses: S03.1, frac_rules Leaf basis: frac_rules + numeric_evaluation Multiply numerator and denominator by −1 (nonzero) to get 4/6 with a positive denominator; then divide both by gcd(4,6)=2 to get 2/3. gcd(2,3)=1 and the denominator 3>0, so this is the reduced form with positive denominator. S04.1 · equivalentBefore \frac{y_0-y_1}{x_0-x_1} After \frac{-(y_1-y_0)}{-(x_1-x_0)}=\frac{y_1-y_0}{x_1-x_0} Conditions: x_1-x_0\neq0 Rule: frac_rules · Uses: frac_rules, neg_mul Leaf basis: frac_rules + neg_mul y₀−y₁=−(y₁−y₀) and x₀−x₁=−(x₁−x₀); then use a/b=(a·(−1))/(b·(−1)) (−1≠0, b≠0). This step proves Lemma L_swap. Swapping only one of the two pairs would change the sign of the quotient. S05.1 · equivalentBefore (mx_1+b)-(mx_0+b) After m(x_1-x_0) Conditions: none Rule: distributive · Uses: distributive Leaf basis: distributive + add_inverse + add_comm The b terms cancel, leaving mx₁−mx₀, and distributivity factors out m. S05.2 · equivalentBefore \frac{m(x_1-x_0)}{x_1-x_0} After m Conditions: x_1-x_0\neq0 Rule: mul_inverse_nonzero · Uses: S05.1, mul_inverse_nonzero Leaf basis: mul_inverse_nonzero + mul_assoc + mul_one Since x₁−x₀≠0, it cancels: m(x₁−x₀)·1/(x₁−x₀)=m. If x₁=x₀ it could not be cancelled, which is exactly what the eligibility condition is for. S05.1 and S05.2 together prove Lemma L_linear_rate. S07.1 · equivalentBefore q(x_1)-q(x_0) After a\bigl[(x_1-h)^2-(x_0-h)^2\bigr] Conditions: none Rule: distributive · Uses: distributive Leaf basis: distributive + add_inverse + add_comm (a(x₁−h)²+k)−(a(x₀−h)²+k): k cancels (it only shifts the output), and distributivity factors out a. S07.2 · equivalentBefore (x_1-h)^2-(x_0-h)^2 After (x_1-x_0)(x_0+x_1-2h) Conditions: none Rule: diff_squares · Uses: S07.1, diff_squares Leaf basis: diff_squares + distributive + add_inverse Take u=x₁−h, v=x₀−h: u−v=x₁−x₀ and u+v=x₀+x₁−2h, so by the difference of squares u²−v²=(u−v)(u+v). S07.3 · equivalentBefore \frac{a(x_1-x_0)(x_0+x_1-2h)}{x_1-x_0} After a(x_0+x_1-2h) Conditions: x_1-x_0\neq0 Rule: mul_inverse_nonzero · Uses: S07.2, mul_inverse_nonzero Leaf basis: mul_inverse_nonzero + mul_comm + mul_one Since x₁−x₀≠0, the factor cancels. S07.1 to S07.3 together prove Lemma L_quad_rate. The simplified expression is still the difference quotient between two endpoints, not an instantaneous rate at either endpoint. ## Reverse audits - S13 · sufficient_goal_reduction · S03, S04, S05, S06, S07, S09, S10, S11, S12, and_intro_elim — Goal G is the three parts of the goal; the sufficient condition H is the conjunction of the step results, all proved forwards, and H⇒G uses only conjunction introduction. - S12 · premise_audit · mko_rate, G1 — The eligibility condition itself excludes this case; no limit or derivative is claimed. - S11 · premise_audit · S07, S09, numeric_evaluation — Two different values suffice to show the dependence on the second endpoint; the guide does not compute the derivative itself. - S10 · premise_audit · S07, numeric_evaluation — One counterexample (q(3)≠q(1)) suffices to refute 'zero average rate ⇒ constant'. - S09 · premise_audit · S07, numeric_evaluation — The formula is proved in S07; agreement of the two computations is only a check. - S08 · premise_audit · mko_rate, numeric_evaluation — Eligibility 4≠1 holds; exact arithmetic. - S07.3 · inverse_equivalence · mul_inverse_nonzero — Cancellation is reversible, given x₁−x₀≠0. - S07.2 · inverse_equivalence · diff_squares, add_inverse — The difference of squares is an identity and holds both ways. - S07.1 · inverse_equivalence · distributive, add_inverse — An identity; it holds both ways. - S07 · inverse_equivalence · L_quad_rate — The lemma is proved by three equational sub-steps and holds both ways. - S06 · premise_audit · S05, numeric_evaluation — The general conclusion comes from S05; the numbers are only a check. - S05.2 · inverse_equivalence · mul_inverse_nonzero — Multiplying by (x₁−x₀) and by its reciprocal undo each other, given x₁−x₀≠0. - S05.1 · inverse_equivalence · distributive, add_inverse — An identity; it holds both ways. - S05 · inverse_equivalence · L_linear_rate — The lemma is an equation and holds both ways. - S04.1 · inverse_equivalence · frac_rules, neg_mul — Both rules are identities whose only condition is a nonzero denominator. - S04 · inverse_equivalence · L_swap — The lemma is an equation and holds both ways. - S03.2 · inverse_equivalence · frac_rules — a/b=(ak)/(bk) for k≠0 holds both ways. - S03.1 · inverse_equivalence · numeric_evaluation — Integer subtraction, checkable backwards. - S03 · inverse_equivalence · frac_rules, numeric_evaluation — Each step rewrites the same rational number, so it holds both ways. - S02 · premise_audit · S01, numeric_evaluation — Exact computation of the input difference and comparison with 0. - S01 · premise_audit · G1, mko_rate — This is only the definition and its eligibility condition; for x₀=x₁ no value is defined. ## Error controls and negative controls Do not assign zero when the inputs coincideOne misconception identified in the MKO is assigning 0 when the inputs coincide. For x₀=x₁=2 the denominator is 0 and the quotient is 0/0, which is not a number; this entry declares the pair ineligible and gives no value (S12). The average rate is not a derivativeThe other misconception is to call the average rate a derivative. Starting from x₀=1, x₁=4 gives 2 and x₁=2 gives 6 (S11), so it is not a quantity of one point; the symmetric endpoints 1, 5 give 0 although q is not constant (S10). It is a finite endpoint quotient; no limit is taken. Swap the endpoints as pairs(q(4)−q(1))/(1−4)=6/(−3)=−2 is wrong: only the order in the denominator was reversed, not in the numerator. Reversing both together keeps the quotient unchanged (S04). - For x₀=x₁=2 the average rate of q is 0 → reject — The denominator is 0, so the pair is ineligible; 0/0 is not a number and may not be replaced by 0. - (q(4)−q(1))/(1−4)=−2 is the average rate between 1 and 4 → reject — Only the denominator was reversed; the correct value is (q(4)−q(1))/(4−1)=2. - q has average rate 0 between 1 and 5, so q is constant on [1,5] → reject — q(3)=5≠−3=q(1). - The average rate from 1 to 4 is 2, so this alone proves that the derivative of q at x=1 is 2, without a derivative definition or limit certificate → reject — This guide computes a finite quotient for two specified endpoints; changing x₁ to 2 gives 6. Such a computation is not a certificate of a derivative value at one point, so the stated inference is rejected. The guide does not compute q′(1), nor does it infer numerical inequality merely from different procedures; for an affine function the two procedures can even give the same value. ## Result and limitations With f(2)=7 and f(−4)=3 the average rate is (3−7)/(−4−2)=2/3, unchanged when both endpoints are swapped. f(x)=mx+b has average rate m between any x₀≠x₁ (−3 for ℓ). q(x)=a(x−h)²+k has average rate a(x₀+x₁−2h); for q(x)=−2(x−3)²+5 it is 2 between 1 and 4, 0 between the symmetric endpoints 1 and 5 (though q is not constant), and 6 between 1 and 2, so it depends on both endpoints and is not a derivative. x₀=x₁ is ineligible: no value is assigned; in particular, the answer is not 0. - This guide neither defines nor computes derivatives; it only proves that the average rate depends on both endpoints. Its relation to the derivative is a separate matter. - The f of G2 is given only through two outputs, and no other information about f is used. ## Verification and source binding 21 declared checks for this guide; only the listed expressions are covered. - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: 9fc30d6fb2c4750764240925dfd0912b58ac51b42cb81e261c6e4f836b55fb55 - original source SHA-256: c2b90bff75e0c55cc21b498fdb786490c14ae05bee992190158da4a7dd811bad - 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-rate-of-change-01.json)