Linear programming: the best supplied candidate, and why it is not the continuous optimum

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 u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• 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

\text{linear program with supplied candidates}

\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\}

P\in F_K

P\in K\ \land\ C_1(P)\land C_2(P)\land C_3(P)\land C_4(P)

C_1,C_2,C_3,C_4\ \text{at}\ P_1,\ P_2,\ P_3,\ P_4,\ P_5,\ P_6,\ P_7

\text{table of left-hand sides}

P_1,\ P_2,\ P_3,\ P_4,\ P_5

C_1\land C_2\land C_3\land C_4\ \text{hold}

P_6=(4,1),\ P_7=(3,2)

P_6,P_7\notin F_K

F_K=\{P\in K\mid C_1\land C_2\land C_3\land C_4\}

F_K=\{P_1,P_2,P_3,P_4,P_5\}

L(P_1),\ L(P_2),\ L(P_3),\ L(P_4),\ L(P_5)

0,\ 4,\ 4,\ 4,\ 3

\max_{P\in F_K}L(P)

4

\arg\max_{P\in F_K}L(P)

\{P_2,P_3,P_4\}

L(P_6)=5,\ L(P_7)=5

5>4\ \text{but}\ P_6,P_7\notin F_K

\max_{F_K}L=4,\ \arg\max=\{P_2,P_3,P_4\}

\text{best among the supplied candidates only}

Q=(3,\tfrac{3}{2})

Q\in F_{\mathbb{R}},\ L(Q)=\tfrac{9}{2}>4

(x,y)\in F_{\mathbb{R}}

x+y\le\tfrac{9}{2}

Q\in F_{\mathbb{R}},\ L(Q)=\tfrac{9}{2},\ \forall P\in F_{\mathbb{R}}:\ L(P)\le\tfrac{9}{2}

\max_{F_{\mathbb{R}}}L=\tfrac{9}{2}

x+y=\tfrac{9}{2},\ (x,y)\in F_{\mathbb{R}}

(x,y)=(3,\tfrac{3}{2})

Substeps and lemmas

3x+2y\ \text{at}\ P_1,\ P_2,\ P_3,\ P_4,\ P_5,\ P_6,\ P_7

0,\ 12,\ 11,\ 10,\ 6,\ 14,\ 13

x+2y\ \text{at}\ P_1,\ P_2,\ P_3,\ P_4,\ P_5,\ P_6,\ P_7

0,\ 4,\ 5,\ 6,\ 6,\ 6,\ 7

-x\le 0,\ -y\le 0\ \text{at all}\ P_i

\text{true for all seven}

x+y

\tfrac{1}{4}(3x+2y)+\tfrac{1}{4}(x+2y)

3x+2y\le 12,\ x+2y\le 6

\tfrac{1}{4}(3x+2y)+\tfrac{1}{4}(x+2y)\le\tfrac{12}{4}+\tfrac{6}{4}=\tfrac{9}{2}

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 optimal

The 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 optimum

The 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 point

P2, 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)