Reference · Signed rationals

rainbow.math.rational.signed.additive-distance

Signed rationalssrc/rainbow/math/rational/signed/additive_distance.clj0 definitions, 4 theorems

Distance bounds from two-sided additive signed inequalities. The Bellman contraction interface is naturally stated as left <= right + epsilon and right <= left + epsilon, while residual arguments use `signed/distance`. This module proves the quotient-safe bridge. Each subtraction inequality is just a rearrangement of the corresponding signed-order cross sum, certified by the checked nnrat ring normalizer; the existing absolute/deviation characterization then gives the distance bound. Native and axiom-free on D63.

Depends onmath.rational.nnrat.ringmath.rational.signed.distance

signed/subtract-at-most-of-additive-upper :
  (left right epsilon : ℚ)
  (upper : left ≤ right + epsilon)
  → left - right ≤ epsilon

signed/distance-at-most-of-additive-closeness :
  (left right epsilon : ℚ)
  (left-close : left ≤ right + epsilon)
  (right-close : right ≤ left + epsilon)
  → signed/distance left right ≤ epsilon

signed/additive-upper-of-subtract-at-most :
  (left right epsilon : ℚ)
  (difference-bound : left - right ≤ epsilon)
  → left ≤ right + epsilon

signed/additive-closeness-of-distance-at-most :
  (left right epsilon : ℚ)
  (bounded : signed/distance left right ≤ epsilon)
  → proposition/conjunction (left ≤ right + epsilon) (right ≤ left + epsilon)