Reference · Non-negative rationals

rainbow.math.rational.nnrat.farkas-elim-two-var

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

Constructive composition of list-sized elimination for two decoupled nnrat variables. Each variable has its own list of lower bounds and non-empty family of upper bounds. The original system nests witnesses for v and w; the reduced system is the conjunction of the two one-variable reductions. The proofs explicitly compose farkas-elim-list extension and projection in both directions. There are no coupling constraints in this bounded milestone. Native and axiom-free.

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

nnrat/farkas-elim-two-var-system :
  (x₁ : List ℚ≥0) (x₂ : ℚ≥0) (x₃ x₄ : List ℚ≥0) (x₅ : ℚ≥0) (x₆ : List ℚ≥0) (x₇ x₈ : ℚ≥0)
  → Prop

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

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

nnrat/farkas-elim-two-var-extends :
  (lowers-v : List ℚ≥0) (u0v : ℚ≥0) (urest-v lowers-w : List ℚ≥0) (u0w : ℚ≥0)
  (urest-w : List ℚ≥0)
  (reduced-feasible : nnrat/farkas-elim-two-var-reduced lowers-v u0v urest-v lowers-w u0w urest-w)
  → nnrat/farkas-elim-two-var-solvable lowers-v u0v urest-v lowers-w u0w urest-w

nnrat/farkas-elim-two-var-projects :
  (lowers-v : List ℚ≥0) (u0v : ℚ≥0) (urest-v lowers-w : List ℚ≥0) (u0w : ℚ≥0)
  (urest-w : List ℚ≥0)
  (solution : nnrat/farkas-elim-two-var-solvable lowers-v u0v urest-v lowers-w u0w urest-w)
  → nnrat/farkas-elim-two-var-reduced lowers-v u0v urest-v lowers-w u0w urest-w

nnrat/farkas-elim-two-var-solvable-iff :
  (lowers-v : List ℚ≥0) (u0v : ℚ≥0) (urest-v lowers-w : List ℚ≥0) (u0w : ℚ≥0)
  (urest-w : List ℚ≥0)
  → proposition/conjunction (reduced → solvable) (solvable → reduced)
  where reduced := nnrat/farkas-elim-two-var-reduced lowers-v u0v urest-v lowers-w u0w urest-w
  where solvable := nnrat/farkas-elim-two-var-solvable lowers-v u0v urest-v lowers-w u0w urest-w