Multi-output arithmetic interaction bounds

All outputs of one arithmetic circuit share the same multiplication gates and hence the same interaction span. The dimension of the requested output feature span is therefore at most the number of multiplication gates. In particular, if the feature values of m requested outputs are linearly independent, the circuit needs at least m multiplications.

The target field of the base Problem is intentionally irrelevant here; the problem supplies the common input family used by the interaction certificate. The requested output family is passed separately.

def Algebraic.Fusion.Arithmetic.Interaction.Multiple.Constructs {C : Type v} {U : Type w} [Add U] [Mul U] {m : ℕ} {constant : C → U} (problem : Problem U) (targets : Fin m → U) (circuit : Circuit (Arithmetic.signature C) problem.inputCount m) : Prop

A multi-output circuit constructs a requested family when all designated outputs have the specified semantic values.

Equations

• Algebraic.Fusion.Arithmetic.Interaction.Multiple.Constructs problem targets circuit = (circuit.eval (Algebraic.Arithmetic.interpretation constant) problem.inputs = targets)

theorem Algebraic.Fusion.Arithmetic.Interaction.Multiple.targetFeature_mem_circuitSubmodule {K : Type u} {C : Type v} {U : Type w} {Q : Type x} [Field K] [Add U] [Mul U] [AddCommGroup 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 : 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 interaction span of a constructing circuit.

theorem Algebraic.Fusion.Arithmetic.Interaction.Multiple.featureSpan_finrank_le_multiplicationCost {K : Type u} {C : Type v} {U : Type w} {Q : Type x} [Field K] [Add U] [Mul U] [AddCommGroup 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 : Constructs problem targets circuit) : Module.finrank K ↥(Submodule.span K (Set.range (certificate.feature ∘ targets))) ≤ circuit.cost Arithmetic.multiplicationCost

The dimension of the requested output-feature span is at most the number of multiplication gates. This rank form permits dependent and redundant output families.

theorem Algebraic.Fusion.Arithmetic.Interaction.Multiple.circuit_multiplication_lowerBound_of_linearIndependent {K : Type u} {C : Type v} {U : Type w} {Q : Type x} [Field K] [Add U] [Mul U] [AddCommGroup 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 : Constructs problem targets circuit) : m ≤ circuit.cost Arithmetic.multiplicationCost

Linearly independent output features force one multiplication interaction per output.