Reference · Signed rationals

rainbow.math.rational.signed.absolute-reciprocal

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

B5 of the limit-reciprocal arc: the absolute value of a reciprocal, kept through the SAME magnitude(x*x) representative (avoids the absent magnitude-respects / nnrat reciprocal-respects lemmas -- the nnrat-radius-cancel philosophy). signed/absolute-reciprocal : |reciprocal x| ~ |x| * (from-nnrat (recip mmag)) where mmag = make (succ (pred (num (magnitude (x*x))))) (den-pred (magnitude (x*x))), so the RHS is exactly |x| * (1/(x*x)). Since reciprocal x = x * (1/(x*x)) and 1/(x*x) = from-nnrat(recip mmag) is nonnegative, |reciprocal x| = |x * (1/(x*x))| ~ |x| * |1/(x*x)| ~ |x| * (1/(x*x)) [absolute-multiply + absolute-of-nonnegative]. No nonzero hypothesis needed (holds structurally for all x). The assembly bounds 1/(x*x) via the antitone lemma applied to mag(x*x) directly, never forming reciprocal|x|. Axiom-free; additive; does not touch the LP checker.

Depends onmath.rational.signed.reciprocalmath.rational.signed.absolute-multiplymath.rational.signed.absolute-signmath.rational.signed.multiply-ringmath.rational.signed.multiply-ordermath.rational.nnrat.farkas-elim-list

signed/absolute-reciprocal :
  (x : ℚ)
  → signed/absolute (signed/reciprocal x) = signed/absolute x · signed/from-nnrat (nnrat/reciprocal (data/pair ℕ ℕ (data/succ (nat/predecessor (nnrat/numerator (signed/magnitude (x · x))))) (nnrat/denominator-predecessor (signed/magnitude (x · x)))))