Reference · Signed rationals

rainbow.math.rational.signed.recovery-laws

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

Two general signed-rational laws that the corpus lacked, proved en route to the Gauss-Seidel exactness theorem and promoted here so any module can reuse them without depending on an application module. - signed/subtract-then-add: the recovery law (a - b) + b ~ a. The corpus had only signed/subtract-add-left ((p+l)-(p+r) ~ l-r), a different statement; this is the plain recover-the-minuend law. - signed/reciprocal-scale-cancel: for a positive rate make(succ p) q, scaling by the reciprocal then the value is the identity, scale(d, scale(reciprocal d, v)) ~ v. Native, kernel-checked, and axiom-free on D63.

Depends onmath.rational.division

signed/subtract-then-add :
  (a b : ℚ)
  → a - b + b = a

signed/reciprocal-scale-cancel :
  (p q : ℕ) (value : ℚ)
  → signed/scale (nnrat/make (data/succ p) q) (scale) = value
  where scale := signed/scale (nnrat/reciprocal (nnrat/make (data/succ p) q)) value