Word polynomials and iterated matrix multiplication

The hard polynomials of Limaye, Srinivasan and Tavenas [LimayeSrinivasanTavenas2021, §2.2]. A word is a tuple w : Fin d → ℤ (Cslib.Circuits.Arithmetic.Word). Its variables X(w) (WordVar w) form d blocks, block i having 2 ^ |w i| variables labelled by the bit strings of length |w i|; here a bit string of length a is a number below 2 ^ a, its first bit the least significant. The blocks with 0 ≤ w i are positive (wordPos w), the others negative (wordNeg w). A set-multilinear monomial m on all blocks (WordChoice w) has a positive string σ(m⁺), the labels of its positive variables concatenated in order, and a negative string σ(m⁻). LST's word polynomial P_w is the sum of the monomials whose two strings are prefix-related: the shorter is a prefix of the longer (wordPolyAllSinks).

The word polynomial with sink τ (wordPoly K w τ) is the sum of the monomials whose shorter string is a prefix of the longer one with rest exactly τ: σ(m⁺) = σ(m⁻) τ when ∑ i, w i ≥ 0, and σ(m⁻) = σ(m⁺) τ otherwise. LST's P_w is the sum of these over all τ of length |∑ i, w i| (sum_wordPoly).

• Full rank (LST §2.2, p. 7, "the matrices M_w(P_w) are full-rank"). For each sink, the relative-rank matrix of wordPoly K w τ with rows the positive and columns the negative blocks has rank equal to the smaller of its dimensions (rank_relMatrix_wordPoly), so its relative rank is 2 ^ (-|∑ i, w i| / 2) (relRank_wordPoly), the largest value LST Claim 7(1) allows.
• Lemma 8 (LST §2.2 and §8). If w is b-unbiased (IsUnbiased w b: every prefix sum has absolute value at most b) and 2 ^ b ≤ n, then wordPoly K w τ is a projection of the iterated matrix multiplication polynomial imm K n d, the entry (0, 0) of the product of d generic n × n matrices (isProjection_wordPoly_imm). The substitution wordSubst maps each variable of matrix i to a variable of block i of X(w) or to 0 (wordSubst_eq_inl, wordSubst_eq_inr), so it maps set-multilinear computations to set-multilinear computations.

The proof follows LST's branching program (Lemma 22): after reading the first i blocks, the state is the unmatched rest of the longer string (wordRestAt), a string of length |∑ j < i, w j| ≤ b, and each block changes it by one step (wordStep, wordRestAt_succ), whose label is determined by its two ends (wordStep_inj). Expanding the entry of the matrix product as a sum over paths (Matrix.list_prod_ofFn_apply), exactly one path of states contributes each monomial with rest τ, and none contributes the others.

Original. LST's branching program identifies all the vertices of its last layer, so the last matrix of their substitution has sums of variables as entries and the substitution is linear, not a projection (their proof of Lemma 8, §8, p. 20, speaks of "linear substitutions"). Fixing one sink τ keeps one vertex of the last layer instead: the substitution becomes a projection, and full rank holds for every sink. The fixed-sink polynomial, the numeric encoding of bit strings, the step function wordStep and the non-asymptotic hypotheses IsUnbiased w b and 2 ^ b ≤ n are original to this formalization.

Main definitions

• Cslib.Circuits.Arithmetic.prefixRest: comparison of two bit strings.
• Cslib.Circuits.Arithmetic.wordStringLen, Cslib.Circuits.Arithmetic.wordStringVal, Cslib.Circuits.Arithmetic.wordPrefixSum: the lengths and values of the strings read from the first blocks of a word, and its prefix sums.
• Cslib.Circuits.Arithmetic.wordRest: comparison of the positive and negative strings of a monomial.
• Cslib.Circuits.Arithmetic.wordPoly: the word polynomial with sink τ.
• Cslib.Circuits.Arithmetic.wordPolyAllSinks: LST's word polynomial P_w.
• Cslib.Circuits.Arithmetic.imm: the iterated matrix multiplication polynomial IMM_{n,d}.
• Cslib.Circuits.Arithmetic.wordSubst: the substitution of Lemma 8.

Main results

• Cslib.Circuits.Arithmetic.coeff_wordPoly: the coefficients of the word polynomial.
• Cslib.Circuits.Arithmetic.isSetMultilinear_wordPoly: it is set-multilinear on all blocks.
• Cslib.Circuits.Arithmetic.sum_wordPoly: P_w is the sum of the word polynomials with the sinks of length |∑ i, w i|.
• Cslib.Circuits.Arithmetic.rank_relMatrix_wordPoly, Cslib.Circuits.Arithmetic.relRank_wordPoly: full rank.
• Cslib.Circuits.Arithmetic.projection_imm: a projection of IMM_{n,d} as a sum over paths.
• Cslib.Circuits.Arithmetic.projection_wordSubst_imm, Cslib.Circuits.Arithmetic.isProjection_wordPoly_imm: LST Lemma 8, fixed-sink form.

References

• N. Limaye, S. Srinivasan, S. Tavenas, Superpolynomial lower bounds against low-depth algebraic circuits, ECCC TR21-081 revision 1, §2 (words, unbiasedness), §2.2 (word polynomials, full rank, Lemma 8) and §8 (Lemma 22 and the proof of Lemma 8).

Bit strings as numbers

def Cslib.Circuits.Arithmetic.prefixRest (A a B b : ℕ) : Option ℕ

The comparison of two bit strings. A bit string of length a is encoded as a number below 2 ^ a, its first bit least significant: the concatenation of A (length a) and B is A + 2 ^ a * B, the prefix of length b of A is A % 2 ^ b, and the rest is A / 2 ^ b. When the shorter of the strings A (length a) and B (length b) is a prefix of the longer, prefixRest A a B b is some of the rest of the longer one, a string of length |a - b|; otherwise it is none.

def Cslib.Circuits.Arithmetic.wordStep (e : ℤ) (s : ℕ) (k : ℤ) (β : ℕ) : Option ℕ

One step of the branching program for word polynomials. The state is the unmatched rest s of the longer string read so far, e is the signed excess (the length of the positive string read minus that of the negative one, so s < 2 ^ |e|), and the next block has signed length k and label β. A block on the side of the excess is appended to the rest; a block on the other side must agree with the beginning of the rest, or, when it is longer, begin with the rest, and the unmatched part of the longer one remains.

Prefixes of a word

def Cslib.Circuits.Arithmetic.wordStringLen (p : ℤ → Prop) [DecidablePred p] (W : ℕ → ℤ) (i : ℕ) : ℕ

The total length of the blocks j < i whose signed length W j satisfies p: with p the nonnegative (negative) integers, the length of the positive (negative) string read from the first i blocks of a word.

def Cslib.Circuits.Arithmetic.wordStringVal (p : ℤ → Prop) [DecidablePred p] (W : ℕ → ℤ) (D : ℕ → ℕ) (i : ℕ) : ℕ

The concatenation of the labels D j of the blocks j < i whose signed length satisfies p, as a number with the first bit least significant.

def Cslib.Circuits.Arithmetic.wordPrefixSum (W : ℕ → ℤ) (i : ℕ) : ℤ

The signed length ∑ j < i, W j of the first i blocks.

def Cslib.Circuits.Arithmetic.wordRestAt (W : ℕ → ℤ) (D : ℕ → ℕ) (i : ℕ) : Option ℕ

The comparison of the positive and the negative strings read from the first i blocks.

The word polynomial

def Cslib.Circuits.Arithmetic.wordSeq {d : ℕ} (w : Fin d → ℤ) (j : ℕ) : ℤ

A word w : Fin d → ℤ, extended by zeros to a sequence.

@[simp]

theorem Cslib.Circuits.Arithmetic.wordSeq_val {d : ℕ} (w : Fin d → ℤ) (i : Fin d) : wordSeq w ↑i = w i

def Cslib.Circuits.Arithmetic.WordChoice.digits {d : ℕ} {w : Fin d → ℤ} (x : WordChoice w) (j : ℕ) : ℕ

The labels of a choice, extended by zeros to a sequence.

theorem Cslib.Circuits.Arithmetic.WordChoice.digits_lt {d : ℕ} {w : Fin d → ℤ} (x : WordChoice w) (j : ℕ) : x.digits j < 2 ^ (wordSeq w j).natAbs

@[simp]

theorem Cslib.Circuits.Arithmetic.WordChoice.digits_val {d : ℕ} {w : Fin d → ℤ} (x : WordChoice w) (i : Fin d) : x.digits ↑i = ↑(x i)

def Cslib.Circuits.Arithmetic.wordRest {d : ℕ} (w : Fin d → ℤ) (x : WordChoice w) : Option ℕ

The comparison of the positive string σ(m⁺) and the negative string σ(m⁻) of the monomial m chosen by x: σ(m⁺) concatenates the labels of the positive blocks in order, and σ(m⁻) those of the negative blocks. It is some τ when the shorter string is a prefix of the longer one, with rest τ, and none otherwise.

noncomputable def Cslib.Circuits.Arithmetic.wordPoly {d : ℕ} (K : Type u_1) [CommSemiring K] (w : Fin d → ℤ) (τ : ℕ) : MvPolynomial (WordVar w) K

The word polynomial with sink τ: the sum of the set-multilinear monomials m = ∏ i, x_i of X(w) whose positive string σ(m⁺) and negative string σ(m⁻) are prefix-related with rest τ, so that σ(m⁺) = σ(m⁻) τ when ∑ i, w i ≥ 0 and σ(m⁻) = σ(m⁺) τ otherwise. The word polynomial P_w of LST §2.2 is the sum of these over all τ; fixing the sink is original (see the module docstring).

noncomputable def Cslib.Circuits.Arithmetic.wordMono {d : ℕ} {w : Fin d → ℤ} (x : WordChoice w) : WordVar w →₀ ℕ

The exponent vector of the monomial chosen by x.

theorem Cslib.Circuits.Arithmetic.wordMono_apply {d : ℕ} {w : Fin d → ℤ} (x : WordChoice w) (j : Fin d) (β : Fin (2 ^ (w j).natAbs)) : (wordMono x) ⟨j, β⟩ = if x j = β then 1 else 0

theorem Cslib.Circuits.Arithmetic.wordMono_injective {d : ℕ} {w : Fin d → ℤ} : Function.Injective wordMono

theorem Cslib.Circuits.Arithmetic.prod_X_eq_monomial {d : ℕ} {w : Fin d → ℤ} {K : Type u_1} [CommSemiring K] (x : WordChoice w) : ∏ i : Fin d, MvPolynomial.X ⟨i, x i⟩ = (MvPolynomial.monomial (wordMono x)) 1

theorem Cslib.Circuits.Arithmetic.coeff_wordPoly {d : ℕ} {w : Fin d → ℤ} {K : Type u_1} [CommSemiring K] (τ : ℕ) (y : WordChoice w) : (wordPoly K w τ).coeff (wordMono y) = if wordRest w y = some τ then 1 else 0

The coefficients of the word polynomial: a set-multilinear monomial has coefficient 1 when its strings are prefix-related with rest τ, and 0 otherwise.

theorem Cslib.Circuits.Arithmetic.isSetMultilinear_prod_X {d : ℕ} {w : Fin d → ℤ} {K : Type u_1} [CommSemiring K] (x : WordChoice w) (s : Finset (Fin d)) : MvPolynomial.IsSetMultilinear Sigma.fst s (∏ i ∈ s, MvPolynomial.X ⟨i, x i⟩)

A product of one variable from each block of s is set-multilinear on s.

theorem Cslib.Circuits.Arithmetic.isSetMultilinear_wordPoly {d : ℕ} {w : Fin d → ℤ} {K : Type u_1} [CommSemiring K] (τ : ℕ) : MvPolynomial.IsSetMultilinear Sigma.fst Finset.univ (wordPoly K w τ)

The word polynomial is set-multilinear on all blocks of X(w).

noncomputable def Cslib.Circuits.Arithmetic.wordPolyAllSinks {d : ℕ} (K : Type u_2) [CommSemiring K] (w : Fin d → ℤ) : MvPolynomial (WordVar w) K

LST's word polynomial P_w (LST §2.2): the sum of the set-multilinear monomials of X(w) whose positive and negative strings are prefix-related.

theorem Cslib.Circuits.Arithmetic.wordRest_lt {d : ℕ} {w : Fin d → ℤ} {x : WordChoice w} {τ : ℕ} (h : wordRest w x = some τ) : τ < 2 ^ (∑ i : Fin d, w i).natAbs

The rest of a monomial's strings has length |∑ i, w i|.

theorem Cslib.Circuits.Arithmetic.sum_wordPoly {d : ℕ} {w : Fin d → ℤ} {K : Type u_1} [CommSemiring K] : ∑ τ ∈ Finset.range (2 ^ (∑ i : Fin d, w i).natAbs), wordPoly K w τ = wordPolyAllSinks K w

LST's word polynomial P_w is the sum of the word polynomials with the sinks of length |∑ i, w i|.

Full rank

theorem Cslib.Circuits.Arithmetic.rank_relMatrix_wordPoly {d : ℕ} {w : Fin d → ℤ} {K : Type u_2} [Field K] {τ : ℕ} (hτ : τ < 2 ^ (∑ i : Fin d, w i).natAbs) : (relMatrix Sigma.fst (wordPos w) (wordNeg w) (wordPoly K w τ)).rank = min (Fintype.card (MvPolynomial.BlockChoice Sigma.fst (wordPos w))) (Fintype.card (MvPolynomial.BlockChoice Sigma.fst (wordNeg w)))

Full rank (LST §2.2): the relative-rank matrix of the word polynomial with sink τ has rank equal to the smaller of its numbers of rows and columns, for every sink τ of the right length |∑ i, w i|.

theorem Cslib.Circuits.Arithmetic.relRank_wordPoly {d : ℕ} {w : Fin d → ℤ} {K : Type u_2} [Field K] {τ : ℕ} (hτ : τ < 2 ^ (∑ i : Fin d, w i).natAbs) : relRank Sigma.fst (wordPos w) (wordNeg w) (wordPoly K w τ) = 2 ^ (-↑(∑ i : Fin d, w i).natAbs / 2)

Relative rank of the word polynomial (LST §2.2): it is 2 ^ (-|∑ i, w i| / 2), the largest value the imbalance bound allows.

Iterated matrix multiplication

noncomputable def Cslib.Circuits.Arithmetic.immMatrix (K : Type u_2) [CommSemiring K] (n d : ℕ) (i : Fin d) : Matrix (Fin n) (Fin n) (MvPolynomial (Fin d × Fin n × Fin n) K)

The generic matrix X_i of iterated matrix multiplication: its entry (a, c) is the variable (i, a, c).

noncomputable def Cslib.Circuits.Arithmetic.imm (K : Type u_2) [CommSemiring K] (n d : ℕ) [NeZero n] : MvPolynomial (Fin d × Fin n × Fin n) K

Iterated matrix multiplication IMM_{n,d}: the entry (0, 0) of the product X_0 X_1 ⋯ X_{d-1} of d generic n × n matrices on disjoint sets of variables. Its variables (i, a, c) are split into the d blocks i, the entries of X_i.

theorem Cslib.Circuits.Arithmetic.projection_imm {d : ℕ} {K : Type u_1} [CommSemiring K] {σ : Type u_2} {n : ℕ} [NeZero n] (ρ : Fin d × Fin n × Fin n → σ ⊕ K) : (projection ρ) (imm K n d) = ∑ p : Fin (d + 1) → Fin n, if p 0 = 0 ∧ p (Fin.last d) = 0 then ∏ i : Fin d, Sum.elim MvPolynomial.X (fun (a : K) => MvPolynomial.C a) (ρ (i, p i.castSucc, p i.succ)) else 0

A projection of IMM_{n,d} is a sum over the paths 0 = p 0, p 1, …, p d = 0 of products of the substituted entries.

Word polynomials are projections of IMM

def Cslib.Circuits.Arithmetic.wordTarget {d : ℕ} (τ : ℕ) (i : Fin d) (c : ℕ) : ℕ

The state at layer i + 1 that the column c of matrix i stands for: the sink τ at the last layer, and c itself elsewhere.

noncomputable def Cslib.Circuits.Arithmetic.wordSubst {d : ℕ} (w : Fin d → ℤ) (τ n : ℕ) (K : Type u_2) [Zero K] : Fin d × Fin n × Fin n → WordVar w ⊕ K

The substitution of Lemma 8: the variable (i, a, c) of IMM_{n,d} becomes the variable ⟨i, β⟩ of block i of X(w) when the branching program for the word polynomial with sink τ has an edge labelled β from state a at layer i to state wordTarget τ i c at layer i + 1, and 0 when it has no such edge.

theorem Cslib.Circuits.Arithmetic.wordSubst_eq_inl {d : ℕ} {w : Fin d → ℤ} {K : Type u_1} [CommSemiring K] {τ n : ℕ} {i : Fin d} {a c : Fin n} {v : WordVar w} (h : wordSubst w τ n K (i, a, c) = Sum.inl v) : v.fst = i

The substitution of Lemma 8 respects the blocks: a variable of block i of IMM_{n,d} becomes a variable of block i of X(w).

theorem Cslib.Circuits.Arithmetic.wordSubst_eq_inr {d : ℕ} {w : Fin d → ℤ} {K : Type u_1} [CommSemiring K] {τ n : ℕ} {i : Fin d} {a c : Fin n} {k : K} (h : wordSubst w τ n K (i, a, c) = Sum.inr k) : k = 0

The substitution of Lemma 8 substitutes no constant but 0.

theorem Cslib.Circuits.Arithmetic.projection_wordSubst_imm {d : ℕ} {w : Fin d → ℤ} {K : Type u_1} [CommSemiring K] {n : ℕ} [NeZero n] {b : ℕ} (hw : IsUnbiased w b) (hn : 2 ^ b ≤ n) {τ : ℕ} (hτ : τ < 2 ^ (∑ i : Fin d, w i).natAbs) : (projection (wordSubst w τ n K)) (imm K n d) = wordPoly K w τ

LST Lemma 8, fixed-sink form (the substitution): substituting wordSubst into IMM_{n,d} gives the word polynomial with sink τ, for a b-unbiased word and 2 ^ b ≤ n.

theorem Cslib.Circuits.Arithmetic.isProjection_wordPoly_imm {d : ℕ} {w : Fin d → ℤ} {K : Type u_1} [CommSemiring K] {n : ℕ} [NeZero n] {b : ℕ} (hw : IsUnbiased w b) (hn : 2 ^ b ≤ n) {τ : ℕ} (hτ : τ < 2 ^ (∑ i : Fin d, w i).natAbs) : IsProjection (wordPoly K w τ) (imm K n d)

LST Lemma 8, fixed-sink form: the word polynomial with sink τ of a b-unbiased word is a projection of IMM_{n,d} for every n ≥ 2 ^ b. The substitution wordSubst maps each variable of block i of IMM_{n,d} to a variable of block i of X(w) or to 0 (wordSubst_eq_inl, wordSubst_eq_inr).