Reference · Non-negative rationals

rainbow.math.rational.nnrat.farkas-cross-vectors-list

Non-negative rationalssrc/rainbow/math/rational/nnrat/farkas_cross_vectors_list.clj2 definitions, 1 theorems

Brick 3 per-pair fold: cross one lower coefficient-vector constraint against a LIST of upper coefficient-vector constraints. Each upper constraint is (coefficient, tail-vector, bound), meaning eval(cons (coeff, x1) tail) <= bound at the eliminated variable x1. Given a lower constraint b_L <= eval(cons (l-coeff, x1) l-tail) and every upper constraint holding at x1, every pairwise reduced constraint holds (nnrat/farkas-cross-vectors-reduced-holds): each is b_L*u_coeff + eval(scale l-coeff u-tail) <= bound*l-coeff + eval(scale u_coeff l-tail), a both-sides coefficient-vector constraint over the tail. By List.rec applying nnrat/farkas-cross-vectors per upper. The full n-variable round maps this over the lower list too (a second List.rec); this is the one-lower core. Native proof data, axiom-free.

Depends onmath.rational.nnrat.farkas-cross-vectors

nnrat/farkas-cross-vectors-uppers-hold :
  (x₁ : List (data/Product ℚ≥0 (Product))) (x₂ : ℚ≥0)
  → Prop
  where Product := data/Product (List (data/Product ℚ≥0 ℚ≥0)) ℚ≥0

nnrat/farkas-cross-vectors-reduced :
  (x₁ : List (data/Product ℚ≥0 (Product))) (x₂ x₃ : ℚ≥0)
  (x₄ : List (data/Product ℚ≥0 ℚ≥0)) (x₅ : ℚ≥0)
  → Prop
  where Product := data/Product (List (data/Product ℚ≥0 ℚ≥0)) ℚ≥0

nnrat/farkas-cross-vectors-reduced-holds :
  (x1 l-coeff : ℚ≥0) (l-tail : List (data/Product ℚ≥0 ℚ≥0)) (b-l : ℚ≥0)
  (uppers : List (data/Product ℚ≥0 (Product)))
  (lower : b-l ≤ nnrat/linear-form (data/cons (data/Product ℚ≥0 ℚ≥0) (data/pair ℚ≥0 ℚ≥0 l-coeff x1) l-tail))
  (uh : nnrat/farkas-cross-vectors-uppers-hold uppers x1)
  → nnrat/farkas-cross-vectors-reduced uppers x1 l-coeff l-tail b-l
  where Product := data/Product (List (data/Product ℚ≥0 ℚ≥0)) ℚ≥0