# 多項式 bracket 與精確中間值

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

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

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



## 目標與範圍

對 f(x)=x^2-1 在 [0,2] 找值 0，並保留端點及非唯一邊界。

完整多項式證書與精確 witness；不把有限 bisection 稱作極限證明。





## 已知條件與符號


- algebra
- polynomial
- IVT


- G1 — f(x)=x^2-1，a=0,b=2，目標 y=0。


- y — 目標值
- c — 包含端點的 witness





## 規則與來源


- mko_definition · cited — 固定a<b、完整interval domain與continuous polynomial certificate，target y須inclusive介於f(a)、f(b)。exact families提供明示c∈[a,b]且f(c)=y；endpoint root保留。IVT只保證存在，不保證唯一、rational closed form或有限bisection已收斂。明示discontinuous step可有sign change但沒有root；有限samples不證continuity。 · mko-intermediate-value-theorem
- algebra · prerequisite — 實數域的等式運算；除法前分母必非零，不等式乘正數保持方向。
- polynomial · prerequisite — 多項式在實數上連續且可逐項微分；d(x^k)/dx=k x^(k-1)，常數導數為零。
- IVT · prerequisite — 若 a<b、f 在整個 [a,b] 連續且 y 介於兩端值（含相等、任一方向），則存在 c∈[a,b] 使 f(c)=y。





## 逐步主鏈

S01 · implies操作前

a=0,\ b=2

操作後

a<b,\quad[a,b]=[0,2]\text{ is the full domain interval}

條件：無

規則：algebra · 依賴：G1

葉節點依據：algebra

先固定完整閉區間，不把零散點集當區間。



S02 · implies操作前

f(x)=x^2-1

操作後

f\text{ continuous at every point of }[0,2]

條件：無

規則：polynomial · 依賴：G1, S01

葉節點依據：polynomial

完整多項式保證全閉區間連續，並非樣本看似平滑。



S03 · implies操作前

f(0)=0^2-1,\quad f(2)=2^2-1

操作後

f(0)=-1\le0\le3=f(2)

條件：無

規則：algebra · 依賴：G1

葉節點依據：algebra

精確核目標在端點值之間。



S04 · theorem_application操作前

f\text{ continuous on }[0,2],\quad-1\le0\le3

操作後

\exists c\in[0,2]:f(c)=0

條件：無

規則：IVT · 依賴：S01, S02, S03

葉節點依據：IVT

明示套用 IVT 前提只得到存在，不包含唯一或可寫有理式。



S05 · implies操作前

c=1

操作後

0<1<2,\quad f(1)=1^2-1=0

條件：無

規則：algebra · 依賴：G1, S04

葉節點依據：algebra

此多項式另有精確有理 witness，獨立核範圍與等式。



S06 · implies操作前

[a,b]=[1,2],\quad y=0

操作後

c=a=1\text{ is a valid endpoint witness}

條件：無

規則：algebra · 依賴：G1

葉節點依據：algebra

IVT 的 c 可在端點，這與 MVT 的嚴格內點責任不同。



S07 · implies操作前

g(x)=x^3-x\text{ on }[-2,2]

操作後

g(-2)=-6,\ g(2)=6,\quad g(-1)=g(0)=g(1)=0

條件：無

規則：polynomial · 依賴：G1

葉節點依據：polynomial

明示另一連續 bracket 例具有三個不同根，保護非唯一界線。



S08 · implies操作前

s(x)=\begin{cases}-1&x<0\\1&x\ge0\end{cases}\quad\text{on }[-1,1]

操作後

s(-1)<0<s(1),\quad0\notin s([-1,1])

條件：無

規則：algebra · 依賴：G1

葉節點依據：algebra

不連續跳躍可變號卻不取零；連續性前提不能刪除。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · G1 — 失敗在 0 的連續性，端點 bracket 本身確實成立。
- S07 · premise_audit · G1 — 不是宣稱原 f 在 [0,2] 有三根；例子分清。
- S06 · premise_audit · G1 — 另分支仍 a<b 且 f(1)=y。
- S05 · premise_audit · G1, S04 — 個別有理根不代表所有 IVT 問題都有有理閉式。
- S04 · premise_audit · S01, S02, S03 — 每個前提都由前步給出，不由端點變號單獨跳結論。
- S03 · premise_audit · G1 — bracket 是包含端點的非嚴格條件。
- S02 · premise_audit · G1, S01 — 連續性的全稱範圍明確。
- S01 · premise_audit · G1 — a=b 不在此應用前提。





## 錯誤控制與反例

前提逐項完整區間、連續性及 bracket 各自核。

有限演算法有限二分只給區間或近似，不自動是無限收斂證明。


- 端點變號即使不連續仍必有根。 → reject — S08 跳躍函數不取零。
- IVT 的 witness 必嚴格在內部。 → reject — S06 的端點值已等於目標。
- 存在就必唯一。 → reject — S07 的三個根反駁。





## 結論與限制

主例 witness c=1；IVT 只保證存在，可在端點且一般不唯一。







## 驗證及來源綁定

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


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

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