Superpolynomial lower bounds for constant-depth circuits computing IMM over any field

The lower bound of Limaye, Srinivasan and Tavenas [LST21] for circuits of unbounded fan-in and constant product-depth, over any field.

Explicit form (SPCircuit.two_rpow_le_of_imm): let 10 d ≤ k, 2 ^ k ≤ n and 1 ≤ Δ. A simple circuit (SPCircuit.IsSimple) with C.size gates and N inputs, of product-depth at most Δ, computing IMM_{n,d} (with its variables renamed) satisfies

2 ^ (k (d ^ (1 / (4 ^ Δ - 1)) / 20 - 1 / 2)) ≤ smCost d ^ Δ * (C.size + N + 1) ^ (2 Δ + 1),

where smCost d = 4 * (2 * (d + 1) ^ 2) ^ (d + 1). It is the formula bound SPFormula.two_rpow_le_of_imm applied to the unfolded formula (SPCircuit.toSPFormula), of at most (C.size + N + 1) ^ (2 Δ + 1) nodes.

Superpolynomial form (SPCircuit.eventually_pow_lt_size_of_imm): fix a field K, a product-depth Δ and an exponent c. For all sufficiently large n, with d = ⌊log₂ ⌊log₂ n⌋⌋, every simple circuit over K of product-depth at most Δ computing IMM_{n,d}, its d n ^ 2 variables in bijection with the inputs, has more than n ^ c gates. At this d, log₂ (smCost d ^ Δ) = O(Δ d log d) is o(log n), so the factor smCost d ^ Δ is n ^ o(1), while the exponent d ^ (1 / (4 ^ Δ - 1)) grows without bound: the bound is n ^ ω(1), at fixed Δ.

Source. [LimayeSrinivasanTavenas2021, Theorem 1, p. 1] states that for d = o(log N) and Δ growing, over a field of characteristic 0 or larger than d, IMM_{n,d} in N = d n ^ 2 variables has no circuit of product-depth Δ and size at most N ^ (d ^ exp (-O(Δ))); its Corollary 4 (p. 4) gives, for d ≤ (log n) / 100, size at least n ^ (d ^ exp (-O(Δ))), and superpolynomial bounds for ω(1) ≤ d ≤ poly(n) at constant Δ (remark after Corollary 4). Here:

• the field is arbitrary, by the set-multilinearization of [Forbes2024, Cor. 27], used in SPFormula.two_rpow_le_of_imm, in place of the source's Proposition 9 (§3, p. 8), which needs characteristic 0 or larger than d;
• the constants are explicit, with the exponent d ^ (1 / (4 ^ Δ - 1)): the source's Lemma 15 (§5, p. 11) at product-depth 2 Δ, the doubling made in its proof of Corollary 4 (§5, p. 12). At Δ = 1 this is d ^ (1 / 3), not the √d of its Lemma 13 (p. 10) and Corollary 4;
• the superpolynomial form is stated at the single value d = ⌊log₂ ⌊log₂ n⌋⌋ and at constant Δ; the asymptotic exponent d ^ exp (-O(Δ)) at growing Δ, the range of d up to poly(n) and the 0/1-substitution remark are not formalized;
• circuits are simple: product gates read pairwise distinct wires, an original rendering of the source's graphs without multiple edges (Complexity.Computability.Circuit.Arithmetic.SPCircuit).

Original. The explicit statements and their constants, the circuit-to-formula bound and the asymptotic derivation.

Main results

• Cslib.Circuits.Arithmetic.SPFormula.smCost_le_two_pow: smCost d ≤ 2 ^ ((2 b + 1) (d + 1) + 2) when d + 1 ≤ 2 ^ b.
• Cslib.Circuits.Arithmetic.SPCircuit.two_rpow_le_of_imm: the explicit lower bound for circuits.
• Cslib.Circuits.Arithmetic.SPCircuit.eventually_pow_lt_size_of_imm: the superpolynomial lower bound.
• Cslib.Circuits.Arithmetic.SPCircuit.exists_isSimple_imm: its hypotheses are satisfiable: for every n and d, a simple circuit of product-depth one computes IMM_{n,d}.

References

• N. Limaye, S. Srinivasan, S. Tavenas, Superpolynomial lower bounds against low-depth algebraic circuits, ECCC TR21-081 revision 1: Theorem 1 (p. 1), Corollary 4 (p. 4) and its proof (§5, p. 12), Proposition 9 (§3, p. 8), Lemma 15 (§5, p. 11)
• M. A. Forbes, Low-depth algebraic circuit lower bounds over any field, Corollary 27 (p. 31:14)

theorem Cslib.Circuits.Arithmetic.SPFormula.smCost_le_two_pow {d b : ℕ} (hd : d + 1 ≤ 2 ^ b) : smCost d ≤ 2 ^ ((2 * b + 1) * (d + 1) + 2)

The size factor of set-multilinearization is at most exponential in d log d: smCost d ≤ 2 ^ ((2 b + 1) (d + 1) + 2) when d + 1 ≤ 2 ^ b.

theorem Cslib.Circuits.Arithmetic.isSimple_immFormula {K : Type u_1} [Zero K] [One K] (n d : ℕ) [NeZero n] : (immFormula K n d).IsSimple

The sum over paths is simple: the variables of a path lie in distinct matrices.

theorem Cslib.Circuits.Arithmetic.SPCircuit.two_rpow_le_of_imm {K : Type u_1} {n d 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 ≤ Δ) {C : SPCircuit K N} (hC : C.IsSimple) (hCΔ : C.productDepth ≤ Δ) (hCP : (MvPolynomial.rename e) C.polynomial = imm K n d) : 2 ^ (↑k * (↑d ^ (1 / (4 ^ Δ - 1)) / 20 - 1 / 2)) ≤ ↑(SPFormula.smCost d) ^ Δ * (↑C.size + ↑N + 1) ^ (2 * Δ + 1)

Lower bound for circuits computing IMM_{n,d} over any field (LST Corollary 4, ECCC TR21-081 rev. 1, p. 4, and through it Theorem 1, p. 1, by [Forbes2024, Cor. 27]; explicit form original): let 10 d ≤ k, 2 ^ k ≤ n and 1 ≤ Δ. If a simple circuit C over a field, with C.size gates and N inputs, of product-depth at most Δ, computes IMM_{n,d} with its variables renamed by e, then 2 ^ (k (d ^ (1 / (4 ^ Δ - 1)) / 20 - 1 / 2)) ≤ smCost d ^ Δ * (C.size + N + 1) ^ (2 Δ + 1). There is no assumption on the characteristic, on homogeneity or on set-multilinearity.

theorem Cslib.Circuits.Arithmetic.SPCircuit.eventually_pow_lt_size_of_imm (K : Type u_2) [Field K] (Δ c : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ [inst : NeZero n] {N : ℕ} (e : Fin N ≃ Fin (Nat.log 2 (Nat.log 2 n)) × Fin n × Fin n) (C : SPCircuit K N), C.IsSimple → C.productDepth ≤ Δ → (MvPolynomial.rename ⇑e) C.polynomial = imm K n (Nat.log 2 (Nat.log 2 n)) → n ^ c < C.size

Superpolynomial lower bound for constant-depth circuits computing IMM over any field (LST Theorem 1, p. 1, and Corollary 4, p. 4, at constant product-depth and d = ⌊log₂ ⌊log₂ n⌋⌋, over any field by [Forbes2024, Cor. 27]; this form original): for every product-depth Δ and exponent c, for all sufficiently large n, every simple circuit over K of product-depth at most Δ computing IMM_{n,d}, with d = ⌊log₂ ⌊log₂ n⌋⌋ and its d n ^ 2 variables in bijection e with the inputs, has more than n ^ c gates.

theorem Cslib.Circuits.Arithmetic.SPCircuit.exists_isSimple_imm (K : Type u_2) [CommSemiring K] (n d : ℕ) [NeZero n] : ∃ (C : SPCircuit K (d * (n * n))), C.IsSimple ∧ C.productDepth ≤ 1 ∧ C.size = n ^ (d + 1) + 1 ∧ (MvPolynomial.rename ⇑(immVarEquiv n d)) C.polynomial = imm K n d

Simple circuits computing IMM exist at every size: the circuit of the sum over paths (immFormula) is simple, has product-depth at most one and n ^ (d + 1) + 1 gates, and computes IMM_{n,d} with its d n ^ 2 variables numbered by immVarEquiv. So the hypotheses of the lower bounds are satisfiable for every n and d.