Reference · Signed rationals

rainbow.math.rational.signed.limit-arithmetic

Signed rationalssrc/rainbow/math/rational/signed/limit_arithmetic.clj0 definitions, 3 theorems

Axiom-free additive arithmetic for signed-rational limits. The local band law is the triangle inequality in the order-band presentation: close L e x, close M f y ==> close (L+M) (e+f) (x+y). `analysis/converges` quantifies over every signed radius, including zero. Thus the sum theorem may use radius `eps` for the first sequence and radius zero for the second, with modulus `Ms eps + Mt zero`; additive closeness gives radius `eps+zero`, and radius-equivalence transport reduces that to `eps`. This avoids importing a positivity premise or postulating signed division while proving the full limit law. Native and axiom-free; chains the D63 signed convergence/order toolkit through signed limit uniqueness (for signed/add-zero-right).

Depends onmath.rational.signed.limit-uniqueness

analysis/close-respects-radius-equivalence :
  (L eps eps-prime x : ℚ)
  (same-radius : eps = eps-prime)
  (bounded : analysis/close L eps x)
  → analysis/close L eps-prime x

analysis/close-additive :
  (L eps-left x M eps-right y : ℚ) (x-close : analysis/close L eps-left x)
  (y-close : analysis/close M eps-right y)
  → analysis/close (L + M) (eps-left + eps-right) (x + y)

analysis/limit-sum :
  (s t : ℕ → ℚ) (L M : ℚ) (Ms Mt : ℚ → ℕ) (s-converges : analysis/converges s L Ms)
  (t-converges : analysis/converges t M Mt)
  → analysis/converges (fun n => s n + t n) (L + M) (fun eps => algebra/nat-add (Ms eps) (Mt 0))