# Linear programming: the best supplied candidate, and why it is not the continuous optimum [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-linear-programming/) 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-programming-01 · production-20261019-adopted-96 ## Goal and scope Constraints 3x+2y≤12, x+2y≤6, −x≤0, −y≤0; objective: maximize L(x,y)=x+y. For the seven supplied candidates P1=(0,0), P2=(4,0), P3=(3,1), P4=(2,2), P5=(0,3), P6=(4,1), P7=(3,2), check feasibility constraint by constraint, compare objective values only among feasible candidates, and find the best value among the candidates and all points attaining it; then use the feasible point Q=(3,3/2) and an inequality certificate to prove that the maximum over the continuous feasible region is 9/2, not the candidate value 4. Works inside the MKO's scope: integer-coefficient constraints ax+by≤c in two variables, an integer-coefficient objective and a complete explicitly supplied finite candidate list (assumption a1). Enumerating candidates yields only 'best among the supplied candidates' (assumption a2). The maximum over the continuous feasible region is proved separately with one feasible witness point and one inequality certificate built from nonnegative weights; this is specific to this problem and proves no general vertex or duality theorem. The canonical MKO and its English edition are not changed. ## Givens and symbols - order_basics - frac_rules - distributive - and_intro_elim - de_morgan_logic - set_builder - numeric_evaluation - G1 — Constraints (form ax+by≤c, integer coefficients): C1: 3x+2y≤12; C2: x+2y≤6; C3: −x≤0; C4: −y≤0. Objective: maximize L(x,y)=x+y. - G2 — The complete supplied candidate list K: P1=(0,0), P2=(4,0), P3=(3,1), P4=(2,2), P5=(0,3), P6=(4,1), P7=(3,2). - G3 — The continuous feasible region F_ℝ={(x,y)∈ℝ² ∣ C1, C2, C3 and C4 all hold}. - C_1,C_2,C_3,C_4 — the four linear constraints - L(x,y)=x+y — the linear objective - K=\{P_1,P_2,P_3,P_4,P_5,P_6,P_7\} — the supplied candidate set - F_K — the set of feasible candidates - F_{\mathbb{R}} — the continuous feasible region - Q=(3,\tfrac{3}{2}) — a feasible witness point outside the candidate list ## Rules and sources - order_basics · prerequisite — Order of the reals: exactly one of uv holds; u0 give uwvw. - frac_rules · prerequisite — Fraction rules (all denominators nonzero): a/c+b/c=(a+b)/c; (a/b)(c/d)=(ac)/(bd); (a/b)/(c/d)=(ad)/(bc) (also needing c≠0); a/b=(ak)/(bk) for k≠0. - distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu. - and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q. - de_morgan_logic · prerequisite — De Morgan's laws for logic: ¬(P∧Q) ⇔ ¬P∨¬Q and ¬(P∨Q) ⇔ ¬P∧¬Q. - set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x). - numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable. - def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable. - def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true. - set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements. - case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility. - finite_counting_basics · prerequisite — Finite counting: for disjoint finite sets A, B, |A∪B|=|A|+|B|; |A×B|=|A|·|B|; there is a bijection between finite sets ⇔ they have the same number of elements. - exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x). - add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w). - add_comm · prerequisite — Commutativity of addition: u+v=v+u. - eq_congruence · prerequisite — Congruence of equality: if u=v, applying the same defined operation f to both sides gives f(u)=f(v). Operating on one side only is not an instance of this rule. - mko_lp · cited — A linear program consists of a linear objective and linear constraints and seeks a minimum or maximum on the feasible domain. A finite candidate grid permits complete checking of its listed points, but unless coverage of the general feasible domain has been proved, its conclusion is only best among the supplied candidates. · mko-linear-programming - mko_opt · cited — For a feasible set S and objective f:S→R, minimization seeks x*∈S with f(x*)≤f(x) for every x∈S; maximization reverses the inequality. Several optimal points may attain the same value. · mko-optimization-problem ## Main derivation S01 · definitionBefore \text{linear program with supplied candidates} After \max L(x,y)=x+y\ \text{s.t.}\ C_1,C_2,C_3,C_4;\ K=\{P_1,P_2,P_3,P_4,P_5,P_6,P_7\} Conditions: none Rule: mko_lp · Uses: G1, G2, G3, mko_lp Leaf basis: mko_lp + def_intro By the MKO, a linear program consists of a linear objective and linear constraints. Two different sets appear here: the supplied candidate set K (seven points) and the continuous feasible region F_ℝ. S02 to S11 work on K only, and their conclusion is called 'best among the supplied candidates'; only S12 to S15 discuss F_ℝ. S02 · equivalentBefore P\in F_K After P\in K\ \land\ C_1(P)\land C_2(P)\land C_3(P)\land C_4(P) Conditions: none Rule: def_unfold · Uses: S01, G1, set_builder Leaf basis: set_builder + def_unfold + and_intro_elim Definition of a feasible candidate: P is feasible exactly when all four constraints hold. This is a conjunction: check constraint by constraint first, then compare objective values only among feasible candidates (MKO, first paragraph). The constraints use '≤', so equality also satisfies them. S03 · equivalentBefore C_1,C_2,C_3,C_4\ \text{at}\ P_1,\ P_2,\ P_3,\ P_4,\ P_5,\ P_6,\ P_7 After \text{table of left-hand sides} Conditions: none Rule: numeric_evaluation · Uses: G1, G2 Leaf basis: numeric_evaluation Substitute every candidate into the left side of every constraint, in three sub-steps: C1, C2, and the sign constraints C3 and C4. S04 · impliesBefore P_1,\ P_2,\ P_3,\ P_4,\ P_5 After C_1\land C_2\land C_3\land C_4\ \text{hold} Conditions: none Rule: and_intro_elim · Uses: S02, S03.1, S03.2, S03.3 Leaf basis: and_intro_elim + order_basics For P1 to P5 the C1 values 0, 12, 11, 10, 6 are all ≤12, the C2 values 0, 4, 5, 6, 6 are all ≤6, and C3, C4 hold. All four constraints hold, so these five points are feasible. P2 makes C1 tight and P4, P5 make C2 tight; equality is still feasible. S05 · impliesBefore P_6=(4,1),\ P_7=(3,2) After P_6,P_7\notin F_K Conditions: none Rule: de_morgan_logic · Uses: S02, S03.1, S03.2 Leaf basis: de_morgan_logic + order_basics Negating a conjunction needs only one failing part: P6 has C1 value 14>12; P7 has C1 value 13>12 (and C2 value 7>6 fails too). So P6 and P7 are infeasible and take no part in comparing objective values. S06 · equivalentBefore F_K=\{P\in K\mid C_1\land C_2\land C_3\land C_4\} After F_K=\{P_1,P_2,P_3,P_4,P_5\} Conditions: none Rule: set_extensionality · Uses: S04, S05, G2 Leaf basis: set_extensionality + case_analysis All seven elements of K have been decided: P1 to P5 are feasible (S04) and P6, P7 are not (S05). So the set of feasible candidates is exactly {P1,P2,P3,P4,P5}. S07 · equivalentBefore L(P_1),\ L(P_2),\ L(P_3),\ L(P_4),\ L(P_5) After 0,\ 4,\ 4,\ 4,\ 3 Conditions: none Rule: numeric_evaluation · Uses: S06, G1 Leaf basis: numeric_evaluation Compute the objective only on feasible candidates: L(0,0)=0, L(4,0)=4, L(3,1)=4, L(2,2)=4, L(0,3)=3. S08 · impliesBefore \max_{P\in F_K}L(P) After 4 Conditions: F_K\neq\varnothing Rule: mko_opt · Uses: S07, mko_opt Leaf basis: mko_opt + order_basics + finite_counting_basics By the definition of maximization, find a feasible P* with L(P)≤L(P*) for every feasible P. The value 4 is attained by P2, and each of 0, 4, 4, 4, 3 is ≤4; so the maximum among the candidates is 4. F_K is a nonempty finite set, so a maximum exists. S09 · equivalentBefore \arg\max_{P\in F_K}L(P) After \{P_2,P_3,P_4\} Conditions: none Rule: mko_opt · Uses: S07, S08, mko_opt Leaf basis: mko_opt + set_builder + numeric_evaluation The feasible candidates attaining the maximum 4 are P2, P3 and P4, a three-way tie; P1 (0) and P5 (3) do not. By the MKO, the argmax keeps all tied points rather than reporting just one. S10 · impliesBefore L(P_6)=5,\ L(P_7)=5 After 5>4\ \text{but}\ P_6,P_7\notin F_K Conditions: none Rule: mko_opt · Uses: S05, S08, G1 Leaf basis: mko_opt + numeric_evaluation P6 and P7 both have objective value 5, larger than 4, but they are infeasible (S05), so they are outside the comparison and do not affect the maximum. Counting them would wrongly report 5 as the optimum, which is one of the mistakes named by the MKO. S11 · impliesBefore \max_{F_K}L=4,\ \arg\max=\{P_2,P_3,P_4\} After \text{best among the supplied candidates only} Conditions: none Rule: mko_lp · Uses: S08, S09, mko_lp Leaf basis: mko_lp By the MKO, without a proof that the candidate list covers the feasible region, the conclusion can only be called 'best among the supplied candidates'. So far no step has considered points of F_ℝ that are not in K. S12 · impliesBefore Q=(3,\tfrac{3}{2}) After Q\in F_{\mathbb{R}},\ L(Q)=\tfrac{9}{2}>4 Conditions: none Rule: numeric_evaluation · Uses: G1, G3, S08 Leaf basis: numeric_evaluation + order_basics + exists_intro Take the point Q=(3,3/2) outside the candidate list: C1: 3·3+2·(3/2)=12≤12; C2: 3+2·(3/2)=6≤6; the coordinates are nonnegative, so C3 and C4 hold. Hence Q∈F_ℝ and L(Q)=3+3/2=9/2>4. Therefore the candidate best value 4 is not the maximum over the continuous feasible region. S13 · impliesBefore (x,y)\in F_{\mathbb{R}} After x+y\le\tfrac{9}{2} Conditions: none Rule: order_basics · Uses: G1, G3 Leaf basis: order_basics + distributive + frac_rules An inequality certificate: combining C1 and C2 with the nonnegative weights 1/4 and 1/4 gives x+y≤9/2 for every feasible point. Two sub-steps: one identity and one addition of inequalities. This is a proof for all points of F_ℝ, not a sample. S14 · impliesBefore Q\in F_{\mathbb{R}},\ L(Q)=\tfrac{9}{2},\ \forall P\in F_{\mathbb{R}}:\ L(P)\le\tfrac{9}{2} After \max_{F_{\mathbb{R}}}L=\tfrac{9}{2} Conditions: none Rule: mko_opt · Uses: S12, S13 Leaf basis: mko_opt + and_intro_elim Both conditions for a maximum hold: 9/2 is attained by the feasible point Q (S12), and every feasible point has value ≤9/2 (S13). So the maximum over the continuous feasible region is 9/2, larger than the candidate best 4. S15 · impliesBefore x+y=\tfrac{9}{2},\ (x,y)\in F_{\mathbb{R}} After (x,y)=(3,\tfrac{3}{2}) Conditions: none Rule: order_basics · Uses: S13.1, S13.2, S14, G1 Leaf basis: order_basics + eq_congruence + numeric_evaluation If x+y=9/2, both inequalities in S13.2 must be equalities: if either were strict, the sum would be strictly below 9/2. So 3x+2y=12 and x+2y=6; subtracting gives 2x=6, x=3, and then y=3/2. Hence the continuous maximum is attained only at Q; Q is not in the candidate list, where the three tied points reach only 4. ## Substeps and lemmas S03.1 · equivalentBefore 3x+2y\ \text{at}\ P_1,\ P_2,\ P_3,\ P_4,\ P_5,\ P_6,\ P_7 After 0,\ 12,\ 11,\ 10,\ 6,\ 14,\ 13 Conditions: none Rule: numeric_evaluation · Uses: G1, G2 Leaf basis: numeric_evaluation + order_basics 3·0+2·0=0, 3·4+2·0=12, 3·3+2·1=11, 3·2+2·2=10, 3·0+2·3=6, 3·4+2·1=14, 3·3+2·2=13. Against the bound 12: the first five are ≤12, while 14 for P6 and 13 for P7 are >12. S03.2 · equivalentBefore x+2y\ \text{at}\ P_1,\ P_2,\ P_3,\ P_4,\ P_5,\ P_6,\ P_7 After 0,\ 4,\ 5,\ 6,\ 6,\ 6,\ 7 Conditions: none Rule: numeric_evaluation · Uses: G1, G2 Leaf basis: numeric_evaluation + order_basics 0+0=0, 4+0=4, 3+2=5, 2+4=6, 0+6=6, 4+2=6, 3+4=7. Against the bound 6: P1 to P6 are all ≤6 (P4, P5 and P6 with equality), while 7 for P7 is >6. S03.3 · equivalentBefore -x\le 0,\ -y\le 0\ \text{at all}\ P_i After \text{true for all seven} Conditions: none Rule: order_basics · Uses: G1, G2 Leaf basis: order_basics All coordinates of the seven candidates are nonnegative integers from 0 to 4; for a nonnegative u, −u≤0. So C3 and C4 hold for every candidate, and feasibility is decided by C1 and C2 alone. S13.1 · equivalentBefore x+y After \tfrac{1}{4}(3x+2y)+\tfrac{1}{4}(x+2y) Conditions: none Rule: distributive · Uses: distributive, frac_rules Leaf basis: distributive + add_assoc + add_comm + frac_rules Expand the right side: (1/4)(3x+2y)+(1/4)(x+2y)=(1/4)(4x+4y)=x+y. This identity holds for all real x and y (N11). S13.2 · impliesBefore 3x+2y\le 12,\ x+2y\le 6 After \tfrac{1}{4}(3x+2y)+\tfrac{1}{4}(x+2y)\le\tfrac{12}{4}+\tfrac{6}{4}=\tfrac{9}{2} Conditions: \tfrac{1}{4}>0 Rule: order_basics · Uses: S13.1, G1, order_basics Leaf basis: order_basics + frac_rules + numeric_evaluation Multiply C1 by the positive number 1/4, keeping the direction: (1/4)(3x+2y)≤3; likewise C2: (1/4)(x+2y)≤3/2. Add the two inequalities (u1≤v1 and u2≤v2 give u1+u2≤v1+u2≤v1+v2) to get a sum ≤9/2; by S13.1, x+y≤9/2. With a negative weight, multiplication would reverse the inequality and the addition would fail. ## Reverse audits - S15 · premise_audit · S13.2, order_basics, eq_congruence — It needs 'a strict inequality plus a non-strict one gives a strict one' and elimination in a 2×2 linear system; uniqueness is not claimed for other objectives. - S14 · premise_audit · S12, S13, mko_opt — The upper-bound certificate and the attaining point are both needed: the witness alone gives only a lower bound, and the certificate alone does not show the bound is attained. - S13.2 · premise_audit · order_basics, S13.1 — It needs positive (or nonnegative) weights; no converse is claimed, that is, C1 and C2 are not recovered from x+y≤9/2. - S13.1 · inverse_equivalence · distributive, frac_rules — Both sides are the same linear expression, so the step holds both ways. - S13 · premise_audit · order_basics, G3 — Only C1, C2 and the nonnegativity of the weights are used; C3 and C4 are not needed for this certificate. - S12 · premise_audit · G3, numeric_evaluation, order_basics — One feasible witness suffices to refute '4 is the maximum on F_ℝ' (N8, N9, N10); this step does not yet prove that 9/2 is the maximum. - S11 · premise_audit · mko_lp, S08 — This step only fixes the scope of the conclusion; S12 shows that the restriction is substantive. - S10 · premise_audit · S05, mko_opt — The definition of maximization quantifies over feasible points only; the objective value of an infeasible point, however large, is irrelevant to the conclusion. - S09 · inverse_equivalence · mko_opt, S07 — The argmax is {P∈F_K ∣ L(P)=4}; checking the five feasible candidates one by one makes this hold both ways. - S08 · premise_audit · mko_opt, S07, order_basics — Two things are needed: 4 is attained by some feasible candidate, and every feasible candidate has value ≤4. The comparison is made within F_K only. - S07 · inverse_equivalence · numeric_evaluation — Exact integer computation. - S06 · inverse_equivalence · set_extensionality, S04, S05 — The element-by-element decision covers all seven points of K, so the two sets have the same elements and are equal by extensionality. - S05 · premise_audit · de_morgan_logic, S03.1 — ¬(A∧B∧C∧D) ⇔ ¬A∨¬B∨¬C∨¬D; one failing constraint is a sufficient witness. - S04 · premise_audit · S02, S03.1, S03.2, S03.3 — The conjunction needs all four constraints checked; no optimality of these feasible points is claimed. - S03.3 · inverse_equivalence · order_basics — u≥0 ⇔ −u≤0 (multiplying by −1 reverses the inequality), which holds both ways. - S03.2 · inverse_equivalence · numeric_evaluation — Integer arithmetic has unique values. - S03.1 · inverse_equivalence · numeric_evaluation — Integer arithmetic has unique values. - S03 · inverse_equivalence · numeric_evaluation — Every value is an exact integer computation and can be recomputed one by one (N1 to N7). - S02 · inverse_equivalence · def_unfold, set_builder, and_intro_elim — Unfolding the set-builder definition holds both ways. - S01 · premise_audit · G1, G2, G3, mko_lp — This step only states the problem and the two sets and derives no new fact. ## Error controls and negative controls An infeasible point cannot be optimalThe first mistake named by the MKO. P6 and P7 have objective value 5, larger than every feasible candidate, but P6 has 3x+2y=14>12 and P7 has 13>12, so they are infeasible (S05, S10). The correct order is to check feasibility constraint by constraint first, and then compare objective values among feasible points only. The best candidate need not attain the LP optimumThe second mistake named by the MKO. The candidate best value 4 covers only the seven supplied points; the feasible point Q=(3,3/2) outside the list gives 9/2 (S12). Claiming a continuous optimum needs an argument covering the whole feasible region, such as the inequality certificate of S13. Keep every tied pointP2, P3 and P4 all have objective value 4. Reporting only one of them suggests a unique best point; by the MKO the argmax keeps every tied index (S09). - P6 has the largest objective value 5, so P6 is optimal → reject — P6 is infeasible: 3·4+2·1=14>12. - The best candidate is unique, namely P2=(4,0) → reject — P3=(3,1) and P4=(2,2) are also feasible with objective value 4, a three-way tie. - The best candidate value is 4, so the maximum of this linear program over the continuous feasible region is 4 → reject — Q=(3,3/2) is feasible and has x+y=9/2>4. - Combining C1 and C2 with weights 1 and −1 gives 2x≤6, that is x≤3, for every feasible point → reject — Multiplying by a negative number reverses the inequality, so the inequalities cannot be added this way; P2=(4,0) is feasible with x=4>3. ## Result and limitations Among the seven supplied candidates, P6 and P7 are infeasible (they violate 3x+2y≤12); among the feasible ones the maximum of x+y is 4, attained in a three-way tie by P2=(4,0), P3=(3,1) and P4=(2,2), which is only the best among the supplied candidates. Over the continuous feasible region, the feasible point Q=(3,3/2) gives 9/2, and the certificate x+y=(1/4)(3x+2y)+(1/4)(x+2y)≤9/2 proves that 9/2 is the maximum, attained only at Q. - The certificate of S13 is specific to this problem; the vertex theorem, standard form and duality theorem for general linear programs belong to the MKO's formal next step and are not proved here. - N11 is a grid check of a degree-one polynomial identity; the other numeric checks are exact single computations. ## Verification and source binding 15 declared checks for this guide; only the listed expressions are covered. - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: 3314594ea08c425708a9014997e20b768f85d871eee2977d20033d7ea5f171e0 - original source SHA-256: 3314594ea08c425708a9014997e20b768f85d871eee2977d20033d7ea5f171e0 - Lean: NOT_RUN · independent AI: NOT_MEASURED [Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-linear-programming-01.json)