Reference · Non-negative rationals

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

Non-negative rationalssrc/rainbow/math/rational/nnrat/farkas_elim_scaled_coupled_lower.clj3 definitions, 3 theorems

Brick 2 of the general LP strong-duality Fourier-Motzkin encoding : elimination of an nnrat variable v whose coupling to a survivor is a scaled LOWER bound. Where brick 1 (nnrat_farkas_elim_scaled_coupled.clj) handled an upper coupling a*v <= w, this handles the lower coupling w <= a*v -- the shape a `>=` row (objective-boundary c.x >= t) produces once c.x is isolated. v is bounded below by a constant lower family and above by a non-empty upper family; eliminating v (witness the LARGEST feasible value, min-ub of the uppers) preserves the reduced condition and transfers w <= a*min-ub(uppers) onto the survivor. Symmetric to brick 1 with min-ub in place of max-lb. The projection needs ge-all lowers value with value <= min-ub to give ge-all lowers min-ub; that monotonicity of ge-all is the dual of the list module's le-all-antitone and was missing, so nnrat/ge-all-monotone is proved here as the brick's supporting lemma (a plain List.rec induction over the lowers). Native proof data, axiom-free.

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

nnrat/ge-all-monotone :
  (lowers : List ℚ≥0) (value target : ℚ≥0)
  (ordered : value ≤ target)
  (base-proof : nnrat/ge-all lowers value)
  → nnrat/ge-all lowers target

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

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

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

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

nnrat/farkas-elim-scaled-coupled-lower-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-lower-reduced lowers u0 urest a w
  where solvable := nnrat/farkas-elim-scaled-coupled-lower-solvable lowers u0 urest a w