Documentation

Complexitylib.Algebraic.LowerBound.Fusion.SumOfTerms.MatrixRank.BlockSum

Weighted block-sum circuit lower bounds #

A dictionary term is now an arbitrary matrix equipped with finite row and column covers. The term is charged the smaller cover size, addition is free, and the target is the identity matrix. The term-dependent weighted rank engine proves that every constructing circuit pays at least the full matrix dimension.

On the middle Boolean layer this gives an unconditional central-binomial, and hence exponential, lower bound for weighted block-sum circuits.

source
@[reducible, inline]
abbrev Algebraic.Fusion.SumOfTerms.MatrixRank.BlockSum.Term (K I : Type) [Field K] [Fintype I] [DecidableEq I] :
Type

Dictionary of row/column-supported square matrix blocks.

Equations
Instances For
    source
    def Algebraic.Fusion.SumOfTerms.MatrixRank.BlockSum.termValue {K I : Type} [Field K] [Fintype I] [DecidableEq I] (term : Term K I) :
    Matrix I I K

    Matrix denoted by a supported block term.

    Equations
    Instances For
      source
      def Algebraic.Fusion.SumOfTerms.MatrixRank.BlockSum.termWeight {K I : Type} [Field K] [Fintype I] [DecidableEq I] (term : Term K I) :
      ℕ

      Smaller-side charge of a supported block term.

      Equations
      Instances For
        source
        def Algebraic.Fusion.SumOfTerms.MatrixRank.BlockSum.blockCost {K I : Type} [Field K] [Fintype I] [DecidableEq I] :
        OperationCost (SumOfTerms.signature (Term K I))

        Term-dependent operation cost for block-sum circuits.

        Equations
        Instances For
          source
          @[simp]
          theorem Algebraic.Fusion.SumOfTerms.MatrixRank.BlockSum.blockCost_add {K I : Type} [Field K] [Fintype I] [DecidableEq I] :
          blockCost SumOfTerms.Op.add = 0
          source
          @[simp]
          theorem Algebraic.Fusion.SumOfTerms.MatrixRank.BlockSum.blockCost_term {K I : Type} [Field K] [Fintype I] [DecidableEq I] (term : Term K I) :
          blockCost (SumOfTerms.Op.term term) = Block.Piece.rankBudget term
          source
          def Algebraic.Fusion.SumOfTerms.MatrixRank.BlockSum.certificate {K I : Type} [Field K] [Fintype I] [DecidableEq I] :
          WeightedRank.Certificate termValue termWeight (identityProblem K I)

          Weighted rank certificate for the identity matrix.

          Equations
          Instances For
            source
            @[simp]
            theorem Algebraic.Fusion.SumOfTerms.MatrixRank.BlockSum.certificate_targetRank {K I : Type} [Field K] [Fintype I] [DecidableEq I] :
            certificate.targetRank = Fintype.card I
            source
            theorem Algebraic.Fusion.SumOfTerms.MatrixRank.BlockSum.identity_lowerBound {K I : Type} [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 blockCost

            Any weighted sum-of-blocks circuit constructing the identity pays at least the matrix dimension.

            source
            theorem Algebraic.Fusion.SumOfTerms.MatrixRank.BlockSum.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 blockCost

            Boolean-layer identity blocks require weighted cost choose n k.

            source
            theorem Algebraic.Fusion.SumOfTerms.MatrixRank.BlockSum.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 blockCost

            Middle-layer weighted block-sum cost is at least the central binomial coefficient.

            source
            theorem Algebraic.Fusion.SumOfTerms.MatrixRank.BlockSum.four_pow_lt_n_mul_cost {K : Type} [Field K] (n : ℕ) (nBig : 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 blockCost

            Explicit exponential lower bound for middle-layer weighted block-sum circuits.