Reference · Signed rationals

rainbow.math.rational.signed.reciprocal-difference

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

The reciprocal-difference identity: the algebraic heart of the limit-reciprocal law. signed/reciprocal-difference : 1 <= num(mag(a*a)) -> 1 <= num(mag(b*b)) -> (reciprocal a - reciprocal b) ~ (reciprocal a * reciprocal b) * (b - a) This turns a difference of reciprocals into a product with (b - a), so the distance d(1/(s n), 1/L) can be bounded by d(s n, L) times a factor -- the step that makes the reciprocal sequence's modulus computable. Pure signed-field algebra; no analysis. Proof: expand X*(b-a) = X*b - X*a (distributes-add-left + multiply-negate-right), with X = 1/a * 1/b; then X*b ~ 1/a (assoc, commute, b*(1/b)~1 via multiply-reciprocal-self, one laws) and X*a ~ 1/b symmetrically; subtract-respects assembles it. Axiom-free; additive; does not touch the LP checker.

Depends onmath.rational.signed.reciprocalmath.rational.signed.unit-lawsmath.linear.matrix.action-scalemath.linear.vector.dot-negatemath.rational.signed.map-sum-algebramath.linear.vector.dot-subtract

signed/reciprocal-difference :
  (a b : ℚ)
  (ha : 1 ≤ nnrat/numerator (signed/magnitude (a · a)))
  (hb : 1 ≤ nnrat/numerator (signed/magnitude (b · b)))
  → signed/reciprocal a - signed/reciprocal b = signed/reciprocal a · signed/reciprocal b · (b - a)