Reference · Signed rationals

rainbow.math.rational.signed.unit-laws

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

The unit and self-cancellation laws the signed layer was missing. Everything about `signed/one` and about `c - c` had to be re-derived by hand at every use site, because the signed layer carried no multiplicative identity and no self-subtraction law. All four proofs below are componentwise: a signed equivalence `a ~ b` IS the nnrat equivalence `Pa + Nb ~ Pb + Na`, so each one reduces to nnrat identity laws applied to the two Grothendieck components. signed/multiply-one-left 1 * z ~ z signed/subtract-self-equivalent-zero c - c ~ 0 signed/subtract-self-nonpositive c - c <= 0 signed/zero-at-most-one 0 <= 1 signed/equivalent-to-at-most a ~ b -> a <= b The last is worth naming: signed order and signed equivalence unfold to the nnrat order and nnrat equivalence of the SAME pair of cross sums, so the nnrat bridge transports directly, giving the signed one for free. Native and axiom-free; chains signed multiplication and the nnrat identity and additive-monotonicity laws on D63.

Depends onmath.rational.signed.multiplymath.rational.nnrat.add-monotonemath.rational.nnrat.identities

signed/equivalent-to-at-most :
  (a b : ℚ)
  (same : a = b)
  → a ≤ b

signed/multiply-one-left :
  (z : ℚ)
  → 1 · z = z

signed/subtract-self-equivalent-zero :
  (c : ℚ)
  → c - c = 0

signed/subtract-self-nonpositive :
  (c : ℚ)
  → c - c ≤ 0

signed/zero-at-most-one :
  → 0 ≤ 1