Reference · Non-negative rationals

rainbow.math.rational.nnrat.farkas-partition-row

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

Piece (ii) brick 1 core: the per-row step of the dependent partition. One elimination round's output, reduced-conditions, is a fold of disjunctions: each reduced row is (EXISTS D, A+D~B /\ P<=D*v+Q) OR (EXISTS D, B+D~A /\ D*v+P<=Q). To thread that into the next round it must become a lower-row list and an upper-row list. This is the per-row core: a reduced row becomes an affine LOWER constraint (EXISTS D, P<=D*v+Q) or an affine UPPER constraint (EXISTS D, D*v+P<=Q) -- dropping the difference-witness conjunct (A+D~B / B+D~A), which the next round does not need; it only needs the affine constraint itself. nnrat/farkas-partition-row proves the reduced disjunction implies this stripped disjunction, by use-disjunction + use-witness + right-conjunct + re-witness. The list accumulation building the two lists from this per-row step is brick 1 proper. Native proof data, axiom-free.

nnrat/farkas-partition-row :
  (a b p q v : ℚ≥0) (reduced : proposition/disjunction (existence) (existence₁))
  → 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))
  where existence₂ := proposition/existence ℚ≥0 (fun d => p ≤ d · v + q)
  where existence₃ := proposition/existence ℚ≥0 (fun d => d · v + p ≤ q)