Reference · Signed rationals

rainbow.math.rational.signed.multiply

Signed rationalssrc/rainbow/math/rational/signed/multiply.clj1 definitions, 3 theorems

Signed-rational multiplication, extending the addition-only signed rationals. A signed rational is a Grothendieck pair (positive, negative); the product is (p1, n1) * (p2, n2) = (p1*p2 + n1*n2, p1*n2 + n1*p2) which is the usual sign rule expressed on the pair, built from nonnegative rational multiplication and addition without any new kernel rule. Worked values are proved on the signed cross-product equivalence (`signed/equivalent`), so they discharge by reflexivity on the reduced nat cross-product. This unblocks inner products, so dot-product and hypergradient methods become expressible.

signed/multiply :
  (x₁ x₂ : ℚ)
  → ℚ

signed/multiply-unfold :
  (left right : ℚ)
  → left · right = signed/make (signed/positive left · signed/positive right + signed/negative left · signed/negative right) (signed/positive left · signed/negative right + signed/negative left · signed/positive right)

signed/multiply-two-times-three :
  → signed/from-nnrat 2 · signed/from-nnrat 3 = signed/from-nnrat 6

signed/multiply-negative-two-times-three :
  → -2 · signed/from-nnrat 3 = -6