Unconditional frontier lower bounds for linear maps

The frontier lower bound for linear maps (Cslib.Circuits.Frontier.eventually_lt_mul_innerSize_of_isTotallyRegular) is conditional on the layout hypothesis LayoutBound (r + 1) A. Spanning trees prove it with coefficient A = 1 in every degree (Cslib.Circuits.Frontier.layoutBound_one), which removes the hypothesis: for every fan-in r ≥ 2, every ε > 0 and all large N, every circuit of fan-in at most r computing a totally regular map F^N → F^N has s inner gates with

(r - 1) s > (2 - ε) N,

over finite fields with any basis, and over infinite fields with polynomial operations. Gates of arity zero, the constants, are not counted.

For the explicit Cauchy matrices 1 / (i - (N + j)) this gives, for fan-in two:

• Arithmetic circuits: over every field of characteristic zero, in particular over ℚ, ℝ and ℂ, every circuit of additions, multiplications and constants computing x ↦ (∑_j x_j / (i - N - j))_i uses more than (2 - ε) N additions and multiplications.
• Prime fields: the same maps over ZMod q, for every prime q ≥ 2 N, need more than (2 - ε) N inner gates in every basis of fan-in two, uniformly in q.

Main results

• Cslib.Circuits.Frontier.eventually_two_sub_mul_lt_mul_innerSize_of_isTotallyRegular: for circuits with linear capacity; ..._finite and ..._isPolynomial specialize it.
• Cslib.Circuits.Frontier.eventually_two_sub_mul_lt_innerSize_arith_cauchyNat: arithmetic circuits for the Cauchy maps.
• Cslib.Circuits.Frontier.eventually_two_sub_mul_lt_innerSize_cauchyNat_zmod: the Cauchy maps over prime fields.

theorem Cslib.Circuits.Frontier.eventually_two_sub_mul_lt_mul_innerSize_of_isTotallyRegular {r : ℕ} (hr : 2 ≤ r) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (F : Type u) [inst : Field F] (σ : Signature) (I : Interpretation σ F) (M : Matrix (Fin N) (Fin N) F) (c : Circuit σ N N), M.IsTotallyRegular → c.FanInAtMost r → (c.Computes I fun (x : Fin N → F) => M.mulVec x) → c.LinearCapacity I → (2 - ε) * ↑N < (↑r - 1) * ↑c.innerSize

The unconditional frontier lower bound for linear maps. Let r ≥ 2. For every ε > 0 and all large N, every circuit of fan-in at most r with linear capacity, over any field and any basis, that computes x ↦ M x for a totally regular N × N matrix M, has s inner gates with (r - 1) s > (2 - ε) N.

theorem Cslib.Circuits.Frontier.eventually_two_sub_mul_lt_mul_innerSize_of_isTotallyRegular_finite {r : ℕ} (hr : 2 ≤ r) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (F : Type u) [inst : Field F] [Finite F] (σ : Signature) (I : Interpretation σ F) (M : Matrix (Fin N) (Fin N) F) (c : Circuit σ N N), M.IsTotallyRegular → c.FanInAtMost r → (c.Computes I fun (x : Fin N → F) => M.mulVec x) → (2 - ε) * ↑N < (↑r - 1) * ↑c.innerSize

The unconditional frontier lower bound for linear maps over finite fields, for every basis: (r - 1) s > (2 - ε) N for fan-in at most r.

theorem Cslib.Circuits.Frontier.eventually_two_sub_mul_lt_mul_innerSize_of_isTotallyRegular_isPolynomial {r : ℕ} (hr : 2 ≤ r) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (F : Type u) [inst : Field F] [Infinite F] (σ : Signature) (I : Interpretation σ F), I.IsPolynomial → ∀ (M : Matrix (Fin N) (Fin N) F) (c : Circuit σ N N), M.IsTotallyRegular → c.FanInAtMost r → (c.Computes I fun (x : Fin N → F) => M.mulVec x) → (2 - ε) * ↑N < (↑r - 1) * ↑c.innerSize

The unconditional frontier lower bound for linear maps over infinite fields, for every basis of polynomial operations: (r - 1) s > (2 - ε) N for fan-in at most r.

theorem Cslib.Circuits.Frontier.eventually_two_sub_mul_lt_innerSize_arith_cauchyNat {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (F : Type u) [inst : Field F] [CharZero F] (c : Circuit (arithSignature F) N N), (c.Computes (arithInterpretation F) fun (x : Fin N → F) => (Matrix.cauchyNat F N).mulVec x) → (2 - ε) * ↑N < ↑c.innerSize

Arithmetic circuits for the Cauchy maps. Over every field of characteristic zero, every arithmetic circuit computing x ↦ (∑_j x_j / (i - N - j))_i uses more than (2 - ε) N additions and multiplications, for all large N. Constants are free.

theorem Cslib.Circuits.Frontier.eventually_two_sub_mul_lt_innerSize_cauchyNat_zmod {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (q : ℕ) [inst : Fact (Nat.Prime q)], 2 * N ≤ q → ∀ (σ : Signature) (I : Interpretation σ (ZMod q)) (c : Circuit σ N N), c.FanInAtMost 2 → (c.Computes I fun (x : Fin N → ZMod q) => (Matrix.cauchyNat (ZMod q) N).mulVec x) → (2 - ε) * ↑N < ↑c.innerSize

The Cauchy maps over prime fields. For all large N and every prime q ≥ 2 N, every circuit of fan-in at most two, over any basis on ZMod q, computing x ↦ (∑_j x_j / (i - N - j))_i has more than (2 - ε) N inner gates.