Reference · Signed rationals

rainbow.math.rational.signed.distance

Signed rationalssrc/rainbow/math/rational/signed/distance.clj1 definitions, 10 theorems

A quotient-safe scalar metric interface for signed rationals. `signed/distance a b` is `|a-b|`. Its laws establish nonnegativity, congruence, symmetry, self-zero, exact separation up to signed equivalence, and the two-row linear encoding of a radius bound. The module reuses only the scalar specs from older vector/counterfactual developments, keeping the metric foundation independent of those larger representations. Native, kernel-checked, and axiom-free on D63.

Depends onmath.rational.signed.absolute-algebra

signed/distance :
  (x₁ x₂ : ℚ)
  → ℚ

signed/negate-subtract :
  (left right : ℚ)
  → signed/negate (left - right) = right - left

signed/distance-unfold :
  (left right : ℚ)
  → signed/distance left right = signed/absolute (left - right)

signed/distance-nonnegative :
  (left right : ℚ)
  → 0 ≤ signed/distance left right

signed/distance-respects-equivalence :
  (left left-prime right right-prime : ℚ)
  (same-left : left = left-prime)
  (same-right : right = right-prime)
  → signed/distance left right = signed/distance left-prime right-prime

signed/distance-symmetric :
  (left right : ℚ)
  → signed/distance left right = signed/distance right left

signed/distance-self-zero :
  (value : ℚ)
  → signed/distance value value = 0

signed/distance-zero-of-equivalent :
  (left right : ℚ)
  (same : left = right)
  → signed/distance left right = 0

signed/equivalent-of-distance-zero :
  (left right : ℚ)
  (distance-zero : signed/distance left right = 0)
  → left = right

signed/distance-zero-iff-equivalent :
  (left right : ℚ)
  → proposition/conjunction (signed/distance left right = 0 → left = right) (left = right → signed/distance left right = 0)

signed/distance-bounded-iff-deviation-rows :
  (left right threshold : ℚ)
  → proposition/conjunction (signed/distance left right ≤ threshold → conjunction) (conjunction → signed/distance left right ≤ threshold)
  where conjunction := proposition/conjunction (left - right ≤ threshold) (signed/negate (left - right) ≤ threshold)