Reference · Non-negative rationals

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

Non-negative rationalssrc/rainbow/math/rational/nnrat/farkas_elim_affine_decidable.clj0 definitions, 2 theorems

Brick 4b of the general LP strong-duality Fourier-Motzkin encoding : decidability of the one-variable affine-list elimination -- the Farkas-alternative half. Feasibility of the eliminated system (brick 4, nnrat_farkas_elim_affine_list.clj) is DECIDABLE: every affine row's coupling a*v + s <= b is a decidable nnrat comparison (nnrat/at-most-decidable), a finite conjunction of decidables is decidable, and the reduced condition is exactly that conjunction at max-lb. Transporting through the brick-4 solvable-iff equivalence yields decidable solvability. The negative branch is the infeasibility certificate -- the object that, in the objective-boundary system, becomes the dual once t exceeds the optimum. So this is the constructive Farkas alternative for affine-row systems, the certificate half of strong duality. Native proof data, axiom-free.

Depends onmath.rational.nnrat.farkas-elim-affine-listmath.rational.nnrat.farkas-alternative

nnrat/farkas-elim-affine-rows-decidable :
  (rows : List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0))) (value : ℚ≥0)
  → proposition/disjunction (satisfied) (proposition/negation (satisfied))
  where satisfied := nnrat/farkas-elim-affine-rows-satisfied rows value

nnrat/farkas-elim-affine-list-solvable-or-not :
  (lowers : List ℚ≥0) (rows : List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0)))
  → proposition/disjunction (solvable) (proposition/negation (solvable))
  where solvable := nnrat/farkas-elim-affine-list-solvable lowers rows