# 合法 Newton 更新與有限 trace

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

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

derivation-mko-newton-method-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

對 x^2-2 從 1 做兩步精確 Newton，並核 root-first 與循環邊界。

只做有限有理 orbit，不宣稱一般收斂、二次率、唯一根或浮點穩定。





## 已知條件與符號


- algebra
- polynomial
- newton_update


- G1 — f(x)=x^2-2，f'(x)=2x，x_0=1，全部資料 exact rationals；本例目標有限兩步。


- x_k — 精確有限 iterate
- |f(x_k)| — 殘差大小





## 規則與來源


- mko_definition · cited — 對可微實函數f，只有在目前iterate x_k位於domain且f'(x_k)不等於0時，Newton update x_{k+1}=x_k-f(x_k)/f'(x_k)才有定義。本輪exact slice使用低次整係數多項式與有理iterate，逐步精確重算f、f'及更新；若已到f(x_k)=0，先以root_found停止，不再對可能同時為0的導數做0/0。有限orbit、residual下降或某一步接近根都不證一般收斂、二次收斂或global root；residual |f(x)|也不是未給定真根時的forward error。 · mko-newton-method
- algebra · prerequisite — 實數域的等式運算；除法前分母必非零，不等式乘正數保持方向。
- polynomial · prerequisite — 多項式在實數上連續且可逐項微分；d(x^k)/dx=k x^(k-1)，常數導數為零。
- newton_update · prerequisite — 每步先核 f(x)=0 則 root_found 停止；否則須在函數及導數域且 f'(x)≠0，才可更新 x-f(x)/f'(x)。





## 逐步主鏈

S01 · implies操作前

f(x)=x^2-2,\quad f'(x)=2x

操作後

\operatorname{dom}f=\operatorname{dom}f'=\mathbb R

條件：無

規則：polynomial · 依賴：G1

葉節點依據：polynomial

完整多項式給每個有理 iterate 的 domain 資格。



S02 · implies操作前

x_0=1,\quad f(x_0)=-1\ne0,\quad f'(x_0)=2\ne0

操作後

x_1=1-(-1)/2=3/2

條件：無

規則：newton_update · 依賴：G1, S01

葉節點依據：newton_update

先 root test，再 derivative test，全部通過才除法。



S03 · implies操作前

f(3/2)=1/4\ne0,\quad f'(3/2)=3\ne0

操作後

x_2=3/2-(1/4)/3=17/12

條件：無

規則：newton_update · 依賴：S02

葉節點依據：newton_update

重算新點的函數與導數，不能沿用上一步值。



S04 · implies操作前

f(x_0)=-1,\quad f(x_1)=1/4

操作後

f(x_2)=289/144-2=1/144

條件：無

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

葉節點依據：algebra

列出殘差大小下降，但這只是有限 trace；沒有未提供真根的 forward error。



S05 · equivalent操作前

x>0

操作後

x-\frac{x^2-2}{2x}=\tfrac12(x+2/x)>0

條件：x>0

規則：algebra · 依賴：G1

葉節點依據：algebra

平方根特殊型的正 iterate 保持正，因此下一步導數不零；仍未證收斂。



S06 · implies操作前

g(x)=x^3,\quad x=0,\quad g(0)=g'(0)=0

操作後

\text{root_found; do not evaluate }0-0/0

條件：無

規則：newton_update · 依賴：G1

葉節點依據：newton_update

根先停止避免在重根執行未定義 0/0。



S07 · implies操作前

p(x)=x^3-2x+2,\quad p'(x)=3x^2-2,\quad z_0=0

操作後

z_1=0-2/(-2)=1,\quad z_2=1-1/1=0

條件：無

規則：newton_update · 依賴：G1

葉節點依據：newton_update

兩步都合法卻回到原點，完整確定性更新因此永遠在 0,1 間循環。



S08 · implies操作前

\text{finite exact Newton traces and a nonconvergent cycle}

操作後

\text{valid updates do not by themselves prove convergence}

條件：無

規則：algebra · 依賴：S04, S06, S07

葉節點依據：algebra

主例可報兩個精確 iterate 與殘差；循環例否定無條件收斂，保留所有未測的率與穩定性界線。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · S04, S06, S07 — 不因算法 trace 成功就升為一般定理。
- S07 · premise_audit · G1 — 兩步本身加上確定性重複證全循環，而非僅有限觀察猜測。
- S06 · premise_audit · G1 — 零導數不應蓋過已驗證 root 的合法停止。
- S05 · inverse_equivalence · G1 — 正性只保合法更新，不自動給局部率或 global basin。
- S04 · premise_audit · G1, S02, S03 — residual 不是 x 與真根的距離。
- S03 · premise_audit · S02 — 精確分母是 12，非浮點近似。
- S02 · premise_audit · G1, S01 — 不是先除後才發現分母為零。
- S01 · premise_audit · G1 — 有 domain 不表示導數一定非零，仍逐步核。





## 錯誤控制與反例

停止順序domain 後先 root，再 derivative 非零，再除法。

有限 trace 邊界精確 orbit 不等於收斂或二次率證明。


- f=f'=0 時仍更新 0/0。 → reject — 已找到根先停止。
- 殘差就是 forward error。 → reject — 未給真根及殘差到距離的界。
- 合法 Newton 必收斂。 → reject — S07 之 0↔1 循環不收斂。





## 結論與限制

兩步為 3/2、17/12，殘差大小 1/4、1/144；root-first 合法停止，另有合法循環反例。







## 驗證及來源綁定

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


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

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