Optimization problem: feasibility first, then objective values, over nine integer candidates

Goal and scope

The candidate set C={0,1,2}² has nine points, the constraint is x+2y≥3 and the objective is f(x,y)=x+y. Minimize with a scan algorithm that first decides feasibility and then compares values one by one, and prove the result with an invariant: optimal value m=2, argmin={(0,2),(1,1)} (a tie of two); explain why (0,0) and (2,0) are excluded although their objective values do not exceed 2; find the maximum; and show that under the same constraint over the real nonnegative quadrant, the minimum is 3/2, attained at (0,3/2), which is not in the declared finite candidate set.

Conclusions cover only the declared finite candidate set C and its feasible subset (MKO assumptions a1 and a2). The real relaxation in S14 serves only to show that a finite enumeration does not extrapolate; no linear programming theory, duality or computational complexity is developed. The canonical MKO and its English edition are not changed.

Givens and symbols

• set_builder
• order_basics
• case_analysis
• nat_induction
• forall_intro

• G1 — Candidate set C={(0,0),(0,1),(0,2),(1,0),(1,1),(1,2),(2,0),(2,1),(2,2)}, listed completely in this order (MKO assumption a1).
• G2 — Constraint: x+2y≥3. Feasible set S={(x,y)∈C ∣ x+2y≥3}.
• G3 — Define the objective formula on the candidate domain C: f:C→ℝ, f(x,y)=x+y. Optimization uses its restriction f|S:S→ℝ to the feasible domain. First minimize; S13 also maximizes.

• C — the nine declared candidates
• g(x,y)=x+2y — left side of the constraint
• S — feasible set {(x,y)∈C ∣ x+2y≥3}
• f(x,y)=x+y — objective function
• m,\ \operatorname{argmin} — optimal value and the set of all optimal points
• s_1,s_2,s_3,s_4,s_5 — scan order of the feasible points
• m_k,\ A_k — current minimum and tie set after scanning k feasible points

Rules and sources

• set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x).
• 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.
• 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.
• nat_induction · prerequisite — Principle of induction: for a family P(n) starting at n₀, if P(n₀) holds and P(n)⇒P(n+1) for every n≥n₀, then P(n) holds for every n≥n₀.
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• 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.
• cartesian_product_def · prerequisite — Cartesian product: A×B is the set of ordered pairs (a,b) with a∈A and b∈B; (a,b)=(c,d) ⇔ a=c and b=d.
• 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.
• set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• set_operations_def · prerequisite — Set operations: x∈A∪B ⇔ x∈A or x∈B; x∈A∩B ⇔ x∈A and x∈B; x∈A∖B ⇔ x∈A and x∉B; in a universe U, Aᶜ=U∖A.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• 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.
• exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_opt_def · 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
• mko_opt_notes · cited — Decide feasibility first, then compare objective values; an infeasible point cannot be optimal even if its value is better. The optimal value is a number, and argmin or argmax is the set of all feasible points attaining it, possibly with ties. · mko-optimization-problem
• L_scan_invariant · lemma — Let m_k be the minimum of f over s_1 to s_k and A_k the set of those points attaining m_k. When processing s_(k+1): if f(s_(k+1))<m_k set m_(k+1)=f(s_(k+1)) and A_(k+1)={s_(k+1)}; if equal set m_(k+1)=m_k and A_(k+1)=A_k∪{s_(k+1)}; if larger keep both. Then m_(k+1) and A_(k+1) have the same property for s_1 to s_(k+1).

Main derivation

\text{find the best candidate}

\min_{s\in S}f(s),\ \ \operatorname{argmin}=\{s^*\in S\mid \forall s\in S:\ f(s^*)\le f(s)\}

C

|C|=9,\ C=\{0,1,2\}\times\{0,1,2\}

g(x,y)=x+2y\ \text{on }C

\text{mask: }0,2,4,1,3,5,2,4,6\ \Rightarrow\ \text{F,F,T,F,T,T,F,T,T}

S=\{(x,y)\in C\mid x+2y\ge 3\}

S=\{(0,2),(1,1),(1,2),(2,1),(2,2)\},\ |S|=5

f(s_1),f(s_2),f(s_3),f(s_4),f(s_5)

2,\ 2,\ 3,\ 3,\ 4

m_1=f(s_1),\ A_1=\{s_1\}

m_k=\min_{1\le j\le k}f(s_j),\ A_k=\{s_j\mid 1\le j\le k,\ f(s_j)=m_k\}\ \text{for }k=1,2,3,4,5

k=1:\ s_1=(0,2)

m_1=2,\ A_1=\{(0,2)\}

k=2:\ f(1,1)=2=m_1

m_2=2,\ A_2=\{(0,2),(1,1)\}

k=3,4,5:\ f=3,3,4

m_5=2,\ A_5=\{(0,2),(1,1)\}

m_5=2,\ A_5=\{(0,2),(1,1)\}

m=\min_{s\in S}f(s)=2,\ \operatorname{argmin}=\{(0,2),(1,1)\}

\forall s\in S:\ f(0,2)\le f(s)\ \land\ f(1,1)\le f(s)

(0,2),(1,1)\ \text{satisfy the MKO definition of minimizer}

f(0,0)=0<2,\ f(2,0)=2=m

(0,0),(2,0)\notin\operatorname{argmin}

\max_{s\in S}f(s)

\max=4,\ \operatorname{argmax}=\{(2,2)\}

\min\{x+y\mid x,y\in\mathbb{R},\ x,y\ge 0,\ x+2y\ge 3\}

=\tfrac{3}{2}\ \text{at }(0,\tfrac{3}{2})\notin C

\text{proved facts}

m=2,\ \operatorname{argmin}=\{(0,2),(1,1)\},\ \max=4,\ \operatorname{argmax}=\{(2,2)\}

Substeps and lemmas

(0,0),(0,1),(0,2)

g=0,2,4;\ \text{feasible only }(0,2)

(1,0),(1,1),(1,2)

g=1,3,5;\ \text{feasible }(1,1),(1,2)

(2,0),(2,1),(2,2)

g=2,4,6;\ \text{feasible }(2,1),(2,2)

f(s_{k+1})<m_k

m_{k+1}=f(s_{k+1}),\ A_{k+1}=\{s_{k+1}\}

f(s_{k+1})=m_k

m_{k+1}=m_k,\ A_{k+1}=A_k\cup\{s_{k+1}\}

f(s_{k+1})>m_k

m_{k+1}=m_k,\ A_{k+1}=A_k

k=3:\ f(1,2)=3

3>2:\ m_3=2,\ A_3=A_2

k=4:\ f(2,1)=3

3>2:\ m_4=2,\ A_4=A_3

k=5:\ f(2,2)=4

4>2:\ m_5=2,\ A_5=A_4

x+y

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

\tfrac{1}{2}(x+2y)+\tfrac{1}{2}x,\ x+2y\ge 3,\ x\ge 0

x+y\ge\tfrac{3}{2}

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

x+2y=3,\ x+y=\tfrac{3}{2},\ (0,\tfrac{3}{2})\notin C

Reverse audits

• S15 · sufficient_goal_reduction · S10, S11, S12, S13, S14, and_intro_elim — Goal G: the determinations in the goal. Sufficient condition H: S10 to S14, each already proved (H⇒G by conjunction introduction). H is derived forwards from the givens; G is never used as a premise.
• S14.3 · premise_audit · S14.2, numeric_evaluation — A lower bound plus a point attaining it gives the minimum; uniqueness of that point is not claimed.
• S14.2 · premise_audit · order_basics, S14.1 — It needs x≥0; without it the bound fails (for example x=−1, y=2 gives x+y=1).
• S14.1 · inverse_equivalence · distributive, frac_rules — An identity; the two expressions agree at every point.
• S14 · premise_audit · order_basics — This is a different problem (a different feasible set), used only for contrast; it does not change the conclusion of S10.
• S13 · premise_audit · S05, mko_opt_def, order_basics — The same complete enumeration as S11, in the opposite direction.
• S12 · premise_audit · S03, S04, mko_opt_notes — It needs only that these two points are infeasible; the definition of argmin requires membership in S first.
• S11 · premise_audit · S05, mko_opt_def, forall_intro — The universal statement 'for every s∈S' is proved by checking each element, because S is a completely listed finite set; this does not extend to points outside S.
• S10 · premise_audit · S06, S09, finite_counting_basics — It needs the scan to cover every point of S; S04 lists all five points, so k=5 means all of S.
• S09.3 · premise_audit · L_scan_invariant — The larger case; k=5=|S|, so the algorithm terminates.
• S09.2 · premise_audit · L_scan_invariant — The larger case.
• S09.1 · premise_audit · L_scan_invariant — The larger case.
• S09 · premise_audit · L_scan_invariant, S08 — The 'larger' case of the lemma, three times; each comparison is an exact integer comparison.
• S08 · premise_audit · L_scan_invariant, S07 — By the equality case of the lemma; an update rule that acts only on strictly smaller values without recording ties would miss (1,1).
• S07 · premise_audit · S05, def_intro — Initialization looks at one point, and the invariant clearly holds.
• S06.3 · premise_audit · order_basics, case_analysis — Trichotomy guarantees exactly one of the three cases, so the case analysis is complete.
• S06.2 · premise_audit · order_basics, set_operations_def — It uses that an equal value is neither below nor above the minimum; discarding the tied point here would give only part of argmin.
• S06.1 · premise_audit · order_basics — It uses transitivity of the order; the old tie set is replaced entirely, since each of its points is strictly larger.
• S06 · premise_audit · L_scan_invariant, nat_induction, finite_counting_basics — It needs a correct start, preservation at each step and finiteness of S (termination); all three are available.
• S05 · inverse_equivalence · numeric_evaluation — Exact integer computation, the same both ways.
• S04 · inverse_equivalence · set_builder, S03 — A point belongs to S exactly when it is in C and satisfies the constraint; all nine points were checked, so both directions hold.
• S03.3 · inverse_equivalence · numeric_evaluation — Exact integer computation, the same both ways.
• S03.2 · inverse_equivalence · numeric_evaluation — Exact integer computation; the constraint uses ≥, so the point with g=3 is feasible.
• S03.1 · inverse_equivalence · numeric_evaluation — Exact integer computation, the same both ways.
• S03 · inverse_equivalence · numeric_evaluation, order_basics — Each value can be recomputed independently; comparison with 3 is an integer comparison with a definite answer.
• S02 · inverse_equivalence · cartesian_product_def, finite_counting_basics, set_extensionality — Both sides have the same elements (matched one by one), so the set equality holds both ways.
• S01 · premise_audit · G1, G2, G3, mko_opt_def — This step only states definitions and derives no new fact; S has not yet been computed.

Error controls and negative controls

Ignoring the constraint and picking the smallest number

One misconception named by the MKO: the smallest value of f among the nine points is f(0,0)=0, but (0,0) is infeasible. The feasibility mask must be computed first (S03), and comparisons made on S only (from S05 on).

With ties, report all optimal points

Another misconception named by the MKO is reporting one tied solution and calling it unique. (0,2) and (1,1) both attain 2; in the equality case the scan algorithm must add the point to the set (S06.2), or it obtains only part of argmin. On the maximization side the optimum happens to be unique, but that is a result of the enumeration, not a general rule.

A finite enumeration does not extrapolate

A complete enumeration proves optimality within the declared finite list. S14 shows that under the same constraint over the reals the minimum is 3/2, smaller than 2; unlisted candidates or continuous feasible regions need a separate argument.

• The minimum is 0, attained at (0,0) → reject — g(0,0)=0<3, so (0,0) is infeasible (S12).
• The unique minimizer is (0,2) → reject — (1,1) is also feasible with f(1,1)=2, tying with (0,2) (S08, S11).
• (2,0) has value 2, so it also belongs to argmin → reject — g(2,0)=2<3, so it is infeasible and cannot belong to argmin (S12).
• Since the enumeration gives minimum 2, the minimum over all real points with x,y≥0 and x+2y≥3 is also 2 → reject — (0,3/2) is feasible with value 3/2<2 (S14).

Result and limitations

On C={0,1,2}², the constraint x+2y≥3 leaves five feasible points; the objective f=x+y has optimal value m=2 with argmin={(0,2),(1,1)}, a tie of two points, proved both by the scan algorithm's invariant and by direct enumeration. (0,0) (value 0) and (2,0) (value 2) are infeasible and excluded. The maximum 4 is attained only at (2,2). Over the real nonnegative quadrant the minimum would be 3/2 (at (0,3/2)), showing that the conclusion of a finite enumeration does not extrapolate.

• N10 is a finite check over all nine points of C; since C is exactly these points it covers the whole declared candidate set, and it says nothing about points outside C.
• Linear programming, feasible polyhedra, duality and optimality certificates belong to the MKO's formal next step and are outside this guide.

Verification and source binding

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 1bd5968b95ef2ca22235bb2a1c2091b089f80b65a2c7d48bcc15eaf7b1e649e2
• original source SHA-256: 1bd5968b95ef2ca22235bb2a1c2091b089f80b65a2c7d48bcc15eaf7b1e649e2
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)