Reference · Non-negative rationals

rainbow.math.rational.nnrat.farkas-additive-cross

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

Brick 5c core of the general LP strong-duality Fourier-Motzkin encoding : the additive cross-elimination crux -- the necessary (certificate) direction, coefficient-1 case. This is the heart of the affine cross-product the payoff needs. Eliminating a variable v that is bounded below by one affine row and above by another, the FM condition on the survivors is that the lower's slack plus the upper's block does not exceed the upper's bound plus the lower's block. In the coefficient-1 case: from w <= v + s_lo (lower) and v + s_hi <= b (upper), the surviving condition is w + s_hi <= b + s_lo -- the additive cross condition, with v eliminated. This is the NECESSARY direction (any feasible v yields the cross condition); its contrapositive is the infeasibility certificate that becomes the dual once the objective bound exceeds the optimum. Proof: add s_hi to the lower row and s_lo to the upper row, reassociate the middle term (v + s_lo) + s_hi ~ (v + s_hi) + s_lo up to nnrat equivalence, and chain by transitivity. Positivity-free (no coefficients yet). The coefficient wrapper -- scale each row by the other's coefficient (multiply-right-monotone), distribute (multiply-distributes-add-right), and align the products (multiply-swap-right) down to this additive core -- is the follow-on brick. Native proof data, axiom-free.

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

nnrat/farkas-additive-cross-necessary :
  (w s-lo s-hi b v : ℚ≥0)
  (lower : w ≤ v + s-lo)
  (upper : v + s-hi ≤ b)
  → w + s-hi ≤ b + s-lo