Upper bound on the relative rank of set-multilinear formulas

This file proves the upper bound of Limaye, Srinivasan and Tavenas [LST21] on the relative rank of small set-multilinear formulas of low product-depth (LST Claim 16, ECCC TR21-081 revision 1, §5, pp. 12–13).

Fix k and a word w : Fin d → ℤ whose letters are ⌊k / √2⌋ and -k, and let block i have 2 ^ |w i| variables. For a set S of blocks, the measure relrk_{w|S} of LST is relRank blk (wordPos w ∩ S) (wordNeg w ∩ S): rows are indexed by the positive blocks of S, columns by the negative ones. If k ≥ 10 d and Δ ≥ 1, a set-multilinear formula on S of product-depth at most Δ with s nodes satisfies relrk_{w|S} ≤ s · 2 ^ (-(k |S| ^ (1 / (2 ^ Δ - 1)) / 20)) (SPFormula.IsSetMultilinear.relRank_polynomial_le, and the case of all blocks SPFormula.IsSetMultilinear.relRank_polynomial_le_univ).

The proof follows the source, along the structure of the formula (SPFormula.relRank_polynomial_le_nodeCount_mul): sum gates by subadditivity, and product gates by multiplicativity (relRank_prod_le). A product gate of product-depth Δ + 1 on m blocks is of type 1 if a factor lives on more than τ = m ^ ((2 ^ Δ - 1) / (2 ^ (Δ + 1) - 1)) blocks, handled by induction on Δ, and of type 2 otherwise. For a type-2 factor on T, the sum w_T is far from zero by the Diophantine bound for 1 / √2 (LST Claim 17, one_div_le_abs_div_sqrt_two_sub), so its relative rank is small by imbalance (relRank_le_two_rpow_abs_sum, LST Claim 7(1)).

Claim 16 holds for every word over the alphabet {⌊k / √2⌋, -k}; the choice of a k-unbiased word (the greedy word Cslib.Circuits.Arithmetic.greedyWord) only matters for the lower bound on the hard polynomial, which is not part of this file.

Departures from the source, all original:

• Claim 17 is stated for all integers a and b; it fails for a = b = 0, which is excluded here. The source only applies it when a + b ≥ 1.
• Claim 16 is stated on every set S of blocks, the form its induction uses.
• Factors on no block (constants, and products of them) have relative rank at most 1 and do not count towards the factors of a type-2 product; the source does not discuss them. A formula of product-depth zero may be set-multilinear on two or more blocks only by computing zero (a sum gate without arguments), which the base case handles separately (SPFormula.IsSetMultilinear.card_le_one_or_polynomial_eq_zero).
• The base case Δ = 1 is the type-2 argument with τ = 1, giving the source's bound.

Main results

• Cslib.Circuits.Arithmetic.relRank_sum_le, Cslib.Circuits.Arithmetic.relRank_inter_biUnion_prod_le: subadditivity and multiplicativity (as an inequality) over finite sums and products.
• Cslib.Circuits.Arithmetic.relRank_le_two_rpow_abs_sum: imbalance for a word, relrk_{w|S} ≤ 2 ^ (-|w_S| / 2).
• Cslib.Circuits.Arithmetic.one_div_le_abs_div_sqrt_two_sub: LST Claim 17.
• Cslib.Circuits.Arithmetic.relRank_le_two_rpow_of_card_le: the type-2 bound for one factor.
• Cslib.Circuits.Arithmetic.SPFormula.relRank_polynomial_le_nodeCount_mul: the induction frame along a set-multilinear formula.
• Cslib.Circuits.Arithmetic.SPFormula.IsSetMultilinear.relRank_polynomial_le: LST Claim 16.

References

• N. Limaye, S. Srinivasan, S. Tavenas, Superpolynomial lower bounds against low-depth algebraic circuits, ECCC TR21-081 revision 1: §2 (words, p. 6), Claim 7 (§2.1, pp. 6–7), proof of Lemma 15 and Claims 16 and 17 (§5, pp. 12–13)

Products of set-multilinear polynomials

theorem Cslib.Circuits.Arithmetic.relRank_sum_le {σ : Type u_1} {K : Type u_2} {d : ℕ} [Fintype σ] [Field K] {blk : σ → Fin d} (A B : Finset (Fin d)) {ι : Type u_3} (s : Finset ι) (f : ι → MvPolynomial σ K) : relRank blk A B (∑ j ∈ s, f j) ≤ ∑ j ∈ s, relRank blk A B (f j)

Subadditivity over finite sums (LST Claim 7(2), iterated).

theorem Cslib.Circuits.Arithmetic.relRank_inter_biUnion_prod_le {σ : Type u_1} {K : Type u_2} {d : ℕ} [Fintype σ] [Field K] {blk : σ → Fin d} (A B : Finset (Fin d)) {ι : Type u_3} (s : Finset ι) (T : ι → Finset (Fin d)) (f : ι → MvPolynomial σ K) (hT : (↑s).PairwiseDisjoint T) (hf : ∀ j ∈ s, MvPolynomial.IsSetMultilinear blk (T j) (f j)) : relRank blk (A ∩ s.biUnion T) (B ∩ s.biUnion T) (∏ j ∈ s, f j) ≤ ∏ j ∈ s, relRank blk (A ∩ T j) (B ∩ T j) (f j)

Multiplicativity over finite products, restricted to the blocks of the product (LST Claim 7(3), relRank_prod_le): the relative rank, on the blocks of ⋃ T j, of a product of set-multilinear polynomials on pairwise disjoint sets of blocks is at most the product of their relative ranks on their own blocks.

theorem Cslib.Circuits.Arithmetic.relRank_prod_le_of_mem {σ : Type u_1} {K : Type u_2} {d : ℕ} [Fintype σ] [Field K] {blk : σ → Fin d} (A B : Finset (Fin d)) {ι : Type u_3} {s : Finset ι} (T : ι → Finset (Fin d)) (f : ι → MvPolynomial σ K) (hT : (↑s).PairwiseDisjoint T) (hf : ∀ j ∈ s, MvPolynomial.IsSetMultilinear blk (T j) (f j)) {j : ι} (hj : j ∈ s) : relRank blk (A ∩ s.biUnion T) (B ∩ s.biUnion T) (∏ j ∈ s, f j) ≤ relRank blk (A ∩ T j) (B ∩ T j) (f j)

The relative rank of a product of set-multilinear polynomials on pairwise disjoint sets of blocks is at most the relative rank of any one factor.

theorem Cslib.Circuits.Arithmetic.relRank_prod_le_two_rpow {σ : Type u_1} {K : Type u_2} {d : ℕ} [Fintype σ] [Field K] {blk : σ → Fin d} (A B : Finset (Fin d)) {ι : Type u_3} (s : Finset ι) (T : ι → Finset (Fin d)) (f : ι → MvPolynomial σ K) (hT : (↑s).PairwiseDisjoint T) (hf : ∀ j ∈ s, MvPolynomial.IsSetMultilinear blk (T j) (f j)) (c : ℝ) (hc : ∀ j ∈ s, relRank blk (A ∩ T j) (B ∩ T j) (f j) ≤ 2 ^ (-(↑(T j).card * c))) : relRank blk (A ∩ s.biUnion T) (B ∩ s.biUnion T) (∏ j ∈ s, f j) ≤ 2 ^ (-(↑(s.biUnion T).card * c))

If each factor of a product of set-multilinear polynomials on pairwise disjoint sets of blocks has relative rank at most 2 ^ (-(|T j| * c)), the product has relative rank at most 2 ^ (-(|⋃ T j| * c)).

The word measure and imbalance

theorem Cslib.Circuits.Arithmetic.relRank_le_two_rpow_abs_sum {σ : Type u_1} {K : Type u_2} {d : ℕ} [Fintype σ] [Field K] {blk : σ → Fin d} (w : Fin d → ℤ) (hblk : ∀ (i : Fin d), Fintype.card { x : σ // blk x = i } = 2 ^ (w i).natAbs) (S : Finset (Fin d)) (f : MvPolynomial σ K) : relRank blk (wordPos w ∩ S) (wordNeg w ∩ S) f ≤ 2 ^ (-(|∑ i ∈ S, ↑(w i)| / 2))

Imbalance for a word (LST Claim 7(1) in the form used in §5): if block i has 2 ^ |w i| variables, then on a set S of blocks, with rows the positive and columns the negative blocks of S, the relative rank is at most 2 ^ (-|w_S| / 2), where w_S = ∑ i ∈ S, w i.

Diophantine approximation of 1 / √2 (LST Claim 17)

theorem Cslib.Circuits.Arithmetic.one_div_le_abs_div_sqrt_two_sub {a b : ℤ} (hab : a ≠ 0 ∨ b ≠ 0) : 1 / (4 * |↑a / √2| + 2) ≤ |↑a / √2 - ↑b|

LST Claim 17 (ECCC TR21-081 rev. 1, §5, proof of Claim 16): for integers a and b, |a / √2 - b| ≥ 1 / (4 |a / √2| + 2). The source states it for all integers; it fails for a = b = 0, which this statement excludes (original correction; the source applies it only when a + b ≥ 1).

Words over the alphabet {⌊k / √2⌋, -k}

theorem Cslib.Circuits.Arithmetic.relRank_le_two_rpow_of_card_le {σ : Type u_1} {K : Type u_2} {d : ℕ} [Field K] {blk : σ → Fin d} [Fintype σ] {k : ℕ} {w : Fin d → ℤ} (hblk : ∀ (i : Fin d), Fintype.card { x : σ // blk x = i } = 2 ^ (w i).natAbs) (hw : ∀ (i : Fin d), w i = ⌊↑k / √2⌋ ∨ w i = -↑k) {T : Finset (Fin d)} {τ : ℝ} (hTτ : ↑T.card ≤ τ) (hτ : 0 < τ) (hk : 10 * τ ^ 2 ≤ ↑k) (f : MvPolynomial σ K) : relRank blk (wordPos w ∩ T) (wordNeg w ∩ T) f ≤ 2 ^ (-(↑T.card * (↑k / (20 * τ ^ 2))))

The relative rank on few blocks is small (LST, proof of Claim 16, type 2): for a word over {⌊k / √2⌋, -k} with block i of 2 ^ |w i| variables, the relative rank on a set T of at most τ blocks is at most 2 ^ (-(|T| k / (20 τ ^ 2))) when k ≥ 10 τ ^ 2.

Set-multilinear formulas

theorem Cslib.Circuits.Arithmetic.SPFormula.nodeCount_le_nodeCount_mul {K : Type u_2} {n m : ℕ} (G : Fin m → SPFormula K n) (j : Fin m) : Formula.nodeCount (G j) ≤ Formula.nodeCount (mul G)

An argument of a product gate has at most as many nodes as the gate.

theorem Cslib.Circuits.Arithmetic.SPFormula.IsSetMultilinear.card_le_one_or_polynomial_eq_zero {K : Type u_2} {d n : ℕ} {blk : Fin n → Fin d} [CommSemiring K] {F : SPFormula K n} {S : Finset (Fin d)} (h : IsSetMultilinear blk F S) (h0 : F.productDepth = 0) : S.card ≤ 1 ∨ F.polynomial = 0

A set-multilinear formula of product-depth zero lives on at most one block, unless it computes zero (a sum gate without arguments is set-multilinear on every set of blocks).

theorem Cslib.Circuits.Arithmetic.SPFormula.relRank_polynomial_le_nodeCount_mul {K : Type u_2} {d n : ℕ} {blk : Fin n → Fin d} [Field K] (A B : Finset (Fin d)) (Δ : ℕ) (β : Finset (Fin d) → ℝ) (hβ : ∀ (S : Finset (Fin d)), 0 ≤ β S) (hsmall : ∀ (S : Finset (Fin d)), S.card ≤ 1 → ∀ (f : MvPolynomial (Fin n) K), relRank blk (A ∩ S) (B ∩ S) f ≤ β S) (hmul : ∀ (m : ℕ) (G : Fin m → SPFormula K n) (T : Fin m → Finset (Fin d)), Pairwise (Function.onFun Disjoint T) → (∀ (j : Fin m), IsSetMultilinear blk (G j) (T j)) → (∀ (j : Fin m), (G j).productDepth < Δ) → relRank blk (A ∩ Finset.univ.biUnion T) (B ∩ Finset.univ.biUnion T) (mul G).polynomial ≤ ↑(Formula.nodeCount (mul G)) * β (Finset.univ.biUnion T)) {F : SPFormula K n} {S : Finset (Fin d)} (hF : IsSetMultilinear blk F S) (hΔ : F.productDepth ≤ Δ) : relRank blk (A ∩ S) (B ∩ S) F.polynomial ≤ ↑(Formula.nodeCount F) * β S

Relative rank along the formula (the induction frame of LST Claim 16): if every polynomial on at most one block has relative rank at most β S, and every product gate of product-depth at most Δ on S has relative rank at most its node count times β S, then every set-multilinear formula on S of product-depth at most Δ has relative rank at most its node count times β S. Sum gates are handled by subadditivity.

theorem Cslib.Circuits.Arithmetic.SPFormula.IsSetMultilinear.relRank_polynomial_le {K : Type u_2} {d n : ℕ} {blk : Fin n → Fin d} [Field K] {k : ℕ} {w : Fin d → ℤ} (hblk : ∀ (i : Fin d), Fintype.card { x : Fin n // blk x = i } = 2 ^ (w i).natAbs) (hk : 10 * d ≤ k) (hw : ∀ (i : Fin d), w i = ⌊↑k / √2⌋ ∨ w i = -↑k) {Δ : ℕ} (hΔ : 1 ≤ Δ) {F : SPFormula K n} {S : Finset (Fin d)} (hF : IsSetMultilinear blk F S) (hFΔ : F.productDepth ≤ Δ) : relRank blk (wordPos w ∩ S) (wordNeg w ∩ S) F.polynomial ≤ ↑(Formula.nodeCount F) * 2 ^ (-(↑k * ↑S.card ^ (1 / (2 ^ Δ - 1)) / 20))

LST Claim 16 (ECCC TR21-081 rev. 1, §5, pp. 12–13): let k ≥ 10 d, and let w be a word whose entries are ⌊k / √2⌋ or -k, with block i of 2 ^ |w i| variables. For Δ ≥ 1, every set-multilinear formula on a set S of blocks with product-depth at most Δ has relative rank (rows: the positive blocks of S, columns: the negative ones) at most nodeCount · 2 ^ (-(k |S| ^ (1 / (2 ^ Δ - 1)) / 20)).

The source states the bound for S the set of all blocks; the induction applies it to the factors, on smaller sets of blocks, so it is stated here for every S. As in the source, the proof splits a product gate by whether some factor has more than τ = |S| ^ ((2 ^ Δ' - 1) / (2 ^ (Δ' + 1) - 1)) blocks. Factors on no block (constants, and products of them) have relative rank at most 1 and contribute nothing, which the source does not discuss (original handling); formulas of product-depth zero that are set-multilinear on two or more blocks compute zero.

theorem Cslib.Circuits.Arithmetic.SPFormula.IsSetMultilinear.relRank_polynomial_le_univ {K : Type u_2} {d n : ℕ} {blk : Fin n → Fin d} [Field K] {k : ℕ} {w : Fin d → ℤ} (hblk : ∀ (i : Fin d), Fintype.card { x : Fin n // blk x = i } = 2 ^ (w i).natAbs) (hk : 10 * d ≤ k) (hw : ∀ (i : Fin d), w i = ⌊↑k / √2⌋ ∨ w i = -↑k) {Δ : ℕ} (hΔ : 1 ≤ Δ) {F : SPFormula K n} (hF : IsSetMultilinear blk F Finset.univ) (hFΔ : F.productDepth ≤ Δ) : relRank blk (wordPos w) (wordNeg w) F.polynomial ≤ ↑(Formula.nodeCount F) * 2 ^ (-(↑k * ↑d ^ (1 / (2 ^ Δ - 1)) / 20))

LST Claim 16 on all blocks: with the hypotheses of relRank_polynomial_le, a set-multilinear formula of product-depth at most Δ on all d blocks has relative rank at most nodeCount · 2 ^ (-(k d ^ (1 / (2 ^ Δ - 1)) / 20)).