The product gadget of set-multilinearization

Gate simulation turns a formula into one computing its set-multilinear parts [Forbes2024, Cor. 27]. A product gate f = ∏ j, f j is simulated by the product gadget SPFormula.mulGadget, a formula computing the part π_S(f) of f on a set S of blocks from formulas g j T computing the parts π_T(f j) of the factors. It writes out the expansion MvPolynomial.smProj_prod_eq_sum_sign of π_S(f):

π_S(f) = A ∑_P ∑_{π ∈ Perm P} sgn π ∑_{Y ⊆ Z} (-1) ^ #Y ∏_{q ∈ orbits π} ∑_{j ∉ Y} u_j ^ #q ∏_{T ∈ q} π_T(f j),

where P runs over the set partitions of S, Z is the set of factors with constant term 0, A is the product of the other constant terms and u_j the inverse of the constant term of f j (or 1 when it is 0). It is 0 when #S < #Z. The scalars ride on the edges of the sum gates. The gadget

• computes π_S(f) (SPFormula.polynomial_mulGadget);
• is syntactically set-multilinear on S when each g j T is on T (SPFormula.isSetMultilinear_mulGadget): each sum over j has children on the same union of the parts in an orbit, and the factors of each product sit on disjoint sets of blocks;
• has product-depth at most two more than the g j T (SPFormula.productDepth_mulGadget_le);
• has at most gadgetCost d * (1 + card ι + ∑ j, w j) nodes, when each g j T with T ⊆ S has at most w j (SPFormula.nodeCount_mulGadget_le). The factor gadgetCost d depends only on the number d of blocks, not on the fan-in of the product gate: the number of products of sums is at most (d + 1) ^ d · d! · 2 ^ d (set partitions, permutations, subsets of Z).

The formula is built from sum and product gates over finite sets of children (SPFormula.sumOn, SPFormula.prodOn).

Main definitions

• Cslib.Circuits.Arithmetic.SPFormula.sumOn, Cslib.Circuits.Arithmetic.SPFormula.prodOn: sum and product gates over the formulas indexed by a finite set.
• Cslib.Circuits.Arithmetic.SPFormula.mulGadget: the product gadget.
• Cslib.Circuits.Arithmetic.SPFormula.gadgetCost: its size factor 2 * (2 * (d + 1) ^ 2) ^ (d + 1).

Main results

• Cslib.Circuits.Arithmetic.SPFormula.polynomial_mulGadget, Cslib.Circuits.Arithmetic.SPFormula.isSetMultilinear_mulGadget, Cslib.Circuits.Arithmetic.SPFormula.productDepth_mulGadget_le, Cslib.Circuits.Arithmetic.SPFormula.nodeCount_mulGadget_le: the four properties above.

References

• M. A. Forbes, Low-depth algebraic circuit lower bounds over any field, Lemma 26 and its proof, pp. 31:13–31:14. Forbes computes the surjective permanents of the proof by Corollary 22 (p. 31:12), reducing them to permanents by Lemma 21 (p. 31:12) and expanding those by the partition form of the Binet–Minc identity, Theorem 13 (p. 31:10). The gadget here uses instead inclusion–exclusion in place of Lemma 21 and the permutation form of the Binet–Minc identity in place of Theorem 13 (Matrix.rectPermSurj_eq_sum_sign_prod_sameCycle), and is original, as are its explicit size bound and the formulas sumOn and prodOn.

Gates over finite sets

noncomputable def Cslib.Circuits.Arithmetic.SPFormula.sumOn {K : Type u_1} {n : ℕ} {ι : Type u_2} (s : Finset ι) (c : ι → K) (G : ι → SPFormula K n) : SPFormula K n

The sum gate over the formulas G i for i ∈ s, with edge constants c i.

noncomputable def Cslib.Circuits.Arithmetic.SPFormula.prodOn {K : Type u_1} {n : ℕ} {ι : Type u_2} (s : Finset ι) (G : ι → SPFormula K n) : SPFormula K n

The product gate over the formulas G i for i ∈ s.

theorem Cslib.Circuits.Arithmetic.SPFormula.polynomial_sumOn {K : Type u_1} {n : ℕ} {ι : Type u_2} (s : Finset ι) (c : ι → K) (G : ι → SPFormula K n) [CommSemiring K] : (sumOn s c G).polynomial = ∑ i ∈ s, MvPolynomial.C (c i) * (G i).polynomial

A sum gate over a finite set computes the linear combination of its children.

theorem Cslib.Circuits.Arithmetic.SPFormula.polynomial_prodOn {K : Type u_1} {n : ℕ} {ι : Type u_2} (s : Finset ι) (G : ι → SPFormula K n) [CommSemiring K] : (prodOn s G).polynomial = ∏ i ∈ s, (G i).polynomial

A product gate over a finite set computes the product of its children.

theorem Cslib.Circuits.Arithmetic.SPFormula.nodeCount_sumOn {K : Type u_1} {n : ℕ} {ι : Type u_2} (s : Finset ι) (c : ι → K) (G : ι → SPFormula K n) : Formula.nodeCount (sumOn s c G) = ∑ i ∈ s, Formula.nodeCount (G i) + 1

A sum gate over a finite set has one node more than its children.

theorem Cslib.Circuits.Arithmetic.SPFormula.nodeCount_prodOn {K : Type u_1} {n : ℕ} {ι : Type u_2} (s : Finset ι) (G : ι → SPFormula K n) : Formula.nodeCount (prodOn s G) = ∑ i ∈ s, Formula.nodeCount (G i) + 1

A product gate over a finite set has one node more than its children.

theorem Cslib.Circuits.Arithmetic.SPFormula.productDepth_sumOn_le {K : Type u_1} {n : ℕ} {ι : Type u_2} {s : Finset ι} (c : ι → K) {G : ι → SPFormula K n} {p : ℕ} (h : ∀ i ∈ s, (G i).productDepth ≤ p) : (sumOn s c G).productDepth ≤ p

A sum gate does not add to the product-depth.

theorem Cslib.Circuits.Arithmetic.SPFormula.productDepth_prodOn_le {K : Type u_1} {n : ℕ} {ι : Type u_2} {s : Finset ι} {G : ι → SPFormula K n} {p : ℕ} (h : ∀ i ∈ s, (G i).productDepth ≤ p) : (prodOn s G).productDepth ≤ p + 1

A product gate adds one to the product-depth.

theorem Cslib.Circuits.Arithmetic.SPFormula.isSetMultilinear_sumOn {K : Type u_1} {n d : ℕ} {ι : Type u_2} {s : Finset ι} (c : ι → K) {G : ι → SPFormula K n} {blk : Fin n → Fin d} {S : Finset (Fin d)} (h : ∀ i ∈ s, IsSetMultilinear blk (G i) S) : IsSetMultilinear blk (sumOn s c G) S

A sum gate over children set-multilinear on S is set-multilinear on S.

theorem Cslib.Circuits.Arithmetic.SPFormula.isSetMultilinear_prodOn {K : Type u_1} {n d : ℕ} {ι : Type u_2} {s : Finset ι} {G : ι → SPFormula K n} {blk : Fin n → Fin d} {T : ι → Finset (Fin d)} (hT : (↑s).PairwiseDisjoint T) (h : ∀ i ∈ s, IsSetMultilinear blk (G i) (T i)) : IsSetMultilinear blk (prodOn s G) (s.biUnion T)

A product gate over children set-multilinear on pairwise disjoint sets T i is set-multilinear on their union.

The product gadget

def Cslib.Circuits.Arithmetic.SPFormula.mulGadget.zeroCols {K : Type u_1} {ι : Type u_2} [Field K] [DecidableEq K] [Fintype ι] (a : ι → K) : Finset ι

The factors with constant term 0.

def Cslib.Circuits.Arithmetic.SPFormula.mulGadget.colScale {K : Type u_1} {ι : Type u_2} [Field K] [DecidableEq K] (a : ι → K) (j : ι) : K

The scale of a factor: the inverse of its constant term, or 1 if that is 0.

noncomputable def Cslib.Circuits.Arithmetic.SPFormula.mulGadget {K : Type u_1} {n d : ℕ} {ι : Type u_2} [Field K] [DecidableEq K] [Fintype ι] [DecidableEq ι] (S : Finset (Fin d)) (a : ι → K) (g : ι → Finset (Fin d) → SPFormula K n) : SPFormula K n

The product gadget (original; it simulates a product gate as in [Forbes2024, Lemma 26]): from formulas g j T for the parts on T of the factors of a product with constant terms a j, the formula for the part on S of the product given by MvPolynomial.smProj_prod_eq_sum_sign, or 0 if more than #S constant terms vanish.

theorem Cslib.Circuits.Arithmetic.SPFormula.polynomial_mulGadget {K : Type u_1} {n d : ℕ} {ι : Type u_2} [Field K] [DecidableEq K] [Fintype ι] [DecidableEq ι] {S : Finset (Fin d)} {a : ι → K} {g : ι → Finset (Fin d) → SPFormula K n} {blk : Fin n → Fin d} {f : ι → MvPolynomial (Fin n) K} (ha : ∀ (j : ι), MvPolynomial.constantCoeff (f j) = a j) (hg : ∀ (j : ι) (T : Finset (Fin d)), (g j T).polynomial = (MvPolynomial.smProj blk T) (f j)) : (mulGadget S a g).polynomial = (MvPolynomial.smProj blk S) (∏ j : ι, f j)

The product gadget computes the part of the product (original).

theorem Cslib.Circuits.Arithmetic.SPFormula.isSetMultilinear_mulGadget {K : Type u_1} {n d : ℕ} {ι : Type u_2} [Field K] [DecidableEq K] [Fintype ι] [DecidableEq ι] {S : Finset (Fin d)} {a : ι → K} {g : ι → Finset (Fin d) → SPFormula K n} {blk : Fin n → Fin d} (hg : ∀ (j : ι) (T : Finset (Fin d)), IsSetMultilinear blk (g j T) T) : IsSetMultilinear blk (mulGadget S a g) S

The product gadget is set-multilinear on S (original) when each g j T is set-multilinear on T.

theorem Cslib.Circuits.Arithmetic.SPFormula.productDepth_mulGadget_le {K : Type u_1} {n d : ℕ} {ι : Type u_2} [Field K] [DecidableEq K] [Fintype ι] [DecidableEq ι] {S : Finset (Fin d)} {a : ι → K} {g : ι → Finset (Fin d) → SPFormula K n} {p : ℕ} (hg : ∀ (j : ι) (T : Finset (Fin d)), (g j T).productDepth ≤ p) : (mulGadget S a g).productDepth ≤ p + 2

The product gadget adds at most two to the product-depth (original).

def Cslib.Circuits.Arithmetic.SPFormula.gadgetCost (d : ℕ) : ℕ

The size factor of the product gadget on d blocks: 2 * (2 * (d + 1) ^ 2) ^ (d + 1). It bounds 4 (d + 1) times the number of products of sums, at most (d + 1) ^ d · d! · 2 ^ d.

theorem Cslib.Circuits.Arithmetic.SPFormula.nodeCount_mulGadget_le {K : Type u_1} {n d : ℕ} {ι : Type u_2} [Field K] [DecidableEq K] [Fintype ι] [DecidableEq ι] {S : Finset (Fin d)} {a : ι → K} {g : ι → Finset (Fin d) → SPFormula K n} {w : ι → ℕ} (hg : ∀ (j : ι), ∀ T ⊆ S, Formula.nodeCount (g j T) ≤ w j) : Formula.nodeCount (mulGadget S a g) ≤ gadgetCost d * (1 + Fintype.card ι + ∑ j : ι, w j)

The size of the product gadget (original): if each g j T with T ⊆ S has at most w j nodes, the gadget has at most gadgetCost d * (1 + card ι + ∑ j, w j) nodes.