合法 Newton 更新與有限 trace

目標與範圍

對 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)。

逐步主鏈

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

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

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

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

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

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

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

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

x>0

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

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

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

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

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

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

局部子步與引理

本稿無局部子步。

逐步反向審查

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