Support-width multiplication bounds over exact-support semirings

This module generalizes the natural-coefficient polynomial bridge for finite- support Fusion. Over any nontrivial zero-sum-free commutative semiring without zero divisors, polynomial support maps addition to union and multiplication to pairwise exponent addition. The map is therefore a homomorphism into the existing finite-support arithmetic interpretation.

Consequently the arbitrary-depth multiplication lower bound applies to polynomial circuits over any exact-support coefficient semiring and any named constant alphabet. The only circuit-local promise remains the actual support width at multiplication inputs.

def Algebraic.Fusion.Arithmetic.MonotonePolynomial.Exact.supportFinset {R : Type u_1} [CommSemiring R] {σ : Type u_2} (polynomial : MvPolynomial σ R) : Finset (Monomial σ)

Exponent support embedded into the multiplicative monomial carrier.

Equations

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

def Algebraic.Fusion.Arithmetic.MonotonePolynomial.Exact.supportValue {R : Type u_1} [CommSemiring R] {σ : Type u_2} (polynomial : MvPolynomial σ R) : FiniteSupport (Monomial σ)

Polynomial support as the reusable finite-support semantic value.

Equations

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

@[simp]

theorem Algebraic.Fusion.Arithmetic.MonotonePolynomial.Exact.supportValue_monomials {R : Type u_2} [CommSemiring R] {σ : Type u_1} (polynomial : MvPolynomial σ R) : (supportValue polynomial).monomials = supportFinset polynomial

@[simp]

theorem Algebraic.Fusion.Arithmetic.MonotonePolynomial.Exact.card_supportFinset {R : Type u_2} [CommSemiring R] {σ : Type u_1} (polynomial : MvPolynomial σ R) : (supportFinset polynomial).card = polynomial.support.card

@[simp]

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

@[simp]

theorem Algebraic.Fusion.Arithmetic.MonotonePolynomial.Exact.supportValue_add {R : Type u_2} [CommSemiring R] [ExactSupport.ZeroSumFree R] {σ : Type u_1} [DecidableEq σ] (left right : MvPolynomial σ R) : supportValue (left + right) = supportValue left + supportValue right

Exact support respects polynomial addition.

@[simp]

theorem Algebraic.Fusion.Arithmetic.MonotonePolynomial.Exact.supportValue_mul {R : Type u_2} [CommSemiring R] [NoZeroDivisors R] [ExactSupport.ZeroSumFree R] {σ : Type u_1} [DecidableEq σ] (left right : MvPolynomial σ R) : supportValue (left * right) = supportValue left * supportValue right

Exact support respects polynomial multiplication.

noncomputable def Algebraic.Fusion.Arithmetic.MonotonePolynomial.Exact.constantSupport {R : Type u_1} [CommSemiring R] {σ : Type u_2} (scalar : R) : FiniteSupport (Monomial σ)

Support of a scalar constant.

Equations

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

theorem Algebraic.Fusion.Arithmetic.MonotonePolynomial.Exact.constantSupport_subset_zero {R : Type u_2} [CommSemiring R] {σ : Type u_1} (scalar : R) : (constantSupport scalar).monomials ⊆ {{ exponent := 0 }}

Every scalar constant support is contained in the zero exponent.

def Algebraic.Fusion.Arithmetic.MonotonePolynomial.Exact.supportHomomorphism {R : Type u_1} [CommSemiring R] [NoZeroDivisors R] [ExactSupport.ZeroSumFree R] {K : Type u_2} (σ : Type u) [DecidableEq σ] (constant : K → R) : Homomorphism (Arithmetic.interpretation fun (scalar : K) => MvPolynomial.C (constant scalar)) (Arithmetic.interpretation fun (scalar : K) => constantSupport (constant scalar))

Exact support is a homomorphism of the two arithmetic interpretations.

Equations

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

theorem Algebraic.Fusion.Arithmetic.MonotonePolynomial.Exact.constantAvoid_of_zero_not_mem {R : Type u_3} [CommSemiring R] {K : Sort u_1} {σ : Type u_2} (constant : K → R) (target : MvPolynomial σ R) (zero_not_mem : 0 ∉ target.support) (witness : ↥(supportFinset target)) (scalar : K) : ↑witness ∉ (constantSupport (constant scalar)).monomials

If the target has no constant monomial, every scalar constant avoids all target witnesses.

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

Disjoint input and target supports imply witness-wise input avoidance.

@[reducible, inline]

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

Multiplication-input support-width promise for a polynomial circuit.

Equations

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

theorem Algebraic.Fusion.Arithmetic.MonotonePolynomial.Exact.constructs_support {R : Type u_3} [CommSemiring R] [NoZeroDivisors R] [ExactSupport.ZeroSumFree R] {σ : Type u_1} {K : Type u_2} {n : ℕ} [DecidableEq σ] (constant : K → R) (inputs : Fin n → MvPolynomial σ R) (target : MvPolynomial σ R) (circuit : Circuit (Arithmetic.signature K) n 1) (constructs : { inputCount := n, inputs := inputs, target := target }.Constructs circuit (Arithmetic.interpretation fun (scalar : K) => MvPolynomial.C (constant scalar))) : (Support.problem (supportValue ∘ inputs) (supportFinset target)).Constructs circuit (Arithmetic.interpretation fun (scalar : K) => constantSupport (constant scalar))

Polynomial construction maps to exact support construction.

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

Arbitrary-depth multiplication lower bound under a circuit-local support width promise.

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

User-facing form using disjointness and a nonconstant target.