Reference · Matrices

rainbow.math.linear.matrix.transpose-involution-positive

Matricessrc/rainbow/math/linear/matrix/transpose_involution_positive.clj0 definitions, 2 theorems

Transpose involution for rectangular matrices of positive width. Positive width is carried constructively by exposing the first row as `head :: tail`; no separate Boolean or existential certificate is needed. A nested-insertion lemma shows how transpose recovers the leading row. Tail induction then proves double transpose matrix-equivalent to the input for every rectangular matrix with a nonempty first row. This is the strongest valid theorem for the row-list representation: nonempty zero-width matrices lose their row count under transpose. Native and axiom-free on D63.

Depends onmath.linear.matrix.transpose-involution

matrix/transpose-prepend-column-after-prepend :
  (head : ℚ) (tail : List ℚ) (next-head : ℚ) (next-tail : List ℚ)
  (columns : List (List ℚ)) (row-tails-shape : vector/same-shape tail next-tail)
  → matrix/equivalent (matrix/transpose (column)) (cons)
  where column := matrix/prepend-column (data/cons ℚ head tail) (matrix/prepend-column (data/cons ℚ next-head next-tail) columns)
  where cons := data/cons (List ℚ) (data/cons ℚ head tail) (matrix/transpose (matrix/prepend-column (data/cons ℚ next-head next-tail) columns))

matrix/transpose-involutive-nonempty-width :
  (head : ℚ) (row-tail : List ℚ) (tail : List (List ℚ))
  (rows-rectangular : matrix/rectangular (cons))
  → matrix/equivalent (matrix/transpose (matrix/transpose (cons))) (cons)
  where cons := data/cons (List ℚ) (data/cons ℚ head row-tail) tail