Waring term counts for a squarefree monomial

A sum of scaled d-th powers of linear forms representing the product of d variables needs at least choose d k terms, for every split k. At degree 2*n, the middle split gives the central binomial coefficient. The field may be any characteristic-zero field.

Restrict the normalized coefficient matrix to squarefree row exponents of degree k and complemented column exponents. Each power term gives rank at most one; the target gives a nonzero scalar identity. The finite-sum endpoint needs no circuit encoding. The circuit endpoint uses native circuits adding dictionary terms, with free additions and wiring. A reused term gate is charged once. These are bounds for this restricted representation model, not for unrestricted arithmetic circuits. All computation premises are formal polynomial equalities.

Main definitions

• Cslib.Circuits.Waring.Term, Cslib.Circuits.Waring.Term.polynomial: scaled powers of homogeneous linear forms, used as the dictionary of SumOfTerms.signature.

Main results

• Cslib.Circuits.Waring.choose_le_card, Cslib.Circuits.Waring.centralBinom_le_card: lower bounds for ordinary finite sums.
• Cslib.Circuits.Waring.choose_le_cost, Cslib.Circuits.Waring.centralBinom_le_cost: lower bounds for any selected output of a zero-input sum-of-terms circuit.

References

• Ported from LowerBound/Fusion/SumOfTerms/Waring.lean, its Rectangular.lean extension, and Applications/Waring.lean in S. Schlesinger, Algebraic circuit formalizations in Complexitylib.
• J. M. Landsberg and Z. Teitler, On the ranks and border ranks of symmetric tensors, equation (1) and Remark 6.5. We use a squarefree restriction of the catalecticant argument; this does not identify the exact Waring rank or formalize the paper's border-rank and singularity bounds.

theorem Cslib.Circuits.Waring.choose_le_card {K : Type u_1} [Field K] [CharZero K] {d : ℕ} {ι : Type u_2} (k : ℕ) (indices : Finset ι) (scale : ι → K) (coefficients : ι → Fin d → K) (hcompute : ∑ i ∈ indices, MvPolynomial.C (scale i) * (∑ j : Fin d, MvPolynomial.C (coefficients i j) * MvPolynomial.X j) ^ d = ∏ j : Fin d, MvPolynomial.X j) : d.choose k ≤ indices.card

Every split of the degree gives a term-count bound for an ordinary sum of scaled powers. The premise is equality of formal polynomials.

theorem Cslib.Circuits.Waring.centralBinom_le_card {K : Type u_1} [Field K] [CharZero K] {ι : Type u_2} (n : ℕ) (indices : Finset ι) (scale : ι → K) (coefficients : ι → Fin (2 * n) → K) (hcompute : ∑ i ∈ indices, MvPolynomial.C (scale i) * (∑ j : Fin (2 * n), MvPolynomial.C (coefficients i j) * MvPolynomial.X j) ^ (2 * n) = ∏ j : Fin (2 * n), MvPolynomial.X j) : n.centralBinom ≤ indices.card

The middle split gives a central-binomial lower bound for a sum of even-degree powers.

theorem Cslib.Circuits.Waring.choose_le_cost {K : Type u_1} [Field K] [CharZero K] {d m : ℕ} (c : Circuit (SumOfTerms.signature (Term K d)) 0 m) (k : ℕ) (j : Fin m) (hcompute : c.eval (SumOfTerms.interpretation Term.polynomial) Fin.elim0 j = ∏ i : Fin d, MvPolynomial.X i) : d.choose k ≤ c.program.cost SumOfTerms.termCost

A sum-of-terms circuit for the squarefree monomial needs at least choose d k term gates. Additions and wiring are free, and shared gates are charged once.

theorem Cslib.Circuits.Waring.centralBinom_le_cost {K : Type u_1} [Field K] [CharZero K] {m : ℕ} (n : ℕ) (c : Circuit (SumOfTerms.signature (Term K (2 * n))) 0 m) (j : Fin m) (hcompute : c.eval (SumOfTerms.interpretation Term.polynomial) Fin.elim0 j = ∏ i : Fin (2 * n), MvPolynomial.X i) : n.centralBinom ≤ c.program.cost SumOfTerms.termCost

The central-binomial term count for any selected output of an even-degree Waring circuit.

theorem Cslib.Circuits.Waring.four_pow_lt_mul_cost {K : Type u_1} [Field K] [CharZero K] {m n : ℕ} (hn : 4 ≤ n) (c : Circuit (SumOfTerms.signature (Term K (2 * n))) 0 m) (j : Fin m) (hcompute : c.eval (SumOfTerms.interpretation Term.polynomial) Fin.elim0 j = ∏ i : Fin (2 * n), MvPolynomial.X i) : 4 ^ n < n * c.program.cost SumOfTerms.termCost

An exponential lower bound on Waring term count, using the central-binomial estimate.