Reference · Non-negative rationals

rainbow.math.rational.nnrat.add-upper

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

The additive upper-bound law: a nonnegative rational is at most itself plus anything, `a <= a + b`. The corpus had the converse cancellation (nnrat/at-most-add-right-cancel) but not this direction. It is the shared core of every 'the extra term only helps' guarantee -- UCB optimism, expected-improvement's exploitation floor, and any acquisition function of the form base + nonnegative-bonus -- each of which reduces to one application of this lemma. Native, kernel-checked, and axiom-free on D63.

nnrat/at-most-add-right :
  (a b : ℚ≥0)
  → a ≤ a + b