Hessian-rank Fusion for arithmetic circuits

Fix an evaluation point. The Hessian of a sum is the sum of the Hessians, while the Hessian of a product is a linear combination of the two old Hessians plus the symmetrized outer product of the two gradients. That new interaction has rank at most two.

Instantiating interaction-span Fusion therefore proves the classical characteristic-independent bound

rank (Hessian target at point) / 2 <= multiplication complexity.

Unlike exact-support arguments, this certificate permits arbitrary field constants, subtraction through negative constants, and cancellation.

noncomputable def Algebraic.Fusion.Arithmetic.Interaction.Hessian.gradient {K σ : Type} [Field K] (point : σ → K) (polynomial : MvPolynomial σ K) : σ → K

Gradient of a polynomial evaluated at a selected point.

Equations

• Algebraic.Fusion.Arithmetic.Interaction.Hessian.gradient point polynomial coordinate = (MvPolynomial.eval point) ((MvPolynomial.pderiv coordinate) polynomial)

noncomputable def Algebraic.Fusion.Arithmetic.Interaction.Hessian.matrix {K σ : Type} [Field K] (point : σ → K) (polynomial : MvPolynomial σ K) : Matrix σ σ K

Hessian matrix of a polynomial evaluated at a selected point.

Equations

• Algebraic.Fusion.Arithmetic.Interaction.Hessian.matrix point polynomial row column = (MvPolynomial.eval point) ((MvPolynomial.pderiv row) ((MvPolynomial.pderiv column) polynomial))

noncomputable def Algebraic.Fusion.Arithmetic.Interaction.Hessian.linearMap {K σ : Type} [Field K] [Fintype σ] [DecidableEq σ] (point : σ → K) (polynomial : MvPolynomial σ K) : (σ → K) →ₗ[K] σ → K

Hessian viewed as an endomorphism of the coordinate space.

Equations

• Algebraic.Fusion.Arithmetic.Interaction.Hessian.linearMap point polynomial = Matrix.toLin' (Algebraic.Fusion.Arithmetic.Interaction.Hessian.matrix point polynomial)

noncomputable def Algebraic.Fusion.Arithmetic.Interaction.Hessian.interactionMatrix {K σ : Type} [Field K] (point : σ → K) (left right : MvPolynomial σ K) : Matrix σ σ K

New Hessian contribution created by one multiplication.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.Fusion.Arithmetic.Interaction.Hessian.interaction {K σ : Type} [Field K] [Fintype σ] [DecidableEq σ] (point : σ → K) (left right : MvPolynomial σ K) : (σ → K) →ₗ[K] σ → K

Multiplication interaction viewed as an endomorphism.

Equations

• Algebraic.Fusion.Arithmetic.Interaction.Hessian.interaction point left right = Matrix.toLin' (Algebraic.Fusion.Arithmetic.Interaction.Hessian.interactionMatrix point left right)

@[simp]

theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.gradient_add {K σ : Type} [Field K] (point : σ → K) (left right : MvPolynomial σ K) : gradient point (left + right) = gradient point left + gradient point right

@[simp]

theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.gradient_C {K σ : Type} [Field K] (point : σ → K) (scalar : K) : gradient point (MvPolynomial.C scalar) = 0

@[simp]

theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.matrix_add {K σ : Type} [Field K] (point : σ → K) (left right : MvPolynomial σ K) : matrix point (left + right) = matrix point left + matrix point right

@[simp]

theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.matrix_C {K σ : Type} [Field K] (point : σ → K) (scalar : K) : matrix point (MvPolynomial.C scalar) = 0

@[simp]

theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.matrix_X {K σ : Type} [Field K] [DecidableEq σ] (point : σ → K) (coordinate : σ) : matrix point (MvPolynomial.X coordinate) = 0

theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.matrix_mul {K σ : Type} [Field K] (point : σ → K) (left right : MvPolynomial σ K) : matrix point (left * right) = (MvPolynomial.eval point) right • matrix point left + (MvPolynomial.eval point) left • matrix point right + interactionMatrix point left right

Product rule for the point-evaluated Hessian.

@[simp]

theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.linearMap_add {K σ : Type} [Field K] [Fintype σ] [DecidableEq σ] (point : σ → K) (left right : MvPolynomial σ K) : linearMap point (left + right) = linearMap point left + linearMap point right

@[simp]

theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.linearMap_C {K σ : Type} [Field K] [Fintype σ] [DecidableEq σ] (point : σ → K) (scalar : K) : linearMap point (MvPolynomial.C scalar) = 0

@[simp]

theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.linearMap_X {K σ : Type} [Field K] [Fintype σ] [DecidableEq σ] (point : σ → K) (coordinate : σ) : linearMap point (MvPolynomial.X coordinate) = 0

theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.linearMap_mul {K σ : Type} [Field K] [Fintype σ] [DecidableEq σ] (point : σ → K) (left right : MvPolynomial σ K) : linearMap point (left * right) = (MvPolynomial.eval point) right • linearMap point left + (MvPolynomial.eval point) left • linearMap point right + interaction point left right

Product rule after viewing Hessians as linear maps.

theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.rank_interaction_le_two {K σ : Type} [Field K] [Fintype σ] [DecidableEq σ] (point : σ → K) (left right : MvPolynomial σ K) : (interaction point left right).rank ≤ 2

Each multiplication creates a Hessian interaction of rank at most two.

noncomputable def Algebraic.Fusion.Arithmetic.Interaction.Hessian.certificate {K σ : Type} [Field K] [Fintype σ] [DecidableEq σ] {C : Type u_1} (constant : C → K) (problem : Problem (MvPolynomial σ K)) (point : σ → K) (input_zero : ∀ (input : Fin problem.inputCount), linearMap point (problem.inputs input) = 0) (targetRank : ℕ) (target_rank_ge : ↑targetRank ≤ (linearMap point problem.target).rank) : Rank.Certificate (fun (scalar : C) => MvPolynomial.C (constant scalar)) problem

Hessian interaction-rank certificate for an arbitrary polynomial construction problem whose free inputs are affine at the selected point.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.circuit_multiplication_lowerBound {K σ : Type} [Field K] [Fintype σ] [DecidableEq σ] {C : Type u_1} (constant : C → K) (problem : Problem (MvPolynomial σ K)) (point : σ → K) (input_zero : ∀ (input : Fin problem.inputCount), linearMap point (problem.inputs input) = 0) (targetRank : ℕ) (target_rank_ge : ↑targetRank ≤ (linearMap point problem.target).rank) (circuit : Circuit (Arithmetic.signature C) problem.inputCount 1) (constructs : problem.Constructs circuit (Arithmetic.interpretation fun (scalar : C) => MvPolynomial.C (constant scalar))) : targetRank ⌈/⌉ 2 ≤ circuit.cost Arithmetic.multiplicationCost

Hessian-rank multiplication lower bound for an arbitrary construction problem with affine free inputs.

theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.polynomial_circuit_multiplication_lowerBound {K : Type} [Field K] {C : Type u_1} {n : ℕ} (constant : C → K) (point : Fin n → K) (target : MvPolynomial (Fin n) K) (targetRank : ℕ) (target_rank_ge : ↑targetRank ≤ (linearMap point target).rank) (circuit : Circuit (Arithmetic.signature C) n 1) (constructs : { inputCount := n, inputs := MvPolynomial.X, target := target }.Constructs circuit (Arithmetic.interpretation fun (scalar : C) => MvPolynomial.C (constant scalar))) : targetRank ⌈/⌉ 2 ≤ circuit.cost Arithmetic.multiplicationCost

User-facing specialization to the standard polynomial generators.