Reference · Non-negative rationals

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

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

Brick 3 full round: cross a LIST of lower coefficient-vector constraints against a LIST of upper coefficient-vector constraints -- the whole round's reduced set. Given a list of lower constraints and a list of upper constraints (each (coefficient, tail-vector, bound)), all holding at the eliminated variable x1, every pairwise reduced both-sides vector constraint holds (nnrat/farkas-cross-vectors-all-reduced): for each lower row, its whole per-upper reduced list (brick 3's one-lower fold nnrat/farkas-cross-vectors-reduced-holds), collected across the lower list by a second List.rec. This is one full elimination round expressed on the coefficient-vector representation: two constraint lists in n variables produce the pairwise reduced both-sides constraints over n-1 variables -- the coefficient-vector analogue of brick 6's cross-product core. The over-variable recursion folds this (partition + head-split feed the next round); the base case grounds it. Native proof data, axiom-free.

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

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

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

nnrat/farkas-cross-vectors-all-reduced :
  (lowers uppers : List (Product)) (x1 : ℚ≥0)
  (lh : nnrat/farkas-cross-vectors-lowers-hold lowers x1)
  (uh : nnrat/farkas-cross-vectors-uppers-hold uppers x1)
  → nnrat/farkas-cross-vectors-all-reduced-conds lowers uppers x1
  where Product := data/Product ℚ≥0 (data/Product (List (data/Product ℚ≥0 ℚ≥0)) ℚ≥0)