# The mean-value point of a quadratic

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

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-mean-value-theorem-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Directly construct a mean-value point for f(t)=A*t^2+B*t+C on a<b.

An exact polynomial family, not a sampling argument for general continuity or differentiability.





## Givens and symbols


- algebra
- polynomial


- G1 — A,B,C,a,b are rational, a<b, and f(t)=A*t^2+B*t+C.


- c — strict-interior mean-value witness
- A,B,C — quadratic, linear, constant coefficients





## Rules and sources


- mko_definition · cited — Question parameters A/B/C explicitly encode f(t)=A*t^2+B*t+C. Require a<b, continuity on the closed interval and differentiability on the open interval. The witness satisfies a<c<b and f'(c)=(f(b)−f(a))/(b−a). It need not be unique: affine and constant cases can have many witnesses. Finite samples, a=b, a jump or an interior cusp do not supply the required theorem hypotheses. · mko-mean-value-theorem
- algebra · prerequisite — Use real-field identities; division requires a nonzero denominator and multiplication by a positive number preserves inequalities.
- polynomial · prerequisite — Real polynomials are continuous and differentiate termwise: the derivative of x^k is k*x^(k-1), and constants differentiate to zero.





## Main derivation

S01 · impliesBefore

f(t)=At^2+Bt+C

After

f\text{ continuous on }[a,b]\text{ and differentiable on }(a,b)

Conditions: a<b

Rule: polynomial · Uses: G1

Leaf basis: polynomial

A polynomial is continuous and differentiable on R, satisfying both interval-specific hypotheses.



S02 · equivalentBefore

f(b)-f(a)

After

A(b^2-a^2)+B(b-a)=(b-a)(A(a+b)+B)

Conditions: none

Rule: algebra · Uses: G1

Leaf basis: algebra

The constants cancel and the difference of squares factors.



S03 · equivalentBefore

(f(b)-f(a))/(b-a)

After

A(a+b)+B

Conditions: b-a>0

Rule: algebra · Uses: G1, S02

Leaf basis: algebra

a<b gives a positive denominator, yielding the secant slope.



S04 · impliesBefore

f(t)=At^2+Bt+C

After

f'(t)=2At+B

Conditions: none

Rule: polynomial · Uses: G1

Leaf basis: polynomial

Termwise differentiation gives the derivative on the entire open interval.



S05 · impliesBefore

c=(a+b)/2

After

c-a=(b-a)/2>0,\quad b-c=(b-a)/2>0

Conditions: none

Rule: algebra · Uses: G1

Leaf basis: algebra

The midpoint lies strictly between both endpoints.



S06 · impliesBefore

f'(c)=2A(a+b)/2+B

After

f'(c)=A(a+b)+B=(f(b)-f(a))/(b-a)

Conditions: none

Rule: algebra · Uses: S03, S04, S05

Leaf basis: algebra

Substituting the midpoint exactly matches the secant slope, directly proving the conclusion for this polynomial family.



S07 · case_splitBefore

2Ac+B=A(a+b)+B

After

A\ne0\Longrightarrow c=(a+b)/2;\quad A=0\Longrightarrow\forall c\in(a,b)\text{ works}

Conditions: none

Rule: algebra · Uses: S03, S04

Leaf basis: algebra

Nonzero A gives the unique midpoint; affine and constant functions have every interior point as a witness.



S08 · impliesBefore

A=2,B=-3,C=1,a=0,b=2

After

f(0)=1,\ f(2)=3,\ c=1,\ f'(1)=1=(3-1)/2

Conditions: none

Rule: algebra · Uses: S06

Leaf basis: algebra

An exact rational instance audits coefficient roles and the witness.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · S06 — The polynomial family was proved earlier; this numerical check is only an audit.
- S07 · premise_audit · S03, S04 — Existence does not imply uniqueness, and division by A is forbidden in the zero branch.
- S06 · premise_audit · S03, S04, S05 — Equality and interior membership were separately checked; a numerical equality is not called a general MVT proof.
- S05 · premise_audit · G1 — A mean-value witness cannot merely be an endpoint.
- S04 · premise_audit · G1 — This is not only a numerical derivative at a candidate c.
- S03 · inverse_equivalence · G1, S02 — This division is unavailable when a=b.
- S02 · inverse_equivalence · G1 — A/B/C remain quadratic, linear and constant coefficients in that order.
- S01 · premise_audit · G1 — Closed-interval continuity and open-interval differentiability are distinct obligations.





## Error controls and negative controls

Denominator firstVerify a<b before dividing by b-a.

Split interval premisesThe full polynomial supplies continuity on the whole closed interval and differentiability on the whole interior.


- The secant division remains valid for a=b. → reject — The denominator is zero.
- MVT applies directly to |t| on [-1,1]. → reject — It is not differentiable at zero, and no interior derivative equals the secant slope zero.
- The mean-value point must be unique. → reject — When A=0 every interior point works.





## Result and limitations

The midpoint is always a mean-value point for this quadratic family; it is unique for A≠0, while every interior point works for A=0.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: e1932f3808c6a6878c0dea094cd386502a613adef2e578fbef51aa5a8ba53736
- original source SHA-256: e1932f3808c6a6878c0dea094cd386502a613adef2e578fbef51aa5a8ba53736
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-mean-value-theorem-01.json)