Reference · Non-negative rationals

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

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

Constructive elimination of an nnrat variable coupled to a survivor. Besides constant lower and non-empty upper families for v, the original system contains v <= w. Eliminating v preserves the ordinary list-sized reduced condition and transfers max-lb(lowers) <= w onto the surviving variable. The witness and projection are native proof data and axiom-free.

Depends onmath.rational.nnrat.farkas-elim-list

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

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

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

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

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