Reference · Vectors

rainbow.math.linear.vector.norm-congruence

Vectorssrc/rainbow/math/linear/vector/norm_congruence.clj0 definitions, 2 theorems

Quotient-safe congruence laws for native squared norms and norm witnesses. norm/norm-squared-respects-equivalence norm/is-norm-respects-vector-equivalence Vector equivalence is length-sensitive and componentwise. A two-List induction transports each head square through signed multiplication congruence and each tail norm through the induction hypothesis. Any exact norm witness then transports by signed equivalence transitivity.

Depends onmath.linear.vector.norm-expansion

norm/norm-squared-respects-equivalence :
  (left right : List ℚ) (same : vector/equivalent left right)
  → norm/norm-squared left = norm/norm-squared right

norm/is-norm-respects-vector-equivalence :
  (left right : List ℚ) (candidate : ℚ) (same : vector/equivalent left right)
  (witness : norm/is-norm left candidate)
  → norm/is-norm right candidate