Fusion for sum-of-terms circuits

For a module-valued sum-of-terms circuit, a fusion witness is a submodule that contains every free input but excludes the target. Addition preserves such a witness. A term gate preserves it exactly when the corresponding dictionary value lies in the submodule.

It follows that the target belongs to the span of the input values and the terms occurring in every fusion cover. This is the algebraic bridge used by rank, flattening, and partial-derivative lower bounds.

structure Algebraic.Fusion.SumOfTerms.SpanWitness {K : Type u} {V : Type v} [Semiring K] [AddCommMonoid V] [Module K V] (problem : Problem V) : Type v

A linear obstruction containing the free inputs but not the target.

• submodule : Submodule K V

  Candidate subspace generated by the available local terms.

• inputs_mem (input : Fin problem.inputCount) : problem.inputs input ∈ self.submodule

  Every free circuit input already belongs to the subspace.

• target_not_mem : problem.target ∉ self.submodule

  The desired target does not belong to the subspace.

def Algebraic.Fusion.SumOfTerms.spanModel {K : Type u} {V : Type v} {T : Type w} [Semiring K] [AddCommMonoid V] [Module K V] (termValue : T → V) (problem : Problem V) : Model SumOfTerms.termCost (SumOfTerms.interpretation termValue) problem

Fusion model of linear-span obstructions.

Equations

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

theorem Algebraic.Fusion.SumOfTerms.add_preserved {K : Type u} {V : Type v} {T : Type w} [Semiring K] [AddCommMonoid V] [Module K V] (termValue : T → V) (problem : Problem V) (arguments : Fin 2 → V) (witness : (spanModel termValue problem).Witness) : { op := SumOfTerms.Op.add, arguments := arguments }.PreservedBy (spanModel termValue problem) witness

Addition preserves every linear-span witness.

theorem Algebraic.Fusion.SumOfTerms.term_preserved_iff {K : Type u} {V : Type v} {T : Type w} [Semiring K] [AddCommMonoid V] [Module K V] (termValue : T → V) (problem : Problem V) (term : T) (arguments : Fin (SumOfTerms.arity (SumOfTerms.Op.term term)) → V) (witness : (spanModel termValue problem).Witness) : { op := SumOfTerms.Op.term term, arguments := arguments }.PreservedBy (spanModel termValue problem) witness ↔ termValue term ∈ witness.submodule

A term gate preserves a witness exactly when its value lies in the witness submodule.

def Algebraic.Fusion.SumOfTerms.Atom.term? {V : Type v} {T : Type w} (atom : Atom (SumOfTerms.signature T) V) : Option T

Retain the dictionary parameter of term atoms and discard additions.

Equations

• Algebraic.Fusion.SumOfTerms.Atom.term? { op := Algebraic.SumOfTerms.Op.add, arguments := arguments } = none
• Algebraic.Fusion.SumOfTerms.Atom.term? { op := Algebraic.SumOfTerms.Op.term term, arguments := arguments } = some term

def Algebraic.Fusion.SumOfTerms.terms {V : Type v} {T : Type w} (atoms : List (Atom (SumOfTerms.signature T) V)) : List T

Dictionary terms occurring in a list of fusion atoms.

Equations

• Algebraic.Fusion.SumOfTerms.terms atoms = List.filterMap Algebraic.Fusion.SumOfTerms.Atom.term? atoms

@[simp]

theorem Algebraic.Fusion.SumOfTerms.terms_cons_add {V : Type v} {T : Type w} (arguments : Fin 2 → V) (atoms : List (Atom (SumOfTerms.signature T) V)) : terms ({ op := SumOfTerms.Op.add, arguments := arguments } :: atoms) = terms atoms

@[simp]

theorem Algebraic.Fusion.SumOfTerms.terms_cons_term {V : Type v} {T : Type w} (term : T) (arguments : Fin (SumOfTerms.arity (SumOfTerms.Op.term term)) → V) (atoms : List (Atom (SumOfTerms.signature T) V)) : terms ({ op := SumOfTerms.Op.term term, arguments := arguments } :: atoms) = term :: terms atoms

theorem Algebraic.Fusion.SumOfTerms.terms_length {V : Type v} {T : Type w} (atoms : List (Atom (SumOfTerms.signature T) V)) : (terms atoms).length = Atom.listCost atoms SumOfTerms.termCost

The number of retained terms is exactly the charged atom cost.

theorem Algebraic.Fusion.SumOfTerms.terms_weight_sum {V : Type v} {T : Type w} (atoms : List (Atom (SumOfTerms.signature T) V)) (weight : T → ℕ) : (List.map weight (terms atoms)).sum = Atom.listCost atoms (SumOfTerms.dictionaryCost weight)

The sum of term-dependent dictionary weights is exactly the corresponding weighted atom cost.

noncomputable def Algebraic.Fusion.SumOfTerms.generatedSubmodule {K : Type u} {V : Type v} {T : Type w} [Semiring K] [AddCommMonoid V] [Module K V] (termValue : T → V) (problem : Problem V) (atoms : List (Atom (SumOfTerms.signature T) V)) : Submodule K V

The submodule generated by free inputs and all terms in an atom list.

Equations

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

theorem Algebraic.Fusion.SumOfTerms.input_mem_generatedSubmodule {K : Type u} {V : Type v} {T : Type w} [Semiring K] [AddCommMonoid V] [Module K V] (termValue : T → V) (problem : Problem V) (atoms : List (Atom (SumOfTerms.signature T) V)) (input : Fin problem.inputCount) : problem.inputs input ∈ generatedSubmodule termValue problem atoms

Every free input belongs to the generated submodule.

theorem Algebraic.Fusion.SumOfTerms.termValue_mem_generatedSubmodule {K : Type u} {V : Type v} {T : Type w} [Semiring K] [AddCommMonoid V] [Module K V] (termValue : T → V) (problem : Problem V) (atoms : List (Atom (SumOfTerms.signature T) V)) (term : T) (arguments : Fin (SumOfTerms.arity (SumOfTerms.Op.term term)) → V) (present : { op := SumOfTerms.Op.term term, arguments := arguments } ∈ atoms) : termValue term ∈ generatedSubmodule termValue problem atoms

A term atom occurring in the list contributes its value to the generated submodule.

theorem Algebraic.Fusion.SumOfTerms.target_mem_generatedSubmodule {K : Type u} {V : Type v} {T : Type w} [Semiring K] [AddCommMonoid V] [Module K V] (termValue : T → V) (problem : Problem V) (cover : Cover (spanModel termValue problem)) : problem.target ∈ generatedSubmodule termValue problem cover.atoms

Every fusion cover spans the target using its term atoms and free inputs.