Reference · Signed rationals

rainbow.math.rational.signed.square-numerator-positive-of-absolute

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

B6f prerequisite (s-n positivity transfer): a lower bound on |x| makes x*x have positive magnitude-numerator. signed/square-numerator-positive-of-absolute-bound : 0 <= b -> 1 <= num(mag(b*b)) -> b <= |x| -> 1 <= num(mag(x*x)) B6d (square-numerator-positive-of-lower-bound) on b <= |x| gives 1 <= num(mag(|x|*|x|)); then transfer |x|*|x| ~ x*x (absolute-multiply + x*x nonnegative) via magnitude-monotone + positive-of-at-most. In the limit-reciprocal assembly this is called with b = |L|/2 and the bound |L|/2 <= |s n| to obtain 1 <= num(mag(s n * s n)) -- the nonzero fact reciprocal-difference / absolute-reciprocal-times-self / reciprocal-antitone need for s n. Axiom-free; additive; does not touch the LP checker.

Depends onmath.rational.signed.square-numerator-positivemath.rational.signed.absolute-multiplymath.rational.signed.absolute-signmath.linear.vector.norm-nonnegativemath.rational.signed.multiply-ordermath.rational.signed.magnitude-monotonemath.rational.nnrat.positive-monotonemath.rational.signed.order-transitivitymath.rational.signed.order-respects

signed/square-numerator-positive-of-absolute-bound :
  (b x : ℚ)
  (hb0 : 0 ≤ b)
  (hbpos : 1 ≤ nnrat/numerator (signed/magnitude (b · b)))
  (hbx : b ≤ signed/absolute x)
  → 1 ≤ nnrat/numerator (signed/magnitude (x · x))