# 二次多項式的均值點

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

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

derivation-mko-mean-value-theorem-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

對 f(t)=A t^2+B t+C 在 a<b 上直接構造均值點。

精確多項式實例族；不由樣本證一般連續或可微。





## 已知條件與符號


- algebra
- polynomial


- G1 — A,B,C,a,b 為有理數，a<b；f(t)=A t^2+B t+C。


- c — 嚴格內點均值見證
- A,B,C — 依序二次一次常數係數





## 規則與來源


- mko_definition · cited — 題族參數A/B/C明確編碼f(t)=A t^2+B t+C。必須a<b、closed interval continuity與open interval differentiability；witness c嚴格位於(a,b)，且f'(c)=(f(b)-f(a))/(b-a)。c不保證唯一，affine或constant case可有多個witness。有限samples、a=b、jump或interior cusp不足。 · mko-mean-value-theorem
- algebra · prerequisite — 實數域的等式運算；除法前分母必非零，不等式乘正數保持方向。
- polynomial · prerequisite — 多項式在實數上連續且可逐項微分；d(x^k)/dx=k x^(k-1)，常數導數為零。





## 逐步主鏈

S01 · implies操作前

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

操作後

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

條件：a<b

規則：polynomial · 依賴：G1

葉節點依據：polynomial

多項式在全實線連續可微，故兩個不同區間責任均滿足。



S02 · equivalent操作前

f(b)-f(a)

操作後

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

條件：無

規則：algebra · 依賴：G1

葉節點依據：algebra

常數 C 抵銷，用平方差分解。



S03 · equivalent操作前

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

操作後

A(a+b)+B

條件：b-a>0

規則：algebra · 依賴：G1, S02

葉節點依據：algebra

a<b 保證 b-a>0 可除，得到割線斜率。



S04 · implies操作前

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

操作後

f'(t)=2At+B

條件：無

規則：polynomial · 依賴：G1

葉節點依據：polynomial

逐項微分取得整個開區間上的導函數。



S05 · implies操作前

c=(a+b)/2

操作後

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

條件：無

規則：algebra · 依賴：G1

葉節點依據：algebra

中點嚴格位於兩端之間。



S06 · implies操作前

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

操作後

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

條件：無

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

葉節點依據：algebra

代中點後與割線斜率完全相等，直接證此多項式族的結論。



S07 · case_split操作前

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

操作後

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

條件：無

規則：algebra · 依賴：S03, S04

葉節點依據：algebra

非零 A 可約去得唯一中點；仿射與常數情況導數處處等於割線斜率。



S08 · implies操作前

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

操作後

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

條件：無

規則：algebra · 依賴：S06

葉節點依據：algebra

以精確有理實例回查係數與 witness。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · S06 — 一般多項式族已在前步證，數值核對只是回查。
- S07 · premise_audit · S03, S04 — 存在不普遍推出唯一，A=0 分支不能除 A。
- S06 · premise_audit · S03, S04, S05 — 等式及內點資格分開已核，沒有把單一數值等式當一般 MVT 證明。
- S05 · premise_audit · G1 — 均值點不允許僅落在端點。
- S04 · premise_audit · G1 — 不是只在候選 c 的單點核數值。
- S03 · inverse_equivalence · G1, S02 — 若 a=b 不能使用這個式子。
- S02 · inverse_equivalence · G1 — A/B/C 依序是二次、一次、常數係數，未調換。
- S01 · premise_audit · G1 — 閉區間連續與開區間可微不能互相替代。





## 錯誤控制與反例

分母先行先核 a<b 再除 b-a。

前提分區全閉區間連續與全開區間可微均由完整多項式給出。


- a=b 仍照除割線分母。 → reject — 分母為零。
- |t| 在 [-1,1] 可直接套 MVT。 → reject — 0 處不可微，且割線斜率 0 無內點導數等於它。
- 均值點必唯一。 → reject — A=0 時每個內點都可以。





## 結論與限制

中點總是此二次族的均值點；A≠0 時唯一，A=0 時任何內點皆可。







## 驗證及來源綁定

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


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

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