Reference · Non-negative rationals

rainbow.math.rational.nnrat.farkas-elim-scaled-coupled

Non-negative rationalssrc/rainbow/math/rational/nnrat/farkas_elim_scaled_coupled.clj2 definitions, 3 theorems

Brick 1 of the general LP strong-duality Fourier-Motzkin encoding : elimination of an nnrat variable v that appears with a COEFFICIENT in its coupling to a survivor. Besides constant lower and non-empty upper families for v, the system contains a*v <= w (the surviving variable w carries coefficient a on the eliminated v -- the shape a real constraint row A_ik*x_k <= ... produces, which the coefficient-1 coupled primitive nnrat/farkas-elim-coupled-solvable-iff cannot express). Eliminating v preserves the list-sized reduced condition and transfers a*max-lb(lowers) <= w onto the surviving variable. The proof mirrors nnrat_farkas_elim_coupled.clj exactly; the only new content is the projection's transferred bound: max-lb <= value gives a*max-lb <= a*value by nnrat/multiply-monotone, and a*value <= w closes it by transitivity. No positivity of a is needed for either direction (multiply-monotone holds for every factor). Native proof data, axiom-free.

Depends onmath.rational.nnrat.farkas-elim-coupledmath.rational.nnrat.multiply-monotone

nnrat/farkas-elim-scaled-coupled-reduced :
  (x₁ : List ℚ≥0) (x₂ : ℚ≥0) (x₃ : List ℚ≥0) (x₄ x₅ : ℚ≥0)
  → Prop

nnrat/farkas-elim-scaled-coupled-solvable :
  (x₁ : List ℚ≥0) (x₂ : ℚ≥0) (x₃ : List ℚ≥0) (x₄ x₅ : ℚ≥0)
  → Prop

nnrat/farkas-elim-scaled-coupled-extends :
  (lowers : List ℚ≥0) (u0 : ℚ≥0) (urest : List ℚ≥0) (a w : ℚ≥0)
  (reduced-feasible : nnrat/farkas-elim-scaled-coupled-reduced lowers u0 urest a w)
  → nnrat/farkas-elim-scaled-coupled-solvable lowers u0 urest a w

nnrat/farkas-elim-scaled-coupled-projects :
  (lowers : List ℚ≥0) (u0 : ℚ≥0) (urest : List ℚ≥0) (a w : ℚ≥0)
  (solution : nnrat/farkas-elim-scaled-coupled-solvable lowers u0 urest a w)
  → nnrat/farkas-elim-scaled-coupled-reduced lowers u0 urest a w

nnrat/farkas-elim-scaled-coupled-solvable-iff :
  (lowers : List ℚ≥0) (u0 : ℚ≥0) (urest : List ℚ≥0) (a w : ℚ≥0)
  → proposition/conjunction (reduced → solvable) (solvable → reduced)
  where reduced := nnrat/farkas-elim-scaled-coupled-reduced lowers u0 urest a w
  where solvable := nnrat/farkas-elim-scaled-coupled-solvable lowers u0 urest a w