Hessian rank bounds multiplication count

At a fixed point, each multiplication adds a symmetrized outer product of gradients to the span of the previously available Hessians. Its rank is at most two. Every wire Hessian lies in the span of the supplied input Hessians and these contributions. Subtracting a suitable linear combination of input Hessians therefore leaves rank at most twice the multiplication count. A shared gate contributes once, however often its value is reused.

The theorem concerns equality of formal polynomials, over a field of any characteristic. Agreement of polynomial functions on a finite field does not suffice. Constants and additions are free; every multiplication, including multiplication by a scalar, costs one. Input and output wiring is free. Supplied input polynomials may be arbitrary. When their Hessians vanish at the chosen point, including for affine inputs, the output Hessian itself satisfies the bound. The residual coefficients may depend on the selected wire and point; no point-independent polynomial decomposition is asserted.

This ports the Hessian application of the Algebraic library to the native circuit API.

Main results

• Cslib.Circuits.Program.exists_hessian_residual, Cslib.Circuits.Circuit.exists_hessian_residual: arbitrary supplied polynomial inputs.
• Cslib.Circuits.Circuit.exists_helper_hessian_residual: raw variables and helper inputs.
• Cslib.Circuits.Program.rank_hessian_trace_le: a bound for every program wire.
• Cslib.Circuits.Circuit.hessian_rank_le: output rank is at most twice multiplication count.
• Cslib.Circuits.Circuit.hessian_rank_ceilDiv_two_le: half the target's Hessian rank, rounded up, lower-bounds the multiplication count of a circuit computing it.

References

• The source applications are Applications/Hessian.lean and LowerBound/Fusion/Arithmetic/Interaction/Hessian/Relative.lean in S. Schlesinger, Algebraic circuit formalizations in Complexitylib.
• P. Bürgisser, M. Clausen, M. A. Shokrollahi, Algebraic Complexity Theory for background on arithmetic circuits.

theorem Cslib.Circuits.Program.exists_hessian_residual {C : Type u_1} {K : Type u_2} {ι : Type u_3} [Field K] [Fintype ι] {n g : ℕ} (p : Program (arithSignature C) n g) (constant : C → K) (point : ι → K) (input : Fin n → MvPolynomial ι K) (w : Wire n g) : ∃ (coefficients : Fin n → K), (MvPolynomial.hessian point (p.trace (arithInterpretationWith C (⇑MvPolynomial.C ∘ constant)) input w) - ∑ i : Fin n, coefficients i • MvPolynomial.hessian point (input i)).rank ≤ 2 * p.cost ArithOp.mulCost

For arbitrary supplied polynomial inputs, subtracting a linear combination of their Hessians leaves rank at most twice the multiplication count. Coefficients may depend on the program, selected wire and evaluation point; no cost is charged for supplying the inputs.

theorem Cslib.Circuits.Program.rank_hessian_trace_le {C : Type u_1} {K : Type u_2} {ι : Type u_3} [Field K] [Fintype ι] {n g : ℕ} (p : Program (arithSignature C) n g) (constant : C → K) (point : ι → K) (input : Fin n → MvPolynomial ι K) (hinput : ∀ (i : Fin n), MvPolynomial.hessian point (input i) = 0) (w : Wire n g) : (MvPolynomial.hessian point (p.trace (arithInterpretationWith C (⇑MvPolynomial.C ∘ constant)) input w)).rank ≤ 2 * p.cost ArithOp.mulCost

With input Hessians zero at the chosen point, every wire's Hessian rank is at most twice the number of multiplication gates. Inputs may be arbitrary affine polynomials.

theorem Cslib.Circuits.Circuit.exists_hessian_residual {C : Type u_1} {K : Type u_2} {ι : Type u_3} [Field K] [Fintype ι] {n m : ℕ} (c : Circuit (arithSignature C) n m) (constant : C → K) (point : ι → K) (input : Fin n → MvPolynomial ι K) (j : Fin m) (polynomial : MvPolynomial ι K) (hcompute : c.eval (arithInterpretationWith C (⇑MvPolynomial.C ∘ constant)) input j = polynomial) : ∃ (coefficients : Fin n → K), (MvPolynomial.hessian point polynomial - ∑ i : Fin n, coefficients i • MvPolynomial.hessian point (input i)).rank ≤ 2 * c.program.cost ArithOp.mulCost

A circuit computing a formal polynomial from arbitrary supplied polynomials has a source-adjusted Hessian of rank at most twice its multiplication count.

theorem Cslib.Circuits.Circuit.exists_helper_hessian_residual {C : Type u_1} {K : Type u_2} [Field K] {n m k : ℕ} (c : Circuit (arithSignature C) (n + k) m) (constant : C → K) (point : Fin n → K) (helpers : Fin k → MvPolynomial (Fin n) K) (j : Fin m) (polynomial : MvPolynomial (Fin n) K) (hcompute : c.eval (arithInterpretationWith C (⇑MvPolynomial.C ∘ constant)) (Fin.append MvPolynomial.X helpers) j = polynomial) : ∃ (coefficients : Fin k → K), (MvPolynomial.hessian point polynomial - ∑ i : Fin k, coefficients i • MvPolynomial.hessian point (helpers i)).rank ≤ 2 * c.program.cost ArithOp.mulCost

When raw variables and helper polynomials are supplied, only helper Hessians need to be subtracted: the raw variables have zero Hessian.

theorem Cslib.Circuits.Circuit.hessian_rank_le {C : Type u_1} {K : Type u_2} [Field K] {n m : ℕ} (c : Circuit (arithSignature C) n m) (constant : C → K) (point : Fin n → K) (j : Fin m) : (MvPolynomial.hessian point (c.eval (arithInterpretationWith C (⇑MvPolynomial.C ∘ constant)) MvPolynomial.X j)).rank ≤ 2 * c.program.cost ArithOp.mulCost

A formal polynomial computed by an arithmetic circuit has Hessian rank at most twice the number of multiplication gates. This applies separately to every selected output.

theorem Cslib.Circuits.Circuit.hessian_rank_ceilDiv_two_le {C : Type u_1} {K : Type u_2} [Field K] {n m : ℕ} (c : Circuit (arithSignature C) n m) (constant : C → K) (point : Fin n → K) (j : Fin m) (polynomial : MvPolynomial (Fin n) K) (hcompute : c.eval (arithInterpretationWith C (⇑MvPolynomial.C ∘ constant)) MvPolynomial.X j = polynomial) : (MvPolynomial.hessian point polynomial).rank ⌈/⌉ 2 ≤ c.program.cost ArithOp.mulCost

Half the target's Hessian rank, rounded up, lower-bounds the multiplication count. The computation premise is equality of formal polynomials.