Selected-coefficient Fusion for polynomial circuits

Project a polynomial onto any finite family of selected monomial coefficients. If the selected monomials are distinct and none is a constant or one of the free input variables, their coefficient vectors form a standard basis. Computing all of them therefore needs one multiplication per output, even with arbitrary field constants, subtraction, and cancellation.

noncomputable def Algebraic.Fusion.Arithmetic.Interaction.Polynomial.coefficientFeature {K : Type u} {σ : Type w} {I : Type x} [CommSemiring K] (exponent : I → σ →₀ ℕ) : MvPolynomial σ K →ₗ[K] I → K

Simultaneously extract the coefficients of a selected exponent family.

Equations

• Algebraic.Fusion.Arithmetic.Interaction.Polynomial.coefficientFeature exponent = LinearMap.pi fun (output : I) => MvPolynomial.lcoeff K (exponent output)

@[simp]

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.coefficientFeature_apply {K : Type u} {σ : Type w} {I : Type x} [CommSemiring K] (exponent : I → σ →₀ ℕ) (polynomial : MvPolynomial σ K) (output : I) : (coefficientFeature exponent) polynomial output = polynomial.coeff (exponent output)

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.coefficientFeature_C_eq_zero {K : Type u} {σ : Type w} {I : Type x} [CommSemiring K] [DecidableEq σ] (exponent : I → σ →₀ ℕ) (nonconstant : ∀ (output : I), exponent output ≠ 0) (scalar : K) : (coefficientFeature exponent) (MvPolynomial.C scalar) = 0

Selected nonconstant coefficients vanish on scalar polynomials.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.coefficientFeature_X_eq_zero {K : Type u} {σ : Type w} {I : Type x} [CommSemiring K] [DecidableEq σ] (exponent : I → σ →₀ ℕ) (coordinate : σ) (notSelected : ∀ (output : I), exponent output ≠ Finsupp.single coordinate 1) : (coefficientFeature exponent) (MvPolynomial.X coordinate) = 0

Selected coefficients vanish on a variable when no selected exponent is that variable's degree-one exponent.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.coefficientFeature_monomial_eq_single {K : Type u} {σ : Type w} {I : Type x} [CommSemiring K] [DecidableEq σ] [DecidableEq I] (exponent : I → σ →₀ ℕ) (injective : Function.Injective exponent) (output : I) : (coefficientFeature exponent) ((MvPolynomial.monomial (exponent output)) 1) = Pi.single output 1

A selected monomial maps to the corresponding standard basis vector.

noncomputable def Algebraic.Fusion.Arithmetic.Interaction.Polynomial.targets {K : Type u} {σ : Type w} {m : ℕ} [CommSemiring K] (exponent : Fin m → σ →₀ ℕ) : Fin m → MvPolynomial σ K

Requested monomials for a selected exponent family.

Equations

• Algebraic.Fusion.Arithmetic.Interaction.Polynomial.targets exponent output = (MvPolynomial.monomial (exponent output)) 1

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.targetFeatures_linearIndependent {K : Type u} {σ : Type w} {m : ℕ} [Field K] [DecidableEq σ] (exponent : Fin m → σ →₀ ℕ) (injective : Function.Injective exponent) : LinearIndependent K (⇑(coefficientFeature exponent) ∘ targets exponent)

The selected-coefficient features of distinct requested monomials are linearly independent.

@[reducible, inline]

noncomputable abbrev Algebraic.Fusion.Arithmetic.Interaction.Polynomial.inputProblem {K : Type u} {σ : Type w} {n : ℕ} [CommSemiring K] (inputVariables : Fin n → σ) : Problem (MvPolynomial σ K)

Polynomial problem whose free inputs are the designated variables. Its dummy target is unused by the multi-output theorem.

Equations

• Algebraic.Fusion.Arithmetic.Interaction.Polynomial.inputProblem inputVariables = { inputCount := n, inputs := fun (input : Fin n) => MvPolynomial.X (inputVariables input), target := 0 }

def Algebraic.Fusion.Arithmetic.Interaction.Polynomial.coefficientMatrix {K : Type u} {σ : Type w} {I : Type x} {m : ℕ} [CommSemiring K] (exponent : I → σ →₀ ℕ) (outputs : Fin m → MvPolynomial σ K) : Matrix I (Fin m) K

Matrix of selected coefficients: rows are selected exponents and columns are requested outputs.

Equations

• Algebraic.Fusion.Arithmetic.Interaction.Polynomial.coefficientMatrix exponent outputs selected output = (outputs output).coeff (exponent selected)

@[simp]

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.coefficientMatrix_col {K : Type u} {σ : Type w} {I : Type x} {m : ℕ} [CommSemiring K] (exponent : I → σ →₀ ℕ) (outputs : Fin m → MvPolynomial σ K) (output : Fin m) : (coefficientMatrix exponent outputs).col output = (coefficientFeature exponent) (outputs output)

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.coefficientSpan_finrank_le_multiplicationCost {K : Type u} {C : Type v} {σ : Type w} {I : Type x} {n m : ℕ} [Field K] [DecidableEq σ] (constant : C → K) (inputVariables : Fin n → σ) (exponent : I → σ →₀ ℕ) (nonconstant : ∀ (selected : I), exponent selected ≠ 0) (notInput : ∀ (selected : I) (input : Fin n), exponent selected ≠ Finsupp.single (inputVariables input) 1) (outputs : Fin m → MvPolynomial σ K) (circuit : Circuit (Arithmetic.signature C) n m) (constructs : Multiple.Constructs (inputProblem inputVariables) outputs circuit) : Module.finrank K ↥(Submodule.span K (Set.range (⇑(coefficientFeature exponent) ∘ outputs))) ≤ circuit.cost Arithmetic.multiplicationCost

The dimension of the selected-coefficient span of arbitrary requested polynomials is at most the multiplication cost of a circuit producing them.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.coefficientMatrix_rank_le_multiplicationCost {K : Type u} {C : Type v} {σ : Type w} {I : Type x} {n m : ℕ} [Field K] [DecidableEq σ] (constant : C → K) (inputVariables : Fin n → σ) (exponent : I → σ →₀ ℕ) (nonconstant : ∀ (selected : I), exponent selected ≠ 0) (notInput : ∀ (selected : I) (input : Fin n), exponent selected ≠ Finsupp.single (inputVariables input) 1) (outputs : Fin m → MvPolynomial σ K) (circuit : Circuit (Arithmetic.signature C) n m) (constructs : Multiple.Constructs (inputProblem inputVariables) outputs circuit) : (coefficientMatrix exponent outputs).rank ≤ circuit.cost Arithmetic.multiplicationCost

The selected coefficient-matrix rank lower-bounds multiplication cost.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.coefficientMatrix_rank_le_gateCost {K : Type u} {C : Type v} {σ : Type w} {I : Type x} {n m : ℕ} [Field K] [DecidableEq σ] (constant : C → K) (inputVariables : Fin n → σ) (exponent : I → σ →₀ ℕ) (nonconstant : ∀ (selected : I), exponent selected ≠ 0) (notInput : ∀ (selected : I) (input : Fin n), exponent selected ≠ Finsupp.single (inputVariables input) 1) (outputs : Fin m → MvPolynomial σ K) (circuit : Circuit (Arithmetic.signature C) n m) (constructs : Multiple.Constructs (inputProblem inputVariables) outputs circuit) : (coefficientMatrix exponent outputs).rank ≤ circuit.cost Arithmetic.gateCost

Selected coefficient-matrix rank also lower-bounds total nonconstant gate cost.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.coefficientMatrix_rank_le_size {K : Type u} {C : Type v} {σ : Type w} {I : Type x} {n m : ℕ} [Field K] [DecidableEq σ] (constant : C → K) (inputVariables : Fin n → σ) (exponent : I → σ →₀ ℕ) (nonconstant : ∀ (selected : I), exponent selected ≠ 0) (notInput : ∀ (selected : I) (input : Fin n), exponent selected ≠ Finsupp.single (inputVariables input) 1) (outputs : Fin m → MvPolynomial σ K) (circuit : Circuit (Arithmetic.signature C) n m) (constructs : Multiple.Constructs (inputProblem inputVariables) outputs circuit) : (coefficientMatrix exponent outputs).rank ≤ circuit.size

Selected coefficient-matrix rank lower-bounds raw circuit size.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.circuit_multiplication_lowerBound {K : Type u} {C : Type v} {σ : Type w} {n m : ℕ} [Field K] [DecidableEq σ] (constant : C → K) (inputVariables : Fin n → σ) (exponent : Fin m → σ →₀ ℕ) (injective : Function.Injective exponent) (nonconstant : ∀ (output : Fin m), exponent output ≠ 0) (notInput : ∀ (output : Fin m) (input : Fin n), exponent output ≠ Finsupp.single (inputVariables input) 1) (circuit : Circuit (Arithmetic.signature C) n m) (constructs : Multiple.Constructs (inputProblem inputVariables) (targets exponent) circuit) : m ≤ circuit.cost Arithmetic.multiplicationCost

Computing m distinct selected monomials, none constant or already a free input, requires at least m multiplication gates.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.circuit_gate_lowerBound {K : Type u} {C : Type v} {σ : Type w} {n m : ℕ} [Field K] [DecidableEq σ] (constant : C → K) (inputVariables : Fin n → σ) (exponent : Fin m → σ →₀ ℕ) (injective : Function.Injective exponent) (nonconstant : ∀ (output : Fin m), exponent output ≠ 0) (notInput : ∀ (output : Fin m) (input : Fin n), exponent output ≠ Finsupp.single (inputVariables input) 1) (circuit : Circuit (Arithmetic.signature C) n m) (constructs : Multiple.Constructs (inputProblem inputVariables) (targets exponent) circuit) : m ≤ circuit.cost Arithmetic.gateCost

Total nonconstant arithmetic-gate cost is at least the number of selected monomial outputs.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.circuit_size_lowerBound {K : Type u} {C : Type v} {σ : Type w} {n m : ℕ} [Field K] [DecidableEq σ] (constant : C → K) (inputVariables : Fin n → σ) (exponent : Fin m → σ →₀ ℕ) (injective : Function.Injective exponent) (nonconstant : ∀ (output : Fin m), exponent output ≠ 0) (notInput : ∀ (output : Fin m) (input : Fin n), exponent output ≠ Finsupp.single (inputVariables input) 1) (circuit : Circuit (Arithmetic.signature C) n m) (constructs : Multiple.Constructs (inputProblem inputVariables) (targets exponent) circuit) : m ≤ circuit.size

Raw circuit size is at least the number of selected monomial outputs.