Reference · Matrices

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

Matricessrc/rainbow/math/linear/matrix/row_length_shape.clj2 definitions, 6 theorems

Bridges executable row-length evidence to abstract matrix shape certificates. Matrix algorithms use `vector/same-shape`, `matrix/compatible`, and `matrix/rectangular` because those propositions compose well in proofs. A parser or certificate checker, however, observes natural-number lengths. This module closes that boundary: equal vector lengths -> vector/same-shape every row has the reference length -> matrix/compatible every row has the reference length -> matrix/rectangular The empty/nonempty mismatch cases are eliminated with Nat no-confusion, not assumed. Native and axiom-free on D63.

Depends onmath.linear.matrix.composable

vector/length :
  (x₁ : List ℚ)
  → ℕ

matrix/row-length-compatible :
  (x₁ : List (List ℚ)) (x₂ : List ℚ)
  → Prop

vector/length-equality-implies-same-shape :
  (left right : List ℚ)
  (same-length : vector/length left = vector/length right)
  → vector/same-shape left right

vector/same-shape-implies-length-equality :
  (left right : List ℚ) (same : vector/same-shape left right)
  → vector/length left = vector/length right

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

matrix/compatible-implies-row-length-compatible :
  (rows : List (List ℚ)) (values : List ℚ)
  (shape-certificate : matrix/compatible rows values)
  → matrix/row-length-compatible rows values

matrix/row-length-compatible-implies-rectangular :
  (rows : List (List ℚ)) (values : List ℚ)
  (length-certificate : matrix/row-length-compatible rows values)
  → matrix/rectangular rows

matrix/rectangular-implies-head-row-length-compatible :
  (head : List ℚ) (tail : List (List ℚ))
  (shape-certificate : matrix/rectangular (data/cons (List ℚ) head tail))
  → matrix/row-length-compatible (data/cons (List ℚ) head tail) head