Linear-feature Fusion for arithmetic circuits

Any linear feature that vanishes on the free inputs and named constants gives an interaction-span certificate: declare the feature of a product itself to be the new interaction created by that multiplication. Thus each multiplication gate can add at most one direction to the common feature span.

This deliberately weak product rule is useful for multi-output lower bounds. It permits arbitrary constants and cancellation and requires no special identity beyond linearity of the chosen feature.

def Algebraic.Fusion.Arithmetic.Interaction.Linear.certificate {K : Type u} {C : Type v} {U : Type w} {Q : Type x} [Semiring K] [AddCommMonoid U] [Module K U] [Mul U] [AddCommMonoid Q] [Module K Q] (constant : C → U) (problem : Problem U) (feature : U →ₗ[K] Q) (input_zero : ∀ (input : Fin problem.inputCount), feature (problem.inputs input) = 0) (constant_zero : ∀ (scalar : C), feature (constant scalar) = 0) : Certificate constant problem

Turn a linear feature annihilating inputs and constants into an interaction certificate. The interaction of a product is its whole feature, so no feature information is propagated from either operand.

Equations

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

@[simp]

theorem Algebraic.Fusion.Arithmetic.Interaction.Linear.certificate_feature {K : Type u} {C : Type v} {U : Type w} {Q : Type x} [Semiring K] [AddCommMonoid U] [Module K U] [Mul U] [AddCommMonoid Q] [Module K Q] (constant : C → U) (problem : Problem U) (feature : U →ₗ[K] Q) (input_zero : ∀ (input : Fin problem.inputCount), feature (problem.inputs input) = 0) (constant_zero : ∀ (scalar : C), feature (constant scalar) = 0) (value : U) : (certificate constant problem feature input_zero constant_zero).feature value = feature value

@[simp]

theorem Algebraic.Fusion.Arithmetic.Interaction.Linear.certificate_interaction {K : Type u} {C : Type v} {U : Type w} {Q : Type x} [Semiring K] [AddCommMonoid U] [Module K U] [Mul U] [AddCommMonoid Q] [Module K Q] (constant : C → U) (problem : Problem U) (feature : U →ₗ[K] Q) (input_zero : ∀ (input : Fin problem.inputCount), feature (problem.inputs input) = 0) (constant_zero : ∀ (scalar : C), feature (constant scalar) = 0) (left right : U) : (certificate constant problem feature input_zero constant_zero).interaction left right = feature (left * right)

theorem Algebraic.Fusion.Arithmetic.Interaction.Linear.circuit_multiplication_lowerBound_of_linearIndependent {K : Type u} {C : Type v} {U : Type w} {Q : Type x} [Field K] [AddCommGroup U] [Module K U] [Mul U] [AddCommGroup Q] [Module K Q] {m : ℕ} (constant : C → U) (problem : Problem U) (feature : U →ₗ[K] Q) (input_zero : ∀ (input : Fin problem.inputCount), feature (problem.inputs input) = 0) (constant_zero : ∀ (scalar : C), feature (constant scalar) = 0) (targets : Fin m → U) (independent : LinearIndependent K (⇑feature ∘ targets)) (circuit : Circuit (Arithmetic.signature C) problem.inputCount m) (constructs : Multiple.Constructs problem targets circuit) : m ≤ circuit.cost Arithmetic.multiplicationCost

If the selected linear feature takes linearly independent values on m requested outputs, any one circuit constructing them needs at least m multiplications.