Reference · Signed rationals

rainbow.math.rational.signed.limit-scale-law

Signed rationalssrc/rainbow/math/rational/signed/limit_scale_law.clj0 definitions, 2 theorems

Scalar multiple of a limit -- the missing piece of limit linearity. `analysis/limit-sum`, `-difference`, `-negate`, `-const` are already proved; this module adds the scaling law: if s converges to L with modulus M, then the sequence n |-> c * s n converges to c * L, for any POSITIVE rational c. Positivity is carried structurally by presenting c as `nnrat/make (succ p) q` (numerator succ p >= 1), which also makes the reciprocal well-behaved with no c=0 split. Proof route (smul-native, matching the band lane's `smul (from-nnrat c)` scaling): the modulus is rescaled by 1/c, `analysis/scaled-sequence-close-to-scaled-limit` gives the band at radius `c * (1/c) * eps`, and the supporting lemma `analysis/scale-reciprocal-radius-cancel` collapses that radius to `eps` up to signed equivalence (via multiply-associative, from-nnrat-multiply, divide-self-positive, multiply-one-left), after which `analysis/close-respects-radius-equivalence` rewrites the band's radius. Axiom-free; additive; does not touch the LP checker. Env chain: signed-limit-scalar-laws (band + converges/close), signed-limit-arithmetic (close-respects-radius-equivalence), signed-multiply-associative, signed-geometric-bridge (from-nnrat-multiply + rational division / reciprocal / unit laws).

Depends onmath.rational.signed.limit-scalar-lawsmath.rational.signed.limit-arithmeticmath.rational.signed.multiply-associativemath.rational.signed.geometric-bridge

analysis/scale-reciprocal-radius-cancel :
  (p q : ℕ) (d : ℚ)
  → signed/from-nnrat (nnrat/make (data/succ p) q) · (signed/from-nnrat (nnrat/reciprocal (nnrat/make (data/succ p) q)) · d) = d

analysis/limit-scale :
  (p q : ℕ) (s : ℕ → ℚ) (L : ℚ) (M : ℚ → ℕ) (conv : analysis/converges s L M)
  → analysis/converges (fun n => signed/from-nnrat (nnrat/make (data/succ p) q) · s n) (signed/from-nnrat (nnrat/make (data/succ p) q) · L) (fun eps => M (signed/from-nnrat (nnrat/reciprocal (nnrat/make (data/succ p) q)) · eps))