Reference · Non-negative rationals

rainbow.math.rational.nnrat.farkas-row-repackage

Non-negative rationalssrc/rainbow/math/rational/nnrat/farkas_row_repackage.clj0 definitions, 1 theorems

Brick 5a of the general LP strong-duality Fourier-Motzkin encoding : the row-repackaging crux, the one genuinely new proof obligation of the strong-duality payoff. Chaining eliminations (eliminate x1, feed the reduced system into x2's elimination) needs brick 4's reduced row -- at x1 = max-lb1, an affine row with survivor block c*w + d reads a*max-lb1 + (c*w + d) <= b -- to be re-presented as a FRESH brick-4 row in the next variable w: c*w + (a*max-lb1 + d) <= b. The two couplings differ only by reassociating m + (cw + d) into cw + (m + d), where m = a*max-lb1. In nnrat that reassociation is an EQUIVALENCE (~), not propositional equality -- the subtlety the whole LP layer works around -- so the <= is transported across it with nnrat/at-most-respects-equivalence, the ~ itself supplied by nnrat/add-swap-right (p + (q + r) ~ q + (p + r)). nnrat/farkas-row-repackage-iff states the equivalence of the two coupling forms, both directions, for all operands. It is deliberately the pure per-row content (no row types, no list) -- the reusable heart that brick 5c maps over a row list to chain the two-variable elimination. Native proof data, axiom-free.

Depends onmath.rational.nnrat.add-monotonemath.rational.nnrat.additive-reassociation

nnrat/farkas-row-repackage-iff :
  (a m c w d b : ℚ≥0)
  → proposition/conjunction (a · m + (c · w + d) ≤ b → c · w + (a · m + d) ≤ b) (c · w + (a · m + d) ≤ b → a · m + (c · w + d) ≤ b)