Reference · Non-negative rationals

rainbow.math.rational.nnrat.ordered-distance

Non-negative rationalssrc/rainbow/math/rational/nnrat/ordered_distance.clj0 definitions, 2 theorems

Exact reconstruction from ordered nonnegative-rational distance. Natural distance reconstructs an ordered upper endpoint: left <= right -> left + distance(left,right) = right. The natural proof extracts the additive witness already carried by `nat/at-most` and removes a common translation with `nat/distance-add-left`. The NNRAT theorem lifts that equality through the quotient-safe cross-product representation. This provides an executable, canonical remainder rather than an existentially chosen gap. Native, kernel-checked, and axiom-free on D63.

Depends onmath.rational.nnrat.distance

nat/add-distance-of-at-most :
  (left right : ℕ)
  (ordered : left ≤ right)
  → algebra/nat-add left (nat/distance left right) = right

nnrat/add-distance-of-at-most :
  (left right : ℚ≥0)
  (ordered : left ≤ right)
  → left + nnrat/distance left right = right