Root-multiplicity shadows for polynomial circuits

For finitely many points, record the root multiplicity of a polynomial at each point and cast those natural numbers into the coefficient field. Away from the zero polynomial, root multiplicities add under multiplication. We send the zero polynomial to the zero vector; if a product is zero, the multiplicative-shadow rule instead uses zero coefficients. This gives a total feature suitable for circuits that may contain zero intermediate values.

As a concrete application, one circuit producing the distinct nonzero shifts X - a_i from X needs one addition per shift. Multiplications, arbitrary field constants, cancellation, and sharing between outputs remain entirely unrestricted.

noncomputable def Algebraic.Fusion.Arithmetic.MultiplicativeShadow.RootMultiplicity.rootMultiplicityFeature {K : Type u} {m : ℕ} [Field K] (points : Fin m → K) (polynomial : Polynomial K) : Fin m → K

Vector of root multiplicities at the selected points, cast into K.

Equations

• Algebraic.Fusion.Arithmetic.MultiplicativeShadow.RootMultiplicity.rootMultiplicityFeature points polynomial point = ↑(Polynomial.rootMultiplicity (points point) polynomial)

@[simp]

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.RootMultiplicity.rootMultiplicityFeature_zero {K : Type u} {m : ℕ} [Field K] (points : Fin m → K) : rootMultiplicityFeature points 0 = 0

@[simp]

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.RootMultiplicity.rootMultiplicityFeature_C {K : Type u} {m : ℕ} [Field K] (points : Fin m → K) (value : K) : rootMultiplicityFeature points (Polynomial.C value) = 0

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.RootMultiplicity.rootMultiplicityFeature_mul_of_ne_zero {K : Type u} {m : ℕ} [Field K] (points : Fin m → K) {left right : Polynomial K} (product_ne_zero : left * right ≠ 0) : rootMultiplicityFeature points (left * right) = rootMultiplicityFeature points left + rootMultiplicityFeature points right

Root-multiplicity vectors add under a nonzero polynomial product.

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.RootMultiplicity.rootMultiplicityFeature_mul_span {K : Type u} {m : ℕ} [Field K] (points : Fin m → K) (left right : Polynomial K) : ∃ (leftScalar : K) (rightScalar : K), rootMultiplicityFeature points (left * right) = leftScalar • rootMultiplicityFeature points left + rightScalar • rootMultiplicityFeature points right

Total span propagation, including products that vanish.

noncomputable def Algebraic.Fusion.Arithmetic.MultiplicativeShadow.RootMultiplicity.certificate {K : Type u} {C : Type v} {m : ℕ} [Field K] (constant : C → K) (problem : Problem (Polynomial K)) (points : Fin m → K) (input_zero : ∀ (input : Fin problem.inputCount) (point : Fin m), Polynomial.rootMultiplicity (points point) (problem.inputs input) = 0) : Certificate (fun (scalar : C) => Polynomial.C (constant scalar)) problem

Root-multiplicity certificate for any polynomial construction problem whose free inputs do not vanish at the selected points.

Equations

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

@[simp]

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.RootMultiplicity.certificate_feature {K : Type u} {C : Type v} {m : ℕ} [Field K] (constant : C → K) (problem : Problem (Polynomial K)) (points : Fin m → K) (input_zero : ∀ (input : Fin problem.inputCount) (point : Fin m), Polynomial.rootMultiplicity (points point) (problem.inputs input) = 0) (polynomial : Polynomial K) : (certificate constant problem points input_zero).feature polynomial = rootMultiplicityFeature points polynomial

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.RootMultiplicity.rootMultiplicityFeatureSpan_finrank_le_additionCost {K : Type u} {C : Type v} {r m : ℕ} [Field K] (constant : C → K) (problem : Problem (Polynomial K)) (points : Fin r → K) (input_zero : ∀ (input : Fin problem.inputCount) (point : Fin r), Polynomial.rootMultiplicity (points point) (problem.inputs input) = 0) (targets : Fin m → Polynomial K) (circuit : Circuit (Arithmetic.signature C) problem.inputCount m) (constructs : Interaction.Multiple.Constructs problem targets circuit) : Module.finrank K ↥(Submodule.span K (Set.range (rootMultiplicityFeature points ∘ targets))) ≤ circuit.cost Arithmetic.additionCost

The span rank of any requested root-multiplicity vectors is bounded by the addition cost of a circuit constructing those polynomials.

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.RootMultiplicity.circuit_addition_lowerBound_of_rootMultiplicityFeature {K : Type u} {C : Type v} {r m : ℕ} [Field K] (constant : C → K) (problem : Problem (Polynomial K)) (points : Fin r → K) (input_zero : ∀ (input : Fin problem.inputCount) (point : Fin r), Polynomial.rootMultiplicity (points point) (problem.inputs input) = 0) (targets : Fin m → Polynomial K) (independent : LinearIndependent K (rootMultiplicityFeature points ∘ targets)) (circuit : Circuit (Arithmetic.signature C) problem.inputCount m) (constructs : Interaction.Multiple.Constructs problem targets circuit) : m ≤ circuit.cost Arithmetic.additionCost

Independent root-multiplicity vectors force one addition per requested output.

noncomputable def Algebraic.Fusion.Arithmetic.MultiplicativeShadow.RootMultiplicity.shiftProblem {K : Type u} [Field K] : Problem (Polynomial K)

The one-input construction problem used for the shift family. Its single-output target is irrelevant to the multi-output theorem.

Equations

• Algebraic.Fusion.Arithmetic.MultiplicativeShadow.RootMultiplicity.shiftProblem = { inputCount := 1, inputs := fun (x : Fin 1) => Polynomial.X, target := 0 }

noncomputable def Algebraic.Fusion.Arithmetic.MultiplicativeShadow.RootMultiplicity.shiftTargets {K : Type u} {m : ℕ} [Field K] (points : Fin m → K) : Fin m → Polynomial K

Distinct affine shifts requested as simultaneous outputs.

Equations

• Algebraic.Fusion.Arithmetic.MultiplicativeShadow.RootMultiplicity.shiftTargets points point = Polynomial.X - Polynomial.C (points point)

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.RootMultiplicity.rootMultiplicity_X_eq_zero {K : Type u} [Field K] {point : K} (point_ne_zero : point ≠ 0) : Polynomial.rootMultiplicity point Polynomial.X = 0

A nonzero point is not a root of the free input X.

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.RootMultiplicity.rootMultiplicityFeature_shiftTargets {K : Type u} {m : ℕ} [Field K] (points : Fin m → K) (injective : Function.Injective points) (point : Fin m) : rootMultiplicityFeature points (shiftTargets points point) = Pi.single point 1

At distinct points, the shift targets have the standard-basis root-multiplicity vectors.

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.RootMultiplicity.linearIndependent_rootMultiplicityFeature_shiftTargets {K : Type u} {m : ℕ} [Field K] (points : Fin m → K) (injective : Function.Injective points) : LinearIndependent K (rootMultiplicityFeature points ∘ shiftTargets points)

Root-multiplicity shadows of distinct shifts are linearly independent.

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.RootMultiplicity.shiftTargets_addition_lowerBound {K : Type u} {C : Type v} {m : ℕ} [Field K] (constant : C → K) (points : Fin m → K) (injective : Function.Injective points) (nonzero : ∀ (point : Fin m), points point ≠ 0) (circuit : Circuit (Arithmetic.signature C) 1 m) (constructs : circuit.eval (Arithmetic.interpretation fun (scalar : C) => Polynomial.C (constant scalar)) shiftProblem.inputs = shiftTargets points) : m ≤ circuit.cost Arithmetic.additionCost

One circuit producing m distinct nonzero affine shifts of its free input needs at least m addition gates.