Reference · Signed rationals

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

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

B6d of the limit-reciprocal arc: the positivity derivation the assembly calls. signed/square-numerator-positive-of-lower-bound : 0 <= a -> 1 <= num(mag(a*a)) -> a <= b -> 1 <= num(mag(b*b)) Composes B6a/B6b/B6c: 0<=a & a<=b give a*a <= b*b (square-monotone); both squares are nonnegative (square-nonnegative), so mag(a*a) <= mag(b*b) (magnitude-monotone); and positivity transfers upward (positive-of-at-most). The hypothesis/goal `1 <= num(mag(.))` is definitionally nnrat/positive (mag .), so B6c applies directly. Called in the assembly with a = |L|/2 and b = |s n| to get 1 <= num(mag(s n * s n)), enabling reciprocal-difference/ antitone/absolute-reciprocal on s n. Axiom-free; additive; does not touch the LP checker.

Depends onmath.rational.signed.square-monotonemath.rational.signed.magnitude-monotonemath.rational.nnrat.positive-monotonemath.linear.vector.norm-nonnegative

signed/square-numerator-positive-of-lower-bound :
  (a b : ℚ)
  (ha : 0 ≤ a)
  (hpos : 1 ≤ nnrat/numerator (signed/magnitude (a · a)))
  (hab : a ≤ b)
  → 1 ≤ nnrat/numerator (signed/magnitude (b · b))