Linear mixtures of monomial outputs

Apply an arbitrary coefficient matrix to a family of distinct selected monomials. The selected coefficient matrix of the resulting outputs is exactly the mixing matrix, so its rank lower-bounds multiplication cost.

The unitriangular prefix matrix supplies a concrete full-rank example over every field: output j is the sum of monomials 0, ..., j. These outputs have strongly overlapping support, unlike the basis family itself.

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

Outputs obtained by using the columns of mix as coefficients of the selected monomial family.

Equations

• Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Mixing.targets exponent mix output = ∑ selected : Fin m, (MvPolynomial.monomial (exponent selected)) (mix selected output)

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Mixing.coefficientMatrix_targets {K : Type u} {σ : Type w} {m : ℕ} [CommSemiring K] [DecidableEq σ] (exponent : Fin m → σ →₀ ℕ) (injective : Function.Injective exponent) (mix : Matrix (Fin m) (Fin m) K) : coefficientMatrix exponent (targets exponent mix) = mix

Distinct monomials make the selected coefficient matrix of mixed outputs equal to the mixing matrix itself.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Mixing.matrix_rank_le_multiplicationCost {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 : ∀ (selected : Fin m), exponent selected ≠ 0) (notInput : ∀ (selected : Fin m) (input : Fin n), exponent selected ≠ Finsupp.single (inputVariables input) 1) (mix : Matrix (Fin m) (Fin m) K) (circuit : Circuit (Arithmetic.signature C) n m) (constructs : Multiple.Constructs (inputProblem inputVariables) (targets exponent mix) circuit) : mix.rank ≤ circuit.cost Arithmetic.multiplicationCost

The rank of any monomial mixing matrix lower-bounds multiplication cost.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Mixing.circuit_multiplication_lowerBound_of_det_ne_zero {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 : ∀ (selected : Fin m), exponent selected ≠ 0) (notInput : ∀ (selected : Fin m) (input : Fin n), exponent selected ≠ Finsupp.single (inputVariables input) 1) (mix : Matrix (Fin m) (Fin m) K) (det_ne_zero : mix.det ≠ 0) (circuit : Circuit (Arithmetic.signature C) n m) (constructs : Multiple.Constructs (inputProblem inputVariables) (targets exponent mix) circuit) : m ≤ circuit.cost Arithmetic.multiplicationCost

A nonsingular mixing of m monomials still requires at least m multiplications.

def Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Mixing.prefixMatrix (K : Type u) [Zero K] [One K] (m : ℕ) : Matrix (Fin m) (Fin m) K

Upper-unitriangular prefix-sum mixing matrix.

Equations

• Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Mixing.prefixMatrix K m selected output = if selected ≤ output then 1 else 0

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Mixing.prefixMatrix_isUpperTriangular {K : Type u} [Semiring K] (m : ℕ) : (prefixMatrix K m).IsUpperTriangular

The prefix matrix is upper triangular.

@[simp]

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Mixing.prefixMatrix_diagonal {K : Type u} [Semiring K] (m : ℕ) (index : Fin m) : prefixMatrix K m index index = 1

@[simp]

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Mixing.prefixMatrix_det {K : Type u} [CommRing K] (m : ℕ) : (prefixMatrix K m).det = 1

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

Prefix sums of a selected monomial family.

Equations

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

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Mixing.prefixTargets_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 : ∀ (selected : Fin m), exponent selected ≠ 0) (notInput : ∀ (selected : Fin m) (input : Fin n), exponent selected ≠ Finsupp.single (inputVariables input) 1) (circuit : Circuit (Arithmetic.signature C) n m) (constructs : Multiple.Constructs (inputProblem inputVariables) (prefixTargets exponent) circuit) : m ≤ circuit.cost Arithmetic.multiplicationCost

Computing all prefix sums of m distinct nonlinear monomials requires at least m multiplications over every field.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Mixing.prefixTargets_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 : ∀ (selected : Fin m), exponent selected ≠ 0) (notInput : ∀ (selected : Fin m) (input : Fin n), exponent selected ≠ Finsupp.single (inputVariables input) 1) (circuit : Circuit (Arithmetic.signature C) n m) (constructs : Multiple.Constructs (inputProblem inputVariables) (prefixTargets exponent) circuit) : m ≤ circuit.cost Arithmetic.gateCost

Prefix-sum outputs also force total gate cost at least m.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Mixing.prefixTargets_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 : ∀ (selected : Fin m), exponent selected ≠ 0) (notInput : ∀ (selected : Fin m) (input : Fin n), exponent selected ≠ Finsupp.single (inputVariables input) 1) (circuit : Circuit (Arithmetic.signature C) n m) (constructs : Multiple.Constructs (inputProblem inputVariables) (prefixTargets exponent) circuit) : m ≤ circuit.size

Prefix-sum outputs force raw circuit size at least m.