# 正對角二次函數的安全下降步

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

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

derivation-mko-gradient-descent-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

以 alpha=1/4 對指定二次函數做兩步並證每步下降條件。

只處理 deterministic unconstrained exact trace，不宣稱一般收斂率、projection 或 stochastic update。





## 已知條件與符號


- algebra
- polynomial
- gd_update


- G1 — f(x,y)=x^2+2y^2-2x+4y，d=(2,4)>0，線性係數 b=(-2,4)，起點 z_0=(0,0)，alpha=1/4。


- z_k — 固定座標 iterate
- L — 最大正對角係數





## 規則與來源


- mko_definition · cited — 對可微f:R^d到R及明示alpha_k>0，unconstrained gradient descent更新x_{k+1}=x_k-alpha_k grad f(x_k)。本輪exact slice固定coordinate order，使用positive diagonal quadratic f(x)=1/2 sum d_i x_i^2+sum b_i x_i，逐步重算gradient、iterate與objective。若0<alpha<2/L且L=max d_i，有限trace可逐項核objective nonincrease；這仍不是一般函數或未驗證無限序列的收斂證書。positive step本身不保證下降，zero gradient可出現在maximum或saddle，且unconstrained step不得冒充projected或constrained descent。 · mko-gradient-descent
- algebra · prerequisite — 實數域的等式運算；除法前分母必非零，不等式乘正數保持方向。
- polynomial · prerequisite — 多項式在實數上連續且可逐項微分；d(x^k)/dx=k x^(k-1)，常數導數為零。
- gd_update · prerequisite — unconstrained gradient descent 在可微域內以正步長更新 z_new=z-alpha*gradient f(z)，不做 projection。





## 逐步主鏈

S01 · implies操作前

f=\tfrac12(2x^2+4y^2)-2x+4y

操作後

\nabla f=(2x-2,4y+4),\quad\text{coordinate order }(x,y)

條件：無

規則：polynomial · 依賴：G1

葉節點依據：polynomial

維度、正對角、線性向量與座標全部對齊，完整多項式全域可微。



S02 · implies操作前

L=\max\{2,4\}=4

操作後

0<\alpha=1/4<2/L=1/2

條件：無

規則：algebra · 依賴：G1, S01

葉節點依據：algebra

本 safe trace 明確核額外安全區間，不以 alpha>0 替代。



S03 · implies操作前

\nabla f(z_0)=(-2,4)

操作後

z_1=(0,0)-(1/4)(-2,4)=(1/2,-1)

條件：無

規則：gd_update · 依賴：G1, S01, S02

葉節點依據：gd_update

兩座標同時使用同一 alpha，逐項精確算。



S04 · implies操作前

f(z_0)=0,\quad f(z_1)=1/4+2-1-4

操作後

f(z_1)=-11/4<0

條件：無

規則：algebra · 依賴：G1, S03

葉節點依據：algebra

獨立回算 objective 確認第一步下降。



S05 · implies操作前

\nabla f(z_1)=(-1,0)

操作後

z_2=(3/4,-1),\quad f(z_2)=-47/16<-11/4

條件：無

規則：gd_update · 依賴：S01, S03, S04

葉節點依據：gd_update

重算新梯度再更新，第二座標保持 -1，objective 再下降。



S06 · implies操作前

g_i=d_i z_i+b_i,\quad z_i'=z_i-\alpha g_i

操作後

f(z')-f(z)=-\alpha\sum_{i=1}^2(1-\alpha d_i/2)g_i^2\le0

條件：d_i>0,\quad0<\alpha<2/L

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

葉節點依據：algebra

展開每個二次項，線性一階項合成 -alpha*g_i^2，二階項為 alpha^2*d_i*g_i^2/2；安全界使各係數正。



S07 · implies操作前

q(u)=u^2/2,\quad u_0=1,\quad\alpha=3>0

操作後

u_1=1-3=-2,\quad q(u_1)=2>1/2=q(u_0)

條件：無

規則：algebra · 依賴：G1

葉節點依據：algebra

正步長若超安全界也可上升，明確反駁 alpha>0 就下降。



S08 · implies操作前

z_0,z_1,z_2\text{ exact and descending}

操作後

\text{two verified steps; no general convergence or constrained certificate}

條件：無

規則：gd_update · 依賴：S03, S04, S05, S06, S07

葉節點依據：gd_update

報告完整有限結果與此對角族的一步界，不把駐點或有限下降升為任意 global optimum。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · S03, S04, S05, S06, S07 — constrained、stochastic 與一般 nonconvex 收斂均不在本證書。
- S07 · premise_audit · G1 — 反例與主 safe alpha 不混用。
- S06 · premise_audit · G1, S01, S02 — 全點的一步恆等式可證每個合法 safe step，但有限 trace 仍不等於一般收斂率。
- S05 · premise_audit · S01, S03, S04 — 不是沿用起點梯度再走同一步。
- S04 · premise_audit · G1, S03 — iterate 改變與 objective 下降兩項分開核。
- S03 · premise_audit · G1, S01, S02 — 沒有投影回任何未指定限制集合。
- S02 · premise_audit · G1, S01 — one-step 定義與下降條件分開。
- S01 · premise_audit · G1 — 不是只依某個偏導更新兩個座標。





## 錯誤控制與反例

安全步長L 與 alpha 由同一正對角 objective 計算。

objective 回算每步重算梯度、iterate 與值，不只列點。


- alpha>0 就保下降。 → reject — S07 的 alpha=3 使值增加。
- 零梯度在一般函數必最小。 → reject — x^2-y^2 原點為 saddle，梯度卻零。
- 本更新也自動是 projected descent。 → reject — 沒有投影或限制集合。





## 結論與限制

兩步為 (1/2,-1)、(3/4,-1)，值 -11/4、-47/16；safe 界保本對角族每步不增。







## 驗證及來源綁定

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


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

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