Reference · Signed rationals

rainbow.math.rational.signed.reciprocal

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

The signed-rational reciprocal operation and its self-inverse law -- the missing field operation. This completes the signed rationals as a field (up to ~) and is the gate for all signed division, including the limit-quotient law. signed/reciprocal x := x * (1 / (x*x)) [sign-free: 1/x = x/x^2] signed/multiply-reciprocal-self : 1 <= numerator (magnitude (x*x)) -> x * (reciprocal x) ~ one The definition is sign-free BY CONSTRUCTION: instead of a signum case-split, it uses 1/x = x/x^2. Since x*x is always nonnegative (signed/square-nonnegative), its magnitude is a genuine nnrat and admits the make(succ p, q)-form reciprocal, so no reciprocal- respects lemma is needed. The nonzero hypothesis is `1 <= numerator (magnitude (x*x))` (equivalently x !~ 0): exactly the positive-numerator shape nnrat divide-self-positive and make-succ-of-positive-numerator consume. Proof of self-inverse: x*(x*R) ~ (x*x)*R [multiply-associative] ~ from-nnrat D * R [x*x ~ from-nnrat D, from-nnrat-magnitude] ~ from-nnrat (D * recip mmag) [from-nnrat-multiply] ~ from-nnrat one ~ one [D ~ mmag then divide-self-positive] where D = magnitude (x*x), mmag = make (succ (pred (num D))) (den-pred D), R = from-nnrat (recip mmag). Axiom-free; additive; does not touch the LP checker.

Depends onmath.rational.signed.multiply-associativemath.rational.signed.geometric-bridgemath.linear.vector.norm-nonnegativemath.rational.signed.magnitudemath.rational.nnrat.positive-succ-formmath.rational.signed.multiply-ringmath.rational.signed.equivalence-lawsmath.rational.divisionmath.nonnegative-rational

signed/reciprocal :
  (x₁ : ℚ)
  → ℚ

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