Reference · Non-negative rationals

rainbow.math.rational.nnrat.add-zero-split

Non-negative rationalssrc/rainbow/math/rational/nnrat/add_zero_split.clj0 definitions, 4 theorems

Nonnegativity forces zero: for nonnegative rationals, a sum equivalent to 0 forces each summand to 0. nnrat/add-zero-split-left : (a + b) ~ 0 -> a ~ 0 nnrat/add-zero-split-right : (a + b) ~ 0 -> b ~ 0 This is the crux behind complementary slackness / KKT optimality conditions: a zero duality gap b.y - c.x = sum of nonnegative slack terms ~ 0 forces every slack term to 0. Because nnrat carries no negatives, cancellation cannot hide a positive term. Proof: (a+b) ~ 0 unfolds to the cross product (na*db + nb*da) * 1 = 0 * den, so the nat numerator na*db + nb*da = 0; nat/sum-zero-left/right split it to na*db = 0 and nb*da = 0; and since db, da are positive (succ _), the new nat lemma multiply-succ-zero-left gives na = 0 and nb = 0, i.e. a ~ 0 and b ~ 0. Native and axiom-free; chains nnrat-nat-at-most-cancellation (for nat/sum-zero-left) on d63.

Depends onmath.nat.at-most-cancellation

nat/sum-zero-right :
  (x y : ℕ)
  (h : algebra/nat-add x y = 0)
  → y = 0

nat/multiply-succ-zero-left :
  (na m : ℕ)
  (h : nat/multiply na (data/succ m) = 0)
  → na = 0

nnrat/add-zero-split-left :
  (a b : ℚ≥0)
  (h : a + b = 0)
  → a = 0

nnrat/add-zero-split-right :
  (a b : ℚ≥0)
  (h : a + b = 0)
  → b = 0