Quadratic forms over every field

The counting proof of MultiOutput.Quadratic needs a finite field. For circuits with polynomial gates the Taylor cut lemma gives the same rank-cut bound over every field: the Hessian of the quadratic form ∑ᵢ ∑ⱼ M i j Xᵢ Xⱼ is M + Mᵀ at every point (hessian_quadFormPolynomial), so by the Hessian consequence (Taylor.blockRank_hessian_le) every split S of a circuit formally computing the form is crossed by at least rank (M + Mᵀ)[X_S, X_T] signals (blockRank_add_transpose_le_of_formallyComputes). The graph-ordering argument of MultiOutput.Quadratic then applies unchanged.

The bound (eventually_lt_size_of_formal_quadForm). For every ε > 0 and all large N, over every field, every circuit with polynomial gates of fan-in at most two, of any degree and with any coefficients, formally computing the quadratic form of an N × N matrix M with M + Mᵀ totally regular has more than (1 + 1/(4 κ_E) - ε) N ≥ (25/9 - ε) N gates. Over an infinite field the same holds for circuits computing the quadratic function (eventually_lt_size_of_quadForm_of_infinite). For an explicit family, the Hankel Cauchy matrix 1 / (i + j + 2) and its symmetrization are totally regular over every field of characteristic zero (totallyRegular_hankelCauchyCharZero_add_transpose), so its quadratic form needs more than (25/9 - ε) N polynomial gates over the rationals, the reals, or the complex numbers (eventually_lt_size_hankelCauchyCharZero).

The quadratic form as a polynomial

theorem Algebraic.Cutwidth.MultiOutput.quadForm_eq_eval {N : ℕ} {K : Type u_1} [CommRing K] (M : Matrix (Fin N) (Fin N) K) (x : Fin N → K) : quadForm M x = (MvPolynomial.eval x) (quadFormPolynomial M)

The polynomial quadratic form evaluates to the quadratic form.

theorem Algebraic.Cutwidth.MultiOutput.hessian_quadFormPolynomial {N : ℕ} {K : Type u_1} [CommRing K] (M : Matrix (Fin N) (Fin N) K) (a : Fin N → K) : Taylor.hessian (quadFormPolynomial M) a = M + M.transpose

The Hessian of a quadratic form is M + Mᵀ at every point.

The rank-cut bound over every field

theorem Algebraic.Cutwidth.MultiOutput.blockRank_add_transpose_le_of_formallyComputes {σ : Signature} {N : ℕ} {K : Type u_1} [Field K] (P : (op : σ.Op) → MvPolynomial (Fin (σ.Arity op)) K) {c : Circuit σ N 1} {M : Matrix (Fin N) (Fin N) K} (hc : Taylor.FormallyComputes P c fun (x : Fin 1) => quadFormPolynomial M) (S : Finset (Wire N c.size)) : blockRank (M + M.transpose) (SingleCut.inputsIn S) (SingleCut.inputsIn S)ᶜ ≤ (SingleCut.forward c.program S).card + (SingleCut.backward c.program S).card

The rank-cut bound for quadratic forms over every field. If a single-output circuit with polynomial gates over a field formally computes the quadratic form of M, every set S of its wires has rank (M + Mᵀ)[X_S, X_T] ≤ |forward S| + |backward S|.

theorem Algebraic.Cutwidth.MultiOutput.half_le_of_formal_quadForm {σ : Signature} {N : ℕ} {A η C : ℝ} (hAη : 0 ≤ A + η) (order : Multigraph.OrderingBound A η C) {K : Type u_1} [Field K] (P : (op : σ.Op) → MvPolynomial (Fin (σ.Arity op)) K) {c : Circuit σ N 1} (hfan : c.FanInAtMost 2) {M : Matrix (Fin N) (Fin N) K} (hM : TotallyRegular (M + M.transpose)) (hc : Taylor.FormallyComputes P c fun (x : Fin 1) => quadFormPolynomial M) : ↑(N / 2) ≤ (A + η) * max (↑c.size - ↑N) 0 + 3 * Real.logb 2 (↑N + 3 * ↑c.size) + C

The finite bound for quadratic forms over every field. If a fan-in-two circuit with polynomial gates over a field formally computes the quadratic form of M, with M + Mᵀ totally regular, then ⌊N/2⌋ ≤ (A + η) (s - N)⁺ + 3 log₂ (N + 3 s) + C for its size s.

Asymptotic bounds

theorem Algebraic.Cutwidth.MultiOutput.eventually_lt_size_of_formal_quadForm {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (K : Type u) [inst : Field K] (M : Matrix (Fin N) (Fin N) K), TotallyRegular (M + M.transpose) → ∀ (σ : Signature) (P : (op : σ.Op) → MvPolynomial (Fin (σ.Arity op)) K) (c : Circuit σ N 1), c.FanInAtMost 2 → (Taylor.FormallyComputes P c fun (x : Fin 1) => quadFormPolynomial M) → (1 + 1 / (4 * Gaussian.frontierCoefficient) - ε) * ↑N < ↑c.size

Quadratic forms need (1 + 1/(4 κ_E) - ε) N polynomial gates over every field. For every ε > 0 and all large N, every circuit with polynomial gates of fan-in at most two over any field formally computing the quadratic form of an N × N matrix M with M + Mᵀ totally regular has more than (1 + 1/(4 κ_E) - ε) N ≈ (2.7812 - ε) N gates.

theorem Algebraic.Cutwidth.MultiOutput.eventually_lt_size_of_formal_quadForm_twentyFive_div_nine {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (K : Type u) [inst : Field K] (M : Matrix (Fin N) (Fin N) K), TotallyRegular (M + M.transpose) → ∀ (σ : Signature) (P : (op : σ.Op) → MvPolynomial (Fin (σ.Arity op)) K) (c : Circuit σ N 1), c.FanInAtMost 2 → (Taylor.FormallyComputes P c fun (x : Fin 1) => quadFormPolynomial M) → (25 / 9 - ε) * ↑N < ↑c.size

Quadratic forms need (25/9 - ε) N polynomial gates over every field.

theorem Algebraic.Cutwidth.MultiOutput.eventually_lt_size_of_quadForm_of_infinite {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (K : Type u) [inst : Field K] [Infinite K] (M : Matrix (Fin N) (Fin N) K), TotallyRegular (M + M.transpose) → ∀ (σ : Signature) (I : Interpretation σ K), Polynomial.IsPolynomial I → ∀ (c : Circuit σ N 1), c.FanInAtMost 2 → (c.Computes I fun (x : Fin N → K) (x_1 : Fin 1) => quadForm M x) → (25 / 9 - ε) * ↑N < ↑c.size

Quadratic functions over an infinite field. For every ε > 0 and all large N, over every infinite field, every circuit whose operations are polynomial functions of at most two arguments and which computes the quadratic form of an N × N matrix M with M + Mᵀ totally regular has more than (25/9 - ε) N gates.

An explicit family in characteristic zero

theorem Algebraic.Cutwidth.MultiOutput.totallyRegular_hankelCauchyCharZero_add_transpose (F : Type u_1) [Field F] [CharZero F] (N : ℕ) : TotallyRegular (hankelCauchyCharZero F N + (hankelCauchyCharZero F N).transpose)

The Hankel Cauchy matrix in characteristic zero. Over a field of characteristic zero, (1 / (i + j + 2)) is the Cauchy matrix with nodes i + 1 and -(j + 1) and is symmetric, so it and its symmetrization are totally regular.

theorem Algebraic.Cutwidth.MultiOutput.eventually_lt_size_hankelCauchyCharZero {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (F : Type u) [inst : Field F] [CharZero F] (σ : Signature) (P : (op : σ.Op) → MvPolynomial (Fin (σ.Arity op)) F) (c : Circuit σ N 1), c.FanInAtMost 2 → (Taylor.FormallyComputes P c fun (x : Fin 1) => quadFormPolynomial (hankelCauchyCharZero F N)) → (25 / 9 - ε) * ↑N < ↑c.size

The explicit family needs (25/9 - ε) N polynomial gates in characteristic zero. For every ε > 0 and all large N, over every field of characteristic zero, every circuit with polynomial gates of fan-in at most two formally computing the quadratic form ∑ᵢ ∑ⱼ xᵢ xⱼ / (i + j + 2) has more than (25/9 - ε) N gates.