Reference · Signed rationals

rainbow.math.rational.signed.magnitude

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

Layer 3 (capstone) of the signed->nnrat magnitude foundation. signed/magnitude x := nnrat/monus (positive x) (negative x) -- a total function signed/from-nnrat-magnitude : nonnegative x -> x ~ from-nnrat (magnitude x) A nonnegative signed value equals from-nnrat of its magnitude (an nnrat), so the magnitude can be reciprocated via the nnrat reciprocal -- the missing lever for the limit-product modulus (dividing a radius by |M|, |L|). Since signed/nonnegative x reduces to (negative x <= positive x), and signed/equivalent x (from-nnrat q) reduces to (positive x + 0) ~ (q + negative x), the property is (magnitude x + negative x) ~ positive x [nnrat/monus-add-cancel] chained through (positive x + 0) ~ positive x [nnrat/add-zero-right]. Axiom-free; additive.

Depends onmath.rational.nnrat.monusmath.rational.nnrat.identities

signed/magnitude :
  (x₁ : ℚ)
  → ℚ≥0

signed/from-nnrat-magnitude :
  (x : ℚ) (h : signed/nonnegative x)
  → x = signed/from-nnrat (signed/magnitude x)