Reference · Non-negative rationals

rainbow.math.rational.nnrat.farkas-vector-both-sides-reduce

Non-negative rationalssrc/rainbow/math/rational/nnrat/farkas_vector_both_sides_reduce.clj0 definitions, 1 theorems

The unified representation, per-row reduction: reduce a both-sides COEFFICIENT-VECTOR row to a lower/upper affine row in the next variable x2 -- as a disjunction, ready for the partition. A reduced both-sides vector row (nnrat/farkas-cross-vectors output) with tails headed by x2 is affine in x2 on both sides: CL + (AL*x2 + EL) <= CR + (AR*x2 + ER), with AL = a2u*l1, AR = a2l*u1, CL = b_L*u1, CR = b_U*l1, EL = eval(scale l1 ru), ER = eval(scale u1 rl). Grouping the x2 term to the front (commute/reassociate, no subtraction) matches the shape nnrat/farkas-both-sides-reduce consumes, so this row reduces exactly as the affine both-sides row does: -> (EXISTS D, AL+D~AR /\ (CL+EL) <= D*x2+(CR+ER)) OR (EXISTS D, AR+D~AL /\ D*x2+(CL+EL) <= (CR+ER)) a LOWER row in x2 when AL<=AR, an UPPER row when AR<=AL. The whole reduction reuses the proved nnrat/farkas-both-sides-reduce (order-totality, the difference witness, the both-sides conversions) after the grouping -- no new arithmetic. This is the vector-level analogue of nnrat/farkas-both-sides-reduce and the per-row core of the coefficient- vector partition: mapping it over the reduced-row list, then stripping the disjunction (nnrat/farkas-partition-row / -list) into a lower-list and an upper-list, is the concrete step the over-variable recursion folds. Native proof data, axiom-free.

Depends onmath.rational.nnrat.farkas-both-sides-reducemath.rational.nnrat.farkas-form-scale

nnrat/farkas-vector-both-sides-reduce :
  (l-coeff u-coeff b-l b-u a2l a2u : ℚ≥0) (rl ru : List (data/Product ℚ≥0 ℚ≥0))
  (x2 : ℚ≥0)
  (h : b-l · u-coeff + nnrat/linear-form (nnrat/farkas-scale-right l-coeff (cons)) ≤ b-u · l-coeff + nnrat/linear-form (nnrat/farkas-scale-right u-coeff (cons₃)))
  → proposition/disjunction (existence) (existence₁)
  where cons := data/cons (data/Product ℚ≥0 ℚ≥0) (data/pair ℚ≥0 ℚ≥0 a2u x2) ru
  where cons₃ := data/cons (data/Product ℚ≥0 ℚ≥0) (data/pair ℚ≥0 ℚ≥0 a2l x2) rl
  where existence := proposition/existence ℚ≥0 (fun d => proposition/conjunction (a2u · l-coeff + d = a2l · u-coeff) (b-l · u-coeff + nnrat/linear-form (nnrat/farkas-scale-right l-coeff ru) ≤ d · x2 + (b-u · l-coeff + nnrat/linear-form (nnrat/farkas-scale-right u-coeff rl))))
  where existence₁ := proposition/existence ℚ≥0 (fun d => proposition/conjunction (a2l · u-coeff + d = a2u · l-coeff) (d · x2 + (b-l · u-coeff + nnrat/linear-form (nnrat/farkas-scale-right l-coeff ru)) ≤ b-u · l-coeff + nnrat/linear-form (nnrat/farkas-scale-right u-coeff rl)))