Reference · Non-negative rationals

rainbow.math.rational.nnrat.farkas-eliminate-base

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

The over-variable recursion's base case: a fully-reduced constraint is a constant comparison. After all variables are eliminated, a both-sides constraint has empty coefficient vectors: eval(nil) + c_L <= eval(nil) + c_R. Since nnrat/linear-form evaluates the empty vector to zero (definitionally, its List.rec nil case), this is 0 + c_L <= 0 + c_R, which nnrat/farkas-eliminate-base reduces to c_L <= c_R -- the condition on the constants alone (the objective value against the accumulated dual bound). This is Feasible 0 in the eliminate-all induction: the base the recursion bottoms out at. Proof: the empty linear form is zero by definition and 0 + x ~ x (add-zero-left), transported by at-most-respects. Native proof data, axiom-free.

Depends onmath.rational.nnrat.farkas-linear-formmath.rational.nnrat.identities

nnrat/farkas-eliminate-base :
  (c-l c-r : ℚ≥0)
  (h : nnrat/linear-form [] + c-l ≤ nnrat/linear-form [] + c-r)
  → c-l ≤ c-r