Applying the Hessian multiplication bound

The endpoint uses the natural rank of the evaluated Hessian matrix and an ordinary polynomial evaluation equality. No Fusion problem, rank certificate, or cardinal arithmetic is needed at the call site. Constants and additions are free; every multiplication, including multiplication by a scalar, costs one.

The computation premise is equality of formal polynomials. Agreement of polynomial functions on a finite field is a different premise and does not suffice for this theorem.

theorem Algebraic.Applications.hessianRank_lowerBound {n : ℕ} {K C : Type} [Field K] (constant : C → K) (point : Fin n → K) (polynomial : MvPolynomial (Fin n) K) (circuit : Circuit (Arithmetic.signature C) n 1) (computes : circuit.eval (Arithmetic.interpretation (⇑MvPolynomial.C ∘ constant)) MvPolynomial.X 0 = polynomial) : (Fusion.Arithmetic.Interaction.Hessian.matrix point polynomial).rank ⌈/⌉ 2 ≤ circuit.cost Arithmetic.multiplicationCost

Half the Hessian rank, rounded up, lower-bounds the multiplication count of a circuit computing a formal polynomial.