Reference · Non-negative rationals

rainbow.math.rational.nnrat.distance

Non-negative rationalssrc/rainbow/math/rational/nnrat/distance.clj1 definitions, 4 theorems

A quotient-safe computational distance on exact nonnegative rationals. For x=nx/dx and y=ny/dy, `nnrat/distance x y` is represented by |nx*dy - ny*dx| / (dx*dy). The numerator uses the existing computational `nat/distance`; the packed denominator uses the same positive denominator-combination operation as NNRAT addition and multiplication. The main theorem identifies this value exactly with the additive-radius interface used by finite Bellman proofs: distance x y <= epsilon iff x <= y + epsilon and y <= x + epsilon. All denominator transports are checked equalities generated by the verified nat-ring normalizer. Native, kernel-checked, and axiom-free on D63.

Depends onmath.nat.contractionmath.nat.distance-radiusmath.rational.nnrat.order-equivalence

nnrat/distance :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

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

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

nnrat/distance-at-most-iff-additive-closeness :
  (left right epsilon : ℚ≥0)
  → proposition/conjunction (nnrat/distance left right ≤ epsilon → conjunction) (conjunction → nnrat/distance left right ≤ epsilon)
  where conjunction := proposition/conjunction (left ≤ right + epsilon) (right ≤ left + epsilon)

nnrat/distance-symmetric :
  (left right : ℚ≥0)
  → nnrat/distance left right = nnrat/distance right left