# The two-way point correspondence for slack variables

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-linear-program-standard-form/)

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-linear-program-standard-form-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Convert a fixed maximize/≤/nonnegative LP to equality slack form and verify both feasible-point directions and objective.

Representation conversion only, not universal feasibility, boundedness or existence of optima.





## Givens and symbols


- algebra
- lp_form


- G1 — A=[[1,1],[2,1]], b=(4,5), c=(3,2); maximize 3*x_1+2*x_2 subject to A*x≤b,x≥0.
- G2 — Candidate x=(1,2).


- s — nonnegative slack
- z^+,z^- — nonnegative split of a free variable





## Rules and sources


- mko_definition · cited — A is an exact rational m-by-n matrix with matching b,c and decision vector x. Qualify dimensions and the chosen sign convention first. Nonnegative slack s=b−A*x converts A*x≤b to A*x+s=b, preserving feasibility and c^T*x in both directions between original and slack points. A free variable splits as x_plus−x_minus with both parts nonnegative; negate a ≥ constraint, replace equality by opposite ≤ rows, and negate a minimization objective. These conversions do not prove feasibility, boundedness or an optimal solution, and another standard-form convention is not silently substituted. · mko-linear-program-standard-form
- algebra · prerequisite — Use real-field identities; division requires a nonzero denominator and multiplication by a positive number preserves inequalities.
- lp_form · prerequisite — Fix the primal as maximize c^T*x subject to A*x≤b,x≥0; its slack equality form is A*x+s=b,x,s≥0 with s=b-A*x; the dual minimizes b^T*y subject to A^T*y≥c,y≥0.





## Main derivation

S01 · definitionBefore

A\in\mathbb Q^{2\times2},\quad b,c,x\in\mathbb R^2

After

\max c^Tx\quad\text{s.t. }Ax\le b,\ x\ge0

Conditions: none

Rule: lp_form · Uses: G1

Leaf basis: lp_form

Align two constraints, two decision coordinates and the objective with one convention.



S02 · impliesBefore

Ax=\begin{pmatrix}1&1\\2&1\end{pmatrix}\binom12

After

Ax=(3,4)\le(4,5),\quad x\ge0

Conditions: none

Rule: algebra · Uses: G1, G2

Leaf basis: algebra

Multiply each row and check nonnegativity to qualify the candidate as primal feasible.



S03 · equivalentBefore

s=b-Ax

After

s=(1,1)\ge0,\quad Ax+s=b

Conditions: none

Rule: algebra · Uses: G1, G2, S02

Leaf basis: algebra

Slack is each row's unused capacity and is unique for a fixed x.



S04 · impliesBefore

x\ge0,\ Ax\le b

After

(x,s)=(x,b-Ax)\ge0,\quad Ax+s=b

Conditions: none

Rule: algebra · Uses: G1

Leaf basis: algebra

For an arbitrary original feasible point, nonnegative slack gives an equality-form feasible point.



S05 · impliesBefore

x,s\ge0,\quad Ax+s=b

After

Ax=b-s\le b,\quad s=b-Ax

Conditions: none

Rule: algebra · Uses: G1, S04

Leaf basis: algebra

Projection back to x is feasible and recovers the same unique slack, giving a bijective correspondence of feasible points.



S06 · equivalentBefore

(c,0)^T(x,s)=c^Tx

After

(3,2,0,0)\cdot(1,2,1,1)=7

Conditions: none

Rule: algebra · Uses: G1, G2, S03

Leaf basis: algebra

New slack variables have zero objective coefficients, preserving the value at every corresponding point.



S07 · impliesBefore

z\in\mathbb R\text{ free}

After

z=z^+-z^-,\quad z^+,z^-\ge0

Conditions: none

Rule: algebra · Uses: G1

Leaf basis: algebra

Positive/negative splitting represents a free variable with nonnegative coordinates; -2=0-2=1-3 shows nonuniqueness.



S08 · equivalentBefore

a^Tx\ge d;\quad a^Tx=d;\quad\min c^Tx

After

-a^Tx\le-d;\quad a^Tx\le d,\ -a^Tx\le-d;\quad\max(-c)^Tx

Conditions: none

Rule: algebra · Uses: G1, S04, S05

Leaf basis: algebra

List the separate conversions for ≥, equality and minimization; the first two preserve feasible points, while the last reverses the objective sign and optimization direction.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · inverse_equivalence · G1, S04, S05 — Representation changes do not supply certificates of feasibility, boundedness or attained optima.
- S07 · premise_audit · G1 — Do not confuse nonunique free-variable splitting with unique slack for a fixed x.
- S06 · inverse_equivalence · G1, G2, S03 — Adding slack to the objective would change the problem.
- S05 · premise_audit · G1, S04 — Two-way correspondence does not assert that either feasible set is nonempty.
- S04 · premise_audit · G1 — This quantifies arbitrary x, not only the candidate (1,2).
- S03 · inverse_equivalence · G1, G2, S02 — The slack sign is b-A*x, not its negative.
- S02 · premise_audit · G1, G2 — An objective value alone does not check feasibility.
- S01 · premise_audit · G1 — A different minimize/≥ convention is not silently substituted.





## Error controls and negative controls

Sign conventionKeep maximize, ≤ and nonnegative variables fixed.

Two-way point mapSpecify forward slack and reverse projection, and check the objective separately.


- s=A*x-b is slack for this ≤ convention. → reject — Nonnegative slack is b-A*x.
- Conversion proves every LP feasible. → reject — It preserves a feasible set without proving it nonempty.
- Both a free split and slack are unique. → reject — -2=0-2=1-3 makes the free split nonunique.





## Result and limitations

Slack form preserves feasible points and objectives in both directions; the candidate has slack (1,1) and value 7, while a free split may be nonunique.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 62dd1386a20c65128c0e6a272ab6a528814d264fa4a1b559339f03e3bf70feff
- original source SHA-256: 62dd1386a20c65128c0e6a272ab6a528814d264fa4a1b559339f03e3bf70feff
- 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-linear-program-standard-form-01.json)