# Safe descent steps for a positive diagonal quadratic

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-gradient-descent/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

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



## Goal and scope

Take two steps with alpha=1/4 for a specified quadratic and prove the per-step descent condition.

Only a deterministic unconstrained exact trace, without general convergence rates, projection or stochastic updates.





## Givens and symbols


- algebra
- polynomial
- gd_update


- G1 — f(x,y)=x^2+2*y^2-2*x+4*y, d=(2,4)>0, linear b=(-2,4), start z_0=(0,0), alpha=1/4.


- z_k — iterate in fixed coordinates
- L — largest positive diagonal coefficient





## Rules and sources


- mko_definition · cited — For differentiable f:R^d→R and explicit alpha_k>0, unconstrained gradient descent updates x_(k+1)=x_k−alpha_k*grad f(x_k). The exact family fixes coordinate order and a positive diagonal quadratic f(x)=1/2*sum_i d_i*x_i^2+sum_i b_i*x_i, recalculating every gradient, iterate and objective. A safe finite trace additionally checks strictly0<alpha<2/L with L=max_i d_i and audits each objective comparison. This is not a convergence certificate for arbitrary functions or an unverified infinite sequence. A positive step alone need not descend, a zero gradient may occur at a maximum or saddle, and an unconstrained step is not projected or constrained descent. · mko-gradient-descent
- algebra · prerequisite — Use real-field identities; division requires a nonzero denominator and multiplication by a positive number preserves inequalities.
- polynomial · prerequisite — Real polynomials are continuous and differentiate termwise: the derivative of x^k is k*x^(k-1), and constants differentiate to zero.
- gd_update · prerequisite — Unconstrained gradient descent updates z_new=z-alpha*gradient f(z) with a positive step in the differentiable domain, without projection.





## Main derivation

S01 · impliesBefore

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

After

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

Conditions: none

Rule: polynomial · Uses: G1

Leaf basis: polynomial

Dimension, positive diagonal, linear vector and coordinates align, and the full polynomial is globally differentiable.



S02 · impliesBefore

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

After

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

Conditions: none

Rule: algebra · Uses: G1, S01

Leaf basis: algebra

Explicitly check the additional safe interval rather than substituting alpha>0.



S03 · impliesBefore

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

After

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

Conditions: none

Rule: gd_update · Uses: G1, S01, S02

Leaf basis: gd_update

Update both coordinates with the same alpha using exact arithmetic.



S04 · impliesBefore

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

After

f(z_1)=-11/4<0

Conditions: none

Rule: algebra · Uses: G1, S03

Leaf basis: algebra

Independently recompute the objective to verify the first decrease.



S05 · impliesBefore

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

After

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

Conditions: none

Rule: gd_update · Uses: S01, S03, S04

Leaf basis: gd_update

Recompute the new gradient; the second coordinate stays -1 and the objective decreases again.



S06 · impliesBefore

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

After

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

Conditions: d_i>0,\quad0<\alpha<2/L

Rule: algebra · Uses: G1, S01, S02

Leaf basis: algebra

Expand each quadratic: first-order terms combine into -alpha*g_i^2 and second-order terms into alpha^2*d_i*g_i^2/2. The safe interval makes every coefficient positive.



S07 · impliesBefore

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

After

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

Conditions: none

Rule: algebra · Uses: G1

Leaf basis: algebra

A positive step beyond the safe interval can increase the objective, refuting positivity alone as descent.



S08 · impliesBefore

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

After

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

Conditions: none

Rule: gd_update · Uses: S03, S04, S05, S06, S07

Leaf basis: gd_update

Report the complete finite trace and the diagonal family's one-step bound without promoting stationarity or finite descent to arbitrary global optimality.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · S03, S04, S05, S06, S07 — Constrained, stochastic and general nonconvex convergence are outside this certificate.
- S07 · premise_audit · G1 — The counterexample's step size is kept separate from the main safe one.
- S06 · premise_audit · G1, S01, S02 — The all-point one-step identity certifies each safe step, but a finite trace still gives no general convergence rate.
- S05 · premise_audit · S01, S03, S04 — The starting gradient is not reused for another identical step.
- S04 · premise_audit · G1, S03 — The changed iterate and decreased objective are separately verified.
- S03 · premise_audit · G1, S01, S02 — No projection onto an unspecified constraint set occurs.
- S02 · premise_audit · G1, S01 — The update definition and descent condition are separate.
- S01 · premise_audit · G1 — Both coordinates use the complete gradient, not one partial.





## Error controls and negative controls

Safe step sizeCompute L and alpha qualification for the same positive-diagonal objective.

Recompute objectiveRecompute the gradient, iterate and objective at every step.


- alpha>0 guarantees descent. → reject — alpha=3 increases the value at S07.
- Zero gradient always means a minimum. → reject — The origin is a zero-gradient saddle for x^2-y^2.
- This update is automatically projected descent. → reject — No projection or constraint set is present.





## Result and limitations

The two iterates are (1/2,-1) and (3/4,-1), with values -11/4 and -47/16; the safe bound ensures nonincrease per step in this diagonal family.







## Verification and source binding

3 declared checks for this guide; only the listed expressions are covered.


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

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-gradient-descent-01.json)