# Regular multipliers and a complete squared-distance solution

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

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-lagrange-multiplier-condition-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Minimize the squared distance to (1,2) subject to x_1+x_2=0; find the point and multiplier and independently prove the minimum.

Fix the positive sign grad f=J_g^T*lambda; general multipliers are necessary only, while this particular distance problem has a separate sufficiency proof.





## Givens and symbols


- algebra
- polynomial
- lagrange_regular


- G1 — f(x_1,x_2)=(x_1-1)^2+(x_2-2)^2, g=x_1+x_2; the Jacobian rows follow the single constraint's order.


- J_g — row Jacobian ordered by constraint
- \lambda — multiplier in the positive-sign convention
- v — arbitrary feasible difference





## Rules and sources


- mko_definition · cited — Source semantic paraphrase: at a feasible local extremum, neighborhood differentiability and full row rank give a unique multiplier representing the objective gradient; the condition is necessary only. · mko-lagrange-multiplier-condition
- 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.
- lagrange_regular · prerequisite — At a feasible local extremum, neighborhood differentiability and independent constraint-gradient rows imply a unique lambda with grad f=J_g^T*lambda; this is necessary only.





## Main derivation

S01 · impliesBefore

n=2,\quad m=1,\quad J_g=(1\ \ 1)

After

\operatorname{rank}J_g=1=m,\quad f,g\text{ differentiable on }\mathbb R^2

Conditions: none

Rule: polynomial · Uses: G1

Leaf basis: polynomial

The single nonzero row has full row rank, and the full polynomials give neighborhood differentiability.



S02 · definitionBefore

\nabla f=(2(x_1-1),2(x_2-2))

After

2(x_1-1)=\lambda,\quad2(x_2-2)=\lambda,\quad x_1+x_2=0

Conditions: none

Rule: lagrange_regular · Uses: G1, S01, lagrange_regular

Leaf basis: lagrange_regular

Form the candidate equations from necessary stationarity and feasibility without yet declaring their solution a minimum.



S03 · equivalentBefore

x_1=1+\lambda/2,\quad x_2=2+\lambda/2

After

3+\lambda=0\Longrightarrow\lambda=-3

Conditions: none

Rule: algebra · Uses: S02

Leaf basis: algebra

Substitution into the single linear constraint determines the multiplier uniquely.



S04 · equivalentBefore

\lambda=-3

After

x^*=(-1/2,1/2)

Conditions: none

Rule: algebra · Uses: S03

Leaf basis: algebra

Substitute into both candidate-coordinate formulas.



S05 · impliesBefore

g(x^*)=-1/2+1/2

After

g(x^*)=0,\quad\nabla f(x^*)=(-3,-3)=J_g^T(-3)

Conditions: none

Rule: algebra · Uses: G1, S01, S04

Leaf basis: algebra

Independently recheck feasibility and stationarity residual at the candidate; full rank remains valid.



S06 · impliesBefore

z=(1,2),\quad x^*-z=(-3/2,-3/2)

After

f(x^*)=9/4+9/4=9/2

Conditions: none

Rule: algebra · Uses: G1, S04, S05

Leaf basis: algebra

Compute the squared distance exactly as the reference for all comparison points.



S07 · impliesBefore

y=x^*+v\text{ feasible}\Longrightarrow v_1+v_2=0

After

f(y)=\|x^*-z\|^2+2(x^*-z)\cdot v+\|v\|^2=9/2+\|v\|^2\ge9/2

Conditions: y\text{ feasible}

Rule: algebra · Uses: G1, S04, S06

Leaf basis: algebra

The offset x*-z is parallel to normal (1,1), orthogonal to every feasible difference v, so the cross term vanishes. Equality forces v=0, separately proving the unique global minimizer.



S08 · impliesBefore

F(u,v)=u^3,\quad G(u,v)=v,\quad(u,v)=(0,0)

After

\nabla F=0=J_G^T\cdot0,\quad\operatorname{rank}J_G=1;\quad F(t,0)=t^3\text{ has both signs}

Conditions: none

Rule: polynomial · Uses: G1

Leaf basis: polynomial

A regular feasible stationary point can still fail to be an extremum, explicitly showing necessity is not sufficiency.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1 — The main distance example's minimum was independently proved at S07 and is not conflated with this counterexample.
- S07 · premise_audit · G1, S04, S06 — Sufficiency and globality come from this squared decomposition, not the general necessary multiplier theorem.
- S06 · premise_audit · G1, S04, S05 — The numerical value alone does not prove minimality.
- S05 · premise_audit · G1, S01, S04 — The constraint is not omitted after solving for lambda.
- S04 · inverse_equivalence · S03 — The center remains (1,2), not the origin.
- S03 · inverse_equivalence · S02 — A unique multiplier does not imply a unique primal point for general problems.
- S02 · premise_audit · G1, S01, lagrange_regular — The positive-sign convention is fixed, not silently changed to grad f+lambda*grad g=0.
- S01 · premise_audit · G1 — Both m≤n and row/column conventions are checked.





## Error controls and negative controls

Regularity firstCheck feasibility, neighborhood differentiability and full row rank before applying the necessary theorem.

Separate sufficiencyThe global minimum follows from a squared decomposition for every feasible y, not lambda alone.


- Solving multiplier equations guarantees a minimum. → reject — The regular stationary example at S08 is not an extremum.
- Rank deficiency means no extremum exists. → reject — In one dimension g(x)=x^2=0 has only feasible point zero, where f(x)=x attains an extremum; g'(0)=0 only withholds the theorem.
- These equality conditions are the full inequality KKT conditions. → reject — Inequality multiplier signs and complementary slackness are absent.





## Result and limitations

x*=(-1/2,1/2), lambda=-3 and minimum squared distance 9/2; uniqueness and globality are separately proved by orthogonal squared decomposition.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 9dfb066e1160c3636dc41e2ce2e4263a60a1d24ba863f56867789a1f48c7bef4
- original source SHA-256: 9dfb066e1160c3636dc41e2ce2e4263a60a1d24ba863f56867789a1f48c7bef4
- 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-lagrange-multiplier-condition-01.json)