Reference · Matrices

rainbow.math.linear.matrix.gram-kernel

Matricessrc/rainbow/math/linear/matrix/gram_kernel.clj0 definitions, 5 theorems

The zero kernel of the native Gram quadratic form. A signed vector has zero self-dot exactly when it is componentwise equivalent to its shape-preserving zero vector. Combining this reflection with the Gram identity proves both directions between a zero Gram quadratic and Ax being zero, then packages them as one conjunction of implications. Dependency activation reuses the existing norm-zero development conditionally, avoiding competing aliases. Native and axiom-free on D63.

Depends onmath.linear.matrix.gram-positive

vector/dot-self-zero-of-equivalent-zero-like :
  (values : List ℚ)
  (zero-equivalent : vector/equivalent values (vector/zero-like values))
  → vector/dot values values = 0

vector/dot-self-zero-reflects :
  (values : List ℚ)
  (self-zero : vector/dot values values = 0)
  → vector/equivalent values (vector/zero-like values)

matrix/gram-action-zero-of-null :
  (rows : List (List ℚ)) (values : List ℚ)
  (rows-compatible : matrix/compatible rows values)
  (image-zero : vector/equivalent (matrix/vector-multiply rows values) (vector/zero-like (matrix/vector-multiply rows values)))
  → vector/dot (multiply) values = 0
  where multiply := matrix/vector-multiply (matrix/transpose rows) (matrix/vector-multiply rows values)

matrix/gram-action-zero-reflects-null :
  (rows : List (List ℚ)) (values : List ℚ)
  (rows-compatible : matrix/compatible rows values)
  (gram-zero : vector/dot (multiply) values = 0)
  → vector/equivalent (matrix/vector-multiply rows values) (vector/zero-like (matrix/vector-multiply rows values))
  where multiply := matrix/vector-multiply (matrix/transpose rows) (matrix/vector-multiply rows values)

matrix/gram-action-zero-characterizes-null :
  (rows : List (List ℚ)) (values : List ℚ)
  (rows-compatible : matrix/compatible rows values)
  → proposition/conjunction (dot = 0 → equivalent) (equivalent → dot = 0)
  where dot := vector/dot (matrix/vector-multiply (matrix/transpose rows) (matrix/vector-multiply rows values)) values
  where equivalent := vector/equivalent (matrix/vector-multiply rows values) (vector/zero-like (matrix/vector-multiply rows values))