Reference · Signed rationals

rainbow.math.rational.signed.square-monotone

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

B6b of the limit-reciprocal arc: squaring is monotone on nonnegatives. signed/square-monotone : 0 <= a -> a <= b -> a*a <= b*b Two applications of multiply-right-monotone: a*a <= b*a (multiply a<=b by a>=0) and a*b <= b*b (multiply a<=b by b>=0, where 0<=b from 0<=a<=b); align b*a ~ a*b by commutativity and chain by transitivity. Feeds the assembly's positivity derivation (with magnitude-monotone: |L|/2 <= |s n| -> (|L|/2)^2 <= (s n)^2 -> mag positive). Axiom-free; additive; does not touch the LP checker.

Depends onmath.rational.signed.multiply-monotonemath.rational.signed.order-transitivitymath.rational.signed.order-respectsmath.rational.signed.multiply-ring

signed/square-monotone :
  (a b : ℚ)
  (ha : 0 ≤ a)
  (hab : a ≤ b)
  → a · a ≤ b · b