Reference · Signed rationals

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

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

Quotient-safe congruence of signed-list sup distance. Componentwise equivalent replacements on either argument preserve the truncating finite sup distance. The left law is structural: equivalent lists have matching constructors, scalar distance transports equivalent heads, and the induction hypothesis transports tails. Symmetry derives the right law, and transitivity composes the two-sided law. No shape hypothesis is needed because each vector-equivalence proof already preserves the shape of the argument it replaces. Native, kernel-checked, and axiom-free on D63.

Depends onmath.rational.signed.vector-sup-distancemath.linear.vector.equivalence

vector/sup-distance-left-respects-equivalence :
  (left left-prime right : List ℚ) (same : vector/equivalent left left-prime)
  → vector/sup-distance left right = vector/sup-distance left-prime right

vector/sup-distance-right-respects-equivalence :
  (left right right-prime : List ℚ) (same : vector/equivalent right right-prime)
  → vector/sup-distance left right = vector/sup-distance left right-prime

vector/sup-distance-respects-equivalence :
  (left left-prime right right-prime : List ℚ)
  (left-same : vector/equivalent left left-prime)
  (right-same : vector/equivalent right right-prime)
  → vector/sup-distance left right = vector/sup-distance left-prime right-prime