Reference · Non-negative rationals

rainbow.math.rational.nnrat.order-difference

Non-negative rationalssrc/rainbow/math/rational/nnrat/order_difference.clj0 definitions, 2 theorems

Nonnegative-rational order is difference-existence, and the two-point rearrangement inequality that follows from it. `nnrat/at-most` is the reflexive-transitive closure of a cross-product nat comparison, so it carries no additive witness on its face. But nat order DOES: `nat/at-most a b` is `exists e, a + e = b`. Transporting that witness through the cross product yields nnrat/at-most-difference : x <= y -> exists w, x + w ~ y with the explicit witness `w = e / (den x * den y)`. Verifying it is a single nat-ring identity around the extracted equation: (num x * (dx*dy) + e*dx) * dy = (dx*dy) * (num x * dy + e) = (dx*dy) * (num y * dx) = num y * (dx * (dx*dy)). The payoff is the TWO-POINT REARRANGEMENT INEQUALITY nnrat/rearrangement-two-point : n <= p -> q <= m -> p*q + n*m <= p*m + n*q -- pairing the larger factor with the larger factor dominates the crossed pairing. It is the multiplicative order fact that no amount of termwise monotonicity can reach (the two terms move in opposite directions), and it is exactly the sign rule `(p-n)*(m-q) >= 0` stated without subtraction. Writing p as n+u turns the goal into `u*q <= u*m` plus additive regrouping, which is ordinary monotonicity. Native and axiom-free; chains the nnrat order toolkit, the nat-ring tactic (for the witness identity) and the nnrat-ring tactic (for the two regroupings) on D63.

Depends onmath.rational.nnrat.order-equivalencemath.rational.nnrat.ringmath.rational.nnrat.add-monotonemath.rational.nnrat.additive-reassociationmath.rational.nnrat.distribute-rightmath.rational.nnrat.multiply-monotone

nnrat/at-most-difference :
  (x y : ℚ≥0)
  (ordered : x ≤ y)
  → proposition/existence ℚ≥0 (fun w => x + w = y)

nnrat/rearrangement-two-point :
  (n p q m : ℚ≥0)
  (hnp : n ≤ p)
  (hqm : q ≤ m)
  → p · q + n · m ≤ p · m + n · q