Reference · Natural numbers

rainbow.math.nat.distance-radius

Natural numberssrc/rainbow/math/nat/distance_radius.clj0 definitions, 3 theorems

Natural distance is the least symmetric additive radius. distance a b <= r iff a <= b + r and b <= a + r The forward direction combines the existing endpoint bounds with monotonicity. The reverse direction strips matching successors from the two additive bounds until one endpoint is zero. This is the arithmetic interface needed to lift computational `nat/distance` through exact-rational cross products. Native, kernel-checked, and axiom-free on D63.

Depends onmath.nat.contractionmath.nat.at-most-cancellation

nat/distance-at-most-of-additive-bounds :
  (left right radius : ℕ)
  (left-bound : left ≤ algebra/nat-add right radius)
  (right-bound : right ≤ algebra/nat-add left radius)
  → nat/distance left right ≤ radius

nat/additive-bounds-of-distance-at-most :
  (left right radius : ℕ)
  (bounded : nat/distance left right ≤ radius)
  → proposition/conjunction (left ≤ algebra/nat-add right radius) (right ≤ algebra/nat-add left radius)

nat/distance-at-most-iff-additive-bounds :
  (left right radius : ℕ)
  → proposition/conjunction (nat/distance left right ≤ radius → conjunction) (conjunction → nat/distance left right ≤ radius)
  where conjunction := proposition/conjunction (left ≤ algebra/nat-add right radius) (right ≤ algebra/nat-add left radius)