Reference · Signed rationals

rainbow.math.rational.signed.absolute-algebra

Signed rationalssrc/rainbow/math/rational/signed/absolute_algebra.clj0 definitions, 5 theorems

Quotient-safe algebra for native signed absolute value. Signed rationals are Grothendieck pairs, so observable algebra is stated with `signed/equivalent`. This layer proves that lattice maximum and absolute value respect that equivalence, that absolute value ignores sign, normalizes zero, and is idempotent. These are the scalar well-definedness laws needed before defining signed distance and finite-vector sup metrics. Native, kernel-checked, and axiom-free on D63.

Depends onmath.rational.signed.absolutemath.rational.signed.limit-uniquenessmath.rational.signed.equivalence-laws

signed/max-respects-equivalence :
  (left right left-prime right-prime : ℚ)
  (same-left : left = left-prime)
  (same-right : right = right-prime)
  → signed/max left right = signed/max left-prime right-prime

signed/absolute-respects-equivalence :
  (left right : ℚ)
  (same : left = right)
  → signed/absolute left = signed/absolute right

signed/absolute-negate :
  (value : ℚ)
  → signed/absolute (signed/negate value) = signed/absolute value

signed/absolute-zero :
  → signed/absolute 0 = 0

signed/absolute-idempotent :
  (value : ℚ)
  → signed/absolute (signed/absolute value) = signed/absolute value