Reference · Signed rationals

rainbow.math.rational.signed.absolute-reciprocal-times-self

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

B6f prerequisite: the multiplicative absolute reciprocal identity. signed/absolute-reciprocal-times-self : 1 <= num(mag(x*x)) -> |reciprocal x| * |x| ~ 1 This is the clean building block for the limit-reciprocal assembly's constant bound on |reciprocal (s n)|. Unlike the additive |1/x| ~ 1/|x| (which crosses magnitude representatives and hits the absent reciprocal-respects lemma), this multiplicative form stays representative-free: |1/x|*|x| ~ |x*(1/x)| ~ |1| ~ 1 via absolute-multiply + multiply-reciprocal-self + |1|~1. In the assembly, combined with |s n| >= |L|/2 and multiply-right-cancel, it yields |reciprocal (s n)| <= reciprocal(|L|/2) = 2/|L|. Axiom-free; additive; does not touch the LP checker.

Depends onmath.rational.signed.reciprocalmath.rational.signed.absolute-multiplymath.rational.signed.absolute-signmath.rational.signed.absolute-algebramath.rational.signed.multiply-ringmath.rational.signed.unit-laws

signed/absolute-reciprocal-times-self :
  (x : ℚ)
  (h : 1 ≤ nnrat/numerator (signed/magnitude (x · x)))
  → signed/absolute (signed/reciprocal x) · signed/absolute x = 1