Documentation

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

Multi-output squarefree-monomial lower bounds #

Enumerate every squarefree degree-k monomial in n variables and request them as simultaneous outputs. The selected-coefficient Fusion theorem gives an exact choose n k multiplication lower bound over every field, with arbitrary constants and cancellation.

At the middle layer this is a central-binomial, hence exponential, direct-sum bound. This is explicitly a multi-output theorem: the output family itself has exponential cardinality.

source
noncomputable def Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Squarefree.indexEquiv (n k : ℕ) :
MonotonePolynomial.Layer.Index n k ≃ Fin (n.choose k)

Canonical finite enumeration of the squarefree degree-k layer.

Equations
Instances For
    source
    noncomputable def Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Squarefree.exponent (n k : ℕ) :
    Fin (n.choose k) → Fin n →₀ ℕ

    Squarefree degree-k exponent selected by an output index.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Squarefree.exponent_injective (n k : ℕ) :
      Function.Injective (exponent n k)

      The enumerated squarefree exponents are pairwise distinct.

      source
      theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Squarefree.exponent_ne_zero {k n : ℕ} (positive : 0 < k) (output : Fin (n.choose k)) :
      exponent n k output ≠ 0

      Positive-degree squarefree exponents are nonconstant.

      source
      theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Squarefree.exponent_ne_input {k n : ℕ} (two_le : 2 ≤ k) (output : Fin (n.choose k)) (input : Fin n) :
      exponent n k output ≠ Finsupp.single input 1

      A squarefree exponent of degree at least two is not any free input variable exponent.

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

      All squarefree degree-k monomials, enumerated as circuit outputs.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[reducible, inline]
        noncomputable abbrev Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Squarefree.inputProblem (K : Type u) [CommSemiring K] (n : ℕ) :
        Problem (MvPolynomial (Fin n) K)

        Common input family for squarefree multi-output circuits.

        Equations
        Instances For
          source
          theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Squarefree.circuit_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) (targets K n k) circuit) :
          n.choose k ≤ circuit.cost Arithmetic.multiplicationCost

          Producing all squarefree degree-k monomials requires one multiplication per monomial.

          source
          theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Squarefree.circuit_gate_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) (targets K n k) circuit) :
          n.choose k ≤ circuit.cost Arithmetic.gateCost

          Total nonconstant arithmetic-gate cost is at least the squarefree layer cardinality.

          source
          theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Squarefree.circuit_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) (targets K n k) circuit) :
          n.choose k ≤ circuit.size

          Raw circuit size is at least the squarefree layer cardinality.

          source
          theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Squarefree.centralBinom_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)) (targets K (2 * n) n) circuit) :
          n.centralBinom ≤ circuit.cost Arithmetic.multiplicationCost

          The middle squarefree layer forces central-binomial multiplication cost.

          source
          theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Squarefree.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)) (targets K (2 * n) n) circuit) :
          4 ^ n < n * circuit.cost Arithmetic.multiplicationCost

          Explicit exponential multiplication lower bound for all middle-layer outputs.

          source
          theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Squarefree.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)) (targets K (2 * n) n) circuit) :
          4 ^ n < n * circuit.size

          Explicit exponential raw-size lower bound for all middle-layer outputs.