The lower bound

Main theorem (Frontier.lowerBound). Fix a fan-in bound r ≥ 2, and suppose that graphs of maximum degree r + 1 have layouts of width (A + o(1)) β₁ + o(|V|) (LayoutBound (r + 1) A). Let S_n ⊆ U^n be K_n-rectangle-free sets over a finite alphabet U, with log K_n = o(n) and |S_n| ≥ |U| ^ (n - o(n)). Then for every ε > 0 and all large n, every circuit deciding S_n over any basis of fan-in at most r on U has s inner gates with

(r - 1) s > (1 + 1/A - ε) n.

Gates of arity zero, the constants, are not counted. For fan-in two (Frontier.lowerBound_fanInTwo) the graphs are subcubic and the bound reads s > (1 + 1/A - ε) n.

The proof is the reduction theorem followed by the comparison of demand and supply (Frontier.eventually_lt_of_demand). A circuit with s gates gives a graph of cycle rank about (r - 1) s - n, all of whose layouts have width about n: that is the demand. The layout hypothesis provides a layout of width about A ((r - 1) s - n): that is the supply. So n ≤ A ((r - 1) s - n) + o(n), that is, (r - 1) s ≥ (1 + 1/A - o(1)) n.

Instances

For fan-in two the layout hypothesis is proved (Frontier.Layouts) with A = (3/π) arccos((1 + 2√2)/4) ≈ 0.2807, from Gaussian edge-score layouts, giving the coefficient 1 + π/(3 arccos((1 + 2√2)/4)) ≈ 4.5625, and with the weaker A = 1/3, giving the coefficient 4 (Frontier.Main).

theorem Complexity.Frontier.logb_ncard_le_self {U : Type u} [Finite U] [Nontrivial U] {n : ℕ} (S : Set (Fin n → U)) (hS : S.Nonempty) : Real.logb ↑(Nat.card U) ↑S.ncard ≤ ↑n

A set of inputs has at most |U| ^ n elements: log_q |S| ≤ n.

theorem Complexity.Frontier.isLittleO_sub_logb_ncard {U : Type u} [Finite U] [Nontrivial U] (S : (n : ℕ) → Set (Fin n → U)) (hdense : (fun (n : ℕ) => ↑n * Real.log ↑(Nat.card U) - Real.log ↑(S n).ncard) =o[Filter.atTop] fun (n : ℕ) => ↑n) : (fun (n : ℕ) => ↑n - Real.logb ↑(Nat.card U) ↑(S n).ncard) =o[Filter.atTop] fun (n : ℕ) => ↑n

A dense set has n - log_q |S_n| = o(n).

theorem Complexity.Frontier.eventually_card_mul_sq_le_ncard {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) : ∀ᶠ (n : ℕ) in Filter.atTop, Nat.card U * K n ^ 2 ≤ (S n).ncard

Eventually a dense rectangle-free set is large enough for the reduction: q K^2 ≤ |S|.

theorem Complexity.Frontier.lowerBound_of_graph {U : Type u} [Finite U] [Nontrivial U] {r : ℕ} (hr : 2 ≤ r) {A : ℝ} (hA : 0 < A) (hlayout : LayoutBound (r + 1) A) (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, ∀ (gates : ℕ) (V E : Type) [Finite V] [Finite E] (G : Multigraph V E), G.Connected → G.Loopless → G.MaxDegreeLE (r + 1) → Nat.card V ≤ 2 * r * gates + 3 → ↑G.cycleRank ≤ ↑((r - 1) * gates) - ↑n + Real.logb ↑(Nat.card U) ↑(K n) + 1 → (∀ (π : Layout V) (w : ℕ), (∀ (t : ℕ), (G.cut (π.initial t)).ncard ≤ w) → Real.logb ↑(Nat.card U) ↑(S n).ncard ≤ ↑w + (↑r + 2) + 3 * Real.logb ↑(Nat.card U) ↑(K n) + Real.logb (↑(Nat.card U)) (↑(Nat.card V) + 1)) → (1 + 1 / A - ε) * ↑n < (↑r - 1) * ↑gates

The numerical demand--supply comparison, exposed independently of the compiler. Any graph with the reduction's size, cycle, and frontier-demand bounds gives the same lower bound on its gate budget.

theorem Complexity.Frontier.lowerBound {U : Type u} [Finite U] [Nontrivial U] {r : ℕ} (hr : 2 ≤ r) {A : ℝ} (hA : 0 < A) (hlayout : LayoutBound (r + 1) A) (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 / A - ε) * ↑n < (↑r - 1) * ↑c.innerSize

The frontier lower bound. Let r ≥ 2 and assume the layout hypothesis for maximum degree r + 1 with coefficient A > 0. 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, for all large n, every circuit with fan-in at most r deciding S_n, over any basis and interpretation on U, has s inner gates with (r - 1) s > (1 + 1/A - ε) n.

theorem Complexity.Frontier.lowerBound_fanInTwo {U : Type u} [Finite U] [Nontrivial U] {A : ℝ} (hA : 0 < A) (hlayout : LayoutBound 3 A) (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 + 1 / A - ε) * ↑n < ↑c.innerSize

The frontier lower bound for fan-in two. Assume the layout hypothesis for subcubic graphs with coefficient A > 0. Under the hypotheses of Frontier.lowerBound, for every ε > 0 and all large n, every circuit with fan-in at most two deciding S_n, over any basis and interpretation on U, has more than (1 + 1/A - ε) n inner gates.