Interaction-span Fusion for arithmetic circuits

Many cancellation-tolerant arithmetic lower bounds use a linear feature with the following product rule: the feature of a product is a linear combination of the two old feature values plus one new interaction term. Hessian matrices are the motivating example; their new term is the symmetrized outer product of the two gradients.

This module isolates the circuit-combinatorial part. It proves that the target feature lies in the span of one interaction term for each multiplication gate. Concrete feature maps and rank estimates are supplied in separate modules.

structure Algebraic.Fusion.Arithmetic.Interaction.Certificate {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) : Type (max w x)

Algebraic data whose product rule creates one new interaction term.

• feature : U → Q

  Linearized feature used to obstruct the target.

• interaction : U → U → Q

  New feature contribution created by multiplying two values.

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

  Free inputs have zero feature.

• feature_add (left right : U) : self.feature (left + right) = self.feature left + self.feature right

  Addition is linear at feature level.

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

  Named scalar 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 + self.interaction left right

  A product propagates its input features linearly and creates exactly one additional interaction.

structure Algebraic.Fusion.Arithmetic.Interaction.SpanWitness {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) : Type x

A submodule obstruction for an interaction certificate.

• submodule : Submodule K Q

  Candidate span of the interactions already made available.

• target_not_mem : certificate.feature problem.target ∉ self.submodule

  The target feature is not yet in the candidate span.

def Algebraic.Fusion.Arithmetic.Interaction.model {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) : Model Arithmetic.multiplicationCost (Arithmetic.interpretation constant) problem

Fusion model induced by an interaction certificate.

Equations

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

theorem Algebraic.Fusion.Arithmetic.Interaction.add_preserved {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) (witness : (model certificate).Witness) : { op := Arithmetic.Op.add, arguments := arguments }.PreservedBy (model certificate) witness

Addition preserves every interaction-span witness.

theorem Algebraic.Fusion.Arithmetic.Interaction.constant_preserved {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) (witness : (model certificate).Witness) : { op := Arithmetic.Op.constant scalar, arguments := arguments }.PreservedBy (model certificate) witness

Named constants preserve every interaction-span witness.

theorem Algebraic.Fusion.Arithmetic.Interaction.mul_preserved_of_interaction_mem {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) (witness : (model certificate).Witness) (interactionMem : certificate.interaction (arguments 0) (arguments 1) ∈ witness.submodule) : { op := Arithmetic.Op.mul, arguments := arguments }.PreservedBy (model certificate) witness

A multiplication preserves a witness whenever its new interaction is already in the witness submodule.

def Algebraic.Fusion.Arithmetic.Interaction.Atom.interaction? {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 new interaction created by a multiplication atom and discard addition and constant atoms.

Equations

• Algebraic.Fusion.Arithmetic.Interaction.Atom.interaction? certificate { op := Algebraic.Arithmetic.Op.add, arguments := arguments } = none
• Algebraic.Fusion.Arithmetic.Interaction.Atom.interaction? certificate { op := Algebraic.Arithmetic.Op.mul, arguments := arguments } = some (certificate.interaction (arguments 0) (arguments 1))
• Algebraic.Fusion.Arithmetic.Interaction.Atom.interaction? certificate { op := Algebraic.Arithmetic.Op.constant value, arguments := arguments } = none

def Algebraic.Fusion.Arithmetic.Interaction.interactions {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

Interaction terms extracted from a list of arithmetic atoms.

Equations

• Algebraic.Fusion.Arithmetic.Interaction.interactions certificate atoms = List.filterMap (Algebraic.Fusion.Arithmetic.Interaction.Atom.interaction? certificate) atoms

@[simp]

theorem Algebraic.Fusion.Arithmetic.Interaction.interactions_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)) : interactions certificate ({ op := Arithmetic.Op.add, arguments := arguments } :: atoms) = interactions certificate atoms

@[simp]

theorem Algebraic.Fusion.Arithmetic.Interaction.interactions_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)) : interactions certificate ({ op := Arithmetic.Op.mul, arguments := arguments } :: atoms) = certificate.interaction (arguments 0) (arguments 1) :: interactions certificate atoms

@[simp]

theorem Algebraic.Fusion.Arithmetic.Interaction.interactions_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)) : interactions certificate ({ op := Arithmetic.Op.constant scalar, arguments := arguments } :: atoms) = interactions certificate atoms

theorem Algebraic.Fusion.Arithmetic.Interaction.interactions_eq_map_multiplicationArguments {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)) : interactions certificate atoms = List.map (fun (arguments : Fin 2 → U) => certificate.interaction (arguments 0) (arguments 1)) (multiplicationArguments atoms)

Extracting interactions is the same ordered projection as first extracting multiplication occurrences and then mapping the certificate's interaction function. In particular, this preserves repeated semantic multiplications as distinct occurrences.

theorem Algebraic.Fusion.Arithmetic.Interaction.interactions_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)) : (interactions certificate atoms).length = Atom.listCost atoms Arithmetic.multiplicationCost

The number of extracted interactions is exactly multiplication cost.

noncomputable def Algebraic.Fusion.Arithmetic.Interaction.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 all multiplication interactions in an atom list.

Equations

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

theorem Algebraic.Fusion.Arithmetic.Interaction.interaction_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.mul, arguments := arguments } ∈ atoms) : certificate.interaction (arguments 0) (arguments 1) ∈ generatedSubmodule certificate atoms

The interaction of a multiplication atom in the list belongs to the generated interaction submodule.

theorem Algebraic.Fusion.Arithmetic.Interaction.targetFeature_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) (cover : Cover (model certificate)) : certificate.feature problem.target ∈ generatedSubmodule certificate cover.atoms

Every interaction-span Fusion cover spans the target feature.

theorem Algebraic.Fusion.Arithmetic.Interaction.targetFeature_mem_circuitSubmodule {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) (circuit : Circuit (Arithmetic.signature C) problem.inputCount 1) (constructs : problem.Constructs circuit (Arithmetic.interpretation constant)) : certificate.feature problem.target ∈ generatedSubmodule certificate (circuitAtoms circuit (Arithmetic.interpretation constant) problem.inputs)

A constructing arithmetic circuit spans its target feature using exactly one extracted interaction per multiplication gate.

theorem Algebraic.Fusion.Arithmetic.Interaction.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 belongs to the interaction span of any atom list that contains all atoms of the program. Unlike the cover argument, this invariant does not single out one output and is therefore the bridge to multi-output lower bounds.

theorem Algebraic.Fusion.Arithmetic.Interaction.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 of a circuit lies in the common span of all its multiplication interactions.