Reference · Non-negative rationals

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

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

Additive cancellation to zero for nonnegative rationals: nnrat/add-cancel-to-zero : (a + g) ~ a -> g ~ 0 If adding g changes nothing, g was 0. The extraction step for complementary slackness: a zero duality gap means the objective is unchanged by the slack term, so the slack term is 0. Proof: (a+g) ~ a unfolds (denominator-combine reduces) to the nat identity (na*dg + ng*da)*da = na*(da*dg); nat-ring isolates it to X + ng*da*da = X, so nat/add-left-cancel gives ng*da*da = 0, and da = succ _ positive lets multiply-succ-zero-left (applied twice) conclude ng = 0, i.e. g ~ 0. Native and axiom-free; chains nnrat-add-zero-split (for multiply-succ-zero-left) and nat-ring on d63.

Depends onmath.rational.nnrat.add-zero-split

nnrat/add-cancel-to-zero :
  (a g : ℚ≥0)
  (h : a + g = a)
  → g = 0