Set-multilinearization of formulas over any field

Let the variables of a formula F over a field be split into d blocks by blk. For a set S of blocks, the formula SPFormula.smPart blk S F computes the set-multilinear part on S of the polynomial computed by F (SPFormula.polynomial_smPart), and is syntactically set-multilinear on S (SPFormula.isSetMultilinear_smPart). It is built by gate simulation [Forbes2024, Cor. 27], one node of F and one set of blocks at a time:

• an input is kept on its own block and replaced by 0 on the others;
• a constant is kept on no block and replaced by 0 on the others;
• a sum gate is simulated by the same sum gate over the parts of its children on S ([Forbes2024, Lemma 25]);
• a product gate is simulated by the product gadget SPFormula.mulGadget over the parts of its children on all sets of blocks ([Forbes2024, Lemma 26]).

Sum gates keep the product-depth and the product gadget adds two, so smPart at most doubles the product-depth (SPFormula.productDepth_smPart_le). The size of the product gadget is linear in the sizes of its inputs with a factor depending only on d; since a formula is a tree, the inputs are copied, and the size grows by at most the factor smCost d per level of product gates (SPFormula.nodeCount_smPart_le):

nodeCount (smPart blk S F) ≤ smCost d ^ productDepth F * nodeCount F, with smCost d = 4 * (2 * (d + 1) ^ 2) ^ (d + 1).

There is no assumption on the characteristic of the field, on homogeneity or on the formula.

Main definitions

• Cslib.Circuits.Arithmetic.SPFormula.smPart: the set-multilinear part of a formula on a set of blocks.
• Cslib.Circuits.Arithmetic.SPFormula.smCost: the size factor per level of product gates.

Main results

• Cslib.Circuits.Arithmetic.SPFormula.polynomial_smPart: it computes the set-multilinear part.
• Cslib.Circuits.Arithmetic.SPFormula.isSetMultilinear_smPart: it is set-multilinear.
• Cslib.Circuits.Arithmetic.SPFormula.productDepth_smPart_le: product-depth at most doubles.
• Cslib.Circuits.Arithmetic.SPFormula.nodeCount_smPart_le: the size bound.

References

• M. A. Forbes, Low-depth algebraic circuit lower bounds over any field, Lemmas 24–26 and Corollary 27, pp. 31:13–31:14. Forbes simulates the gates of a circuit and bounds the size by poly(s, Θ(d / ln d) ^ d); the simulation here is done on formulas, with the product gadget SPFormula.mulGadget, the explicit factor smCost d and the bound linear in the size, and is original in this form.

noncomputable def Cslib.Circuits.Arithmetic.SPFormula.smPart {K : Type u_1} [Field K] [DecidableEq K] {n d : ℕ} (blk : Fin n → Fin d) : Finset (Fin d) → SPFormula K n → SPFormula K n

The set-multilinear part of a formula on the set S of blocks, by gate simulation ([Forbes2024, Cor. 27], original on formulas): inputs and constants are kept on their own sets of blocks and replaced by 0 on the others, a sum gate is simulated by the same sum gate over the parts on S of its children, and a product gate by the product gadget over the parts of its children on all sets of blocks.

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

The size factor of smPart per level of product gates: 4 * (2 * (d + 1) ^ 2) ^ (d + 1), twice the size factor of the product gadget.

theorem Cslib.Circuits.Arithmetic.SPFormula.one_le_smCost (d : ℕ) : 1 ≤ smCost d

The size factor is positive.

theorem Cslib.Circuits.Arithmetic.SPFormula.polynomial_smPart {K : Type u_1} [Field K] [DecidableEq K] {n d : ℕ} {blk : Fin n → Fin d} (S : Finset (Fin d)) (F : SPFormula K n) : (smPart blk S F).polynomial = (MvPolynomial.smProj blk S) F.polynomial

smPart computes the set-multilinear part (original on formulas; [Forbes2024, Cor. 27]): smPart blk S F computes the part on S of the polynomial computed by F.

theorem Cslib.Circuits.Arithmetic.SPFormula.isSetMultilinear_smPart {K : Type u_1} [Field K] [DecidableEq K] {n d : ℕ} {blk : Fin n → Fin d} (S : Finset (Fin d)) (F : SPFormula K n) : IsSetMultilinear blk (smPart blk S F) S

smPart is set-multilinear (original on formulas): smPart blk S F is syntactically set-multilinear on S.

theorem Cslib.Circuits.Arithmetic.SPFormula.productDepth_smPart_le {K : Type u_1} [Field K] [DecidableEq K] {n d : ℕ} {blk : Fin n → Fin d} (S : Finset (Fin d)) (F : SPFormula K n) : (smPart blk S F).productDepth ≤ 2 * F.productDepth

smPart at most doubles the product-depth (original on formulas; [Forbes2024, Cor. 27]): sum gates keep it and the product gadget adds two.

theorem Cslib.Circuits.Arithmetic.SPFormula.nodeCount_smPart_le {K : Type u_1} [Field K] [DecidableEq K] {n d : ℕ} {blk : Fin n → Fin d} (S : Finset (Fin d)) (F : SPFormula K n) : Formula.nodeCount (smPart blk S F) ≤ smCost d ^ F.productDepth * Formula.nodeCount F

The size of smPart (original; [Forbes2024, Cor. 27] bounds the size of the simulating circuit by poly(s, Θ(d / ln d) ^ d)): smPart blk S F has at most smCost d ^ productDepth F * nodeCount F nodes.