Reference · Signed rationals

rainbow.math.rational.signed.vector-sup-separation

Signed rationalssrc/rainbow/math/rational/signed/vector_sup_separation.clj0 definitions, 3 theorems

Zero separation for signed-list sup distance at fixed shape. Componentwise vector equivalence always implies zero sup distance. The converse needs `vector/same-shape`, because this truncating representation assigns zero distance when either list is empty. Together the directions give the exact fixed-dimension separation law. Native, kernel-checked, and axiom-free on D63.

Depends onmath.rational.signed.vector-sup-distancemath.linear.vector.shape-cancellation

vector/sup-distance-zero-of-equivalent :
  (left right : List ℚ) (same : vector/equivalent left right)
  → vector/sup-distance left right = 0

vector/equivalent-of-sup-distance-zero :
  (left right : List ℚ) (shape : vector/same-shape left right)
  (distance-zero : vector/sup-distance left right = 0)
  → vector/equivalent left right

vector/sup-distance-zero-iff-equivalent-same-shape :
  (left right : List ℚ) (shape : vector/same-shape left right)
  → proposition/conjunction (vector/sup-distance left right = 0 → vector/equivalent left right) (vector/equivalent left right → vector/sup-distance left right = 0)