Polynomial coordinates on the canonical nonlinear quotient

Selected nonconstant, non-input coefficients vanish on the polynomial free-data submodule, so the coefficient feature factors through the canonical quotient by inputs and named constants. The rank of a selected coefficient matrix is therefore bounded by the coordinate-free quotient-output rank.

This identifies coefficient arguments as explicit coordinate witnesses for the canonical quotient obstruction rather than a separate lower-bound method.

noncomputable def Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Quotient.coefficientFeatureOnQuotient {K : Type u} {C : Type v} {σ : Type w} {I : Type x} {n : ℕ} [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) : MvPolynomial σ K ⧸ Linear.Quotient.freeSubmodule K (fun (scalar : C) => MvPolynomial.C (constant scalar)) (inputProblem inputVariables) →ₗ[K] I → K

Selected coefficients, descended to the quotient by free inputs and named constants.

Equations

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

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Quotient.coefficientFeatureOnQuotient_mkQ {K : Type u} {C : Type v} {σ : Type w} {I : Type x} {n : ℕ} [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) (polynomial : MvPolynomial σ K) : (coefficientFeatureOnQuotient constant inputVariables exponent nonconstant notInput) ((Linear.Quotient.freeSubmodule K (fun (scalar : C) => MvPolynomial.C (constant scalar)) (inputProblem inputVariables)).mkQ polynomial) = (coefficientFeature exponent) polynomial

Descending to the quotient and then taking selected coefficients agrees with taking selected coefficients directly.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Quotient.coefficientMatrix_rank_le_outputRank {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) : (coefficientMatrix exponent outputs).rank ≤ Linear.Quotient.outputRank (fun (scalar : C) => MvPolynomial.C (constant scalar)) (inputProblem inputVariables) outputs

Selected coefficient-matrix rank cannot exceed the canonical output rank modulo free inputs and named constants.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Quotient.coefficientMatrix_rank_eq_outputRank_of_ker_eq {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) (kernel_eq : (coefficientFeature exponent).ker = Linear.Quotient.freeSubmodule K (fun (scalar : C) => MvPolynomial.C (constant scalar)) (inputProblem inputVariables)) (outputs : Fin m → MvPolynomial σ K) : (coefficientMatrix exponent outputs).rank = Linear.Quotient.outputRank (fun (scalar : C) => MvPolynomial.C (constant scalar)) (inputProblem inputVariables) outputs

If the selected coefficient feature has exactly the free-data submodule as its kernel, then its matrix rank equals the canonical quotient-output rank.

theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Quotient.coefficientMatrix_rank_le_multiplicationCost_viaQuotient {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 coordinate comparison and canonical quotient theorem recover the selected coefficient-matrix multiplication lower bound.