Block decompositions of matrix flattenings

A matrix block comes with finite row and column covers. Its rank is bounded by the smaller cover size. If a matrix is a finite sum of such blocks, rank subadditivity bounds its rank by the sum of those block budgets.

This witness-oriented interface is deliberately independent of how the blocks are obtained. Later polynomial adapters may use monomial partitions, rectangle covers, or semantic decompositions without changing the linear algebra layer.

structure Algebraic.Fusion.SumOfTerms.MatrixRank.Block.Piece (K I J : Type) [Field K] [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] : Type

A matrix together with certified finite covers of its nonzero rows and columns.

• matrix : Matrix I J K

  Matrix represented by this block.

• rows : Finset I

  Rows allowed to contain nonzero entries.

• columns : Finset J

  Columns allowed to contain nonzero entries.

• rows_supported : Function.support self.matrix.row ⊆ ↑self.rows

  Every nonzero row lies in rows.

• columns_supported : Function.support self.matrix.col ⊆ ↑self.columns

  Every nonzero column lies in columns.

def Algebraic.Fusion.SumOfTerms.MatrixRank.Block.Piece.rankBudget {K I J : Type} [Field K] [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] (piece : Piece K I J) : ℕ

Rank budget charged to one supported block.

Equations

• piece.rankBudget = min piece.rows.card piece.columns.card

theorem Algebraic.Fusion.SumOfTerms.MatrixRank.Block.Piece.rank_toLin'_le_rankBudget {K I J : Type} [Field K] [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] (piece : Piece K I J) : (Matrix.toLin' piece.matrix).rank ≤ ↑piece.rankBudget

A supported block has rank at most its smaller side.

noncomputable def Algebraic.Fusion.SumOfTerms.MatrixRank.Block.Piece.ofMatrix {K I J : Type} [Field K] [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] (matrix : Matrix I J K) : Piece K I J

The canonical single block using the exact nonzero row and column supports of a matrix.

Equations

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

@[simp]

theorem Algebraic.Fusion.SumOfTerms.MatrixRank.Block.Piece.ofMatrix_rankBudget {K I J : Type} [Field K] [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] (matrix : Matrix I J K) : (ofMatrix matrix).rankBudget = min (Support.rowSupport matrix).card (Support.columnSupport matrix).card

structure Algebraic.Fusion.SumOfTerms.MatrixRank.Block.Decomposition {K I J : Type} [Field K] [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] (matrix : Matrix I J K) : Type

A finite additive decomposition into supported matrix blocks.

• blockCount : ℕ

  Number of block occurrences.

• block : Fin self.blockCount → Piece K I J

  The blocks, counted with multiplicity.

• sum_eq : ∑ index : Fin self.blockCount, (self.block index).matrix = matrix

  Their matrix sum is the represented matrix.

def Algebraic.Fusion.SumOfTerms.MatrixRank.Block.Decomposition.rankBudget {K I J : Type} [Field K] [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] {matrix : Matrix I J K} (decomposition : Decomposition matrix) : ℕ

Sum of the smaller-side budgets of all block occurrences.

Equations

• decomposition.rankBudget = ∑ index : Fin decomposition.blockCount, (decomposition.block index).rankBudget

theorem Algebraic.Fusion.SumOfTerms.MatrixRank.Block.Decomposition.rank_toLin'_le_rankBudget {K I J : Type} [Field K] [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] {matrix : Matrix I J K} (decomposition : Decomposition matrix) : (Matrix.toLin' matrix).rank ≤ ↑decomposition.rankBudget

Rank subadditivity converts a block decomposition into a flattening-rank bound.

def Algebraic.Fusion.SumOfTerms.MatrixRank.Block.Decomposition.zero {K I J : Type} [Field K] [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] : Decomposition 0

Empty decomposition of the zero matrix.

Equations

• Algebraic.Fusion.SumOfTerms.MatrixRank.Block.Decomposition.zero = { blockCount := 0, block := Fin.elim0, sum_eq := ⋯ }

@[simp]

theorem Algebraic.Fusion.SumOfTerms.MatrixRank.Block.Decomposition.zero_rankBudget {K I J : Type} [Field K] [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] : zero.rankBudget = 0

@[reducible, inline]

abbrev Algebraic.Fusion.SumOfTerms.MatrixRank.Block.Decomposition.add {K I J : Type} [Field K] [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] {left right : Matrix I J K} (leftDecomposition : Decomposition left) (rightDecomposition : Decomposition right) : Decomposition (left + right)

Concatenate decompositions to represent the sum of their matrices.

Equations

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

@[simp]

theorem Algebraic.Fusion.SumOfTerms.MatrixRank.Block.Decomposition.add_rankBudget {K I J : Type} [Field K] [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] {left right : Matrix I J K} (leftDecomposition : Decomposition left) (rightDecomposition : Decomposition right) : (leftDecomposition.add rightDecomposition).rankBudget = leftDecomposition.rankBudget + rightDecomposition.rankBudget

noncomputable def Algebraic.Fusion.SumOfTerms.MatrixRank.Block.Decomposition.single {K I J : Type} [Field K] [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] (matrix : Matrix I J K) : Decomposition matrix

Every matrix has the one-block decomposition given by its exact row and column supports.

Equations

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

@[simp]

theorem Algebraic.Fusion.SumOfTerms.MatrixRank.Block.Decomposition.single_rankBudget {K I J : Type} [Field K] [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] (matrix : Matrix I J K) : (single matrix).rankBudget = min (Support.rowSupport matrix).card (Support.columnSupport matrix).card