Squarefree-layer lower bounds for monotone polynomial circuits

The degree-k squarefree layer in n variables has exactly choose n k monomials. Its support is disjoint from the individual variable generators when k ≥ 2, and it has no constant monomial. The arbitrary-depth support fusion theorem therefore yields a binomial multiplication lower bound for circuits whose multiplication inputs have bounded support width.

At the middle layer this becomes a central-binomial bound and, using Mathlib's explicit estimate, an exponential size-width tradeoff.

@[reducible, inline]

abbrev Algebraic.Fusion.Arithmetic.MonotonePolynomial.Layer.Index (n k : ℕ) : Type

The type of k-subsets of an n-element variable set.

Equations

• Algebraic.Fusion.Arithmetic.MonotonePolynomial.Layer.Index n k = ↥(Finset.powersetCard k Finset.univ)

theorem Algebraic.Fusion.Arithmetic.MonotonePolynomial.Layer.card_index (n k : ℕ) : Fintype.card (Index n k) = n.choose k

noncomputable def Algebraic.Fusion.Arithmetic.MonotonePolynomial.Layer.exponent {n k : ℕ} (set : Index n k) : Fin n →₀ ℕ

Squarefree exponent vector associated to one layer element.

Equations

• Algebraic.Fusion.Arithmetic.MonotonePolynomial.Layer.exponent set = Finsupp.indicator ↑set fun (x : Fin n) (x_1 : x ∈ ↑set) => 1

@[simp]

theorem Algebraic.Fusion.Arithmetic.MonotonePolynomial.Layer.exponent_apply {n k : ℕ} (set : Index n k) (coordinate : Fin n) : (exponent set) coordinate = if coordinate ∈ ↑set then 1 else 0

theorem Algebraic.Fusion.Arithmetic.MonotonePolynomial.Layer.exponent_sum {n k : ℕ} (set : Index n k) : ((exponent set).sum fun (x : Fin n) (multiplicity : ℕ) => multiplicity) = k

Total degree of a layer exponent.

theorem Algebraic.Fusion.Arithmetic.MonotonePolynomial.Layer.exponent_injective {n k : ℕ} : Function.Injective exponent

Distinct subsets give distinct squarefree exponent vectors.

noncomputable def Algebraic.Fusion.Arithmetic.MonotonePolynomial.Layer.exponentEmbedding (n k : ℕ) : Index n k ↪ Fin n →₀ ℕ

Embedding of the layer into exponent vectors.

Equations

• Algebraic.Fusion.Arithmetic.MonotonePolynomial.Layer.exponentEmbedding n k = { toFun := Algebraic.Fusion.Arithmetic.MonotonePolynomial.Layer.exponent, inj' := ⋯ }

noncomputable def Algebraic.Fusion.Arithmetic.MonotonePolynomial.Layer.exponents (n k : ℕ) : Finset (Fin n →₀ ℕ)

Finite set of all squarefree degree-k exponent vectors.

Equations

• Algebraic.Fusion.Arithmetic.MonotonePolynomial.Layer.exponents n k = Finset.map (Algebraic.Fusion.Arithmetic.MonotonePolynomial.Layer.exponentEmbedding n k) Finset.univ

@[simp]

theorem Algebraic.Fusion.Arithmetic.MonotonePolynomial.Layer.card_exponents (n k : ℕ) : (exponents n k).card = n.choose k

noncomputable def Algebraic.Fusion.Arithmetic.MonotonePolynomial.Layer.monomial {n k : ℕ} (set : Index n k) : MvPolynomial (Fin n) ℕ

One monomial in the squarefree layer.

Equations

• Algebraic.Fusion.Arithmetic.MonotonePolynomial.Layer.monomial set = (MvPolynomial.monomial (Algebraic.Fusion.Arithmetic.MonotonePolynomial.Layer.exponent set)) 1

noncomputable def Algebraic.Fusion.Arithmetic.MonotonePolynomial.Layer.polynomial (n k : ℕ) : MvPolynomial (Fin n) ℕ

Sum of all squarefree monomials of degree k in n variables.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.Fusion.Arithmetic.MonotonePolynomial.Layer.support_finset_sum {σ : Type u_1} {ι : Type u_2} [DecidableEq σ] (indices : Finset ι) (term : ι → MvPolynomial σ ℕ) : (∑ index ∈ indices, term index).support = indices.biUnion fun (index : ι) => (term index).support

Exact support of a finite sum over natural coefficients.

theorem Algebraic.Fusion.Arithmetic.MonotonePolynomial.Layer.support_polynomial (n k : ℕ) : (polynomial n k).support = exponents n k

The squarefree-layer polynomial has exactly the expected exponent support.

@[simp]

theorem Algebraic.Fusion.Arithmetic.MonotonePolynomial.Layer.card_support_polynomial (n k : ℕ) : (polynomial n k).support.card = n.choose k

theorem Algebraic.Fusion.Arithmetic.MonotonePolynomial.Layer.zero_not_mem_support_polynomial {k n : ℕ} (positive : 0 < k) : 0 ∉ (polynomial n k).support

A positive-degree squarefree layer has no constant monomial.

theorem Algebraic.Fusion.Arithmetic.MonotonePolynomial.Layer.support_polynomial_disjoint_X {k n : ℕ} (two_le : 2 ≤ k) (coordinate : Fin n) : Disjoint (polynomial n k).support (MvPolynomial.X coordinate).support

When k ≥ 2, the target layer support is disjoint from each individual variable support.

@[reducible, inline]

noncomputable abbrev Algebraic.Fusion.Arithmetic.MonotonePolynomial.Layer.problem (n k : ℕ) : Problem (MvPolynomial (Fin n) ℕ)

Construct the squarefree layer from the individual variables.

Equations

• Algebraic.Fusion.Arithmetic.MonotonePolynomial.Layer.problem n k = { inputCount := n, inputs := MvPolynomial.X, target := Algebraic.Fusion.Arithmetic.MonotonePolynomial.Layer.polynomial n k }

theorem Algebraic.Fusion.Arithmetic.MonotonePolynomial.Layer.multiplication_lowerBound {k n : ℕ} (two_le : 2 ≤ k) (width : ℕ) (positive : 0 < width) (circuit : Circuit (Arithmetic.signature ℕ) n 1) (constructs : (problem n k).Constructs circuit (Arithmetic.interpretation ⇑MvPolynomial.C)) (widthBound : MultiplicationSupportWidthAtMost circuit MvPolynomial.X width) : n.choose k ⌈/⌉ (width * width) ≤ circuit.cost Arithmetic.multiplicationCost

A bounded multiplication-input support width gives the binomial lower bound for the squarefree layer, at arbitrary circuit depth.

theorem Algebraic.Fusion.Arithmetic.MonotonePolynomial.Layer.centralBinom_multiplication_lowerBound (n : ℕ) (two_le : 2 ≤ n) (width : ℕ) (positive : 0 < width) (circuit : Circuit (Arithmetic.signature ℕ) (2 * n) 1) (constructs : (problem (2 * n) n).Constructs circuit (Arithmetic.interpretation ⇑MvPolynomial.C)) (widthBound : MultiplicationSupportWidthAtMost circuit MvPolynomial.X width) : n.centralBinom ⌈/⌉ (width * width) ≤ circuit.cost Arithmetic.multiplicationCost

The middle squarefree layer gives a central-binomial lower bound.

theorem Algebraic.Fusion.Arithmetic.MonotonePolynomial.Layer.four_pow_lt_mul_width_sq_cost (n : ℕ) (n_big : 4 ≤ n) (width : ℕ) (positive : 0 < width) (circuit : Circuit (Arithmetic.signature ℕ) (2 * n) 1) (constructs : (problem (2 * n) n).Constructs circuit (Arithmetic.interpretation ⇑MvPolynomial.C)) (widthBound : MultiplicationSupportWidthAtMost circuit MvPolynomial.X width) : 4 ^ n < n * (width * width * circuit.cost Arithmetic.multiplicationCost)

Explicit exponential size-width tradeoff for the middle squarefree layer.