二次多項式的均值點

目標與範圍

對 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)，常數導數為零。

逐步主鏈

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

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

f(b)-f(a)

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

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

A(a+b)+B

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

f'(t)=2At+B

c=(a+b)/2

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

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

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

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

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

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

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

局部子步與引理

本稿無局部子步。

逐步反向審查

• 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、反控制與修訂記錄）