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

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

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-optimization-problem-01 · production-20261019-adopted-96



## 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

S01 · definitionBefore

\text{find the best candidate}

After

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

Conditions: none

Rule: mko_opt_def · Uses: G1, G2, G3

Leaf basis: mko_opt_def + def_intro

State the problem as in the MKO: an optimal point must belong to the feasible set S and its objective value must not exceed that of any point of S. The optimal value is a number; argmin is the set of all optimal points and may have more than one element. Apply the MKO definition to the objective f|S. The same formula on C may describe values at infeasible candidates, but those candidates are excluded from the optimization comparison.



S02 · equivalentBefore

C

After

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

Conditions: none

Rule: cartesian_product_def · Uses: G1

Leaf basis: cartesian_product_def + finite_counting_basics

The nine points listed in G1 are exactly all ordered pairs of {0,1,2}×{0,1,2}, 3·3=9, with no repetition or omission. Every later conclusion is about these nine points only.



S03 · equivalentBefore

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

After

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

Conditions: none

Rule: numeric_evaluation · Uses: S02, G2

Leaf basis: numeric_evaluation + order_basics

By the MKO, decide feasibility first. Compute g=x+2y at the nine points in order and compare with 3 to get the feasibility mask; the computation is split into three rows by x in S03.1 to S03.3.



S04 · equivalentBefore

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

After

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

Conditions: none

Rule: set_builder · Uses: S03, G2

Leaf basis: set_builder + set_extensionality

By set-builder notation, S consists exactly of the five points whose mask is true; (0,0), (0,1), (1,0) and (2,0) are infeasible. S is nonempty, so a minimum can exist. In scan order write s_1=(0,2), s_2=(1,1), s_3=(1,2), s_4=(2,1), s_5=(2,2).



S05 · equivalentBefore

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

After

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

Conditions: none

Rule: numeric_evaluation · Uses: S04, G3

Leaf basis: numeric_evaluation

Compute objective values on feasible points only: f(0,2)=2, f(1,1)=2, f(1,2)=3, f(2,1)=3, f(2,2)=4.



S06 · impliesBefore

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

After

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

Conditions: none

Rule: L_scan_invariant · Uses: S04, L_scan_invariant

Leaf basis: nat_induction + case_analysis + order_basics

Scan algorithm: start with m_1=f(s_1) and A_1={s_1} (clearly correct for one point), then update by the three cases of L_scan_invariant. The lemma (proved by cases in S06.1 to S06.3) shows that each update preserves the invariant, so by induction from k=1 to k=5 the invariant always holds. The algorithm stops after processing |S|=5 points.



S07 · impliesBefore

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

After

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

Conditions: none

Rule: def_intro · Uses: S05, S06

Leaf basis: def_intro + numeric_evaluation

Trace: the starting point is s_1=(0,2) with f=2, so m_1=2 and A_1={(0,2)}.



S08 · impliesBefore

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

After

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

Conditions: f(s_2)=m_1

Rule: L_scan_invariant · Uses: S07, S05, L_scan_invariant

Leaf basis: L_scan_invariant

The value 2 of s_2=(1,1) equals the current minimum, which is the tie case (S06.2), so it joins the tie set.



S09 · impliesBefore

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

After

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

Conditions: 3>2,\ 3>2,\ 4>2

Rule: L_scan_invariant · Uses: S08, S05, L_scan_invariant

Leaf basis: L_scan_invariant + order_basics

The remaining three points all fall in the 'larger' case, so m and A do not change; the point-by-point details are in S09.1 to S09.3.



S10 · impliesBefore

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

After

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

Conditions: k=|S|=5

Rule: L_scan_invariant · Uses: S06, S09

Leaf basis: L_scan_invariant + finite_counting_basics

At termination k=5, and the invariant says that m_5 is the minimum of f over s_1 to s_5, that is over all of S, and A_5 is the set of all points attaining it. So the optimal value is m=2 and argmin={(0,2),(1,1)}, with two tied optimal points.



S11 · impliesBefore

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

After

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

Conditions: none

Rule: mko_opt_def · Uses: S05, S10, mko_opt_def

Leaf basis: mko_opt_def + forall_intro + order_basics

Cross-check directly against the MKO definition: 2≤2, 2≤2, 2≤3, 2≤3, 2≤4; these five comparisons cover every point of S, so (0,2) and (1,1) are both minimizers; the other three points, with values 3, 3 and 4, exceed the value 2 of a feasible point, so they are not minimizers.



S12 · impliesBefore

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

After

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

Conditions: (0,0),(2,0)\notin S

Rule: mko_opt_notes · Uses: S03, S04, mko_opt_notes

Leaf basis: mko_opt_notes + set_builder

By the MKO, an infeasible point cannot be optimal even if its value is better. (0,0) has value 0, below 2, but g(0,0)=0<3; (2,0) has value exactly 2, but g(2,0)=2<3. Neither is in S, so neither is in argmin, and the optimal value does not become 0.



S13 · impliesBefore

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

After

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

Conditions: none

Rule: mko_opt_def · Uses: S05, mko_opt_def

Leaf basis: mko_opt_def + order_basics

Maximization reverses the inequality: f(s*)≥f(s) for every s∈S. Comparing one by one: 4≥2, 4≥2, 4≥3, 4≥3, 4≥4, so (2,2) is a maximizer; every other point has a value below 4, so here the maximizer is unique. Uniqueness has to be read off the enumeration: on the minimization side it fails.



S14 · impliesBefore

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

After

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

Conditions: x\ge 0,\ y\ge 0

Rule: order_basics · Uses: G2, G3

Leaf basis: order_basics + distributive

To show that a finite enumeration does not extrapolate: if the candidates are changed to the real nonnegative quadrant, the minimum under the same constraint is 3/2, attained at (0,3/2), which is not in C; the proof is in S14.1 to S14.3. So 'optimal value 2' is a conclusion about the declared nine-point set only.



S15 · impliesBefore

\text{proved facts}

After

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

Conditions: none

Rule: and_intro_elim · Uses: S10, S11, S12, S13, S14

Leaf basis: and_intro_elim

Combine the conclusions: among the nine declared points five are feasible; the minimum 2 is attained by (0,2) and (1,1) in a tie; the infeasible (0,0) and (2,0) are excluded; the maximum 4 is attained only by (2,2); these conclusions do not extend to the real feasible region (where the minimum is 3/2).







## Substeps and lemmas

S03.1 · equivalentBefore

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

After

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

Conditions: none

Rule: numeric_evaluation · Uses: G2

Leaf basis: numeric_evaluation + order_basics

x=0: g(0,0)=0<3, g(0,1)=2<3, g(0,2)=4≥3.



S03.2 · equivalentBefore

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

After

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

Conditions: none

Rule: numeric_evaluation · Uses: G2

Leaf basis: numeric_evaluation + order_basics

x=1: g(1,0)=1<3, g(1,1)=3≥3 (equality is feasible), g(1,2)=5≥3.



S03.3 · equivalentBefore

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

After

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

Conditions: none

Rule: numeric_evaluation · Uses: G2

Leaf basis: numeric_evaluation + order_basics

x=2: g(2,0)=2<3, g(2,1)=4≥3, g(2,2)=6≥3.



S06.1 · impliesBefore

f(s_{k+1})<m_k

After

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

Conditions: f(s_{k+1})<m_k

Rule: order_basics · Uses: order_basics

Leaf basis: order_basics

If f(s_(k+1))<m_k, then for j≤k we have f(s_j)≥m_k>f(s_(k+1)), so f(s_(k+1)) is the minimum over the first k+1 points, and only s_(k+1) attains it (the others are strictly larger).



S06.2 · impliesBefore

f(s_{k+1})=m_k

After

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

Conditions: f(s_{k+1})=m_k

Rule: order_basics · Uses: order_basics

Leaf basis: order_basics + set_operations_def

If equal, the minimum does not change and one more point, s_(k+1), attains it: this is a tie. Adding s_(k+1) rather than discarding it is what lets the algorithm report all optimal points.



S06.3 · impliesBefore

f(s_{k+1})>m_k

After

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

Conditions: f(s_{k+1})>m_k

Rule: order_basics · Uses: order_basics

Leaf basis: order_basics + case_analysis

If larger, the minimum does not change, s_(k+1) does not attain it, and the tie set stays the same. By trichotomy the three cases cover every possibility. S06.1 to S06.3 together prove Lemma L_scan_invariant.



S09.1 · impliesBefore

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

After

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

Conditions: 3>2

Rule: L_scan_invariant · Uses: S08, S05, L_scan_invariant

Leaf basis: L_scan_invariant + order_basics

f(1,2)=3>2, no change.



S09.2 · impliesBefore

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

After

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

Conditions: 3>2

Rule: L_scan_invariant · Uses: S09.1, S05, L_scan_invariant

Leaf basis: L_scan_invariant + order_basics

f(2,1)=3>2, no change.



S09.3 · impliesBefore

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

After

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

Conditions: 4>2

Rule: L_scan_invariant · Uses: S09.2, S05, L_scan_invariant

Leaf basis: L_scan_invariant + order_basics

f(2,2)=4>2, no change. The scan ends.



S14.1 · equivalentBefore

x+y

After

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

Conditions: none

Rule: distributive · Uses: distributive

Leaf basis: distributive + frac_rules

Expanding the right side: x/2+y+x/2=x+y, so this is an identity for all reals (N9).



S14.2 · impliesBefore

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

After

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

Conditions: x\ge 0; x+2y\ge 3

Rule: order_basics · Uses: S14.1, order_basics

Leaf basis: order_basics

From x+2y≥3, (x+2y)/2≥3/2 (multiplying by the positive 1/2); from x≥0, x/2≥0; adding gives x+y≥3/2.



S14.3 · impliesBefore

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

After

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

Conditions: none

Rule: numeric_evaluation · Uses: S14.2

Leaf basis: numeric_evaluation + exists_intro

(0,3/2) satisfies x,y≥0 and 0+2·(3/2)=3≥3, with value 3/2, so the bound is attained and the minimum of the real relaxation is 3/2. 3/2 is not an integer, so (0,3/2) is not in 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 numberOne 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 pointsAnother 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 extrapolateA 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)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-optimization-problem-01.json)