Hessian bounds for minimum multiplication cost

Minimum residual Hessian rank is at most twice the minimum multiplication cost from arbitrary supplied formal polynomials. No construction of the supplied polynomials is charged. The common source domain is Unit and the carrier consists of formal polynomials: correctness is polynomial equality, not equality of polynomial functions. All field characteristics are allowed.

The bounds remain valid when no circuit computes the target, since its complexity is then ⊤. When raw variables are supplied alongside helpers, only the helper Hessians need to be subtracted.

Main results

• Cslib.Circuits.hessianResidualRank_le_two_mul_ecomplexityFrom: arbitrary supplied polynomials.
• Cslib.Circuits.hessianResidualRank_le_two_mul_ecomplexityFrom_with_helpers: raw variables and helpers.
• Cslib.Circuits.le_ecomplexityFrom_of_hessian_rank: a uniform residual-rank lower bound.

References

• Ported from LowerBound/Fusion/Arithmetic/Interaction/Hessian/Relative.lean in S. Schlesinger, Algebraic circuit formalizations in Complexitylib.

theorem Cslib.Circuits.hessianResidualRank_le_two_mul_ecomplexityFrom {C : Type u_1} {K : Type u_2} {ι : Type u_3} [Field K] [Fintype ι] {n : ℕ} (constant : C → K) (point : ι → K) (target : MvPolynomial ι K) (sources : Fin n → MvPolynomial ι K) : MvPolynomial.hessianResidualRank point target sources ≤ 2 * ecomplexityFrom (arithInterpretationWith C (⇑MvPolynomial.C ∘ constant)) ArithOp.mulCost (fun (x : Unit) (x_1 : Fin 1) => target) fun (x : Unit) => sources

The least residual Hessian rank is at most twice the least multiplication cost.

theorem Cslib.Circuits.hessianResidualRank_le_two_mul_ecomplexityFrom_with_helpers {C : Type u_1} {K : Type u_2} [Field K] {n k : ℕ} (constant : C → K) (point : Fin n → K) (target : MvPolynomial (Fin n) K) (helpers : Fin k → MvPolynomial (Fin n) K) : MvPolynomial.hessianResidualRank point target helpers ≤ 2 * ecomplexityFrom (arithInterpretationWith C (⇑MvPolynomial.C ∘ constant)) ArithOp.mulCost (fun (x : Unit) (x_1 : Fin 1) => target) fun (x : Unit) => Fin.append MvPolynomial.X helpers

Supplying raw variables with helpers requires subtracting only the helper Hessians.

theorem Cslib.Circuits.le_ecomplexityFrom_of_hessian_rank {C : Type u_1} {K : Type u_2} {ι : Type u_3} [Field K] [Fintype ι] {n : ℕ} (constant : C → K) (point : ι → K) (target : MvPolynomial ι K) (sources : Fin n → MvPolynomial ι K) (lower : ℕ) (hlower : ∀ (coefficients : Fin n → K), 2 * lower ≤ (MvPolynomial.hessian point target - ∑ i : Fin n, coefficients i • MvPolynomial.hessian point (sources i)).rank) : ↑lower ≤ ecomplexityFrom (arithInterpretationWith C (⇑MvPolynomial.C ∘ constant)) ArithOp.mulCost (fun (x : Unit) (x_1 : Fin 1) => target) fun (x : Unit) => sources

A lower bound on every residual Hessian bounds minimum multiplication cost.