Multiplicative-shadow lower bounds for arithmetic circuits

An additive interaction certificate linearizes addition and charges the new directions created by multiplication. This module records the operation-dual principle. Suppose a feature of a product always belongs to the span of the two operand features. Free inputs and named constants start with zero feature. A multiplication gate then creates no new feature direction, while one addition gate can create at most the direction of its result.

Consequently, the common span of the requested output features has dimension at most the number of addition gates. The argument permits arbitrary constants, cancellation, zero intermediate values, and sharing between all outputs. It deliberately asks for no rule governing the feature of a sum.

The motivating specialization sends a nonzero rational function to its factor-exponent, divisor, or valuation vector modulo the free inputs and constants. Multiplication is addition in that vector space, whereas an addition can introduce at most one new divisor direction.

This is a machine-checked feature-span presentation of the classical addition-rank viewpoint, not a claim that addition rank is new. See:

• D. G. Kirkpatrick and Z. M. Kedem, Addition Requirements for Rational Functions (1977), https://doi.org/10.1137/0206015.
• C. P. Schnorr and J. P. Van de Wiele, On the Additive Complexity of Polynomials (1980), https://doi.org/10.1016/0304-3975(80)90068-7.

structure Algebraic.Fusion.Arithmetic.MultiplicativeShadow.Certificate {K : Type u} {C : Type v} {U : Type w} {Q : Type x} [Semiring K] [Mul U] [AddCommMonoid Q] [Module K Q] (constant : C → U) (problem : Problem U) : Type (max w x)

A feature for which multiplication creates no direction outside the span of the operand features.

• feature : U → Q

  Feature used to obstruct the requested outputs.

• input_zero (input : Fin problem.inputCount) : self.feature (problem.inputs input) = 0

  Free inputs have zero feature.

• constant_zero (scalar : C) : self.feature (constant scalar) = 0

  Named constants have zero feature.

• feature_mul (left right : U) : ∃ (leftScalar : K) (rightScalar : K), self.feature (left * right) = leftScalar • self.feature left + rightScalar • self.feature right

  A product feature belongs to the span of its two operand features.

def Algebraic.Fusion.Arithmetic.MultiplicativeShadow.Certificate.comap {K : Type u} {C : Type v} {Q : Type x} [Semiring K] [AddCommMonoid Q] [Module K Q] {U₁ : Type y} {U₂ : Type z} [Mul U₁] [Mul U₂] (sourceConstant : C → U₁) (targetConstant : C → U₂) (problem : Problem U₁) (map : U₁ → U₂) (map_mul : ∀ (left right : U₁), map (left * right) = map left * map right) (map_constant : ∀ (scalar : C), map (sourceConstant scalar) = targetConstant scalar) (certificate : Certificate targetConstant (problem.map map)) : Certificate sourceConstant problem

Pull a multiplicative-shadow certificate back along a multiplication-preserving semantic map. The map need not preserve addition: addition results are retained as fresh shadow generators anyway.

Equations

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

@[simp]

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.Certificate.comap_feature {K : Type u} {C : Type v} {Q : Type x} [Semiring K] [AddCommMonoid Q] [Module K Q] {U₁ : Type y} {U₂ : Type z} [Mul U₁] [Mul U₂] (sourceConstant : C → U₁) (targetConstant : C → U₂) (problem : Problem U₁) (map : U₁ → U₂) (map_mul : ∀ (left right : U₁), map (left * right) = map left * map right) (map_constant : ∀ (scalar : C), map (sourceConstant scalar) = targetConstant scalar) (certificate : Certificate targetConstant (problem.map map)) (value : U₁) : (comap sourceConstant targetConstant problem map map_mul map_constant certificate).feature value = certificate.feature (map value)

def Algebraic.Fusion.Arithmetic.MultiplicativeShadow.Atom.additionShadow? {K : Type u} {C : Type v} {U : Type w} {Q : Type x} [Semiring K] [Add U] [Mul U] [AddCommMonoid Q] [Module K Q] {constant : C → U} {problem : Problem U} (certificate : Certificate constant problem) (atom : Atom (Arithmetic.signature C) U) : Option Q

Retain the feature of an addition result and discard multiplication and constant atoms.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.Fusion.Arithmetic.MultiplicativeShadow.Atom.additionShadow? certificate { op := Algebraic.Arithmetic.Op.mul, arguments := arguments } = none
• Algebraic.Fusion.Arithmetic.MultiplicativeShadow.Atom.additionShadow? certificate { op := Algebraic.Arithmetic.Op.constant value, arguments := arguments } = none

def Algebraic.Fusion.Arithmetic.MultiplicativeShadow.additionShadows {K : Type u} {C : Type v} {U : Type w} {Q : Type x} [Semiring K] [Add U] [Mul U] [AddCommMonoid Q] [Module K Q] {constant : C → U} {problem : Problem U} (certificate : Certificate constant problem) (atoms : List (Atom (Arithmetic.signature C) U)) : List Q

Addition-result shadows extracted from a list of arithmetic atoms.

Equations

• Algebraic.Fusion.Arithmetic.MultiplicativeShadow.additionShadows certificate atoms = List.filterMap (Algebraic.Fusion.Arithmetic.MultiplicativeShadow.Atom.additionShadow? certificate) atoms

@[simp]

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.additionShadows_cons_add {K : Type u} {C : Type v} {U : Type w} {Q : Type x} [Semiring K] [Add U] [Mul U] [AddCommMonoid Q] [Module K Q] {constant : C → U} {problem : Problem U} (certificate : Certificate constant problem) (arguments : Fin 2 → U) (atoms : List (Atom (Arithmetic.signature C) U)) : additionShadows certificate ({ op := Arithmetic.Op.add, arguments := arguments } :: atoms) = certificate.feature (arguments 0 + arguments 1) :: additionShadows certificate atoms

@[simp]

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.additionShadows_cons_mul {K : Type u} {C : Type v} {U : Type w} {Q : Type x} [Semiring K] [Add U] [Mul U] [AddCommMonoid Q] [Module K Q] {constant : C → U} {problem : Problem U} (certificate : Certificate constant problem) (arguments : Fin 2 → U) (atoms : List (Atom (Arithmetic.signature C) U)) : additionShadows certificate ({ op := Arithmetic.Op.mul, arguments := arguments } :: atoms) = additionShadows certificate atoms

@[simp]

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.additionShadows_cons_constant {K : Type u} {C : Type v} {U : Type w} {Q : Type x} [Semiring K] [Add U] [Mul U] [AddCommMonoid Q] [Module K Q] {constant : C → U} {problem : Problem U} (certificate : Certificate constant problem) (scalar : C) (arguments : Fin (Arithmetic.arity (Arithmetic.Op.constant scalar)) → U) (atoms : List (Atom (Arithmetic.signature C) U)) : additionShadows certificate ({ op := Arithmetic.Op.constant scalar, arguments := arguments } :: atoms) = additionShadows certificate atoms

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.additionShadows_length {K : Type u} {C : Type v} {U : Type w} {Q : Type x} [Semiring K] [Add U] [Mul U] [AddCommMonoid Q] [Module K Q] {constant : C → U} {problem : Problem U} (certificate : Certificate constant problem) (atoms : List (Atom (Arithmetic.signature C) U)) : (additionShadows certificate atoms).length = Atom.listCost atoms Arithmetic.additionCost

The number of retained shadows is exactly the addition cost.

noncomputable def Algebraic.Fusion.Arithmetic.MultiplicativeShadow.generatedSubmodule {K : Type u} {C : Type v} {U : Type w} {Q : Type x} [Semiring K] [Add U] [Mul U] [AddCommMonoid Q] [Module K Q] {constant : C → U} {problem : Problem U} (certificate : Certificate constant problem) (atoms : List (Atom (Arithmetic.signature C) U)) : Submodule K Q

Submodule generated by the shadows of all addition results in an atom list.

Equations

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

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.additionShadow_mem_generatedSubmodule {K : Type u} {C : Type v} {U : Type w} {Q : Type x} [Semiring K] [Add U] [Mul U] [AddCommMonoid Q] [Module K Q] {constant : C → U} {problem : Problem U} (certificate : Certificate constant problem) (atoms : List (Atom (Arithmetic.signature C) U)) (arguments : Fin 2 → U) (present : { op := Arithmetic.Op.add, arguments := arguments } ∈ atoms) : certificate.feature (arguments 0 + arguments 1) ∈ generatedSubmodule certificate atoms

The shadow of an addition atom in the list belongs to the generated submodule.

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.feature_trace_mem_of_programAtoms_subset {K : Type u} {C : Type v} {U : Type w} {Q : Type x} [Semiring K] [Add U] [Mul U] [AddCommMonoid Q] [Module K Q] {g : ℕ} {constant : C → U} {problem : Problem U} (certificate : Certificate constant problem) (program : Program (Arithmetic.signature C) problem.inputCount g) (allAtoms : List (Atom (Arithmetic.signature C) U)) (atomsSubset : ∀ atom ∈ programAtoms (Arithmetic.interpretation constant) problem.inputs program, atom ∈ allAtoms) (wire : Wire problem.inputCount g) : certificate.feature (program.trace (Arithmetic.interpretation constant) problem.inputs wire) ∈ generatedSubmodule certificate allAtoms

Every wire feature lies in the span of addition-result shadows from any atom list containing the whole program.

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.feature_circuit_output_mem {K : Type u} {C : Type v} {U : Type w} {Q : Type x} [Semiring K] [Add U] [Mul U] [AddCommMonoid Q] [Module K Q] {m : ℕ} {constant : C → U} {problem : Problem U} (certificate : Certificate constant problem) (circuit : Circuit (Arithmetic.signature C) problem.inputCount m) (output : Fin m) : certificate.feature (circuit.eval (Arithmetic.interpretation constant) problem.inputs output) ∈ generatedSubmodule certificate (circuitAtoms circuit (Arithmetic.interpretation constant) problem.inputs)

Every output feature lies in the common span of the circuit's addition result shadows.

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.targetFeature_mem_circuitSubmodule {K : Type u} {C : Type v} {U : Type w} {Q : Type x} [Field K] [Add U] [Mul U] [AddCommMonoid Q] [Module K Q] {m : ℕ} {constant : C → U} {problem : Problem U} (certificate : Certificate constant problem) (targets : Fin m → U) (circuit : Circuit (Arithmetic.signature C) problem.inputCount m) (constructs : Interaction.Multiple.Constructs problem targets circuit) (output : Fin m) : certificate.feature (targets output) ∈ generatedSubmodule certificate (circuitAtoms circuit (Arithmetic.interpretation constant) problem.inputs)

Every requested output feature belongs to the common addition-shadow span of a constructing circuit.

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.featureSpan_finrank_le_additionCost {K : Type u} {C : Type v} {U : Type w} {Q : Type x} [Field K] [Add U] [Mul U] [AddCommMonoid Q] [Module K Q] {m : ℕ} {constant : C → U} {problem : Problem U} (certificate : Certificate constant problem) (targets : Fin m → U) (circuit : Circuit (Arithmetic.signature C) problem.inputCount m) (constructs : Interaction.Multiple.Constructs problem targets circuit) : Module.finrank K ↥(Submodule.span K (Set.range (certificate.feature ∘ targets))) ≤ circuit.cost Arithmetic.additionCost

The dimension of the requested output-shadow span is at most the number of addition gates.

theorem Algebraic.Fusion.Arithmetic.MultiplicativeShadow.circuit_addition_lowerBound_of_linearIndependent {K : Type u} {C : Type v} {U : Type w} {Q : Type x} [Field K] [Add U] [Mul U] [AddCommMonoid Q] [Module K Q] {m : ℕ} {constant : C → U} {problem : Problem U} (certificate : Certificate constant problem) (targets : Fin m → U) (independent : LinearIndependent K (certificate.feature ∘ targets)) (circuit : Circuit (Arithmetic.signature C) problem.inputCount m) (constructs : Interaction.Multiple.Constructs problem targets circuit) : m ≤ circuit.cost Arithmetic.additionCost

Linearly independent output shadows force one addition gate per output.