Reference · Non-negative rationals

rainbow.math.rational.nnrat.order-total

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

Totality of the nnrat order: for all a b, a <= b OR b <= a. A prerequisite for the recursive-reduction sub-brick of the general LP Fourier-Motzkin encoding: reducing a both-sides cross row A*v + P <= B*v + Q to an affine row needs to case-split on A vs B, and the both-sides->upper direction needs B <= A from the failure of A <= B -- which requires the order to be TOTAL, not merely decidable. nnrat/at-most-decidable gives a <= b OR NOT (a <= b); this gives a <= b OR b <= a. Proof mirrors nnrat/at-most-decidable but the false branch yields the reverse inequality instead of a negation: case on the boolean decision audit/decide-nnrat-at-most a b (Bool.rec with the standard equality motive), true -> a <= b (nnrat/decide-at-most-true-sound), false -> b <= a (nnrat/decide-at-most-false-reverse). Native proof data, axiom-free.

Depends onmath.finite.rational-argmax

nnrat/at-most-total :
  (a b : ℚ≥0)
  → proposition/disjunction (a ≤ b) (b ≤ a)