Reference · Non-negative rationals

rainbow.math.rational.nnrat.multiply-monotone

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

Universal monotonicity of nonnegative-rational multiplication under the rational order -- the algebra gap flagged in rainbow-universal-foundation-layer that blocks convex-combination / weighted-average bounds: multiply-monotone-base : base-at-most a b -> base-at-most (c*a) (c*b) (all c a b) multiply-monotone : a <= b -> (c*a) <= (c*b) (all c a b) The base lemma is pure nat reasoning: with num/den written out, base-at-most a b = (num a * den b) <= (num b * den a) base-at-most (c*a)(c*b)= ((num c * num a) * (den c * den b)) <= ((num c * num b) * (den c * den a)) Reassociate both sides by nat/multiply-four-reorder into (num c * den c) * (num a * den b) <= (num c * den c) * (num b * den a) which is nat/multiply-left-monotone applied to the hypothesis; the product denominators (den c * den b) are converted to the packed product-denominator succ(combine ..) via the nnrat/denominator-combine law, transported with nat/at-most-rewrite-left / -right. The full theorem lifts the base lemma across the reflexive-transitive closure nnrat/at-most by instantiating the closure recursor at the motive (\y. c*a <= c*y): reflexivity for the base, and for each step at-most-from-cross (multiply-monotone-base ..) chained by at-most-transitive. Native and axiom-free; chains rainbow.algorithms.proofs.decision-guarantee-audit (order), rainbow.math.nat.semiring / nat-order (nat algebra), and nonnegative-rational.

nnrat/multiply-monotone-base :
  (c a b : ℚ≥0) (h : nnrat/base-at-most a b)
  → nnrat/base-at-most (c · a) (c · b)

nnrat/multiply-monotone :
  (c a b : ℚ≥0)
  (h : a ≤ b)
  → c · a ≤ c · b