Support fusion for monotone multivariate-polynomial circuits

Natural-coefficient multivariate polynomials have exact support semantics: support turns addition into union and multiplication into pairwise addition of exponent vectors. This file packages that map as an Algebraic.Homomorphism from genuine arithmetic circuits over MvPolynomial σ ℕ to the finite-support interpretation.

The resulting lower bound applies to arbitrary-depth monotone arithmetic circuits whose multiplication gates have bounded input-support width. The width promise is evaluated in the support interpretation, equivalently on the supports of the polynomials at the corresponding source-circuit wires.

structure Algebraic.Fusion.Arithmetic.MonotonePolynomial.Monomial (σ : Type u) : Type u

A polynomial monomial represented by its exponent vector, with multiplication given by addition of exponents.

• exponent : σ →₀ ℕ

  Exponent vector of the monomial.

def Algebraic.Fusion.Arithmetic.MonotonePolynomial.instDecidableEqMonomial.decEq {σ✝ : Type u_1} [DecidableEq σ✝] (x✝ x✝¹ : Monomial σ✝) : Decidable (x✝ = x✝¹)

Equations

• Algebraic.Fusion.Arithmetic.MonotonePolynomial.instDecidableEqMonomial.decEq { exponent := a } { exponent := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Algebraic.Fusion.Arithmetic.MonotonePolynomial.instDecidableEqMonomial {σ✝ : Type u_1} [DecidableEq σ✝] : DecidableEq (Monomial σ✝)

Equations

• Algebraic.Fusion.Arithmetic.MonotonePolynomial.instDecidableEqMonomial = Algebraic.Fusion.Arithmetic.MonotonePolynomial.instDecidableEqMonomial.decEq

theorem Algebraic.Fusion.Arithmetic.MonotonePolynomial.Monomial.ext {σ : Type u_1} {left right : Monomial σ} (equal : left.exponent = right.exponent) : left = right

theorem Algebraic.Fusion.Arithmetic.MonotonePolynomial.Monomial.ext_iff {σ : Type u_1} {left right : Monomial σ} : left = right ↔ left.exponent = right.exponent

@[instance_reducible]

noncomputable instance Algebraic.Fusion.Arithmetic.MonotonePolynomial.instMulMonomial {σ : Type u_1} : Mul (Monomial σ)

Equations

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

@[simp]

theorem Algebraic.Fusion.Arithmetic.MonotonePolynomial.exponent_mul {σ : Type u_1} (left right : Monomial σ) : (left * right).exponent = left.exponent + right.exponent

def Algebraic.Fusion.Arithmetic.MonotonePolynomial.monomialEmbedding (σ : Type u) : (σ →₀ ℕ) ↪ Monomial σ

Inject exponent vectors into the multiplicative monomial wrapper.

Equations

• Algebraic.Fusion.Arithmetic.MonotonePolynomial.monomialEmbedding σ = { toFun := fun (exponent : σ →₀ ℕ) => { exponent := exponent }, inj' := ⋯ }

def Algebraic.Fusion.Arithmetic.MonotonePolynomial.supportFinset {σ : Type u_1} (polynomial : MvPolynomial σ ℕ) : Finset (Monomial σ)

The support of a natural-coefficient polynomial, expressed in the multiplicative monomial wrapper.

Equations

• Algebraic.Fusion.Arithmetic.MonotonePolynomial.supportFinset polynomial = Finset.map (Algebraic.Fusion.Arithmetic.MonotonePolynomial.monomialEmbedding σ) polynomial.support

def Algebraic.Fusion.Arithmetic.MonotonePolynomial.supportValue {σ : Type u_1} (polynomial : MvPolynomial σ ℕ) : FiniteSupport (Monomial σ)

A polynomial support as the reusable finite-support semantic carrier.

Equations

• Algebraic.Fusion.Arithmetic.MonotonePolynomial.supportValue polynomial = { monomials := Algebraic.Fusion.Arithmetic.MonotonePolynomial.supportFinset polynomial }

@[simp]

theorem Algebraic.Fusion.Arithmetic.MonotonePolynomial.supportValue_monomials {σ : Type u_1} (polynomial : MvPolynomial σ ℕ) : (supportValue polynomial).monomials = supportFinset polynomial

@[simp]

theorem Algebraic.Fusion.Arithmetic.MonotonePolynomial.card_supportFinset {σ : Type u_1} (polynomial : MvPolynomial σ ℕ) : (supportFinset polynomial).card = polynomial.support.card

@[simp]

theorem Algebraic.Fusion.Arithmetic.MonotonePolynomial.monomial_mem_supportFinset {σ : Type u_1} (exponent : σ →₀ ℕ) (polynomial : MvPolynomial σ ℕ) : { exponent := exponent } ∈ supportFinset polynomial ↔ exponent ∈ polynomial.support

theorem Algebraic.Fusion.Arithmetic.MonotonePolynomial.polynomial_support_add {σ : Type u_1} [DecidableEq σ] (left right : MvPolynomial σ ℕ) : (left + right).support = left.support ∪ right.support

Natural coefficients cannot cancel under addition, so support of a sum is exactly the union of supports.

theorem Algebraic.Fusion.Arithmetic.MonotonePolynomial.polynomial_support_mul {σ : Type u_1} [DecidableEq σ] (left right : MvPolynomial σ ℕ) : (left * right).support = left.support + right.support

Natural coefficients cannot cancel and have no zero divisors, so every pairwise sum of supported exponent vectors survives in the product.

@[simp]

theorem Algebraic.Fusion.Arithmetic.MonotonePolynomial.supportValue_add {σ : Type u_1} [DecidableEq σ] (left right : MvPolynomial σ ℕ) : supportValue (left + right) = supportValue left + supportValue right

@[simp]

theorem Algebraic.Fusion.Arithmetic.MonotonePolynomial.supportValue_mul {σ : Type u_1} [DecidableEq σ] (left right : MvPolynomial σ ℕ) : supportValue (left * right) = supportValue left * supportValue right

noncomputable def Algebraic.Fusion.Arithmetic.MonotonePolynomial.constantSupport {σ : Type u_1} (scalar : ℕ) : FiniteSupport (Monomial σ)

Support of the scalar constants used by the target support interpretation.

Equations

• Algebraic.Fusion.Arithmetic.MonotonePolynomial.constantSupport scalar = Algebraic.Fusion.Arithmetic.MonotonePolynomial.supportValue (MvPolynomial.C scalar)

theorem Algebraic.Fusion.Arithmetic.MonotonePolynomial.constantSupport_subset_zero {σ : Type u_1} (scalar : ℕ) : (constantSupport scalar).monomials ⊆ {{ exponent := 0 }}

Constant supports contain only the zero exponent vector.

theorem Algebraic.Fusion.Arithmetic.MonotonePolynomial.constantAvoid_of_zero_not_mem {σ : Type u_1} (target : MvPolynomial σ ℕ) (zero_not_mem : 0 ∉ target.support) (witness : ↥(supportFinset target)) (scalar : ℕ) : ↑witness ∉ (constantSupport scalar).monomials

If the target has no constant monomial, every named natural constant is sound for the support-fusion model.

theorem Algebraic.Fusion.Arithmetic.MonotonePolynomial.inputAvoid_of_disjoint {n : ℕ} {σ : Type u_1} (inputs : Fin n → MvPolynomial σ ℕ) (target : MvPolynomial σ ℕ) (disjoint : ∀ (input : Fin n), Disjoint target.support (inputs input).support) (witness : ↥(supportFinset target)) (input : Fin n) : ↑witness ∉ (supportValue (inputs input)).monomials

Disjoint source supports imply the witness-wise input-avoidance premise.

def Algebraic.Fusion.Arithmetic.MonotonePolynomial.supportHomomorphism (σ : Type u) [DecidableEq σ] : Homomorphism (Arithmetic.interpretation ⇑MvPolynomial.C) (Arithmetic.interpretation constantSupport)

Exact polynomial support is a homomorphism of arithmetic interpretations.

Equations

• Algebraic.Fusion.Arithmetic.MonotonePolynomial.supportHomomorphism σ = { map := Algebraic.Fusion.Arithmetic.MonotonePolynomial.supportValue, homomorphic := ⋯ }

@[reducible, inline]

abbrev Algebraic.Fusion.Arithmetic.MonotonePolynomial.MultiplicationSupportWidthAtMost {σ : Type u_1} {n : ℕ} [DecidableEq σ] (circuit : Circuit (Arithmetic.signature ℕ) n 1) (inputs : Fin n → MvPolynomial σ ℕ) (width : ℕ) : Prop

The multiplication-input support-width promise for a genuine polynomial circuit. Its definition evaluates the same syntax in the exact support interpretation furnished by supportHomomorphism.

Equations

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

theorem Algebraic.Fusion.Arithmetic.MonotonePolynomial.constructs_support {σ : Type u_1} {n : ℕ} [DecidableEq σ] (inputs : Fin n → MvPolynomial σ ℕ) (target : MvPolynomial σ ℕ) (circuit : Circuit (Arithmetic.signature ℕ) n 1) (constructs : { inputCount := n, inputs := inputs, target := target }.Constructs circuit (Arithmetic.interpretation ⇑MvPolynomial.C)) : (Support.problem (supportValue ∘ inputs) (supportFinset target)).Constructs circuit (Arithmetic.interpretation constantSupport)

A polynomial construction maps to the corresponding exact support construction.

theorem Algebraic.Fusion.Arithmetic.MonotonePolynomial.circuit_multiplication_lowerBound {σ : Type u_1} {n : ℕ} [DecidableEq σ] (inputs : Fin n → MvPolynomial σ ℕ) (target : MvPolynomial σ ℕ) (inputAvoid : ∀ (witness : ↥(supportFinset target)) (input : Fin n), ↑witness ∉ (supportValue (inputs input)).monomials) (constantAvoid : ∀ (witness : ↥(supportFinset target)) (scalar : ℕ), ↑witness ∉ (constantSupport scalar).monomials) (width : ℕ) (positive : 0 < width) (circuit : Circuit (Arithmetic.signature ℕ) n 1) (constructs : { inputCount := n, inputs := inputs, target := target }.Constructs circuit (Arithmetic.interpretation ⇑MvPolynomial.C)) (widthBound : MultiplicationSupportWidthAtMost circuit inputs width) : target.support.card ⌈/⌉ (width * width) ≤ circuit.cost Arithmetic.multiplicationCost

Transfer the arbitrary-depth support-width fusion bound to a genuine monotone arithmetic circuit over MvPolynomial σ ℕ.

theorem Algebraic.Fusion.Arithmetic.MonotonePolynomial.circuit_multiplication_lowerBound_of_singletonWidth {σ : Type u_1} {n : ℕ} [DecidableEq σ] (inputs : Fin n → MvPolynomial σ ℕ) (target : MvPolynomial σ ℕ) (inputAvoid : ∀ (witness : ↥(supportFinset target)) (input : Fin n), ↑witness ∉ (supportValue (inputs input)).monomials) (constantAvoid : ∀ (witness : ↥(supportFinset target)) (scalar : ℕ), ↑witness ∉ (constantSupport scalar).monomials) (circuit : Circuit (Arithmetic.signature ℕ) n 1) (constructs : { inputCount := n, inputs := inputs, target := target }.Constructs circuit (Arithmetic.interpretation ⇑MvPolynomial.C)) (widthBound : MultiplicationSupportWidthAtMost circuit inputs 1) : target.support.card ≤ circuit.cost Arithmetic.multiplicationCost

Singleton support at every multiplication input forces one multiplication per target monomial.

theorem Algebraic.Fusion.Arithmetic.MonotonePolynomial.circuit_multiplication_lowerBound_of_disjoint {σ : Type u_1} {n : ℕ} [DecidableEq σ] (inputs : Fin n → MvPolynomial σ ℕ) (target : MvPolynomial σ ℕ) (inputDisjoint : ∀ (input : Fin n), Disjoint target.support (inputs input).support) (target_nonconstant : 0 ∉ target.support) (width : ℕ) (positive : 0 < width) (circuit : Circuit (Arithmetic.signature ℕ) n 1) (constructs : { inputCount := n, inputs := inputs, target := target }.Constructs circuit (Arithmetic.interpretation ⇑MvPolynomial.C)) (widthBound : MultiplicationSupportWidthAtMost circuit inputs width) : target.support.card ⌈/⌉ (width * width) ≤ circuit.cost Arithmetic.multiplicationCost

User-facing form with ordinary support-disjointness and nonconstant-target hypotheses.