Reference · Signed rationals

rainbow.math.rational.signed.distance-multiply-nonnegative

Signed rationalssrc/rainbow/math/rational/signed/distance_multiply_nonnegative.clj0 definitions, 1 theorems

Nonnegative signed multiplication bounds quotient-safe distance. Rather than requiring an absolute-value product theorem, the proof opens a distance bound into its two deviation rows. Nonnegative multiplication preserves each row, distributivity identifies the scaled subtraction, and negation congruence identifies the reverse deviation. Folding the rows back yields `d(w*x,w*y) <= w*d(x,y)` for `0 <= w`, exactly the component law needed by nonnegative matrix rows. Native, kernel-checked, and axiom-free on D63.

Depends onmath.rational.signed.distancemath.rational.signed.multiply-monotonemath.linear.vector.dot-negatemath.linear.matrix.signed-scale-subtract

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