Reference · Matrices

rainbow.math.linear.matrix.row-length-decider

Matricessrc/rainbow/math/linear/matrix/row_length_decider.clj1 definitions, 8 theorems

Executable, sound dimension checking for finite signed matrices. `matrix/decide-row-length-compatible` computes one Boolean by comparing each row's exact natural length with the reference vector's length. A successful result is converted, inside the kernel, into the abstract certificates used by matrix and LP theorems: decision = true -> row-length-compatible -> compatible -> rectangular. This is output verification for the dimension check. It does not prove a host Clojure parser or arbitrary executable correct, and it does not inspect matrix entries. Native and axiom-free on D63.

Depends onmath.linear.matrix.row-length-shape

matrix/decide-row-length-compatible :
  (x₁ : List (List ℚ)) (x₂ : List ℚ)
  → data/Bool

nat/decide-equality-true-sound :
  (left right : ℕ)
  (decided : nat/decide-equality left right = data/true)
  → left = right

matrix/decide-row-length-compatible-true-sound :
  (rows : List (List ℚ)) (values : List ℚ)
  (decided : matrix/decide-row-length-compatible rows values = data/true)
  → matrix/row-length-compatible rows values

nat/decide-equality-reflexive-true :
  (value : ℕ)
  → nat/decide-equality value value = data/true

nat/equality-implies-decide-equality-true :
  (left right : ℕ)
  (same : left = right)
  → nat/decide-equality left right = data/true

boolean/and-true-introduction :
  (left right : data/Bool)
  (left-true : left = data/true)
  (right-true : right = data/true)
  → boolean/and left right = data/true

matrix/row-length-compatible-implies-decide-true :
  (rows : List (List ℚ)) (values : List ℚ)
  (certificate : matrix/row-length-compatible rows values)
  → matrix/decide-row-length-compatible rows values = data/true

matrix/decide-row-length-compatible-true-implies-compatible :
  (rows : List (List ℚ)) (values : List ℚ)
  (decided : matrix/decide-row-length-compatible rows values = data/true)
  → matrix/compatible rows values

matrix/decide-row-length-compatible-true-implies-rectangular :
  (rows : List (List ℚ)) (values : List ℚ)
  (decided : matrix/decide-row-length-compatible rows values = data/true)
  → matrix/rectangular rows