Reference · Non-negative rationals

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

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

Recursive-reduction sub-brick of brick 6 (single-row core): reduce a both-sides cross row to an affine row in the surviving variable. Eliminating a variable v across the general Fourier-Motzkin step, each bilist cross condition is a both-sides row A*v + P <= B*v + Q (brick 6 cross-product core). This reduces it, subtraction-free, to an affine row in v: nnrat/farkas-both-sides-reduce proves (A*v+P <= B*v+Q) -> (EXISTS D, A+D~B /\ P <= D*v+Q) OR (EXISTS D, B+D~A /\ D*v+P <= Q) -- a LOWER affine row when A<=B, an UPPER affine row when B<=A. The case-split uses nnrat/at-most-total (the order is total), the difference witness comes from nnrat/at-most-difference, and the conversions are nnrat/farkas-both-sides-to-lower and -to-upper. So the both-sides cross system becomes a mixed affine-row system in one fewer variable, which bricks 4/5b eliminate. Mapping this over the bilist cross-condition list (and threading it through the variable-count induction) is the remaining n-variable capstone. Native proof data, axiom-free.

Depends onmath.rational.nnrat.order-totalmath.rational.nnrat.farkas-both-sidesmath.rational.nnrat.order-difference

nnrat/farkas-both-sides-reduce :
  (a b p q v : ℚ≥0)
  (both : a · v + p ≤ b · v + q)
  → proposition/disjunction (existence) (existence₁)
  where existence := proposition/existence ℚ≥0 (fun d => proposition/conjunction (a + d = b) (p ≤ d · v + q))
  where existence₁ := proposition/existence ℚ≥0 (fun d => proposition/conjunction (b + d = a) (d · v + p ≤ q))