Documentation

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

Pairing with arbitrary preprocessing of one argument #

Supplying any finite family of formal polynomials in the left variables does not reduce the multiplication complexity of sum i, x_i * y_i: it remains exactly n. No degree bound or cost bound on the supplied polynomials is used.

source
theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairing.rank_hessian_residual {K : Type} [Field K] {n k : ℕ} (point : Fin n ⊕ Fin n → K) (supplied : Fin k → MvPolynomial (Fin n) K) (coefficients : Fin k → K) :
(linearMap point (polynomial K n) - ∑ j : Fin k, coefficients j • linearMap point ((MvPolynomial.rename Sum.inl) (supplied j))).rank = 2 * ↑n

Subtracting any linear combination of left-only helper Hessians leaves the pairing Hessian of full rank, over every field and at every point.

source
noncomputable def Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairing.preprocessedSources {K : Type} [Field K] {k n : ℕ} (supplied : Fin k → MvPolynomial (Fin n) K) :
Fin (2 * n + k) → MvPolynomial (Fin n ⊕ Fin n) K

Original coordinates followed by arbitrary polynomial preprocessing of the left coordinate block.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairing.preprocessedMultiplicationComplexity {K : Type} [Field K] {k n : ℕ} (supplied : Fin k → MvPolynomial (Fin n) K) :
    ℕ∞

    Exact formal multiplication complexity with left-only preprocessing.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairing.preprocessedMultiplicationComplexity_lowerBound {K : Type} [Field K] {k n : ℕ} (supplied : Fin k → MvPolynomial (Fin n) K) :
      ↑n ≤ preprocessedMultiplicationComplexity supplied

      Arbitrarily complicated preprocessing of the left input cannot save any multiplications in a formal circuit for pairing.

      source
      theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairing.preprocessedMultiplicationComplexity_upperBound {K : Type} [Field K] {k n : ℕ} (supplied : Fin k → MvPolynomial (Fin n) K) :
      preprocessedMultiplicationComplexity supplied ≤ ↑n

      The usual sum of n products supplies a matching upper bound.

      source
      theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairing.preprocessedMultiplicationComplexity_eq {K : Type} [Field K] {k n : ℕ} (supplied : Fin k → MvPolynomial (Fin n) K) :
      preprocessedMultiplicationComplexity supplied = ↑n

      Pairing still costs exactly n multiplications with any finite family of left-only polynomial helpers, including when n = 0.