Reference · Non-negative rationals

rainbow.math.rational.nnrat.farkas-elim-affine-list-lower

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

Brick 5b of the general LP strong-duality Fourier-Motzkin encoding : the one-variable elimination step over a list of affine LOWER rows -- the mirror of brick 4 (nnrat_farkas_elim_affine_list.clj) for the other bound direction. Where brick 4 eliminated v from affine UPPER rows a*v+s<=b with a constant lower family, this eliminates v from affine LOWER rows w <= a*v + s with a constant UPPER family. Each row is a data/Product triple (a, s, w). v's largest feasible value is min-ub of the uppers, so eliminating v (witness min-ub) is solvable iff every lower row holds at min-ub: w <= a*min-ub + s. Both affine-row directions -- upper (brick 4) and lower (here) -- are the two input row sets the affine CROSS-PRODUCT (the real remaining crux; see the scoping note in the design doc) combines. Structural mirror of brick 4 with min-ub for max-lb and le-all for ge-all: the projection maps the per-row argument (v <= min-ub gives a*v <= a*min-ub by multiply-monotone, then + s by add-right-monotone, then w <= that by transitivity) across the list by List.rec, rows destructured by product/first,second. Native proof data, axiom-free.

Depends onmath.rational.nnrat.farkas-elim-coupledmath.rational.nnrat.multiply-monotonemath.rational.nnrat.add-monotone

nnrat/farkas-elim-affine-lower-rows-satisfied :
  (x₁ : List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0))) (x₂ : ℚ≥0)
  → Prop

nnrat/farkas-elim-affine-list-lower-reduced :
  (x₁ : ℚ≥0) (x₂ : List ℚ≥0) (x₃ : List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0)))
  → Prop

nnrat/farkas-elim-affine-list-lower-solvable :
  (x₁ : ℚ≥0) (x₂ : List ℚ≥0) (x₃ : List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0)))
  → Prop

nnrat/farkas-elim-affine-list-lower-extends :
  (u0 : ℚ≥0) (urest : List ℚ≥0) (rows : List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0)))
  (reduced-feasible : nnrat/farkas-elim-affine-list-lower-reduced u0 urest rows)
  → nnrat/farkas-elim-affine-list-lower-solvable u0 urest rows

nnrat/farkas-elim-affine-list-lower-projects :
  (u0 : ℚ≥0) (urest : List ℚ≥0) (rows : List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0)))
  (solution : nnrat/farkas-elim-affine-list-lower-solvable u0 urest rows)
  → nnrat/farkas-elim-affine-list-lower-reduced u0 urest rows

nnrat/farkas-elim-affine-list-lower-solvable-iff :
  (u0 : ℚ≥0) (urest : List ℚ≥0) (rows : List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0)))
  → proposition/conjunction (reduced → solvable) (solvable → reduced)
  where reduced := nnrat/farkas-elim-affine-list-lower-reduced u0 urest rows
  where solvable := nnrat/farkas-elim-affine-list-lower-solvable u0 urest rows