Matrix-flattening fusion lower bounds

The identity matrix has full rank, whereas an outer product has rank at most one. Instantiating the generic sum-of-terms rank certificate therefore proves that a circuit expressing an N × N identity flattening as a sum of charged rank-one terms needs at least N terms.

Taking the index set to be the middle layer of the Boolean lattice gives the explicit lower bound choose (2 * n) n. Mathlib's central-binomial estimate then makes the exponential growth formal.

structure Algebraic.Fusion.SumOfTerms.MatrixRank.Term (K I : Type u) : Type u

Parameters of one rank-one outer-product term.

• left : I → K

  Column vector of the outer product.

• right : I → K

  Row vector of the outer product.

def Algebraic.Fusion.SumOfTerms.MatrixRank.termValue {K I : Type u_1} [Mul K] (term : Term K I) : Matrix I I K

Matrix represented by a rank-one term.

Equations

• Algebraic.Fusion.SumOfTerms.MatrixRank.termValue term = Matrix.vecMulVec term.left term.right

@[reducible, inline]

abbrev Algebraic.Fusion.SumOfTerms.MatrixRank.identityProblem (K I : Type u) [Zero K] [One K] [DecidableEq I] : Problem (Matrix I I K)

Construct the identity matrix with no free inputs.

Equations

• Algebraic.Fusion.SumOfTerms.MatrixRank.identityProblem K I = { inputCount := 0, inputs := fun (input : Fin 0) => input.elim0, target := 1 }

theorem Algebraic.Fusion.SumOfTerms.MatrixRank.rank_termValue_le_one {K I : Type u} [Field K] [Fintype I] [DecidableEq I] (term : Term K I) : (Matrix.toLin' (termValue term)).rank ≤ 1

An outer-product term has flattening rank at most one.

theorem Algebraic.Fusion.SumOfTerms.MatrixRank.card_le_rank_identity (K I : Type u) [Field K] [Fintype I] [DecidableEq I] : ↑(Fintype.card I) ≤ (Matrix.toLin' 1).rank

The identity flattening has rank equal to the size of its index type.

noncomputable def Algebraic.Fusion.SumOfTerms.MatrixRank.identityCertificate (K I : Type u) [Field K] [Fintype I] [DecidableEq I] : RankCertificate termValue (identityProblem K I)

Matrix multiplication on vectors is the flattening feature.

Equations

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

@[simp]

theorem Algebraic.Fusion.SumOfTerms.MatrixRank.identityCertificate_targetRank (K I : Type u) [Field K] [Fintype I] [DecidableEq I] : (identityCertificate K I).targetRank = Fintype.card I

@[simp]

theorem Algebraic.Fusion.SumOfTerms.MatrixRank.identityCertificate_termRank (K I : Type u) [Field K] [Fintype I] [DecidableEq I] : (identityCertificate K I).termRank = 1

theorem Algebraic.Fusion.SumOfTerms.MatrixRank.identity_lowerBound {K I : Type u} [Field K] [Fintype I] [DecidableEq I] (circuit : Circuit (SumOfTerms.signature (Term K I)) 0 1) (constructs : (identityProblem K I).Constructs circuit (SumOfTerms.interpretation termValue)) : Fintype.card I ≤ circuit.cost SumOfTerms.termCost

Full matrix rank forces one charged term for every index.

@[reducible, inline]

abbrev Algebraic.Fusion.SumOfTerms.MatrixRank.Layer (n k : ℕ) : Type

The type of k-subsets of an n-element set.

Equations

• Algebraic.Fusion.SumOfTerms.MatrixRank.Layer n k = ↥(Finset.powersetCard k Finset.univ)

theorem Algebraic.Fusion.SumOfTerms.MatrixRank.card_layer (n k : ℕ) : Fintype.card (Layer n k) = n.choose k

theorem Algebraic.Fusion.SumOfTerms.MatrixRank.layer_lowerBound {K : Type} [Field K] (n k : ℕ) (circuit : Circuit (SumOfTerms.signature (Term K (Layer n k))) 0 1) (constructs : (identityProblem K (Layer n k)).Constructs circuit (SumOfTerms.interpretation termValue)) : n.choose k ≤ circuit.cost SumOfTerms.termCost

The Boolean-lattice layer flattening gives a binomial term lower bound.

theorem Algebraic.Fusion.SumOfTerms.MatrixRank.centralBinom_lowerBound {K : Type} [Field K] (n : ℕ) (circuit : Circuit (SumOfTerms.signature (Term K (Layer (2 * n) n))) 0 1) (constructs : (identityProblem K (Layer (2 * n) n)).Constructs circuit (SumOfTerms.interpretation termValue)) : n.centralBinom ≤ circuit.cost SumOfTerms.termCost

The middle-layer flattening needs the central binomial number of terms.

theorem Algebraic.Fusion.SumOfTerms.MatrixRank.four_pow_lt_mul_cost {K : Type} [Field K] (n : ℕ) (n_big : 4 ≤ n) (circuit : Circuit (SumOfTerms.signature (Term K (Layer (2 * n) n))) 0 1) (constructs : (identityProblem K (Layer (2 * n) n)).Constructs circuit (SumOfTerms.interpretation termValue)) : 4 ^ n < n * circuit.cost SumOfTerms.termCost

A fully explicit exponential consequence of the middle-layer rank bound.