Reference · Non-negative rationals

rainbow.math.rational.nnrat.lp-two-var-strong-duality

Non-negative rationalssrc/rainbow/math/rational/nnrat/lp_two_var_strong_duality.clj0 definitions, 2 theorems

Brick 5d-iii of the general LP strong-duality Fourier-Motzkin encoding : a two-variable strong-duality instance whose primal-optimality is proved BY THE FM ENGINE. The LP: maximize x1 + 2*x2 subject to x1 + x2 <= 1, x1,x2 >= 0. Its optimum is 2, attained at (0,1); the dual (single multiplier y = 2 on the binding constraint) has b*y = 2, so the gap is zero. This instance is chosen because its optimality genuinely REQUIRES combining the objective with the constraint -- it cannot be read off by scaling one constraint -- so the Fourier-Motzkin cross + both-sides machinery is doing real work, not decoration. nnrat/lp-two-var-example-primal-optimal proves the primal bound: every feasible (x1,x2) has x1 + 2*x2 <= 2. The proof runs the FM elimination of x1: the additive cross crux (brick 5c core) against the constraint gives (x1+2*x2) + x2 <= 1 + 2*x2 -- x2 on both sides -- which the both-sides conversion (brick 5d-ii, difference witness 1+1~2) turns into x1+2*x2 <= x2 + 1; then x2 <= 1 (x2 <= x1+x2 <= 1) closes it to x1+2*x2 <= 2. First multi-variable LP optimality proved through actual variable elimination. Native proof data, axiom-free.

Depends onmath.rational.nnrat.farkas-additive-crossmath.rational.nnrat.farkas-both-sidesmath.rational.nnrat.add-upper

nnrat/lp-two-var-example-primal-optimal :
  (x1 x2 : ℚ≥0)
  (feasible : x1 + x2 ≤ 1)
  → x1 + (1 + 1) · x2 ≤ 1 + 1

nnrat/lp-two-var-example-strong-duality :
  → proposition/conjunction (0 + 1 ≤ 1) (conjunction)
  where conjunction := proposition/conjunction (0 + (1 + 1) · 1 = 1 + 1) (1 · (1 + 1) = 1 + 1)