Reference · Non-negative rationals

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

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

Brick 4 of the general LP strong-duality Fourier-Motzkin encoding : the one-primal-variable FM elimination step over a LIST of affine upper rows -- the first genuinely new formalization of the lane. A real elimination sees v constrained by many rows at once. Each row is a triple (a, s, b) meaning a*v + s <= b, with a the coefficient on the eliminated v, s the additive survivor-sum block, b the constant bound (brick 3's affine coupling, per row). Rows are `data/Product`-triples in a List; `rows-satisfied rows value` folds the per-row coupling with conjunction. v is bounded below by a constant lower family. Eliminating v (witness max-lb(lowers), the smallest feasible value) is solvable iff every row holds at max-lb -- rows-satisfied rows (max-lb lowers). The projection is the new content: it maps brick 3's per-row argument (max-lb <= value gives a*max-lb <= a*value by multiply-monotone, then + s by add-right-monotone, then <= b by transitivity) across the whole row list by List.rec induction. The extension witnesses max-lb directly. Native proof data, axiom-free.

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

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

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

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

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

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

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