Bounded-failure arithmetic fusion

For multiplicative-complexity lower bounds, additions and constants are free. Consequently an arithmetic fusion model only needs three local facts:

• addition preserves every witness;
• each named constant preserves every witness;
• a multiplication fails on at most a bounded number of witnesses.

FailureRules packages exactly this interface and compiles it to the generic finite-witness counting framework. Concrete applications can use degree thresholds, derivative directions, rank increments, monomial cuts, or other observations without rebuilding the cover-counting proof.

structure Algebraic.Fusion.Arithmetic.FailureRules {K : Type u} {R : Type v} [Add R] [Mul R] {constant : K → R} {problem : Problem R} (model : Model Arithmetic.multiplicationCost (Arithmetic.interpretation constant) problem) [Fintype model.Witness] : Type

Local arithmetic rules sufficient for a bounded-failure fusion argument.

• capacity : ℕ

  Maximum number of witnesses destroyed by one multiplication.

• add_preserved (arguments : Fin 2 → R) (witness : model.Witness) : { op := Arithmetic.Op.add, arguments := arguments }.PreservedBy model witness

  Free additions must preserve every witness.

• constant_preserved (scalar : K) (arguments : Fin (Arithmetic.arity (Arithmetic.Op.constant scalar)) → R) (witness : model.Witness) : { op := Arithmetic.Op.constant scalar, arguments := arguments }.PreservedBy model witness

  Free constants must preserve every witness.

• mul_failure_card_le (arguments : Fin 2 → R) : ({ op := Arithmetic.Op.mul, arguments := arguments }.failures model).card ≤ self.capacity

  The local combinatorial estimate charged to one multiplication.

noncomputable def Algebraic.Fusion.Arithmetic.FailureRules.failureBound {K : Type u} {R : Type v} [Add R] [Mul R] {constant : K → R} {problem : Problem R} {model : Model Arithmetic.multiplicationCost (Arithmetic.interpretation constant) problem} [Fintype model.Witness] (rules : FailureRules model) : FailureBound model

Arithmetic local rules compile to a generic weighted failure bound.

Equations

• rules.failureBound = { capacity := rules.capacity, failure_card_le := ⋯ }

theorem Algebraic.Fusion.Arithmetic.FailureRules.cover_lowerBound {K : Type u} {R : Type v} [Add R] [Mul R] {constant : K → R} {problem : Problem R} {model : Model Arithmetic.multiplicationCost (Arithmetic.interpretation constant) problem} [Fintype model.Witness] (rules : FailureRules model) (positive : 0 < rules.capacity) (cover : Cover model) : Fintype.card model.Witness ⌈/⌉ rules.capacity ≤ cover.cost

A positive arithmetic failure capacity lower-bounds every fusion cover.

theorem Algebraic.Fusion.Arithmetic.FailureRules.circuit_lowerBound {K : Type u} {R : Type v} [Add R] [Mul R] {constant : K → R} {problem : Problem R} {model : Model Arithmetic.multiplicationCost (Arithmetic.interpretation constant) problem} [Fintype model.Witness] (rules : FailureRules model) (positive : 0 < rules.capacity) (circuit : Circuit (Arithmetic.signature K) problem.inputCount 1) (constructs : problem.Constructs circuit (Arithmetic.interpretation constant)) : Fintype.card model.Witness ⌈/⌉ rules.capacity ≤ circuit.cost Arithmetic.multiplicationCost

The bounded-failure arithmetic argument transferred to a circuit.