Hessian lower bounds with arbitrary polynomial sources

Pass to the quotient by the span of the supplied Hessians. In this quotient the free inputs have zero feature, so interaction-span Fusion applies. Lift the resulting span membership back to matrices: subtracting a linear combination of source Hessians leaves rank at most twice multiplication cost. All statements use formal polynomial equality and work in every characteristic.

theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.exists_source_hessian_residual {K σ : Type} [Field K] [Fintype σ] [DecidableEq σ] {C : Type u_1} (constant : C → K) (problem : Problem (MvPolynomial σ K)) (point : σ → K) (circuit : Circuit (Arithmetic.signature C) problem.inputCount 1) (constructs : problem.Constructs circuit (Arithmetic.interpretation fun (scalar : C) => MvPolynomial.C (constant scalar))) : ∃ (coefficients : Fin problem.inputCount → K), (linearMap point problem.target - ∑ i : Fin problem.inputCount, coefficients i • linearMap point (problem.inputs i)).rank ≤ 2 * ↑(circuit.cost Arithmetic.multiplicationCost)

Arbitrary supplied polynomial values contribute their Hessians for free. The coefficients may depend on both the circuit and the evaluation point.

theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.exists_helper_hessian_residual {K : Type} [Field K] {C : Type u_1} {n k : ℕ} (constant : C → K) (target : MvPolynomial (Fin n) K) (supplied : Fin k → MvPolynomial (Fin n) K) (point : Fin n → K) (circuit : Circuit (Arithmetic.signature C) (n + k) 1) (computes : circuit.eval (Arithmetic.interpretation fun (scalar : C) => MvPolynomial.C (constant scalar)) (Fin.append MvPolynomial.X supplied) 0 = target) : ∃ (coefficients : Fin k → K), (linearMap point target - ∑ j : Fin k, coefficients j • linearMap point (supplied j)).rank ≤ 2 * ↑(circuit.cost Arithmetic.multiplicationCost)

With raw polynomial generators and helpers supplied, only the helpers need coefficients in the residual: the raw generators have zero Hessian.

noncomputable def Algebraic.Fusion.Arithmetic.Interaction.Hessian.residualRank {K σ : Type} [Field K] [Fintype σ] [DecidableEq σ] {n : ℕ} (point : σ → K) (target : MvPolynomial σ K) (sources : Fin n → MvPolynomial σ K) : ℕ∞

Minimum rank remaining after subtracting a linear combination of the supplied Hessians. This is an ordinary matrix rank, recorded in ℕ∞.

Equations

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

theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.residualRank_le_twice_relativeCostComplexity {K σ : Type} [Field K] [Fintype σ] [DecidableEq σ] {C : Type u_1} {n : ℕ} (constant : C → K) (target : MvPolynomial σ K) (sources : Fin n → MvPolynomial σ K) (point : σ → K) : residualRank point target sources ≤ 2 * Circuit.relativeCostComplexity (Arithmetic.interpretation fun (scalar : C) => MvPolynomial.C (constant scalar)) Arithmetic.multiplicationCost (fun (x : Unit) (x_1 : Fin 1) => target) fun (x : Unit) => sources

Minimum residual Hessian rank is at most twice relative multiplication complexity, including the case of unrepresentable targets.

theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.residualRank_le_twice_with_helpers {K : Type} [Field K] {C : Type u_1} {n k : ℕ} (constant : C → K) (target : MvPolynomial (Fin n) K) (supplied : Fin k → MvPolynomial (Fin n) K) (point : Fin n → K) : residualRank point target supplied ≤ 2 * Circuit.relativeCostComplexity (Arithmetic.interpretation fun (scalar : C) => MvPolynomial.C (constant scalar)) Arithmetic.multiplicationCost (fun (x : Unit) (x_1 : Fin 1) => target) fun (x : Unit) => Fin.append MvPolynomial.X supplied

Conditional form of the rank bound, with the original polynomial variables available for free alongside the helper polynomials.

theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.relativeCostComplexity_lowerBound {K σ : Type} [Field K] [Fintype σ] [DecidableEq σ] {C : Type u_1} {n : ℕ} (constant : C → K) (target : MvPolynomial σ K) (sources : Fin n → MvPolynomial σ K) (point : σ → K) (lower : ℕ) (hard : ∀ (coefficients : Fin n → K), 2 * ↑lower ≤ (linearMap point target - ∑ i : Fin n, coefficients i • linearMap point (sources i)).rank) : ↑lower ≤ Circuit.relativeCostComplexity (Arithmetic.interpretation fun (scalar : C) => MvPolynomial.C (constant scalar)) Arithmetic.multiplicationCost (fun (x : Unit) (x_1 : Fin 1) => target) fun (x : Unit) => sources

A uniform lower bound on every source-adjusted Hessian bounds relative multiplication complexity. The source family can be completely arbitrary.