二分法：四步 bracket 更新、不變量與根存在的獨立責任

目標與範圍

對 f(x)=x²−2，從 [1,2] 與所提供的端點符號 f(1)<0、f(2)>0 出發，依所提供的中點符號執行四步二分，追蹤 bracket；證明「端點異號且 a<b」是不變量、n 步後寬度為 1/2^n、在每次所需符號可取得且更新有效的延伸執行中，寬度停止準則必在有限步內終止；再證明這些 bracket 資料本身不證明有根，並另外引用中間值定理，對連續的 f 得出最終 bracket 內有根。

在 MKO 的範圍內工作：端點與中點符號由題目直接提供（假設 a1），演算法只做 bracket 資料更新；寬度界 w/2^n 是幾何減半結果，不是根存在證明（假設 a2）。根存在作為獨立責任，以引用的中間值定理（citation_verified）與多項式的連續性處理。不處理浮點誤差、收斂速度比較或其他求根法；不改動 canonical MKO 或英文 edition。

已知條件與符號

• order_basics
• frac_rules
• power_laws
• nat_induction
• archimedean
• case_analysis
• numeric_evaluation

• G1 — f(x)=x²−2。初始 bracket [a0,b0]=[1,2]，所提供的端點符號 s(1)=−、s(2)=+。
• G2 — 所提供的中點符號：s(3/2)=+，s(5/4)=−，s(11/8)=−，s(23/16)=+。這些是題目提供的資料（MKO 假設 a1）；本稿以精確有理數計算 f 的值作交叉核對，不由圖形推斷。
• G3 — 演算法（MKO）：給 a<b 且端點符號相反的 [a,b]，取 m=(a+b)/2；若已觀察 f(m)=0 就停在 m；否則保留端點符號相反的半區。本題執行四步，除非提前停止。
• G4 — 用於獨立的根存在步驟：f 是多項式，因此在 ℝ 上連續。

• [a_n,b_n] — 第 n 步後的 bracket
• m_n — 第 n 步的中點 (a_{n-1}+b_{n-1})/2
• s(x) — 所提供的 f(x) 的符號，取 −、0、+
• w_n=b_n-a_n — 第 n 步後的寬度
• \tau — 寬度停止準則的容許值

規則與來源

• order_basics · prerequisite — 實數的序：任兩數恰有 u<v、u=v、u>v 之一；u<v 且 v<w 推出 u<w；u<v 推出 u+w<v+w；u<v 且 w>0 推出 uw<vw；u<v 且 w<0 推出 uw>vw。
• frac_rules · prerequisite — 分數運算（分母皆非零）：a/c+b/c=(a+b)/c；(a/b)(c/d)=(ac)/(bd)；(a/b)/(c/d)=(ad)/(bc)（另需 c≠0）；a/b=(ak)/(bk)（k≠0）。
• power_laws · prerequisite — 整數指數律（底數非零或指數為正整數）：a^m·a^n=a^{m+n}，(a^m)^n=a^{mn}，(ab)^n=a^n b^n，a^0=1。
• nat_induction · prerequisite — 數學歸納原理：對從 n₀ 起的命題族 P(n)，若 P(n₀) 成立，且對每個 n≥n₀ 都有 P(n)⇒P(n+1)，則所有 n≥n₀ 都有 P(n)。
• archimedean · prerequisite — 阿基米德性質：對任意實數 x，存在自然數 n>x；因此對任意 ε>0，存在 n 使 1/n<ε。
• case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。
• abs_rules · prerequisite — 絕對值（實數）：|u|=u（u≥0）、|u|=−u（u<0）；|u|≥0；|uv|=|u||v|；三角不等式 |u+v|≤|u|+|v|；|u|<r ⇔ −r<u<r。
• exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
• mko_bisect · cited — 給定有序區間 [a,b] 及已提供的端點符號 bracket，每步取 m=(a+b)/2。若已觀察 f(m)=0 就停在 m；否則保留端點符號相反的半區。沒有另行使用中間值定理時，這只是 bracket 資料更新，不自行證明根存在。 · mko-bisection-method
• ivt · cited — 中間值定理（符號形式）：若 f 在 [a,b] 上連續且 f(a)<0<f(b)，則存在 x∈[a,b] 使 f(x)=0。 · OpenStax, Calculus Volume 1, Section 2.4, Intermediate Value Theorem
• poly_continuous · prerequisite — 多項式函數在 ℝ 上處處連續，因此在任何閉區間上連續。
• L_mid · lemma — 若 a<b，m=(a+b)/2，則 a<m<b，且 m−a=b−m=(b−a)/2。
• L_half · lemma — 若 s(a)、s(b) 一為 − 一為 +，且 s(m)≠0，則 [a,m] 與 [m,b] 中恰有一個端點符號相反。
• L_width · lemma — 沒有提前停止時，n 次有效二分後 b_n−a_n=(b_0−a_0)/2^n。

逐步主鏈

\text{bisection with supplied sign data}

[a_0,b_0]=[1,2],\ m_{n}=\tfrac{a_{n-1}+b_{n-1}}{2}

[1,2],\ s(1)=-,\ s(2)=+

\text{valid input: } 1<2,\ \text{opposite endpoint signs}

[a_0,b_0]=[1,2]

m_1=\tfrac{1+2}{2}=\tfrac{3}{2},\ 1<\tfrac{3}{2}<2

\{s(a),s(b)\}=\{-,+\},\ s(m)\neq 0

\text{exactly one of }[a,m],\ [m,b]\ \text{has opposite endpoint signs}

[1,2],\ s(\tfrac{3}{2})=+

[a_1,b_1]=[1,\tfrac{3}{2}]

[1,\tfrac{3}{2}],\ m_2=\tfrac{5}{4},\ s(\tfrac{5}{4})=-

[a_2,b_2]=[\tfrac{5}{4},\tfrac{3}{2}]

[\tfrac{5}{4},\tfrac{3}{2}],\ m_3=\tfrac{11}{8},\ s(\tfrac{11}{8})=-

[a_3,b_3]=[\tfrac{11}{8},\tfrac{3}{2}]

[\tfrac{11}{8},\tfrac{3}{2}],\ m_4=\tfrac{23}{16},\ s(\tfrac{23}{16})=+

[a_4,b_4]=[\tfrac{11}{8},\tfrac{23}{16}]

a_0<b_0,\ s(a_0)=-,\ s(b_0)=+

\forall n\le 4:\ a_n<b_n,\ s(a_n)=-,\ s(b_n)=+,\ [a_{n}, b_{n}]\subseteq[a_{n-1},b_{n-1}]\ (n\geq 1)

w_0=b_0-a_0=1

w_n=\tfrac{1}{2^n}

[a_4,b_4]=[\tfrac{11}{8},\tfrac{23}{16}]

w_4=\tfrac{1}{16},\ m_5=\tfrac{45}{32},\ |x-m_5|\le\tfrac{1}{32}\ \ \forall x\in[a_4,b_4]

\tau>0

\exists N:\ \tfrac{1}{2^N}<\tau

g(x)=\begin{cases}-1 & x<\tfrac{7}{5}\\ 1 & x\ge\tfrac{7}{5}\end{cases}

g\ \text{gives the same signs and brackets, and}\ g(x)\neq 0\ \forall x

f\ \text{continuous on}\ [\tfrac{11}{8},\tfrac{23}{16}],\ f(\tfrac{11}{8})=-\tfrac{7}{64}<0<\tfrac{17}{256}=f(\tfrac{23}{16})

\exists c\in[\tfrac{11}{8},\tfrac{23}{16}]:\ f(c)=0,\ |c-\tfrac{45}{32}|\le\tfrac{1}{32}

\text{trace, invariant, width, termination, root duty}

[a_4,b_4]=[\tfrac{11}{8},\tfrac{23}{16}],\ w_4=\tfrac{1}{16},\ \text{root in}\ [a_4,b_4]\ \text{only via IVT}

局部子步與引理

a<b,\ m=\tfrac{a+b}{2}

m-a=b-m=\tfrac{b-a}{2}>0

s(m)=s(a)

[a,m]\ \text{same signs},\ [m,b]\ \text{opposite signs}

s(m)=s(b)

[a,m]\ \text{opposite signs},\ [m,b]\ \text{same signs}

s(m)\in\{-,+\},\ \{s(a),s(b)\}=\{-,+\}

s(m)=s(a)\ \veebar\ s(m)=s(b)

n=0

w_0=\tfrac{w_0}{2^0}

w_n=\tfrac{w_0}{2^n}

w_{n+1}=\tfrac{w_n}{2}=\tfrac{w_0}{2^{n+1}}

逐步反向審查

• S15 · sufficient_goal_reduction · S08, S09, S10, S12, S13, S14 — 目標 G：追蹤結果、不變量、寬度、終止與有根的結論。足夠條件 H：S08、S09、S10、S12、S14 各別成立；S13 界定哪些結論不能只由資料得到。H 都由資料、引理與引用定理正向得出，沒有把 G 當作前提。
• S14 · premise_audit · ivt, poly_continuous, G4, S11 — 定理需要連續性與端點嚴格異號的實際函數值；兩者都由本步另外提供，而不是由 bracket 更新得到。S13 的 g 缺連續性，所以同樣的論證對 g 不能做。
• S13 · premise_audit · case_analysis, numeric_evaluation — 一個「資料相同、卻無根」的函數就足以說明資料不蘊含根存在；g 在 7/5 不連續，這正是中間值定理的前提所排除的情形。
• S12 · premise_audit · archimedean, nat_induction, S10 — 需要 τ>0；τ=0 時寬度永遠不會 ≤0，準則不會觸發。這是演算法的終止，不是根的存在。
• S11 · premise_audit · L_mid, S10 — 只用中點與寬度；距離界套用到根之前，必須先另外證明根在區間內。
• S10.2 · premise_audit · S03.1, power_laws, frac_rules — 兩種選擇的寬度相同，所以不必知道選了哪一半。
• S10.1 · premise_audit · power_laws — 只用 a^0=1。
• S10 · premise_audit · L_width, S03.1 — 只需要中點的位置；不宣稱寬度界是根的誤差界（那需要根確實在區間內，見 S14）。
• S09 · premise_audit · S02, L_mid, L_half, nat_induction — 歸納步需要 s(m)≠0；若觀察到 s(m)=0，演算法停止，不變量不再需要延伸。不變量只描述符號資料與區間位置，不包含「區間內有根」。
• S08 · premise_audit · L_half, L_mid, G2 — 同 S06；結束是因為達到 G3 指定的步數。
• S07 · premise_audit · L_half, L_mid, G2 — 同 S06。
• S06 · premise_audit · L_half, L_mid, G2 — 同 S05：中點由 L_mid 定位，半區由 L_half 選定。
• S05 · premise_audit · L_half, G2 — 只用所提供的中點符號與引理；f 的精確值是交叉核對。
• S04.3 · premise_audit · case_analysis, S04.1, S04.2 — 分情況論證要求情況涵蓋全部可能；這裡的兩種情況正好窮盡 s(m) 的非零值。
• S04.2 · premise_audit · G3, def_unfold — 與 S04.1 對稱。
• S04.1 · premise_audit · G3, def_unfold — 只用符號相等的傳遞性與 s(a)≠s(b)。
• S04 · premise_audit · L_half, case_analysis — 引理只用符號資料，不用 f 的連續性或任何函數值；因此它也不能推出根存在。
• S03.1 · premise_audit · order_basics, frac_rules — 需要 a<b；若 a=b，中點等於端點，不再有兩個非退化半區。
• S03 · premise_audit · L_mid, S02 — 需要 a0<b0（S02）；引理在 S03.1 證明。
• S02 · premise_audit · G1, and_intro_elim — 合格性是兩個條件的合取；精確計算只是交叉核對，演算法使用的是所提供的符號。
• S01 · premise_audit · G1, G2, G3, mko_bisect — 此步只陳述演算法與資料，不推出新事實。

錯誤控制與反例

異號不等於有根

MKO 指出的誤解之一是看到異號就省略中間值定理而直接宣稱有根。S13 的階梯函數 g 與 f 在所有用到的點上符號相同，產生相同的 bracket，卻沒有根。有根需要連續性加上中間值定理（S14），這是 bracket 更新之外的獨立責任。

區間寬度不是函數值誤差

MKO 指出的另一誤解。最終寬度 1/16 只界定 x 方向的距離（且要先知道根在區間內）。函數 h(x)=100(x²−2) 有完全相同的符號與 bracket，但 h(11/8)=−175/16，絕對值約 10.9（N15），遠大於 1/16。寬度界與 |f(x)| 的大小是兩回事。

選半區時看端點符號

最容易做錯的是保留錯的一半：s(m) 與 s(a) 同號時要保留 [m,b]，不是 [a,m]（S04.1）。檢查方法是看保留的區間兩端是否一負一正；S09 的不變量要求左端為 −、右端為 +。

• f(1)<0<f(2)，所以二分法本身證明了 [1,2] 中有根 → reject — 階梯函數 g 有相同的端點與中點符號，卻沒有根（S13）；有根要另用連續性與中間值定理。
• 僅由最終 bracket 寬度為 1/16，就能保證任何給出同樣符號資料的函數 h 都滿足 |h(45/32)|≤1/16。 → reject — 寬度只控制 x 的距離，不一般控制函數值。取 h(x)=100(x²−2)，它給出同樣符號與 bracket，但在同一中點 |h(45/32)|=575/256>1/16。原 f 的 |f(45/32)|=23/1024≤1/16 只是本例的數值事實，並非由寬度單獨保證。
• s(3/2)=+，所以保留 [3/2,2] → reject — [3/2,2] 兩端都是 +；異號的是 [1,3/2]（S05）。
• 從 [1,2] 出發但所提供的符號是 s(1)=+、s(2)=+，二分法仍可正常進行 → reject — 兩端同號不符合本演算法要求的端點異號輸入契約（S02），因此不能直接引用該 bracket 不變量；不據此宣稱不存在可由額外符號資料找出的端點異號子區間。

結論與限制

從 [1,2] 依所提供的符號 +、−、−、+ 執行四步二分，bracket 依序為 [1,3/2]、[5/4,3/2]、[11/8,3/2]、[11/8,23/16]，寬度 1/16=1/2⁴；端點異號是不變量，寬度準則對任何 τ>0 都會終止。這些 bracket 資料本身不證明有根（階梯函數 g 給出相同資料卻無根）；另以多項式的連續性與中間值定理，得出 f(x)=x²−2 在 [11/8,23/16] 內有根 c，且 |c−45/32|≤1/32。

• 中間值定理以引用方式使用（citation_verified），本稿沒有證明它；多項式的連續性作為前置知識。
• N14 是 n=0 到 20 的有限核對，2^n≥n+1 對所有 n 的證明是 S12 中的歸納；N12、N13 是一次多項式恆等式的網格核對。

驗證及來源綁定

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: fc6815b2e34c1a498109d7c25fa634c56e668faddafc9d05c16b74cc9206e49d
• original source SHA-256: 6785e2b4757cf8bcdb04bf8c2e24e02150a9f5d955df275d9ba4228ece867aaa
• Lean: NOT_RUN · independent AI: NOT_MEASURED

同源完整 JSON（含公式、AST、反控制與修訂記錄）