Lower bound for set-multilinear formulas computing iterated matrix multiplication

LST Lemma 15 (Limaye, Srinivasan and Tavenas [LST21], ECCC TR21-081 revision 1, §5, statement p. 11, proof p. 12), for formulas, in explicit form: if 10 d ≤ k, 2 ^ k ≤ n and 1 ≤ Δ, a syntactically set-multilinear formula of product-depth at most Δ computing IMM_{n,d} (with its variables renamed) has at least 2 ^ (k (d ^ (1 / (2 ^ Δ - 1)) / 20 - 1 / 2)) nodes (SPFormula.IsSetMultilinear.two_rpow_le_nodeCount_of_imm). The source assumes n ≥ 2 ^ (10 d + 1) and takes k = ⌊log₂ n⌋; these satisfy 10 d ≤ k and 2 ^ k ≤ n, so the hypotheses here are weaker. The bound exceeds 1 only when d ^ (1 / (2 ^ Δ - 1)) > 10.

The model. LST's set-multilinear circuits are gate-wise semantic: each internal gate computes a set-multilinear polynomial in a subset of the blocks [LimayeSrinivasanTavenas2021, §1, p. 2]. The hypothesis here is the stricter syntactic predicate SPFormula.IsSetMultilinear, for the blocks of IMM_{n,d} (block i holds the entries of the i-th matrix): the children of a sum gate are set-multilinear on the same set of blocks, and the children of a product gate on sets partitioning it. The headline is LST Lemma 15 restricted to such formulas; turning a semantically set-multilinear formula into a syntactically set-multilinear one of no larger size and product-depth is a normalization step not done here. The hypotheses are met for every n and d by the sum over paths of product-depth one (immFormula).

The proof follows the source. Let w be the greedy word of the proof of LST Lemma 13 over the alphabet {⌊k / √2⌋, -k} (sqrtTwoWord): it is k-unbiased (isUnbiased_sqrtTwoWord). By LST Lemma 8 in its fixed-sink form (projection_wordSubst_imm), substituting into IMM_{n,d} a variable of block i of X(w) or 0 for each variable of block i gives the word polynomial wordPoly K w 0. Doing the same substitution in the formula (SPFormula.subst) keeps it set-multilinear (SPFormula.IsSetMultilinear.subst), and keeps its size and product-depth (SPFormula.nodeCount_subst, SPFormula.productDepth_subst). The word polynomial has relative rank 2 ^ (-|∑ w| / 2) ≥ 2 ^ (-k / 2) (relRank_wordPoly), and LST Claim 16 (SPFormula.IsSetMultilinear.relRank_polynomial_le_univ) bounds it by nodeCount · 2 ^ (-k d ^ (1 / (2 ^ Δ - 1)) / 20).

Original. The explicit non-asymptotic statement, and the substitution of formulas, which replaces a variable set to 0 by the formula SPFormula.zero (a sum gate without arguments, set-multilinear on every set of blocks), so that the substitution keeps syntactic set-multilinearity without changing the size or the product-depth. LST state Lemma 15 for circuits, which they first expand into formulas; this file works with formulas directly. The relative rank is invariant under renaming the variables along their blocks (relRank_rename), which moves the word polynomial onto the variables Fin m of a formula.

Main definitions

• Cslib.Circuits.Arithmetic.sqrtTwoWord: the word of LST Lemma 15.
• Cslib.Circuits.Arithmetic.SPFormula.subst: substitute variables or 0 for the variables of a formula.
• Cslib.Circuits.Arithmetic.immFormula: the sum over paths computing IMM_{n,d}, on the variables numbered by immVarEquiv.

Main results

• Cslib.Circuits.Arithmetic.isUnbiased_sqrtTwoWord: the word is k-unbiased.
• Cslib.Circuits.Arithmetic.SPFormula.polynomial_subst, Cslib.Circuits.Arithmetic.SPFormula.IsSetMultilinear.subst: substitution of formulas.
• Cslib.Circuits.Arithmetic.SPFormula.IsSetMultilinear.two_rpow_le_nodeCount_of_imm: LST Lemma 15 for syntactically set-multilinear formulas.
• Cslib.Circuits.Arithmetic.isSetMultilinear_immFormula, Cslib.Circuits.Arithmetic.productDepth_immFormula_le, Cslib.Circuits.Arithmetic.rename_polynomial_immFormula: the hypotheses of the lower bound are met by a formula, for every n and d.

References

• N. Limaye, S. Srinivasan, S. Tavenas, Superpolynomial lower bounds against low-depth algebraic circuits, ECCC TR21-081 revision 1: the definition of set-multilinear circuits (§1, p. 2), Lemma 8 (§2.2, p. 7), proof of Lemma 13 (§4, p. 10), Lemma 15 and its proof (§5, pp. 11–12)

The word of Lemma 15

theorem Cslib.Circuits.Arithmetic.floor_div_sqrt_two_mem_Icc (k : ℕ) : 0 ≤ ⌊↑k / √2⌋ ∧ ⌊↑k / √2⌋ ≤ ↑k

0 ≤ ⌊k / √2⌋ ≤ k, so the greedy word over {⌊k / √2⌋, -k} is k-unbiased.

noncomputable def Cslib.Circuits.Arithmetic.sqrtTwoWord (k d : ℕ) : Fin d → ℤ

The word of LST Lemma 15 (proof of Lemma 15, p. 12, following the proof of Lemma 13, p. 10): the greedy word of length d over the alphabet {⌊k / √2⌋, -k}, whose i-th letter is ⌊k / √2⌋ if the sum of the earlier letters is at most 0, and -k otherwise.

theorem Cslib.Circuits.Arithmetic.sqrtTwoWord_eq_or {d : ℕ} (k : ℕ) (i : Fin d) : sqrtTwoWord k d i = ⌊↑k / √2⌋ ∨ sqrtTwoWord k d i = -↑k

Every letter of the word of Lemma 15 is ⌊k / √2⌋ or -k.

theorem Cslib.Circuits.Arithmetic.isUnbiased_sqrtTwoWord (k d : ℕ) : IsUnbiased (sqrtTwoWord k d) k

The word of Lemma 15 is k-unbiased (LST, proof of Lemma 13): every prefix sum has absolute value at most k.

theorem Cslib.Circuits.Arithmetic.natAbs_sum_sqrtTwoWord_le (k d : ℕ) : (∑ i : Fin d, sqrtTwoWord k d i).natAbs ≤ k

The sum of all the letters of the word of Lemma 15 has absolute value at most k.

Substitution in formulas

def Cslib.Circuits.Arithmetic.SPFormula.subst {K : Type u_1} {n m : ℕ} (ρ : Fin n → Option (Fin m)) (F : SPFormula K n) : SPFormula K m

Substitution of variables or 0: replace each input i by the input j when ρ i = some j, and by the formula 0 (a sum gate without arguments) when ρ i = none. It is the substitution Cslib.Circuits.Formula.bind of these formulas.

@[simp]

theorem Cslib.Circuits.Arithmetic.SPFormula.subst_input {K : Type u_1} {n m : ℕ} (ρ : Fin n → Option (Fin m)) (i : Fin n) : subst ρ (Formula.input i) = (ρ i).elim zero Formula.input

Substitution replaces an input by an input or by 0.

@[simp]

theorem Cslib.Circuits.Arithmetic.SPFormula.subst_gate {K : Type u_1} {n m : ℕ} (ρ : Fin n → Option (Fin m)) (op : SigmaPiOp K) (args : Fin ((sigmaPiSignature K).Arity op) → SPFormula K n) : subst ρ (Formula.gate op args) = Formula.gate op fun (j : Fin ((sigmaPiSignature K).Arity op)) => subst ρ (args j)

Substitution in an operation node substitutes in each argument.

@[simp]

theorem Cslib.Circuits.Arithmetic.SPFormula.nodeCount_subst {K : Type u_1} {n m : ℕ} (ρ : Fin n → Option (Fin m)) (F : SPFormula K n) : Formula.nodeCount (subst ρ F) = Formula.nodeCount F

Substitution keeps the number of nodes.

@[simp]

theorem Cslib.Circuits.Arithmetic.SPFormula.productDepth_subst {K : Type u_1} {n m : ℕ} (ρ : Fin n → Option (Fin m)) (F : SPFormula K n) : (subst ρ F).productDepth = F.productDepth

Substitution keeps the product-depth.

theorem Cslib.Circuits.Arithmetic.SPFormula.polynomial_subst {K : Type u_1} {n m : ℕ} [CommSemiring K] (ρ : Fin n → Option (Fin m)) (F : SPFormula K n) : (subst ρ F).polynomial = (MvPolynomial.aeval fun (i : Fin n) => (ρ i).elim 0 MvPolynomial.X) F.polynomial

The substituted formula computes the substituted polynomial.

theorem Cslib.Circuits.Arithmetic.SPFormula.IsSetMultilinear.subst {K : Type u_1} {d n m : ℕ} {blk : Fin n → Fin d} {blk' : Fin m → Fin d} {ρ : Fin n → Option (Fin m)} (hρ : ∀ (i : Fin n) (j : Fin m), ρ i = some j → blk' j = blk i) {F : SPFormula K n} {S : Finset (Fin d)} (hF : IsSetMultilinear blk F S) : IsSetMultilinear blk' (SPFormula.subst ρ F) S

Substitution keeps set-multilinearity: if every variable is replaced by a variable of the same block or by 0, a formula set-multilinear on S stays set-multilinear on S.

The lower bound

theorem Cslib.Circuits.Arithmetic.SPFormula.IsSetMultilinear.two_rpow_le_nodeCount_of_imm {K : Type u_1} {d n N : ℕ} [Field K] [NeZero n] (e : Fin N → Fin d × Fin n × Fin n) {k Δ : ℕ} (hk : 10 * d ≤ k) (hn : 2 ^ k ≤ n) (hΔ : 1 ≤ Δ) {F : SPFormula K N} (hF : IsSetMultilinear (fun (v : Fin N) => (e v).1) F Finset.univ) (hFΔ : F.productDepth ≤ Δ) (hFP : (MvPolynomial.rename e) F.polynomial = imm K n d) : 2 ^ (↑k * (↑d ^ (1 / (2 ^ Δ - 1)) / 20 - 1 / 2)) ≤ ↑(Formula.nodeCount F)

LST Lemma 15 for syntactically set-multilinear formulas (ECCC TR21-081 rev. 1, §5, statement p. 11, proof p. 12, explicit form): let 10 d ≤ k, 2 ^ k ≤ n and 1 ≤ Δ. If F is a formula that is syntactically set-multilinear (SPFormula.IsSetMultilinear) on all d blocks of IMM_{n,d}, block i being the entries of the i-th matrix, of product-depth at most Δ, and computes IMM_{n,d} with its variables renamed by e, then F has at least 2 ^ (k (d ^ (1 / (2 ^ Δ - 1)) / 20 - 1 / 2)) nodes. The bound is nontrivial only when d ^ (1 / (2 ^ Δ - 1)) > 10. The hypotheses are met by immFormula for every n and d.

The source assumes n ≥ 2 ^ (10 d + 1) and takes k = ⌊log₂ n⌋, which gives 10 d ≤ k and 2 ^ k ≤ n; the hypotheses here are weaker. It states the bound n ^ Ω(d ^ (1 / (2 ^ Δ - 1)) / Δ) for set-multilinear circuits in the gate-wise semantic sense, each internal gate computing a set-multilinear polynomial in a subset of the blocks (§1, p. 2); this is the formula bound in its proof, before the expansion of circuits into formulas, under the stricter syntactic predicate: the children of a sum gate share their set of blocks, and the children of a product gate partition it. Reaching it from a semantically set-multilinear formula is a normalization step not proved here. The non-asymptotic statement is original.

The sum over paths computes IMM_{n,d}

def Cslib.Circuits.Arithmetic.immVarEquiv (n d : ℕ) : Fin (d * (n * n)) ≃ Fin d × Fin n × Fin n

The numbering of the d n² variables of IMM_{n,d}: the variable (i, a, c), the entry (a, c) of the i-th matrix, is numbered i n² + a n + c.

def Cslib.Circuits.Arithmetic.immFormula (K : Type u_1) [Zero K] [One K] (n d : ℕ) [NeZero n] : SPFormula K (d * (n * n))

The sum over paths for IMM_{n,d}, a formula of product-depth one: a sum gate over all sequences p : Fin (d + 1) → Fin n of the products ∏ i, x_{(i, p i, p (i + 1))}, with edge constant 1 on the paths from 0 to 0 and 0 on the others.

theorem Cslib.Circuits.Arithmetic.productDepth_immFormula_le {K : Type u_1} {d : ℕ} (n : ℕ) [NeZero n] [Zero K] [One K] : (immFormula K n d).productDepth ≤ 1

The sum over paths has product-depth at most one.

theorem Cslib.Circuits.Arithmetic.isSetMultilinear_immFormula {K : Type u_1} {d : ℕ} (n : ℕ) [NeZero n] [Zero K] [One K] : SPFormula.IsSetMultilinear (fun (v : Fin (d * (n * n))) => ((immVarEquiv n d) v).1) (immFormula K n d) Finset.univ

The sum over paths is set-multilinear on all blocks of IMM_{n,d}.

theorem Cslib.Circuits.Arithmetic.rename_polynomial_immFormula {K : Type u_1} {d : ℕ} (n : ℕ) [NeZero n] [CommSemiring K] : (MvPolynomial.rename ⇑(immVarEquiv n d)) (immFormula K n d).polynomial = imm K n d

The sum over paths computes IMM_{n,d} on the numbered variables.