Reference · Signed rationals

rainbow.math.rational.signed.magnitude-monotone

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

B6 prerequisite: magnitude is monotone on nonnegatives. signed/magnitude-monotone : nonnegative a -> nonnegative b -> a <= b -> nnrat/at-most (magnitude a) (magnitude b) Immediate: a ~ from-nnrat(magnitude a), b ~ from-nnrat(magnitude b) [from-nnrat-magnitude], so a <= b transports to from-nnrat(mag a) <= from-nnrat(mag b) [at-most-respects-equivalence], and from-nnrat-at-most-reverse drops it to the nnrat order. Reusable; feeds the limit-reciprocal assembly's positivity derivation (|s n| >= |L|/2 -> mag(s n^2) positive). Axiom-free; additive; does not touch the LP checker.

Depends onmath.rational.signed.magnitudemath.rational.signed.geometric-bridgemath.rational.signed.order-respects

signed/magnitude-monotone :
  (a b : ℚ) (ha : signed/nonnegative a) (hb : signed/nonnegative b)
  (hab : a ≤ b)
  → signed/magnitude a ≤ signed/magnitude b