Documentation

Complexitylib.Algebraic.LowerBound.Fusion.Arithmetic.Interaction.Polynomial.Squarefree.Mixing

Mixed squarefree-layer output bounds #

Specialize monomial mixing to the squarefree degree-k layer. Any mixing matrix contributes its full rank as a multiplication lower bound. In particular, the unitriangular prefix sums of the layer require choose n k multiplications over every field.

For the middle layer this is an exponential multi-output lower bound whose outputs have nested, highly overlapping supports.

source
noncomputable def Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Squarefree.Mixing.targets (K : Type u) [CommSemiring K] (n k : ℕ) (mix : Matrix (Fin (n.choose k)) (Fin (n.choose k)) K) :
Fin (n.choose k) → MvPolynomial (Fin n) K

A matrix mixture of all squarefree degree-k monomials.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Squarefree.Mixing.matrix_rank_le_multiplicationCost {K : Type u} {C : Type v} [Field K] (constant : C → K) (n k : ℕ) (two_le : 2 ≤ k) (mix : Matrix (Fin (n.choose k)) (Fin (n.choose k)) K) (circuit : Circuit (Arithmetic.signature C) n (n.choose k)) (constructs : Multiple.Constructs (inputProblem K n) (targets K n k mix) circuit) :
    mix.rank ≤ circuit.cost Arithmetic.multiplicationCost

    Mixing-matrix rank lower-bounds multiplication cost for the squarefree layer.

    source
    theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Squarefree.Mixing.circuit_multiplication_lowerBound_of_det_ne_zero {K : Type u} {C : Type v} [Field K] (constant : C → K) (n k : ℕ) (two_le : 2 ≤ k) (mix : Matrix (Fin (n.choose k)) (Fin (n.choose k)) K) (det_ne_zero : mix.det ≠ 0) (circuit : Circuit (Arithmetic.signature C) n (n.choose k)) (constructs : Multiple.Constructs (inputProblem K n) (targets K n k mix) circuit) :
    n.choose k ≤ circuit.cost Arithmetic.multiplicationCost

    Every nonsingular mixing of the squarefree layer needs one multiplication per layer monomial.

    source
    noncomputable def Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Squarefree.Mixing.prefixTargets (K : Type u) [CommSemiring K] (n k : ℕ) :
    Fin (n.choose k) → MvPolynomial (Fin n) K

    Unitriangular prefix sums of the squarefree layer.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Squarefree.Mixing.prefixTargets_multiplication_lowerBound {K : Type u} {C : Type v} [Field K] (constant : C → K) (n k : ℕ) (two_le : 2 ≤ k) (circuit : Circuit (Arithmetic.signature C) n (n.choose k)) (constructs : Multiple.Constructs (inputProblem K n) (prefixTargets K n k) circuit) :
      n.choose k ≤ circuit.cost Arithmetic.multiplicationCost

      Computing every prefix sum of the squarefree degree-k layer requires choose n k multiplications.

      source
      theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Squarefree.Mixing.prefixTargets_size_lowerBound {K : Type u} {C : Type v} [Field K] (constant : C → K) (n k : ℕ) (two_le : 2 ≤ k) (circuit : Circuit (Arithmetic.signature C) n (n.choose k)) (constructs : Multiple.Constructs (inputProblem K n) (prefixTargets K n k) circuit) :
      n.choose k ≤ circuit.size

      Prefix squarefree outputs force raw size at least the layer cardinality.

      source
      theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Squarefree.Mixing.centralBinom_prefixTargets_multiplication_lowerBound {K : Type u} {C : Type v} [Field K] (constant : C → K) (n : ℕ) (two_le : 2 ≤ n) (circuit : Circuit (Arithmetic.signature C) (2 * n) n.centralBinom) (constructs : Multiple.Constructs (inputProblem K (2 * n)) (prefixTargets K (2 * n) n) circuit) :
      n.centralBinom ≤ circuit.cost Arithmetic.multiplicationCost

      Middle-layer prefix outputs require central-binomial multiplication cost.

      source
      theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Squarefree.Mixing.four_pow_lt_mul_multiplicationCost {K : Type u} {C : Type v} [Field K] (constant : C → K) (n : ℕ) (n_big : 4 ≤ n) (circuit : Circuit (Arithmetic.signature C) (2 * n) n.centralBinom) (constructs : Multiple.Constructs (inputProblem K (2 * n)) (prefixTargets K (2 * n) n) circuit) :
      4 ^ n < n * circuit.cost Arithmetic.multiplicationCost

      Explicit exponential cost bound for nested middle-layer prefix outputs.

      source
      theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Squarefree.Mixing.four_pow_lt_mul_size {K : Type u} {C : Type v} [Field K] (constant : C → K) (n : ℕ) (n_big : 4 ≤ n) (circuit : Circuit (Arithmetic.signature C) (2 * n) n.centralBinom) (constructs : Multiple.Constructs (inputProblem K (2 * n)) (prefixTargets K (2 * n) n) circuit) :
      4 ^ n < n * circuit.size

      Explicit exponential raw-size bound for nested middle-layer prefixes.