Exact nonlinear coordinates for polynomial quotient Fusion

In the standard n-variable polynomial model, every field constant and every variable is free. The free-data submodule is therefore the affine-linear polynomials. Extract all coefficients except the constant and degree-one variable coefficients.

This module proves that the joint nonlinear coefficient map has exactly the affine-linear submodule as its kernel. Consequently, the rank of the full nonlinear coefficient matrix of any output family equals—rather than merely lower-bounds—the canonical quotient-output rank.

@[reducible, inline]

abbrev Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Nonlinear.Exponent (n : ℕ) : Type

Exponents other than the constant exponent and individual degree-one variable exponents.

Equations

• Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Nonlinear.Exponent n = { exponent : Fin n →₀ ℕ // exponent ≠ 0 ∧ ∀ (input : Fin n), exponent ≠ Finsupp.single input 1 }

noncomputable def Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Nonlinear.coefficientFeature {K : Type u} [Field K] (n : ℕ) : MvPolynomial (Fin n) K →ₗ[K] Exponent n → K

Joint extraction of every nonlinear monomial coefficient.

Equations

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

@[reducible, inline]

noncomputable abbrev Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Nonlinear.inputProblem (K : Type u) [Field K] (n : ℕ) : Problem (MvPolynomial (Fin n) K)

Standard polynomial problem with all variables free.

Equations

• Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Nonlinear.inputProblem K n = Algebraic.Fusion.Arithmetic.Interaction.Polynomial.inputProblem fun (input : Fin n) => input

@[reducible, inline]

noncomputable abbrev Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Nonlinear.affineSubmodule (K : Type u) [Field K] (n : ℕ) : Submodule K (MvPolynomial (Fin n) K)

Affine-linear polynomial submodule generated by all constants and variables.

Equations

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

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Nonlinear.C_mem_affineSubmodule {K : Type u} [Field K] (n : ℕ) (scalar : K) : MvPolynomial.C scalar ∈ affineSubmodule K n

Every constant polynomial is affine-linear.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Nonlinear.X_mem_affineSubmodule {K : Type u} [Field K] (n : ℕ) (input : Fin n) : MvPolynomial.X input ∈ affineSubmodule K n

Every variable polynomial is affine-linear.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Nonlinear.monomial_mem_affineSubmodule_of_not_nonlinear {K : Type u} [Field K] (n : ℕ) (exponent : Fin n →₀ ℕ) (notNonlinear : ¬(exponent ≠ 0 ∧ ∀ (input : Fin n), exponent ≠ Finsupp.single input 1)) (coefficient : K) : (MvPolynomial.monomial exponent) coefficient ∈ affineSubmodule K n

A monomial whose exponent is not nonlinear is affine-linear.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Nonlinear.affineSubmodule_le_ker_coefficientFeature {K : Type u} [Field K] (n : ℕ) : affineSubmodule K n ≤ (coefficientFeature n).ker

Affine-linear polynomials have no nonlinear coefficients.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Nonlinear.ker_coefficientFeature_le_affineSubmodule {K : Type u} [Field K] (n : ℕ) : (coefficientFeature n).ker ≤ affineSubmodule K n

Vanishing of every nonlinear coefficient forces a polynomial to be affine-linear.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Nonlinear.ker_coefficientFeature {K : Type u} [Field K] (n : ℕ) : (coefficientFeature n).ker = affineSubmodule K n

Exact kernel characterization of the joint nonlinear coefficient map.

def Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Nonlinear.coefficientMatrix {K : Type u} {m : ℕ} [Field K] (n : ℕ) (outputs : Fin m → MvPolynomial (Fin n) K) : Matrix (Exponent n) (Fin m) K

Full nonlinear coefficient matrix of an output family.

Equations

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

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Nonlinear.coefficientMatrix_rank_eq_outputRank {K : Type u} {m : ℕ} [Field K] (n : ℕ) (outputs : Fin m → MvPolynomial (Fin n) K) : (coefficientMatrix n outputs).rank = Linear.Quotient.outputRank (⇑MvPolynomial.C) (inputProblem K n) outputs

Full nonlinear coefficient rank is exactly the canonical quotient-output rank modulo affine-linear polynomials.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Nonlinear.coefficientMatrix_rank_le_multiplicationCost {K : Type u} {m : ℕ} [Field K] (n : ℕ) (outputs : Fin m → MvPolynomial (Fin n) K) (circuit : Circuit (Arithmetic.signature K) n m) (constructs : Multiple.Constructs (inputProblem K n) outputs circuit) : (coefficientMatrix n outputs).rank ≤ circuit.cost Arithmetic.multiplicationCost

Full nonlinear coefficient rank lower-bounds multiplication cost for standard polynomial circuits with arbitrary field constants and cancellation.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Nonlinear.coefficientMatrix_rank_le_size {K : Type u} {m : ℕ} [Field K] (n : ℕ) (outputs : Fin m → MvPolynomial (Fin n) K) (circuit : Circuit (Arithmetic.signature K) n m) (constructs : Multiple.Constructs (inputProblem K n) outputs circuit) : (coefficientMatrix n outputs).rank ≤ circuit.size

Full nonlinear coefficient rank lower-bounds raw standard-circuit size.