Reference · Non-negative rationals

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

Non-negative rationalssrc/rainbow/math/rational/nnrat/farkas_elim_affine_coupled.clj2 definitions, 3 theorems

Brick 3 of the general LP strong-duality Fourier-Motzkin encoding : elimination of an nnrat variable v whose upper coupling carries an additive SURVIVOR-SUM term. Bricks 1-2 coupled v to a single survivor (a*v <= w, w <= a*v). A real constraint row isolating x_k reads (subtraction-free) A_ik*x_k + sum_{j!=k} A_ij*x_j <= b_i: the coefficient a=A_ik on the eliminated variable, PLUS an additive block s = sum_{j!=k} A_ij*x_j over the surviving variables, all bounded by the constant b=b_i. This brick eliminates v from the affine coupling `a*v + s <= b`, transferring `a*max-lb(lowers) + s <= b` onto the survivors. Here s is an arbitrary nnrat -- the elimination does not depend on its being a sum; brick 4 instantiates s to the map-sum block and tracks how it is rebuilt. Structural mirror of brick 1 with the additive term carried through: in the projection, max-lb <= value gives a*max-lb <= a*value (multiply-monotone), then a*max-lb + s <= a*value + s (add-right-monotone), then a*value + s <= b (the coupling) closes it by transitivity. No positivity required. Native proof data, axiom-free.

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

nnrat/farkas-elim-affine-coupled-reduced :
  (x₁ : List ℚ≥0) (x₂ : ℚ≥0) (x₃ : List ℚ≥0) (x₄ x₅ x₆ : ℚ≥0)
  → Prop

nnrat/farkas-elim-affine-coupled-solvable :
  (x₁ : List ℚ≥0) (x₂ : ℚ≥0) (x₃ : List ℚ≥0) (x₄ x₅ x₆ : ℚ≥0)
  → Prop

nnrat/farkas-elim-affine-coupled-extends :
  (lowers : List ℚ≥0) (u0 : ℚ≥0) (urest : List ℚ≥0) (a s b : ℚ≥0)
  (reduced-feasible : nnrat/farkas-elim-affine-coupled-reduced lowers u0 urest a s b)
  → nnrat/farkas-elim-affine-coupled-solvable lowers u0 urest a s b

nnrat/farkas-elim-affine-coupled-projects :
  (lowers : List ℚ≥0) (u0 : ℚ≥0) (urest : List ℚ≥0) (a s b : ℚ≥0)
  (solution : nnrat/farkas-elim-affine-coupled-solvable lowers u0 urest a s b)
  → nnrat/farkas-elim-affine-coupled-reduced lowers u0 urest a s b

nnrat/farkas-elim-affine-coupled-solvable-iff :
  (lowers : List ℚ≥0) (u0 : ℚ≥0) (urest : List ℚ≥0) (a s b : ℚ≥0)
  → proposition/conjunction (reduced → solvable) (solvable → reduced)
  where reduced := nnrat/farkas-elim-affine-coupled-reduced lowers u0 urest a s b
  where solvable := nnrat/farkas-elim-affine-coupled-solvable lowers u0 urest a s b