Polynomial gates computing totally regular linear maps

Every fan-in-two circuit of polynomial gates computing a totally regular linear map requires more than (L-ε)n gates eventually, with L ≈ 4.5625. Degrees, coefficients, depth, and fanout are unrestricted. The threshold is uniform over fields, matrices, signatures, and gate polynomials.

Over infinite fields, formal differentiation at zero supplies a local linear realization on the original wires. Over finite fields, the earlier cardinality argument supplies the same cut-rank bound, even for arbitrary gate functions. The common graph-layout theorem then applies without changing the gate count. Coefficients are part of a polynomial gate and incur no separate cost. Explicit nullary gate occurrences are included in Circuit.size.

The totally-regular-map method is due to Valiant; the classical indegree-two superconcentrator bound of Lev and Valiant gives coefficient four. This transfer uses the library's stronger Gaussian ordering theorem. No historical-priority claim for the resulting arithmetic coefficient is made here.

theorem Algebraic.Cutwidth.MultiOutput.Polynomial.blockRank_add_blockRank_le {σ : Signature} {F : Type u_1} [Field F] {I : Interpretation σ F} (polynomial : IsPolynomial I) {n m : ℕ} (c : Circuit σ n m) {M : Matrix (Fin m) (Fin n) F} (computes : c.Computes I fun (x : Fin n → F) => M.mulVec x) (S : Finset (Wire n c.size)) : blockRank M (outputsIn c.outputs S)ᶜ (SingleCut.inputsIn S) + blockRank M (outputsIn c.outputs S) (SingleCut.inputsIn S)ᶜ ≤ (SingleCut.forward c.program S).card + (SingleCut.backward c.program S).card

Polynomial circuits obey the rank bound at every wire cut over any field.

theorem Algebraic.Cutwidth.MultiOutput.Polynomial.sub_one_le_of_totallyRegular {σ : Signature} {F : Type u_1} [Field F] {A η C : ℝ} (hAη : 0 ≤ A + η) (order : Multigraph.OrderingBound A η C) {I : Interpretation σ F} (polynomial : IsPolynomial I) {n : ℕ} (c : Circuit σ n n) (fan : c.FanInAtMost 2) {M : Matrix (Fin n) (Fin n) F} (regular : TotallyRegular M) (computes : c.Computes I fun (x : Fin n → F) => M.mulVec x) : ↑n - 1 ≤ (A + η) * max (↑c.size - ↑n) 0 + 3 * Real.logb 2 (↑n + 3 * ↑c.size) + C

The finite polynomial-gate lower bound, with the original circuit's gate count.

theorem Algebraic.Cutwidth.MultiOutput.Polynomial.eventually_lt_size_of_totallyRegular_of_orderingBound {A : ℝ} (hA : 0 < A) (order : ∀ (η : ℝ), 0 < η → ∃ (C : ℝ), Multigraph.OrderingBound A η C) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (F : Type u) [inst : Field F] (M : Matrix (Fin n) (Fin n) F), TotallyRegular M → ∀ (σ : Signature) (I : Interpretation σ F), IsPolynomial I → ∀ (c : Circuit σ n n), c.FanInAtMost 2 → (c.Computes I fun (x : Fin n → F) => M.mulVec x) → (1 + 1 / A - ε) * ↑n < ↑c.size

Any ordering coefficient transfers uniformly to polynomial circuits over all fields.

theorem Algebraic.Cutwidth.MultiOutput.Polynomial.eventually_lt_size_of_totallyRegular {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (F : Type u) [inst : Field F] (M : Matrix (Fin n) (Fin n) F), TotallyRegular M → ∀ (σ : Signature) (I : Interpretation σ F), IsPolynomial I → ∀ (c : Circuit σ n n), c.FanInAtMost 2 → (c.Computes I fun (x : Fin n → F) => M.mulVec x) → (1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4)) - ε) * ↑n < ↑c.size

Totally regular linear maps need (4.5625…-ε)n polynomial gates of fan-in at most two.

theorem Algebraic.Cutwidth.MultiOutput.Polynomial.eventually_lt_size {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (F : Type u) [inst : Field F] (M : Matrix (Fin n) (Fin n) F), TotallyRegular M → ∀ (c : Circuit (signature F) n n), c.FanInAtMost 2 → (c.Computes (interpretation F) fun (x : Fin n → F) => M.mulVec x) → (1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4)) - ε) * ↑n < ↑c.size

The full polynomial signature allows arbitrary coefficients and polynomial degrees.