# 三次多項式的精確 Lagrange 餘項

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-taylor-remainder-theorem/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-taylor-remainder-theorem-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

以 f(x)=x^3、a=1、n=2、x=2 核精確餘項及有效導數界。

完整 degree n+1 多項式；不以中心 finite jet 證一般區間定理。





## 已知條件與符號


- algebra
- polynomial
- taylor_def


- G1 — f(x)=x^3，a=1，n=2，評估點 2，連接區間 [1,2]。


- R_2 — f-T 的餘項
- D,M — 精確導數 sup 與候選界





## 規則與來源


- mko_definition · cited — 明示center a、point x、order n與完整polynomial coefficients，直接算Taylor polynomial與remainder。degree≤n時remainder為0；degree n+1時以constant (n+1)th derivative及strictly intermediate midpoint給exact Lagrange witness。exact boundary只接受M至少為derivative supremum的valid bound，或0≤M<D的undersized witness；負M與其他假mode拒絕。finite jet不推出一般remainder theorem、Taylor-series equality或analyticity。 · mko-taylor-remainder-theorem
- algebra · prerequisite — 實數域的等式運算；除法前分母必非零，不等式乘正數保持方向。
- polynomial · prerequisite — 多項式在實數上連續且可逐項微分；d(x^k)/dx=k x^(k-1)，常數導數為零。
- taylor_def · prerequisite — 中心 a 的 T_n 為 k=0 至 n 的 f^(k)(a)*(x-a)^k/k! 之和；remainder 為 f-T_n；導數 sup 取完整連接區間的絕對值最小上界。





## 逐步主鏈

S01 · implies操作前

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

操作後

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

條件：無

規則：polynomial · 依賴：G1

葉節點依據：polynomial

全部所需階在整區間存在，三階導數更是常數。



S02 · definition操作前

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

操作後

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

條件：無

規則：taylor_def · 依賴：G1, S01, taylor_def

葉節點依據：taylor_def

逐階除 factorial 並保留中心位移。



S03 · equivalent操作前

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

操作後

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

條件：無

規則：algebra · 依賴：S02

葉節點依據：algebra

先獨立算函數和近似，再作指定 signed remainder。



S04 · implies操作前

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

操作後

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

條件：無

規則：algebra · 依賴：G1, S01, S03

葉節點依據：algebra

常三階導數使任意內點都可，明示中點為嚴格內部 Lagrange witness。



S05 · definition操作前

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

操作後

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

條件：無

規則：taylor_def · 依賴：S01, taylor_def

葉節點依據：taylor_def

完整區間導數恆為 6，所以 supremum 已精確算出。



S06 · implies操作前

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

操作後

1\le1\quad(M=6)

條件：無

規則：algebra · 依賴：S03, S04, S05

葉節點依據：algebra

有效導數界給剛好取等的餘項界。



S07 · implies操作前

M=3<D=6

操作後

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

條件：無

規則：algebra · 依賴：S03, S05

葉節點依據：algebra

非負但過小的 M 既非導數界，且此點真的違反誤差不等式。



S08 · implies操作前

x=a=1

操作後

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

條件：無

規則：algebra · 依賴：S02, S05

葉節點依據：algebra

中心點的零因子可偶然讓錯 M 的數值式成立，不修補導數界資格；degree≤n 的多項式則整個 remainder 才為零。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · S02, S05 — 區分 bound 資格與偶然單點不等式。
- S07 · premise_audit · S03, S05 — 負 M 更不合 bound 定義，但不是本 undersized witness 的混入。
- S06 · premise_audit · S03, S04, S05 — 界前提 M≥D 獨立於最後數值比較。
- S05 · premise_audit · S01, taylor_def — 不是只在中心或若干 sample 找最大。
- S04 · premise_audit · G1, S01, S03 — 評估點不同中心，才有此嚴格中點可選。
- S03 · inverse_equivalence · S02 — 此處 remainder 是 f-T，不是反號。
- S02 · premise_audit · G1, S01, taylor_def — 二階 6/2!=3。
- S01 · premise_audit · G1 — 中心 jet 與區間三階資料都由完整多項式給出。





## 錯誤控制與反例

區間責任M 要控制整個連接區間的所需導數。

符號及 factorial固定 R=f-T 並除 (n+1)!。


- 有限二階 jet 自動給任意連接區間的三階導數界。 → reject — f_K(x)=1+3(x-1)+3(x-1)^2+K(x-1)^3 的中心二階 jet 都是 (1,3,6)，但三階導數 6K 可任意大。
- M=3 是有效三階界。 → reject — 三階導數絕對值恆為 6。
- x=a 時誤差式成立就證 M 合格。 → reject — 零位移可掩蓋錯界，S08 明示。





## 結論與限制

餘項 1、內點 witness 3/2、有效界 M=6；M=3 在此例失敗。







## 驗證及來源綁定

3 個本稿宣告算術檢查；只支持所列算式。


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

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-taylor-remainder-theorem-01.json)