Weighted rectangle covers of identity flattenings

Every rectangle cover of the nonzero support of an identity matrix has total weight at least the matrix dimension, where a rectangle's weight is the smaller of its row and column cardinalities. If every rectangle has weight at most r, this gives the count bound ceil(dimension / r).

The middle Boolean layer turns these statements into central-binomial and explicit exponential lower bounds for two-dimensional covers.

theorem Algebraic.Fusion.SumOfTerms.MatrixRank.Cover.Identity.card_le_rankBudget {K I : Type} [Field K] [Fintype I] [DecidableEq I] (certificate : Certificate 1) : Fintype.card I ≤ certificate.rankBudget

Weighted size of every rectangle cover of an identity matrix is at least the matrix dimension.

theorem Algebraic.Fusion.SumOfTerms.MatrixRank.Cover.Identity.rankBudget_le_rectangleCount_mul_capacity {K I : Type} [Field K] [DecidableEq I] (certificate : Certificate 1) (capacity : ℕ) (bounded : ∀ (index : Fin certificate.rectangleCount), min (certificate.rows index).card (certificate.columns index).card ≤ capacity) : certificate.rankBudget ≤ certificate.rectangleCount * capacity

A uniform per-rectangle capacity bounds total cover weight by rectangle count times capacity.

theorem Algebraic.Fusion.SumOfTerms.MatrixRank.Cover.Identity.card_le_rectangleCount_mul_capacity {K I : Type} [Field K] [Fintype I] [DecidableEq I] (certificate : Certificate 1) (capacity : ℕ) (bounded : ∀ (index : Fin certificate.rectangleCount), min (certificate.rows index).card (certificate.columns index).card ≤ capacity) : Fintype.card I ≤ certificate.rectangleCount * capacity

Identity dimension is bounded by rectangle count times a uniform local capacity.

theorem Algebraic.Fusion.SumOfTerms.MatrixRank.Cover.Identity.card_ceilDiv_le_rectangleCount {K I : Type} [Field K] [Fintype I] [DecidableEq I] (certificate : Certificate 1) (capacity : ℕ) (capacityPositive : 0 < capacity) (bounded : ∀ (index : Fin certificate.rectangleCount), min (certificate.rows index).card (certificate.columns index).card ≤ capacity) : Fintype.card I ⌈/⌉ capacity ≤ certificate.rectangleCount

Ceiling-divided rectangle-count lower bound.

theorem Algebraic.Fusion.SumOfTerms.MatrixRank.Cover.Identity.centralBinom_le_rankBudget {K : Type} [Field K] (n : ℕ) (certificate : Certificate 1) : n.centralBinom ≤ certificate.rankBudget

Middle-layer rectangle covers have central-binomial weighted size.

theorem Algebraic.Fusion.SumOfTerms.MatrixRank.Cover.Identity.centralBinom_ceilDiv_le_rectangleCount {K : Type} [Field K] (n : ℕ) (certificate : Certificate 1) (capacity : ℕ) (capacityPositive : 0 < capacity) (bounded : ∀ (index : Fin certificate.rectangleCount), min (certificate.rows index).card (certificate.columns index).card ≤ capacity) : n.centralBinom ⌈/⌉ capacity ≤ certificate.rectangleCount

Uniform-capacity middle-layer rectangle covers need at least the ceiling-divided central binomial number of rectangles.

theorem Algebraic.Fusion.SumOfTerms.MatrixRank.Cover.Identity.four_pow_lt_n_mul_rankBudget {K : Type} [Field K] (n : ℕ) (nBig : 4 ≤ n) (certificate : Certificate 1) : 4 ^ n < n * certificate.rankBudget

Explicit exponential lower bound on total middle-layer cover weight.

theorem Algebraic.Fusion.SumOfTerms.MatrixRank.Cover.Identity.four_pow_lt_n_mul_rectangleCount_mul_capacity {K : Type} [Field K] (n : ℕ) (nBig : 4 ≤ n) (certificate : Certificate 1) (capacity : ℕ) (bounded : ∀ (index : Fin certificate.rectangleCount), min (certificate.rows index).card (certificate.columns index).card ≤ capacity) : 4 ^ n < n * (certificate.rectangleCount * capacity)

Explicit exponential count/capacity tradeoff for middle-layer rectangle covers.