# An exact Lagrange remainder for a cubic

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-taylor-remainder-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-taylor-remainder-theorem-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

For f(x)=x^3, a=1, n=2, x=2, audit the exact remainder and a qualified derivative bound.

A complete degree-n+1 polynomial, not a proof of a general interval theorem from a finite center jet.





## Givens and symbols


- algebra
- polynomial
- taylor_def


- G1 — f(x)=x^3, a=1, n=2, evaluation point 2, connecting interval [1,2].


- R_2 — remainder f-T
- D,M — exact derivative supremum and candidate bound





## Rules and sources


- mko_definition · cited — Declare center a, point x, order n and the complete polynomial coefficients, then compute the Taylor polynomial and exact remainder directly. Degree≤n gives zero remainder. For degree n+1 the next derivative is constant, and a strictly intermediate midpoint supplies an exact Lagrange witness when x differs from a. Boundary families accept a qualified M at least the exact derivative supremum D or an undersized witness0≤M<D, rejecting negative M and unknown modes. A finite center jet does not prove the general remainder theorem, equality with a Taylor series or analyticity. · mko-taylor-remainder-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.
- taylor_def · prerequisite — T_n at center a sums f^(k)(a)*(x-a)^k/k! from zero through n; the remainder is f-T_n; a derivative supremum is its magnitude's least upper bound on the full connecting interval.





## Main derivation

S01 · impliesBefore

f'=3x^2,\quad f''=6x,\quad f'''=6

After

(f(1),f'(1),f''(1))=(1,3,6)

Conditions: none

Rule: polynomial · Uses: G1

Leaf basis: polynomial

Every required order exists on the entire interval, and the third derivative is constant.



S02 · definitionBefore

T_2(x)=\sum_{k=0}^2\frac{f^{(k)}(1)}{k!}(x-1)^k

After

T_2(x)=1+3(x-1)+3(x-1)^2

Conditions: none

Rule: taylor_def · Uses: G1, S01, taylor_def

Leaf basis: taylor_def

Divide by each factorial and retain the center shift.



S03 · equivalentBefore

f(2)=8,\quad T_2(2)=7

After

R_2(2)=f(2)-T_2(2)=1

Conditions: none

Rule: algebra · Uses: S02

Leaf basis: algebra

Evaluate the function and polynomial independently before forming the signed remainder.



S04 · impliesBefore

\xi=(1+2)/2=3/2\in(1,2)

After

\frac{f'''(\xi)}{3!}(2-1)^3=\frac6{6}=1=R_2(2)

Conditions: none

Rule: algebra · Uses: G1, S01, S03

Leaf basis: algebra

The constant third derivative makes every interior point valid; explicitly use the strict midpoint as a Lagrange witness.



S05 · definitionBefore

D=\sup_{t\in[1,2]}|f'''(t)|

After

D=6,\quad M=6\ge D

Conditions: none

Rule: taylor_def · Uses: S01, taylor_def

Leaf basis: taylor_def

The derivative is constantly six on the whole interval, so the supremum is exact.



S06 · impliesBefore

|R_2(2)|\le\frac M{3!}|2-1|^3

After

1\le1\quad(M=6)

Conditions: none

Rule: algebra · Uses: S03, S04, S05

Leaf basis: algebra

The qualified derivative bound gives a remainder estimate attained with equality.



S07 · impliesBefore

M=3<D=6

After

\frac M{3!}|2-1|^3=1/2<|R_2(2)|=1

Conditions: none

Rule: algebra · Uses: S03, S05

Leaf basis: algebra

The nonnegative undersized M is not a derivative bound and actually violates the error inequality at this point.



S08 · impliesBefore

x=a=1

After

R_2(1)=0;\quad M=0\text{ gives }0\le0\text{ but is not a bound on }|f'''|

Conditions: none

Rule: algebra · Uses: S02, S05

Leaf basis: algebra

At the center a zero factor may accidentally satisfy the inequality with invalid M; this does not qualify the derivative bound. A degree≤n polynomial separately has identically zero remainder.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · S02, S05 — Separate bound qualification from an accidentally true pointwise inequality.
- S07 · premise_audit · S03, S05 — A negative M would also be invalid, but is not being mixed into this nonnegative undersized witness.
- S06 · premise_audit · S03, S04, S05 — The premise M≥D is separate from the final numerical comparison.
- S05 · premise_audit · S01, taylor_def — This is not a maximum from the center or a few samples.
- S04 · premise_audit · G1, S01, S03 — A strict midpoint exists here because the evaluation point differs from the center.
- S03 · inverse_equivalence · S02 — The remainder here is f-T, not its negative.
- S02 · premise_audit · G1, S01, taylor_def — The quadratic coefficient is 6/2!=3.
- S01 · premise_audit · G1 — The full polynomial supplies both the center jet and interval-wide third derivative.





## Error controls and negative controls

Interval obligationM must control the required derivative on the entire connecting interval.

Sign and factorialKeep R=f-T and divide by (n+1)!.


- A finite second-order jet automatically supplies a third-derivative bound on any connecting interval. → reject — Every f_K(x)=1+3*(x-1)+3*(x-1)^2+K*(x-1)^3 has the same order-two jet (1,3,6) at one, but third derivative 6K is arbitrarily large.
- M=3 bounds the third derivative. → reject — The third derivative has constant magnitude 6.
- The error inequality at x=a proves M is qualified. → reject — A zero displacement can hide an invalid bound, as S08 shows.





## Result and limitations

The remainder is 1, an interior witness is 3/2, M=6 is valid, and M=3 fails here.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: dba2c7065fa51f643663241941c7b9b8831b346d4847714aa8db67441be9746d
- original source SHA-256: dba2c7065fa51f643663241941c7b9b8831b346d4847714aa8db67441be9746d
- 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-taylor-remainder-theorem-01.json)