Finite-support fusion for arbitrary-depth monotone arithmetic circuits

This module interprets arithmetic circuits directly on finite monomial supports. Addition is union and multiplication is pairwise monomial product, so multiplication gates may be nested to arbitrary depth.

Witnesses are target monomials absent from the generators and named constants. Addition preserves absence. A multiplication can fail only on target monomials appearing in its product support, which is bounded by the product of the two input-support cardinalities.

The final theorem is deliberately circuit-local: if every multiplication gate actually occurring in a constructing circuit has input supports of size at most width, then the circuit needs at least ceil(target.card / (width * width)) multiplications. This is a restricted monotone-support result, not a lower bound for unrestricted arithmetic circuits with cancellation.

@[reducible, inline]

abbrev Algebraic.Fusion.Arithmetic.Support.problem {n : ℕ} {M : Type u_1} (inputs : Fin n → FiniteSupport M) (target : Finset M) : Problem (FiniteSupport M)

Construct a target support from the supplied input supports.

Equations

• Algebraic.Fusion.Arithmetic.Support.problem inputs target = { inputCount := n, inputs := inputs, target := { monomials := target } }

@[reducible, inline]

abbrev Algebraic.Fusion.Arithmetic.Support.model {M : Type u_1} {K : Type u_2} {n : ℕ} [DecidableEq M] [Mul M] (constantSupport : K → FiniteSupport M) (inputs : Fin n → FiniteSupport M) (target : Finset M) (inputAvoid : ∀ (witness : ↥target) (input : Fin n), ↑witness ∉ (inputs input).monomials) : Model Arithmetic.multiplicationCost (Arithmetic.interpretation constantSupport) (problem inputs target)

Fusion model recording which target monomials remain absent.

Equations

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

@[instance_reducible]

noncomputable instance Algebraic.Fusion.Arithmetic.Support.witnessFintype {M : Type u_1} {K : Type u_2} {n : ℕ} [DecidableEq M] [Mul M] (constantSupport : K → FiniteSupport M) (inputs : Fin n → FiniteSupport M) (target : Finset M) (inputAvoid : ∀ (witness : ↥target) (input : Fin n), ↑witness ∉ (inputs input).monomials) : Fintype (model constantSupport inputs target inputAvoid).Witness

Equations

• Algebraic.Fusion.Arithmetic.Support.witnessFintype constantSupport inputs target inputAvoid = id inferInstance

theorem Algebraic.Fusion.Arithmetic.Support.witness_card {M : Type u_1} {K : Type u_2} {n : ℕ} [DecidableEq M] [Mul M] (constantSupport : K → FiniteSupport M) (inputs : Fin n → FiniteSupport M) (target : Finset M) (inputAvoid : ∀ (witness : ↥target) (input : Fin n), ↑witness ∉ (inputs input).monomials) : Fintype.card (model constantSupport inputs target inputAvoid).Witness = target.card

theorem Algebraic.Fusion.Arithmetic.Support.add_preserved {M : Type u_1} {K : Type u_2} {n : ℕ} [DecidableEq M] [Mul M] (constantSupport : K → FiniteSupport M) (inputs : Fin n → FiniteSupport M) (target : Finset M) (inputAvoid : ∀ (witness : ↥target) (input : Fin n), ↑witness ∉ (inputs input).monomials) (arguments : Fin 2 → FiniteSupport M) (witness : (model constantSupport inputs target inputAvoid).Witness) : { op := Arithmetic.Op.add, arguments := arguments }.PreservedBy (model constantSupport inputs target inputAvoid) witness

Union preserves absence of every target monomial.

theorem Algebraic.Fusion.Arithmetic.Support.constant_preserved {M : Type u_1} {K : Type u_2} {n : ℕ} [DecidableEq M] [Mul M] (constantSupport : K → FiniteSupport M) (inputs : Fin n → FiniteSupport M) (target : Finset M) (inputAvoid : ∀ (witness : ↥target) (input : Fin n), ↑witness ∉ (inputs input).monomials) (constantAvoid : ∀ (witness : ↥target) (scalar : K), ↑witness ∉ (constantSupport scalar).monomials) (scalar : K) (arguments : Fin (Arithmetic.arity (Arithmetic.Op.constant scalar)) → FiniteSupport M) (witness : (model constantSupport inputs target inputAvoid).Witness) : { op := Arithmetic.Op.constant scalar, arguments := arguments }.PreservedBy (model constantSupport inputs target inputAvoid) witness

Named constants preserve absence when their supports avoid the target.

theorem Algebraic.Fusion.Arithmetic.Support.mem_mul_of_not_preserved {M : Type u_1} {K : Type u_2} {n : ℕ} [DecidableEq M] [Mul M] (constantSupport : K → FiniteSupport M) (inputs : Fin n → FiniteSupport M) (target : Finset M) (inputAvoid : ∀ (witness : ↥target) (input : Fin n), ↑witness ∉ (inputs input).monomials) (arguments : Fin 2 → FiniteSupport M) (witness : (model constantSupport inputs target inputAvoid).Witness) (failure : ¬{ op := Arithmetic.Op.mul, arguments := arguments }.PreservedBy (model constantSupport inputs target inputAvoid) witness) : ↑witness ∈ (arguments 0 * arguments 1).monomials

Failure of a multiplication implies that its result support contains the failed target monomial.

theorem Algebraic.Fusion.Arithmetic.Support.mul_failure_card_le_productSupport {M : Type u_1} {K : Type u_2} {n : ℕ} [DecidableEq M] [Mul M] (constantSupport : K → FiniteSupport M) (inputs : Fin n → FiniteSupport M) (target : Finset M) (inputAvoid : ∀ (witness : ↥target) (input : Fin n), ↑witness ∉ (inputs input).monomials) (arguments : Fin 2 → FiniteSupport M) : ({ op := Arithmetic.Op.mul, arguments := arguments }.failures (model constantSupport inputs target inputAvoid)).card ≤ (arguments 0 * arguments 1).monomials.card

A multiplication fails on no more witnesses than the cardinality of its pairwise product support.

theorem Algebraic.Fusion.Arithmetic.Support.mul_failure_card_le {M : Type u_1} {K : Type u_2} {n : ℕ} [DecidableEq M] [Mul M] (constantSupport : K → FiniteSupport M) (inputs : Fin n → FiniteSupport M) (target : Finset M) (inputAvoid : ∀ (witness : ↥target) (input : Fin n), ↑witness ∉ (inputs input).monomials) (arguments : Fin 2 → FiniteSupport M) : ({ op := Arithmetic.Op.mul, arguments := arguments }.failures (model constantSupport inputs target inputAvoid)).card ≤ (arguments 0).monomials.card * (arguments 1).monomials.card

The elementary product-width bound on failed target witnesses.

def Algebraic.Fusion.Arithmetic.Support.MultiplicationWidthAtMost {K : Type u_1} {M : Type u_2} (atoms : List (Atom (Arithmetic.signature K) (FiniteSupport M))) (width : ℕ) : Prop

Every multiplication atom in a list receives supports of cardinality at most width.

Equations

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

theorem Algebraic.Fusion.Arithmetic.Support.local_failure_card_le {M : Type u_1} {K : Type u_2} {n : ℕ} [DecidableEq M] [Mul M] (constantSupport : K → FiniteSupport M) (inputs : Fin n → FiniteSupport M) (target : Finset M) (inputAvoid : ∀ (witness : ↥target) (input : Fin n), ↑witness ∉ (inputs input).monomials) (constantAvoid : ∀ (witness : ↥target) (scalar : K), ↑witness ∉ (constantSupport scalar).monomials) (atoms : List (Atom (Arithmetic.signature K) (FiniteSupport M))) (width : ℕ) (widthBound : MultiplicationWidthAtMost atoms width) (atom : Atom (Arithmetic.signature K) (FiniteSupport M)) : atom ∈ atoms → (atom.failures (model constantSupport inputs target inputAvoid)).card ≤ width * width * atom.cost Arithmetic.multiplicationCost

A support-width promise gives the required local failure estimate on the atoms that actually occur.

theorem Algebraic.Fusion.Arithmetic.Support.circuit_multiplication_lowerBound {M : Type u_1} {K : Type u_2} {n : ℕ} [DecidableEq M] [Mul M] (constantSupport : K → FiniteSupport M) (inputs : Fin n → FiniteSupport M) (target : Finset M) (inputAvoid : ∀ (witness : ↥target) (input : Fin n), ↑witness ∉ (inputs input).monomials) (constantAvoid : ∀ (witness : ↥target) (scalar : K), ↑witness ∉ (constantSupport scalar).monomials) (width : ℕ) (positive : 0 < width) (circuit : Circuit (Arithmetic.signature K) n 1) (constructs : (problem inputs target).Constructs circuit (Arithmetic.interpretation constantSupport)) (widthBound : MultiplicationWidthAtMost (circuitAtoms circuit (Arithmetic.interpretation constantSupport) inputs) width) : target.card ⌈/⌉ (width * width) ≤ circuit.cost Arithmetic.multiplicationCost

Arbitrary-depth monotone support circuits of multiplication-input width width need at least ceil(target.card / width^2) multiplication gates.

theorem Algebraic.Fusion.Arithmetic.Support.circuit_multiplication_lowerBound_of_singletonWidth {M : Type u_1} {K : Type u_2} {n : ℕ} [DecidableEq M] [Mul M] (constantSupport : K → FiniteSupport M) (inputs : Fin n → FiniteSupport M) (target : Finset M) (inputAvoid : ∀ (witness : ↥target) (input : Fin n), ↑witness ∉ (inputs input).monomials) (constantAvoid : ∀ (witness : ↥target) (scalar : K), ↑witness ∉ (constantSupport scalar).monomials) (circuit : Circuit (Arithmetic.signature K) n 1) (constructs : (problem inputs target).Constructs circuit (Arithmetic.interpretation constantSupport)) (widthBound : MultiplicationWidthAtMost (circuitAtoms circuit (Arithmetic.interpretation constantSupport) inputs) 1) : target.card ≤ circuit.cost Arithmetic.multiplicationCost

In the singleton-width case, every target monomial costs a distinct multiplication gate.