Documentation

Complexitylib.Algebraic.LowerBound.Fusion.Arithmetic.Interaction.Hessian.Pairwise

Quadratic multi-output lower bound for pairwise products #

From two blocks of n inputs, request all n^2 bilinear products x_i y_j. Their Hessian features are linearly independent: the upper-right Hessian entry (i,j) uniquely identifies the corresponding output. The common-span multi-output Fusion theorem therefore forces n^2 multiplication gates.

This is tight, quadratic in the block size, and holds over every field with arbitrary named constants and cancellation.

source
def Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairwise.upperRight (K : Type) [Field K] (n : ℕ) :
((Fin n ⊕ Fin n → K) →ₗ[K] Fin n ⊕ Fin n → K) →ₗ[K] Fin n × Fin n → K

Extract the upper-right block of an endomorphism on the two coordinate blocks.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairwise.upperRight_linearMap_product {K : Type} [Field K] {n : ℕ} (point : Fin n ⊕ Fin n → K) (left right : Fin n) :
    (upperRight K n) (linearMap point (MvPolynomial.X (Sum.inl left) * MvPolynomial.X (Sum.inr right))) = Pi.single (left, right) 1

    One pairwise product maps to the corresponding standard basis vector of the upper-right Hessian block.

    source
    theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairwise.productFeatures_linearIndependent {K : Type} [Field K] {n : ℕ} (point : Fin n ⊕ Fin n → K) :
    LinearIndependent K fun (pair : Fin n × Fin n) => linearMap point (MvPolynomial.X (Sum.inl pair.1) * MvPolynomial.X (Sum.inr pair.2))

    Hessians of the pairwise products are linearly independent.

    source
    noncomputable def Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairwise.targets (K : Type) [Field K] (n : ℕ) :
    Fin (n * n) → MvPolynomial (Fin n ⊕ Fin n) K

    Enumerate all pairwise products by the standard n * n output type.

    Equations
    Instances For
      source
      theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairwise.targetFeatures_linearIndependent {K : Type} [Field K] {n : ℕ} (point : Fin n ⊕ Fin n → K) :
      LinearIndependent K (linearMap point ∘ targets K n)

      Features of the enumerated output family remain linearly independent.

      source
      @[reducible, inline]
      noncomputable abbrev Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairwise.inputProblem (K : Type) [Field K] (n : ℕ) :
      Problem (MvPolynomial (Fin n ⊕ Fin n) K)

      Input family used by the multi-output circuit. Its dummy target is not used by the multi-output theorem.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairwise.interactionCertificate {K : Type} [Field K] {C : Type u_1} (constant : C → K) (n : ℕ) (point : Fin n ⊕ Fin n → K) :
        Certificate (fun (scalar : C) => MvPolynomial.C (constant scalar)) (inputProblem K n)

        Hessian interaction certificate for the common input family.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairwise.circuit_multiplication_lowerBound {K : Type} [Field K] {C : Type u_1} (constant : C → K) (n : ℕ) (circuit : Circuit (Arithmetic.signature C) (2 * n) (n * n)) (constructs : Multiple.Constructs (inputProblem K n) (targets K n) circuit) :
          n * n ≤ circuit.cost Arithmetic.multiplicationCost

          Computing all n^2 pairwise products requires at least n^2 multiplications.

          source
          theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairwise.circuit_gate_lowerBound {K : Type} [Field K] {C : Type u_1} (constant : C → K) (n : ℕ) (circuit : Circuit (Arithmetic.signature C) (2 * n) (n * n)) (constructs : Multiple.Constructs (inputProblem K n) (targets K n) circuit) :
          n * n ≤ circuit.cost Arithmetic.gateCost

          Total nonconstant arithmetic-gate cost is at least n^2.

          source
          theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairwise.circuit_size_lowerBound {K : Type} [Field K] {C : Type u_1} (constant : C → K) (n : ℕ) (circuit : Circuit (Arithmetic.signature C) (2 * n) (n * n)) (constructs : Multiple.Constructs (inputProblem K n) (targets K n) circuit) :
          n * n ≤ circuit.size

          Raw circuit size is at least n^2.