def Hex.Matrix.principalSubmatrix {R : Type u_1} {n : Nat} (M : Matrix R n n) (k : Nat) (hk : k ≤ n) : Matrix R k k

Leading principal k × k submatrix of a square matrix: the top-left block indexed by {0, …, k-1} along both axes. Includes the empty submatrix (k = 0) and is convenient for Bareiss pivot/minor statements.

Equations

• M.principalSubmatrix k hk = Hex.Matrix.ofFn fun (i j : Fin k) => have ii := ⟨↑i, ⋯⟩; have jj := ⟨↑j, ⋯⟩; M[(ii, jj)]

def Hex.Matrix.takeRows {R : Type u_1} {n m : Nat} (M : Matrix R n m) (k : Nat) (hk : k ≤ n) : Matrix R k m

The first k rows of a matrix, retaining all source columns.

Equations

• M.takeRows k hk = Hex.Matrix.ofFn fun (i : Fin k) (j : Fin m) => have ii := ⟨↑i, ⋯⟩; M[(ii, j)]

theorem Hex.Matrix.getElem_principalSubmatrix {R : Type u_1} {n : Nat} (M : Matrix R n n) (k : Nat) (hk : k ≤ n) (i j : Fin k) : (M.principalSubmatrix k hk)[i][j] = have ii := ⟨↑i, ⋯⟩; let jj := ⟨↑j, ⋯⟩; M[ii][jj]

Entry formula for the k × k principal submatrix.

@[simp]

theorem Hex.Matrix.row_principalSubmatrix {R : Type u_1} {n : Nat} (M : Matrix R n n) (k : Nat) (hk : k ≤ n) (i : Fin k) : (M.principalSubmatrix k hk).row i = Vector.ofFn fun (j : Fin k) => have ii := ⟨↑i, ⋯⟩; let jj := ⟨↑j, ⋯⟩; M[ii][jj]

Row i of the k × k principal submatrix is row i of M, restricted to the first k columns.

@[simp]

theorem Hex.Matrix.col_principalSubmatrix {R : Type u_1} {n : Nat} (M : Matrix R n n) (k : Nat) (hk : k ≤ n) (j : Fin k) : (M.principalSubmatrix k hk).col j = Vector.ofFn fun (i : Fin k) => have ii := ⟨↑i, ⋯⟩; let jj := ⟨↑j, ⋯⟩; M[ii][jj]

Column j of the k × k principal submatrix is column j of M, restricted to the first k rows.

def Hex.Matrix.takeCols {R : Type u_1} {n m : Nat} (M : Matrix R n m) (k : Nat) (hk : k ≤ m) : Matrix R n k

The first k columns of a matrix, retaining all source rows.

Equations

• M.takeCols k hk = Hex.Matrix.ofFn fun (i : Fin n) (j : Fin k) => have jj := ⟨↑j, ⋯⟩; M[(i, jj)]

theorem Hex.Matrix.getElem_takeRows {R : Type u_1} {n m : Nat} (M : Matrix R n m) (k : Nat) (hk : k ≤ n) (i : Fin k) (j : Fin m) : (M.takeRows k hk)[i][j] = have ii := ⟨↑i, ⋯⟩; M[ii][j]

Entry formula for the first-k-rows slice.

theorem Hex.Matrix.getElem_takeCols {R : Type u_1} {n m : Nat} (M : Matrix R n m) (k : Nat) (hk : k ≤ m) (i : Fin n) (j : Fin k) : (M.takeCols k hk)[i][j] = let jj := ⟨↑j, ⋯⟩; M[i][jj]

Entry formula for the first-k-columns slice.

@[simp]

theorem Hex.Matrix.principalSubmatrix_identity {R : Type u} [OfNat R 0] [OfNat R 1] {n : Nat} (k : Nat) (hk : k ≤ n) : (Matrix.identity n).principalSubmatrix k hk = Matrix.identity k

The leading principal k × k submatrix of the identity is the identity.

structure Hex.Submatrix (R : Type u) (rows cols : Nat) : Type u

A copy-free view of a rows × cols block, possibly zero-padded past its real-data extent, into a shared backing Matrix R N M. Reading (i, j) returns base[(r0 + i, c0 + j)] when r0 + i < rhi ∧ c0 + j < chi (real data) and 0 otherwise (pad). The invariants pin the window endpoints inside the backing and inside the logical block, so the real data is a prefix of each axis. There is deliberately no r0 ≤ rhi invariant: a reversed window (rhi ≤ r0) is the canonical empty-window encoding — every real-data test is false and the view denotes an all-zero block, which is exactly what a quadrant lying wholly in the pad fringe needs.

• baseRows : Nat

  Backing row count.

• baseCols : Nat

  Backing column count.

• base : Matrix R self.baseRows self.baseCols

  Shared backing buffer; sub-views alias it, never copy it.

• r0 : Nat

  Row offset into the backing.

• c0 : Nat

  Column offset into the backing.

• rhi : Nat

  One past the last real-data row (backing coordinate).

• chi : Nat

  One past the last real-data column (backing coordinate).

• hrN : self.rhi ≤ self.baseRows

  Real rows stay inside the backing.

• hcM : self.chi ≤ self.baseCols

  Real columns stay inside the backing.

• hrR : self.rhi ≤ self.r0 + rows

  Real rows are a prefix of the logical rows.

• hcC : self.chi ≤ self.c0 + cols

  Real columns are a prefix of the logical columns.

def Hex.Submatrix.entry {R : Type u} {rows cols : Nat} [OfNat R 0] (A : Submatrix R rows cols) (i : Fin rows) (j : Fin cols) : R

Read entry (i, j) of a view: the flat backing read at (r0 + i, c0 + j) inside the real-data window, 0 in the zero-pad fringe.

Equations

• A.entry i j = if h : A.r0 + ↑i < A.rhi ∧ A.c0 + ↑j < A.chi then A.base[(A.r0 + ↑i, A.c0 + ↑j)] else 0

def Hex.Submatrix.toMatrix {R : Type u} {rows cols : Nat} [OfNat R 0] (A : Submatrix R rows cols) : Matrix R rows cols

Materialize a view into a genuine Matrix (a copy of the block, with the zero-pad fringe filled in). This is the leaf/operand allocation the recursion pays; interior quadrants stay views.

Equations

• A.toMatrix = Hex.Matrix.ofFn fun (i : Fin rows) (j : Fin cols) => A.entry i j

@[simp]

theorem Hex.Submatrix.getElem_toMatrix {R : Type u} {rows cols : Nat} [OfNat R 0] (A : Submatrix R rows cols) (i : Fin rows) (j : Fin cols) : A.toMatrix[i][j] = A.entry i j

Entry access of a materialized view is the view read.

def Hex.Submatrix.ofMatrix {R : Type u} {n m : Nat} (Mx : Matrix R n m) : Submatrix R n m

The full-matrix view of a Matrix: offset 0, real extent the whole matrix.

Equations

• Hex.Submatrix.ofMatrix Mx = { baseRows := n, baseCols := m, base := Mx, r0 := 0, c0 := 0, rhi := n, chi := m, hrN := ⋯, hcM := ⋯, hrR := ⋯, hcC := ⋯ }

@[simp]

theorem Hex.Submatrix.entry_ofMatrix {R : Type u} {n m : Nat} [OfNat R 0] (Mx : Matrix R n m) (i : Fin n) (j : Fin m) : (ofMatrix Mx).entry i j = Mx[i][j]

Reading the full-matrix view is reading the matrix.

@[simp]

theorem Hex.Submatrix.toMatrix_ofMatrix {R : Type u} {n m : Nat} [OfNat R 0] (Mx : Matrix R n m) : (ofMatrix Mx).toMatrix = Mx

Materializing the full-matrix view returns the matrix.

def Hex.Submatrix.pad {R : Type u} {n m : Nat} (A : Submatrix R n m) (n' m' : Nat) (hn : n ≤ n') (hm : m ≤ m') : Submatrix R n' m'

Widen a view's logical shape to n' × m' (n ≤ n', m ≤ m') without copying: the real-data window is unchanged, so the new fringe reads 0. This is the zero-padding the Strassen recursion applies before splitting.

Equations

• A.pad n' m' hn hm = { baseRows := A.baseRows, baseCols := A.baseCols, base := A.base, r0 := A.r0, c0 := A.c0, rhi := A.rhi, chi := A.chi, hrN := ⋯, hcM := ⋯, hrR := ⋯, hcC := ⋯ }

theorem Hex.Submatrix.entry_pad {R : Type u} {n m : Nat} [OfNat R 0] (A : Submatrix R n m) (n' m' : Nat) (hn : n ≤ n') (hm : m ≤ m') (i : Fin n') (j : Fin m') : (A.pad n' m' hn hm).entry i j = if h : ↑i < n ∧ ↑j < m then A.entry ⟨↑i, ⋯⟩ ⟨↑j, ⋯⟩ else 0

Reading a widened view agrees with the source view inside the source shape.

def Hex.Submatrix.toBlocks₁₁ {R : Type u} {h w : Nat} (A : Submatrix R (h + h) (w + w)) : Submatrix R h w

Top-left h × w quadrant of an (h+h) × (w+w) view: same offset, real extent capped at the block boundary. No copy.

Equations

• One or more equations did not get rendered due to their size.

def Hex.Submatrix.toBlocks₁₂ {R : Type u} {h w : Nat} (A : Submatrix R (h + h) (w + w)) : Submatrix R h w

Top-right h × w quadrant of an (h+h) × (w+w) view. No copy.

Equations

• A.toBlocks₁₂ = { baseRows := A.baseRows, baseCols := A.baseCols, base := A.base, r0 := A.r0, c0 := A.c0 + w, rhi := min A.rhi (A.r0 + h), chi := A.chi, hrN := ⋯, hcM := ⋯, hrR := ⋯, hcC := ⋯ }

def Hex.Submatrix.toBlocks₂₁ {R : Type u} {h w : Nat} (A : Submatrix R (h + h) (w + w)) : Submatrix R h w

Bottom-left h × w quadrant of an (h+h) × (w+w) view. No copy.

Equations

• A.toBlocks₂₁ = { baseRows := A.baseRows, baseCols := A.baseCols, base := A.base, r0 := A.r0 + h, c0 := A.c0, rhi := A.rhi, chi := min A.chi (A.c0 + w), hrN := ⋯, hcM := ⋯, hrR := ⋯, hcC := ⋯ }

def Hex.Submatrix.toBlocks₂₂ {R : Type u} {h w : Nat} (A : Submatrix R (h + h) (w + w)) : Submatrix R h w

Bottom-right h × w quadrant of an (h+h) × (w+w) view. No copy.

Equations

• A.toBlocks₂₂ = { baseRows := A.baseRows, baseCols := A.baseCols, base := A.base, r0 := A.r0 + h, c0 := A.c0 + w, rhi := A.rhi, chi := A.chi, hrN := ⋯, hcM := ⋯, hrR := ⋯, hcC := ⋯ }

def Hex.Submatrix.add {R : Type u} {rows cols : Nat} [Add R] [OfNat R 0] (A B : Submatrix R rows cols) : Submatrix R rows cols

Entrywise sum of two views, materialized into a fresh matrix (an operand-sum allocation).

Equations

• A.add B = Hex.Submatrix.ofMatrix (Hex.Matrix.ofFn fun (i : Fin rows) (j : Fin cols) => A.entry i j + B.entry i j)

def Hex.Submatrix.sub {R : Type u} {rows cols : Nat} [Sub R] [OfNat R 0] (A B : Submatrix R rows cols) : Submatrix R rows cols

Entrywise difference of two views, materialized into a fresh matrix.

Equations

• A.sub B = Hex.Submatrix.ofMatrix (Hex.Matrix.ofFn fun (i : Fin rows) (j : Fin cols) => A.entry i j - B.entry i j)

@[simp]

theorem Hex.Submatrix.toMatrix_add {R : Type u} {rows cols : Nat} [Add R] [OfNat R 0] (A B : Submatrix R rows cols) : (A.add B).toMatrix = A.toMatrix + B.toMatrix

Materializing a view sum is the matrix sum of the materializations.

@[simp]

theorem Hex.Submatrix.toMatrix_sub {R : Type u} {rows cols : Nat} [Sub R] [OfNat R 0] (A B : Submatrix R rows cols) : (A.sub B).toMatrix = A.toMatrix - B.toMatrix

Materializing a view difference is the matrix difference of the materializations.