Reference · Matrices

rainbow.math.linear.matrix.signed-scale-congruence

Matricessrc/rainbow/math/linear/matrix/signed_scale_congruence.clj0 definitions, 9 theorems

Quotient congruence for signed scalar, vector, and matrix scaling. Signed rationals are Grothendieck representatives, so algebraic module laws are only reusable when scaling transports representative equivalence. This milestone proves factor congruence, value congruence, and their joint form for the scalar scale-difference operation, then lifts the same family through vectors and matrices. Native and axiom-free on D63.

Depends onmath.linear.matrix.signed-scale-units

signed/scale-difference-respects-factor-equivalence :
  (factor factor* value : ℚ)
  (same-factor : factor = factor*)
  → signed/scale (signed/positive factor) value - signed/scale (signed/negative factor) value = signed/scale (signed/positive factor*) value - signed/scale (signed/negative factor*) value

signed/scale-difference-respects-value-equivalence :
  (factor value value* : ℚ)
  (same-value : value = value*)
  → signed/scale (signed/positive factor) value - signed/scale (signed/negative factor) value = signed/scale (signed/positive factor) value* - signed/scale (signed/negative factor) value*

signed/scale-difference-respects-equivalence :
  (factor factor* value value* : ℚ)
  (same-factor : factor = factor*)
  (same-value : value = value*)
  → signed/scale (signed/positive factor) value - signed/scale (signed/negative factor) value = signed/scale (signed/positive factor*) value* - signed/scale (signed/negative factor*) value*

vector/signed-scale-respects-factor-equivalence :
  (factor factor* : ℚ) (values : List ℚ)
  (same-factor : factor = factor*)
  → vector/equivalent (vector/signed-scale factor values) (vector/signed-scale factor* values)

vector/signed-scale-respects-value-equivalence :
  (factor : ℚ) (left right : List ℚ) (same-values : vector/equivalent left right)
  → vector/equivalent (vector/signed-scale factor left) (vector/signed-scale factor right)

vector/signed-scale-respects-equivalence :
  (factor factor* : ℚ) (left right : List ℚ)
  (same-factor : factor = factor*)
  (same-values : vector/equivalent left right)
  → vector/equivalent (vector/signed-scale factor left) (vector/signed-scale factor* right)

matrix/signed-scale-respects-factor-equivalence :
  (factor factor* : ℚ) (rows : List (List ℚ))
  (same-factor : factor = factor*)
  → matrix/equivalent (matrix/signed-scale factor rows) (matrix/signed-scale factor* rows)

matrix/signed-scale-respects-value-equivalence :
  (factor : ℚ) (left right : List (List ℚ)) (same-values : matrix/equivalent left right)
  → matrix/equivalent (matrix/signed-scale factor left) (matrix/signed-scale factor right)

matrix/signed-scale-respects-equivalence :
  (factor factor* : ℚ) (left right : List (List ℚ))
  (same-factor : factor = factor*)
  (same-values : matrix/equivalent left right)
  → matrix/equivalent (matrix/signed-scale factor left) (matrix/signed-scale factor* right)