Reference · Signed rationals

rainbow.math.rational.signed.absolute-sign

Signed rationalssrc/rainbow/math/rational/signed/absolute_sign.clj0 definitions, 2 theorems

Sign characterization of absolute value over signed rationals: 0 <= w => |w| ~ w w <= 0 => |w| ~ -w Foundational reusable lemmas (needed by the sign case-splits in limit-product's distance-multiply and absolute-multiply bricks). Axiom-free; additive. Proof of absolute-of-nonnegative: |w| <= w from absolute-bounded-iff-deviation-rows (backward) given w<=w and -w<=w (the latter from 0<=w via negate-reverses-order + transitivity); w <= |w| is at-most-absolute; antisymmetry closes it. absolute-of-nonpositive reduces to the nonnegative case at -w plus absolute-negate.

Depends onmath.rational.signed.absolute-algebramath.linear.vector.dot-negatemath.rational.signed.decide-order

signed/absolute-of-nonnegative :
  (w : ℚ)
  (h : 0 ≤ w)
  → signed/absolute w = w

signed/absolute-of-nonpositive :
  (w : ℚ)
  (h : w ≤ 0)
  → signed/absolute w = signed/negate w