Reference · Non-negative rationals

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

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

Brick 5c full of the general LP strong-duality Fourier-Motzkin encoding : the affine cross-elimination crux WITH COEFFICIENTS -- the coefficient wrapper around the additive core. Eliminating v bounded below by a coefficient-bearing affine row and above by another: from w_lo <= a_lo*v + s_lo (lower) and a_hi*v + s_hi <= b_hi (upper), the survivor condition (v eliminated) is w_lo*a_hi + s_hi*a_lo <= b_hi*a_lo + s_lo*a_hi -- the subtraction-free cross condition obtained by cross-multiplying the two rows by each other's coefficient. Necessary (certificate) direction; positivity-free. The proof REUSES the additive core (nnrat/farkas-additive-cross-necessary): scale the lower row on the right by a_hi and the upper by a_lo (multiply-right-monotone), distribute (multiply-distributes-add-right) so each becomes an additive row whose variable term is a triple product, align the two triple products D1 = (a_lo*v)*a_hi ~ (a_hi*v)*a_lo = D2 (multiply-swap-right + multiply-commutative through multiply-respects-equivalence), then hand the two additive rows to the core. This is the last new proof obligation of brick 5c; 5d lifts it to row lists and wires the objective. Native proof data, axiom-free.

Depends onmath.rational.nnrat.farkas-additive-crossmath.rational.nnrat.multiply-right-monotonemath.rational.nnrat.distribute-rightmath.rational.nnrat.multiply-commutemath.rational.nnrat.product-reassociation

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