The unconditional lower bounds

Combining the main theorem (Frontier.lowerBound_fanInTwo) with the layout bounds of Frontier.Layouts removes the layout hypothesis.

Let S_n ⊆ U^n be K_n-rectangle-free over a finite alphabet with at least two symbols, with log K_n = o(n) and n log |U| - log |S_n| = o(n). Then for every ε > 0 and all large n, every circuit with fan-in at most two deciding S_n, over any basis on U, has more than

• (L - ε) n gates, with L = 1 + π / (3 arccos ((1 + 2√2)/4)) ≈ 4.5625 (lowerBound_gaussian), and in particular
• (4 - ε) n gates (lowerBound_four).

For every fixed fan-in r ≥ 2, Gaussian vertex layouts give (r - 1) s > (1 + 1/A_(r+1) - ε)n (lowerBound_degree), with A_d = 3d/(2d-3) * arccos(2√(d-1)/d)/π < 3/4. The simpler spanning-tree bound gives (r - 1) s > (2 - ε)n (lowerBound_all_fanIn). At fan-in three the Gaussian vertex layout improves this to s > (7/4 - ε)n (lowerBound_fanInThree).

Constant gates are free: the bounds hold for the number of gates of positive arity (Cslib.Circuits.Circuit.innerSize), and so for the size.

theorem Complexity.Frontier.lowerBound_gaussian {U : Type u} [Finite U] [Nontrivial U] (S : (n : ℕ) → Set (Fin n → U)) (K : ℕ → ℕ) (hfree : ∀ᶠ (n : ℕ) in Filter.atTop, RectangleFree (S n) (K n)) (hK : (fun (n : ℕ) => Real.log ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (hdense : (fun (n : ℕ) => ↑n * Real.log ↑(Nat.card U) - Real.log ↑(S n).ncard) =o[Filter.atTop] fun (n : ℕ) => ↑n) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (σ : Cslib.Circuits.Signature) (I : Cslib.Circuits.Interpretation σ U) (Acc : Set U) (c : Cslib.Circuits.Circuit σ n 1), c.FanInAtMost 2 → Decides c I Acc (S n) → (1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4)) - ε) * ↑n < ↑c.innerSize

The (L - ε) n lower bound, with L = 1 + π / (3 arccos ((1 + 2√2)/4)) ≈ 4.5625.

theorem Complexity.Frontier.lowerBound_four {U : Type u} [Finite U] [Nontrivial U] (S : (n : ℕ) → Set (Fin n → U)) (K : ℕ → ℕ) (hfree : ∀ᶠ (n : ℕ) in Filter.atTop, RectangleFree (S n) (K n)) (hK : (fun (n : ℕ) => Real.log ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (hdense : (fun (n : ℕ) => ↑n * Real.log ↑(Nat.card U) - Real.log ↑(S n).ncard) =o[Filter.atTop] fun (n : ℕ) => ↑n) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (σ : Cslib.Circuits.Signature) (I : Cslib.Circuits.Interpretation σ U) (Acc : Set U) (c : Cslib.Circuits.Circuit σ n 1), c.FanInAtMost 2 → Decides c I Acc (S n) → (4 - ε) * ↑n < ↑c.innerSize

The (4 - ε) n lower bound.

theorem Complexity.Frontier.lowerBound_degree {U : Type u} [Finite U] [Nontrivial U] {r : ℕ} (hr : 2 ≤ r) (S : (n : ℕ) → Set (Fin n → U)) (K : ℕ → ℕ) (hfree : ∀ᶠ (n : ℕ) in Filter.atTop, RectangleFree (S n) (K n)) (hK : (fun (n : ℕ) => Real.log ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (hdense : (fun (n : ℕ) => ↑n * Real.log ↑(Nat.card U) - Real.log ↑(S n).ncard) =o[Filter.atTop] fun (n : ℕ) => ↑n) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (σ : Cslib.Circuits.Signature) (I : Cslib.Circuits.Interpretation σ U) (Acc : Set U) (c : Cslib.Circuits.Circuit σ n 1), c.FanInAtMost r → Decides c I Acc (S n) → (1 + 1 / Gaussian.degreeCoefficient (r + 1) - ε) * ↑n < (↑r - 1) * ↑c.innerSize

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

theorem Complexity.Frontier.lowerBound_all_fanIn {U : Type u} [Finite U] [Nontrivial U] {r : ℕ} (hr : 2 ≤ r) (S : (n : ℕ) → Set (Fin n → U)) (K : ℕ → ℕ) (hfree : ∀ᶠ (n : ℕ) in Filter.atTop, RectangleFree (S n) (K n)) (hK : (fun (n : ℕ) => Real.log ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (hdense : (fun (n : ℕ) => ↑n * Real.log ↑(Nat.card U) - Real.log ↑(S n).ncard) =o[Filter.atTop] fun (n : ℕ) => ↑n) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (σ : Cslib.Circuits.Signature) (I : Cslib.Circuits.Interpretation σ U) (Acc : Set U) (c : Cslib.Circuits.Circuit σ n 1), c.FanInAtMost r → Decides c I Acc (S n) → (2 - ε) * ↑n < (↑r - 1) * ↑c.innerSize

Every fixed fan-in, with the spanning-tree coefficient. The general-degree bound gives (r - 1) s > (2 - ε)n for every fixed r ≥ 2. The Gaussian theorem is sharper at r = 2.

theorem Complexity.Frontier.lowerBound_fanInThree {U : Type u} [Finite U] [Nontrivial U] (S : (n : ℕ) → Set (Fin n → U)) (K : ℕ → ℕ) (hfree : ∀ᶠ (n : ℕ) in Filter.atTop, RectangleFree (S n) (K n)) (hK : (fun (n : ℕ) => Real.log ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (hdense : (fun (n : ℕ) => ↑n * Real.log ↑(Nat.card U) - Real.log ↑(S n).ncard) =o[Filter.atTop] fun (n : ℕ) => ↑n) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (σ : Cslib.Circuits.Signature) (I : Cslib.Circuits.Interpretation σ U) (Acc : Set U) (c : Cslib.Circuits.Circuit σ n 1), c.FanInAtMost 3 → Decides c I Acc (S n) → (7 / 4 - ε) * ↑n < ↑c.innerSize

Ternary gates. The degree-four layout coefficient 2/5 gives 7n/4 - o(n) gates over every basis of fan-in at most three.