Reference · Signed rationals

rainbow.math.rational.signed.limit-scale

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

Axiom-free nonnegative scaling of signed-rational order bands. The convergence predicate installed by signed-convergence quantifies over all signed radii. Consequently a constant sequence cannot inhabit it: at radius -1 its band would require 1 <= 0. The reusable local law below is the strongest non-vacuous scaling result available without changing that predicate or adding signed division: close L e x -> close ((from-nnrat c) * L) ((from-nnrat c) * e) ((from-nnrat c) * x). Multiplication by the nonnegative Grothendieck pair (c,0) preserves signed order. The proof reduces the signed comparison to nnrat/multiply-monotone and transports through distributivity and the nnrat zero laws.

analysis/close-scale-nonnegative :
  (c : ℚ≥0) (L eps x : ℚ) (bounded : analysis/close L eps x)
  → analysis/close (signed/from-nnrat c · L) (signed/from-nnrat c · eps) (signed/from-nnrat c · x)