Unconditional lower bounds for linear maps

Combining the lower bound for linear maps (Frontier.lowerBound_linear) with the layout bound for subcubic graphs (Frontier.layoutBound_gaussian) gives, with L = 1 + π / (3 arccos ((1 + 2√2)/4)) ≈ 4.5625:

• Finite fields, any basis (Frontier.linear_finite_gaussian): every circuit of fan-in two computing a totally regular map F^N → F^N has more than (L - ε) N inner gates, uniformly in the finite field F.
• Infinite fields, polynomial operations (Frontier.linear_polynomial_gaussian): the same, for operations of fan-in two given by polynomials of any degree with any coefficients.
• Arithmetic circuits (Frontier.arith_cauchy_gaussian): over every field of characteristic zero, in particular over ℚ, ℝ, and ℂ, every circuit of additions, multiplications, and constants computing the Cauchy map x ↦ (∑_j x_j / (i - N - j))_i uses more than (L - ε) N additions and multiplications. Constants are free.
• Prime fields (Frontier.cauchyZMod_gaussian): the same Cauchy matrices over ZMod q, for every prime q ≥ 2 N, need more than (L - ε) N gates in every basis of fan-in two.

theorem Complexity.Frontier.linear_finite_gaussian {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (F : Type u) [inst : Field F] [Finite F] (σ : Cslib.Circuits.Signature) (I : Cslib.Circuits.Interpretation σ F) (M : Matrix (Fin N) (Fin N) F) (c : Cslib.Circuits.Circuit σ N N), TotallyRegular M → 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.innerSize

Totally regular maps over finite fields, for every basis of fan-in two.

theorem Complexity.Frontier.linear_polynomial_gaussian {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (F : Type u) [inst : Field F] [Infinite F] (σ : Cslib.Circuits.Signature) (I : Cslib.Circuits.Interpretation σ F), IsPolynomial I → ∀ (M : Matrix (Fin N) (Fin N) F) (c : Cslib.Circuits.Circuit σ N N), TotallyRegular M → 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.innerSize

Totally regular maps over infinite fields, for every basis of fan-in two whose operations are polynomials.

theorem Complexity.Frontier.fanInAtMost_two_arith {F : Type u} {n s : ℕ} (p : Cslib.Circuits.Program (arithSignature F) n s) : p.FanInAtMost 2

Arithmetic circuits have fan-in at most two.

theorem Complexity.Frontier.arith_cauchy_gaussian {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (F : Type u) [inst : Field F] [CharZero F] (c : Cslib.Circuits.Circuit (arithSignature F) N N), (c.Computes (arithInterpretation F) fun (x : Fin N → F) => (cauchyNat F N).mulVec x) → (1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4)) - ε) * ↑N < ↑c.innerSize

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

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

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

theorem Complexity.Frontier.linear_finite_fanInThree {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (F : Type u) [inst : Field F] [Finite F] (σ : Cslib.Circuits.Signature) (I : Cslib.Circuits.Interpretation σ F) (M : Matrix (Fin N) (Fin N) F) (c : Cslib.Circuits.Circuit σ N N), TotallyRegular M → c.FanInAtMost 3 → (c.Computes I fun (x : Fin N → F) => M.mulVec x) → (7 / 4 - ε) * ↑N < ↑c.innerSize

Totally regular maps over finite fields also have the ternary 7N/4 - o(N) bound.

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

Every fixed fan-in over finite fields, with the Gaussian degree coefficient.

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

Every fixed fan-in over infinite fields, for polynomial operations.

theorem Complexity.Frontier.linear_polynomial_fanInThree {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (F : Type u) [inst : Field F] [Infinite F] (σ : Cslib.Circuits.Signature) (I : Cslib.Circuits.Interpretation σ F), IsPolynomial I → ∀ (M : Matrix (Fin N) (Fin N) F) (c : Cslib.Circuits.Circuit σ N N), TotallyRegular M → c.FanInAtMost 3 → (c.Computes I fun (x : Fin N → F) => M.mulVec x) → (7 / 4 - ε) * ↑N < ↑c.innerSize

The ternary bound over infinite fields with polynomial operations.