Reference · Non-negative rationals

rainbow.math.rational.nnrat.add-monotone

Non-negative rationalssrc/rainbow/math/rational/nnrat/add_monotone.clj0 definitions, 5 theorems

Universal (one-sided) monotonicity of nonnegative-rational addition under the rational order -- the additive companion to nnrat/multiply-monotone, and the keystone for convex-combination / weighted-average bounds: add-right-monotone-base : base-at-most a b -> base-at-most (a+c) (b+c) (all c a b) add-right-monotone : a <= b -> (a+c) <= (b+c) (all c a b) Base lemma is pure nat. With num/den written out and the packed product denominators expanded by the nnrat/denominator-combine law, the goal ((n_a*d_c) + (n_c*d_a)) * (d_b*d_c) <= ((n_b*d_c) + (n_c*d_b)) * (d_a*d_c) right-distributes (nat/multiply-add-left) into a sum of two products on each side, compared summand-wise by nat/add-monotone: * the a-summand reduces -- via two EXACT nat/multiply-four-reorder rewrites, no commutation -- to nat/multiply-right-monotone applied to the hypothesis (n_a*d_b <= n_b*d_a) scaled by (d_c*d_c); * the c-summand is an equality (four-reorder nc da db dc), lifted to <= from nat/at-most-reflexive. The denominators are transported between packed succ(combine ..) and product form with equality/congruent-function over the combine law. The full theorem lifts the base lemma across the reflexive-transitive closure nnrat/at-most exactly as nnrat/multiply-monotone does: apply the closure recursor at motive (\y. a+c <= y+c), reflexivity for the base and at-most-from-cross + at-most-transitive per step. Native and axiom-free; chains rainbow.algorithms.proofs.decision-guarantee-audit (order), nat-order / nat-semiring (nat algebra), and nonnegative-rational.

nnrat/add-right-monotone-base :
  (c a b : ℚ≥0) (h : nnrat/base-at-most a b)
  → nnrat/base-at-most (a + c) (b + c)

nnrat/add-right-monotone :
  (c a b : ℚ≥0)
  (h : a ≤ b)
  → a + c ≤ b + c

nnrat/add-commutative :
  (a b : ℚ≥0)
  → a + b = b + a

nnrat/add-left-monotone :
  (c a b : ℚ≥0)
  (h : a ≤ b)
  → c + a ≤ c + b

nnrat/add-monotone :
  (a a-hi b b-hi : ℚ≥0)
  (ha : a ≤ a-hi)
  (hb : b ≤ b-hi)
  → a + b ≤ a-hi + b-hi