# Coordinate gradients, stationarity and differentiability [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-gradient-vector/) 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-vector-01 · ocme-new142-reader-adoption-20261021 ## Goal and scope Compute the gradient of a specified bivariate polynomial and audit two false inferences. Fixed standard Euclidean coordinate order (x,y), with no implicit optimization or descent certificate. ## Givens and symbols - algebra - polynomial - definition_here - G1 — f(x,y)=x^2+x*y+2*y^2-4*x+2*y, coordinates ordered (x,y), evaluation point p=(1,-1). - \nabla f — gradient in fixed coordinate order - p — exact evaluation point ## Rules and sources - mko_definition · cited — Source semantic paraphrase: the gradient contains each coordinate partial in fixed order; existing partials and stationarity do not automatically imply differentiability or an extremum. · mko-gradient-vector - 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. - definition_here · prerequisite — In fixed standard Euclidean coordinates, the gradient is the ordered vector of all coordinate partials; a stationary point has all gradient coordinates zero. ## Main derivation S01 · impliesBefore f=x^2+xy+2y^2-4x+2y After \partial_x f=2x+y-4 Conditions: none Rule: polynomial · Uses: G1 Leaf basis: polynomial Differentiate with respect to x while holding y fixed, preserving coordinate order. S02 · impliesBefore f=x^2+xy+2y^2-4x+2y After \partial_y f=x+4y+2 Conditions: none Rule: polynomial · Uses: G1 Leaf basis: polynomial Differentiate with respect to y holding x fixed; the mixed term gives x. S03 · definitionBefore \nabla f=(\partial_x f,\partial_y f) After \nabla f(x,y)=(2x+y-4,x+4y+2) Conditions: none Rule: definition_here · Uses: S01, S02 Leaf basis: definition_here Assemble the two coordinates in fixed order, matching the R^2 source dimension. S04 · impliesBefore p=(1,-1) After \nabla f(p)=(-3,-1)\ne(0,0) Conditions: none Rule: algebra · Uses: G1, S03 Leaf basis: algebra Evaluate every coordinate exactly; this point is not stationary. S05 · equivalentBefore 2x+y=4,\quad x+4y=-2 After (x,y)=(18/7,-8/7),\quad\nabla f=0 Conditions: none Rule: algebra · Uses: S03 Leaf basis: algebra Eliminate to get the unique stationary point: substitute y=4-2x into the second equation to obtain -7x=-18. S06 · impliesBefore s(x,y)=x^2-y^2 After \nabla s(0,0)=0,\quad s(t,0)>0>s(0,t)\ (t\ne0) Conditions: none Rule: polynomial · Uses: G1 Leaf basis: polynomial An explicit saddle has positive and negative values in every neighborhood, so a zero gradient is insufficient for an extremum. S07 · impliesBefore h(x,y)=x^3/(x^2+y^2)\ ((x,y)\ne0),\quad h(0,0)=0 After \partial_xh(0,0)=1,\quad\partial_yh(0,0)=0 Conditions: none Rule: algebra · Uses: G1 Leaf basis: algebra Along the x-axis h(t,0)=t, while h(0,t)=0 on the y-axis, giving partial difference quotients 1 and 0. S08 · impliesBefore h(t,t)=t/2,\quad Dh_{\text{candidate}}(t,t)=t After \frac{|h(t,t)-t|}{\|(t,t)\|_2}=\frac1{2\sqrt2}\not\to0 Conditions: t\ne0 Rule: algebra · Uses: S07 Leaf basis: algebra Differentiability would force derivative (1,0), but the normalized diagonal remainder does not vanish, proving nondifferentiability. ## Substeps and lemmas No substeps in this guide. ## Reverse audits - S08 · premise_audit · S07 — The necessary differentiability remainder condition explicitly refutes existing partials implying differentiability. - S07 · premise_audit · G1 — Coordinate partials exist, but a full-direction linear remainder is not yet proved. - S06 · premise_audit · G1 — Both directional values are supplied instead of only a saddle label. - S05 · inverse_equivalence · S03 — This proves stationarity only, without declaring a minimum merely from zero gradient. - S04 · premise_audit · G1, S03 — The nonzero gradient is not converted into an unspecified descent step or optimum classification. - S03 · premise_audit · S01, S02 — One partial alone cannot be called the complete gradient. - S02 · premise_audit · G1 — 4y comes from 2y^2 without dropping a factor two. - S01 · premise_audit · G1 — The x-derivatives of 2y^2 and 2y vanish. ## Error controls and negative controls Coordinate orderBoth symbolic differentiation and evaluation use (x,y). Separate obligationsKeep stationarity, differentiability, extrema and global optimality separate. - A gradient needs only one coordinate. → reject — An R^2 source requires both ordered partials. - A zero gradient guarantees a minimum. → reject — The saddle x^2-y^2 has both signs near the origin. - All partials existing imply differentiability. → reject — The diagonal remainder at S07-S08 does not vanish. ## Result and limitations The gradient is (2x+y-4,x+4y+2), at p it is (-3,-1); zero gradient and existing partials do not imply extrema and differentiability respectively. ## Verification and source binding 4 declared checks for this guide; only the listed expressions are covered. - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: 5d7de98af659977808b6bdfbc360956ccd0ca6a6d166fe2b4f428078f3673915 - original source SHA-256: 5d7de98af659977808b6bdfbc360956ccd0ca6a6d166fe2b4f428078f3673915 - 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-vector-01.json)