# The weak-duality chain and a zero-gap optimality certificate

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

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



## Goal and scope

Construct the full dual, check feasibility of x=(1,3), y=(1,1), and certify both optimal by zero gap.

Fixed maximize/≤/nonnegative convention; weak duality and supplied points only, not general strong duality from a finite grid.





## Givens and symbols


- algebra
- lp_form


- G1 — A=[[1,1],[2,1]], b=(4,5), c=(3,2); primal max c^T*x with A*x≤b,x≥0; x=(1,3), y=(1,1).


- g(x,y) — candidate-dependent gap
- u,v — arbitrary feasible comparison points





## Rules and sources


- mko_definition · cited — Qualify the exact rational m-by-n matrix A and matching b,c. The dual variable has m components and A^T*y≥c has n constraints. For a feasible primal point x and dual point y verify c^T*x≤y^T*A*x≤b^T*y. If both are feasible and the objective values agree, weak duality certifies both points optimal. Equality without both feasibility checks is insufficient. A finite grid does not prove general strong duality or settle infeasible/unbounded cases. General finite-dimensional LP strong duality remains a separately stated theorem, not the result of these finite candidate checks. · mko-linear-program-duality
- 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 x,c\in\mathbb R^2,\quad y,b\in\mathbb R^2

After

\min b^Ty\quad\text{s.t. }A^Ty\ge c,\ y\ge0

Conditions: none

Rule: lp_form · Uses: G1

Leaf basis: lp_form

Two primal constraints give two dual variables, and two primal coordinates give two dual inequalities.



S02 · impliesBefore

x=(1,3)

After

x\ge0,\quad Ax=(4,5)=b

Conditions: none

Rule: algebra · Uses: G1

Leaf basis: algebra

Check primal feasibility row by row.



S03 · equivalentBefore

A^Ty=(y_1+2y_2,y_1+y_2)

After

y_1+2y_2\ge3,\quad y_1+y_2\ge2,\quad y_1,y_2\ge0

Conditions: none

Rule: algebra · Uses: G1, S01

Leaf basis: algebra

Expand both dual constraints, retaining the fixed sign direction.



S04 · impliesBefore

y=(1,1)

After

y\ge0,\quad A^Ty=(3,2)=c

Conditions: none

Rule: algebra · Uses: G1, S03

Leaf basis: algebra

Check dual feasibility column by column; every slack is zero.



S05 · impliesBefore

u\ge0,\ Au\le b,\quad v\ge0,\ A^Tv\ge c

After

c^Tu\le(A^Tv)^Tu=v^TAu\le v^Tb

Conditions: u,v\text{ primal/dual feasible}

Rule: algebra · Uses: S01

Leaf basis: algebra

The first inequality uses u≥0 and the second v≥0; finite matrix associativity gives the middle equality.



S06 · impliesBefore

c^Tx=3+6,\quad b^Ty=4+5

After

c^Tx=b^Ty=9

Conditions: none

Rule: algebra · Uses: G1, S02, S04

Leaf basis: algebra

Compute both objective values independently and exactly.



S07 · equivalentBefore

g(x,y)=b^Ty-c^Tx

After

g=y^T(b-Ax)+x^T(A^Ty-c)=0

Conditions: none

Rule: algebra · Uses: S02, S04, S06

Leaf basis: algebra

Decompose the gap into two nonnegative slack products; A is fixed problem data and x,y are candidate points.



S08 · impliesBefore

c^Tu\le b^Ty=9=c^Tx\quad\forall u\text{ primal feasible}

After

x\text{ maximizes primal};\quad y\text{ minimizes dual}

Conditions: none

Rule: algebra · Uses: S05, S06

Leaf basis: algebra

For every dual-feasible v, b^T*v≥c^T*x=9 as well, so each candidate attains its own best bound.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · S05, S06 — No general strong-duality existence theorem is needed because equal-valued feasible points were supplied.
- S07 · inverse_equivalence · S02, S04, S06 — The gap depends on x,y, without an ambiguous D(A,b,c) conflating candidates and optimal values.
- S06 · premise_audit · G1, S02, S04 — Equality is a certificate only with the established feasibility checks.
- S05 · premise_audit · S01 — This is a universal weak bound for arbitrary feasible u,v, enabling the later optimality argument.
- S04 · premise_audit · G1, S03 — Primal and dual feasibility have separate evidence.
- S03 · inverse_equivalence · G1, S01 — Changing the primal convention requires reconstructing the dual, not changing one sign.
- S02 · premise_audit · G1 — Objective equality cannot replace this qualification.
- S01 · premise_audit · G1 — Check dimensions and transpose direction before treating y as a dual candidate.





## Error controls and negative controls

Both feasibility gatesFirst check x≥0,A*x≤b,y≥0,A^T*y≥c.

Weak bound before zero gapA bound against every feasible comparison point promotes equality to optimality.


- Equal objectives certify optimality even for infeasible points. → reject — The weak bound requires feasibility on both sides; infeasible points do not qualify.
- A finite-grid equality proves general strong duality. → reject — It certifies these feasible points, not existence for every LP.
- The candidate gap depends only on A,b,c. → reject — The expression b^T*y-c^T*x also depends on candidate x,y.





## Result and limitations

x=(1,3) is primal-optimal and y=(1,1) dual-optimal with common value 9, certified by weak duality and zero gap.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 4dbbe01008153ab71828d6d5e0589260df9825bedd57436dfebb4de98ad56e3a
- original source SHA-256: 4dbbe01008153ab71828d6d5e0589260df9825bedd57436dfebb4de98ad56e3a
- 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-duality-01.json)