# Qualified Newton updates and a finite trace

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

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-newton-method-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Take two exact Newton steps for x^2-2 from one, and audit root-first stopping and a cycle boundary.

A finite rational orbit only, without general convergence, quadratic rate, root uniqueness or floating-point stability.





## Givens and symbols


- algebra
- polynomial
- newton_update


- G1 — f(x)=x^2-2, f'(x)=2x, x_0=1, using exact rationals; the requested trace has two steps.


- x_k — exact finite iterate
- |f(x_k)| — residual magnitude





## Rules and sources


- mko_definition · cited — For a differentiable real function, the Newton update x_(k+1)=x_k−f(x_k)/f_prime(x_k) requires the current iterate in the domain and a nonzero derivative. The exact polynomial families use coefficients in low-to-high degree order and bounded rational iterates, recalculating f, its derivative and every update. If f(x_k)=0, stop as root_found before any division, even if the derivative also vanishes. A finite orbit, decreasing residual or one iterate near a root does not prove general or quadratic convergence, a global root basin or root uniqueness. Residual |f(x)| is not forward error to an unprovided true root. · mko-newton-method
- 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.
- newton_update · prerequisite — At each step first stop as root_found when f(x)=0; otherwise require the function/derivative domain and f'(x)≠0 before updating x-f(x)/f'(x).





## Main derivation

S01 · impliesBefore

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

After

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

Conditions: none

Rule: polynomial · Uses: G1

Leaf basis: polynomial

The full polynomial supplies domain qualification for every rational iterate.



S02 · impliesBefore

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

After

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

Conditions: none

Rule: newton_update · Uses: G1, S01

Leaf basis: newton_update

Perform the root test before the derivative test; divide only after both qualify.



S03 · impliesBefore

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

After

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

Conditions: none

Rule: newton_update · Uses: S02

Leaf basis: newton_update

Recompute the new function and derivative values instead of reusing the previous step's data.



S04 · impliesBefore

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

After

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

Conditions: none

Rule: algebra · Uses: G1, S02, S03

Leaf basis: algebra

The residual magnitudes decrease in this finite trace, but no forward error to an unprovided root is asserted.



S05 · equivalentBefore

x>0

After

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

Conditions: x>0

Rule: algebra · Uses: G1

Leaf basis: algebra

The square-root special form preserves positive iterates and hence nonzero derivatives, without yet proving convergence.



S06 · impliesBefore

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

After

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

Conditions: none

Rule: newton_update · Uses: G1

Leaf basis: newton_update

Stopping at the root first avoids an undefined 0/0 update at a multiple root.



S07 · impliesBefore

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

After

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

Conditions: none

Rule: newton_update · Uses: G1

Leaf basis: newton_update

Both updates are legal but return to the start; deterministic repetition therefore cycles forever between zero and one.



S08 · impliesBefore

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

After

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

Conditions: none

Rule: algebra · Uses: S04, S06, S07

Leaf basis: algebra

Report the two exact iterates and residuals for the main example; the cycle refutes unconditional convergence while rates and stability remain unclaimed.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · S04, S06, S07 — A successful trace is not promoted to a general theorem.
- S07 · premise_audit · G1 — The two steps plus deterministic repetition prove the whole cycle, not a guess from a finite observation.
- S06 · premise_audit · G1 — A zero derivative must not override an already verified root stop.
- S05 · inverse_equivalence · G1 — Positivity qualifies updates but does not supply a local rate or global basin.
- S04 · premise_audit · G1, S02, S03 — Residual is not the distance from x to a true root.
- S03 · premise_audit · S02 — The denominator is exactly twelve, not a floating approximation.
- S02 · premise_audit · G1, S01 — Division does not precede checking its denominator.
- S01 · premise_audit · G1 — Domain membership does not ensure a nonzero derivative, which remains a per-step check.





## Error controls and negative controls

Stopping orderAfter domain qualification test root first, then nonzero derivative, then divide.

Finite-trace boundaryAn exact orbit is not a convergence or quadratic-rate proof.


- At f=f'=0 still update via 0/0. → reject — Stop first at the verified root.
- Residual is forward error. → reject — No true root or residual-to-distance bound is provided.
- Legal Newton updates must converge. → reject — The 0-to-1 cycle at S07 does not converge.





## Result and limitations

The two iterates are 3/2 and 17/12 with residual magnitudes 1/4 and 1/144; root-first stopping is qualified and a separate legal cycle exists.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: a8402cf26e4f5f76569b37ad78c171902dc851990ef0d99bdc44bcfc7413eea7
- original source SHA-256: a8402cf26e4f5f76569b37ad78c171902dc851990ef0d99bdc44bcfc7413eea7
- 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-newton-method-01.json)