Frontier lower bounds for fan-in two

The frontier lower bound for fan-in two (Cslib.Circuits.Frontier.eventually_lt_innerSize) is conditional on the layout hypothesis LayoutBound 3 A, and gives s > (1 + 1/A - ε) n. Two layout bounds remove the hypothesis:

• median edge-score layouts give A = 2p with p = (3 / (2π)) arccos ((1 + 2√2)/4) (Cslib.Circuits.Frontier.layoutBound_gaussian), so 1 + 1/A = L;
• vertex-score layouts give A = 1/3 (Cslib.Circuits.Frontier.layoutBound_one_third), so 1 + 1/A = 4.

Let S_n ⊆ U^n be K_n-rectangle-free sets over a finite alphabet U 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 of fan-in at most two deciding S_n, over any basis and interpretation on U, has more than

• (L - ε) n inner gates, with L = 1 + π / (3 arccos ((1 + 2√2)/4)) ≈ 4.5624977 (Cslib.Circuits.Frontier.eventually_gaussian_sub_mul_lt_innerSize);
• (114/25 - ε) n = (4.56 - ε) n inner gates, since L ≥ 114/25 (Cslib.Circuits.Frontier.eventually_114_div_25_sub_mul_lt_innerSize);
• (4 - ε) n inner gates (Cslib.Circuits.Frontier.eventually_four_sub_mul_lt_innerSize).

Gates of arity zero, the constants, are not counted. The hypotheses are those of Cslib.Circuits.Frontier.eventually_two_sub_mul_lt_innerSize: the bounds apply to every family of dense rectangle-free sets, and to a particular family once it is shown to be one.

The same three coefficients hold for the bundled worst-case claim CircuitLowerBound and for the average-case claim AverageCaseBound: circuits of fan-in two with at most (L - ε) n inner gates agree with a set of bias at most b_n on large rectangles on at most a 1/2 + b_n + exp (-γ n) fraction of the inputs.

Main results

• Cslib.Circuits.Frontier.eventually_gaussian_sub_mul_lt_innerSize: s > (L - ε) n.
• Cslib.Circuits.Frontier.eventually_114_div_25_sub_mul_lt_innerSize: s > (114/25 - ε) n.
• Cslib.Circuits.Frontier.eventually_four_sub_mul_lt_innerSize: s > (4 - ε) n.
• Cslib.Circuits.Frontier.circuitLowerBound_gaussian, circuitLowerBound_114_div_25, circuitLowerBound_four: the bundled worst-case claims.
• Cslib.Circuits.Frontier.averageCaseBound_gaussian, averageCaseBound_114_div_25, averageCaseBound_four: the average-case claims.

theorem Cslib.Circuits.Frontier.eventually_gaussian_sub_mul_lt_innerSize {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, ∀ (σ : Signature) (I : Interpretation σ U) (Acc : Set U) (c : Circuit σ n 1), c.FanInAtMost 2 → c.Decides I Acc (S n) → (1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4)) - ε) * ↑n < ↑c.innerSize

The Gaussian frontier lower bound for fan-in two. Let S_n ⊆ U^n be K_n-rectangle-free sets over a finite alphabet U 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 of fan-in at most two deciding S_n, over any basis and interpretation on U, has more than (L - ε) n inner gates, where L = 1 + π / (3 arccos ((1 + 2√2)/4)) ≈ 4.5625.

theorem Cslib.Circuits.Frontier.eventually_114_div_25_sub_mul_lt_innerSize {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, ∀ (σ : Signature) (I : Interpretation σ U) (Acc : Set U) (c : Circuit σ n 1), c.FanInAtMost 2 → c.Decides I Acc (S n) → (114 / 25 - ε) * ↑n < ↑c.innerSize

The (4.56 - ε) n frontier lower bound for fan-in two. Under the hypotheses of eventually_gaussian_sub_mul_lt_innerSize, for every ε > 0 and all large n, every circuit of fan-in at most two deciding S_n, over any basis and interpretation on U, has more than (114/25 - ε) n inner gates.

theorem Cslib.Circuits.Frontier.eventually_four_sub_mul_lt_innerSize {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, ∀ (σ : Signature) (I : Interpretation σ U) (Acc : Set U) (c : Circuit σ n 1), c.FanInAtMost 2 → c.Decides I Acc (S n) → (4 - ε) * ↑n < ↑c.innerSize

The (4 - ε) n frontier lower bound for fan-in two. Under the hypotheses of eventually_gaussian_sub_mul_lt_innerSize, for every ε > 0 and all large n, every circuit of fan-in at most two deciding S_n, over any basis and interpretation on U, has more than (4 - ε) n inner gates. The layout bound is that of Gaussian vertex scores.

The bundled claims

theorem Cslib.Circuits.Frontier.circuitLowerBound_gaussian : CircuitLowerBound (1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4)))

Circuits of fan-in two need (L - ε) n gates, by median edge-score layouts, where L = 1 + π / (3 arccos ((1 + 2√2)/4)) ≈ 4.5625.

theorem Cslib.Circuits.Frontier.circuitLowerBound_114_div_25 : CircuitLowerBound (114 / 25)

Circuits of fan-in two need (4.56 - ε) n gates: the Gaussian coefficient is at least 114/25.

theorem Cslib.Circuits.Frontier.circuitLowerBound_four : CircuitLowerBound 4

Circuits of fan-in two need (4 - ε) n gates, by Gaussian vertex-score layouts.

theorem Cslib.Circuits.Frontier.averageCaseBound_gaussian : AverageCaseBound (1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4)))

Circuits of fan-in two below (L - ε) n gates barely beat guessing on sets of small bias on large rectangles, by median edge-score layouts, where L = 1 + π / (3 arccos ((1 + 2√2)/4)) ≈ 4.5625.

theorem Cslib.Circuits.Frontier.averageCaseBound_114_div_25 : AverageCaseBound (114 / 25)

Circuits of fan-in two below (4.56 - ε) n gates barely beat guessing: the Gaussian coefficient is at least 114/25.

theorem Cslib.Circuits.Frontier.averageCaseBound_four : AverageCaseBound 4

Circuits of fan-in two below (4 - ε) n gates barely beat guessing, by Gaussian vertex-score layouts.