The frontier lower bound

Main theorem (eventually_lt_mul_innerSize). Fix a fan-in bound r ≥ 2, and suppose that the graphs of maximum degree r + 1 have layouts of width (A + o(1)) β₁ + o(|V|), where β₁ is the cycle rank (the layout hypothesis 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 (eventually_lt_innerSize) 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 (eventually_lt_of_demand). A circuit with s inner 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.

The theorems of this file are conditional on the layout hypothesis, which is stated as LayoutBound; any instance of it yields an unconditional lower bound.

The worst-case claim (CircuitLowerBound L) bundles the statement for fan-in two with coefficient L, so that each layout theorem reads as one line: circuitLowerBound_of_layoutBound : LayoutBound 3 A → CircuitLowerBound (1 + 1/A).

Main definitions

• Cslib.Circuits.Frontier.CircuitLowerBound L: circuits of fan-in at most two deciding dense rectangle-free sets need more than (L - ε) n inner gates.

Main results

• Cslib.Circuits.Frontier.eventually_lt_of_frontier: the comparison of demand and supply with the error terms of the problem and a sublinear slack, shared by all frontier lower bounds.
• Cslib.Circuits.Frontier.eventually_lt_of_graph: the comparison of demand and supply for any family of graphs with the bounds of the reduction theorem.
• Cslib.Circuits.Frontier.eventually_lt_mul_innerSize: the frontier lower bound for fan-in at most r.
• Cslib.Circuits.Frontier.eventually_lt_innerSize: the frontier lower bound for fan-in two.
• Cslib.Circuits.Frontier.circuitLowerBound_of_layoutBound: the same, as a bundled claim.

theorem Cslib.Circuits.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_|U| |S| ≤ n.

theorem Cslib.Circuits.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 family of sets has n - log_|U| |S_n| = o(n).

theorem Cslib.Circuits.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

A dense family of rectangle-free sets is eventually large enough for the reduction: |U| K_n ^ 2 ≤ |S_n|.

theorem Cslib.Circuits.Frontier.eventually_lt_of_frontier {U : Type u} [Finite U] [Nontrivial U] {S : (n : ℕ) → Set (Fin n → U)} {K : ℕ → ℕ} {A : ℝ} (hA : 0 < A) (d : ℝ) (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β : β =o[Filter.atTop] fun (n : ℕ) => ↑n) {ε : ℝ} (hε : 0 < ε) : ∃ η > 0, ∀ (C : ℝ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (s v ρ w : ℝ), 0 ≤ s → 0 ≤ v → v ≤ 7 * s + 3 * ↑n + 3 → ρ ≤ s - Real.logb ↑(Nat.card U) ↑(S n).ncard + 2 * Real.logb ↑(Nat.card U) ↑(K n) + Real.logb (↑(Nat.card U)) (v + 1) + β n + 1 → Real.logb ↑(Nat.card U) ↑(S n).ncard ≤ w + d + 3 * Real.logb ↑(Nat.card U) ↑(K n) + Real.logb (↑(Nat.card U)) (v + 1) + β n → w ≤ (A + η) * ρ + η * v + C → (1 + 1 / A - ε) * ↑n < s

Demand against supply for the frontier method, with the error terms of the problem and a sublinear slack. Let S_n be dense sets with log K_n = o(n), let β(n) = o(n), let d be a constant and A > 0. For every ε > 0 there is a slack η > 0 of the layout hypothesis such that, for every constant C and all large n, the following holds for reals s, v ≥ 0 (a gate budget and a number of vertices with v ≤ 7 s + 3 n + 3) and ρ, w, where q = |U|:

• if ρ ≤ s - log_q |S_n| + 2 log_q K_n + log_q (v + 1) + β(n) + 1 (a cycle rank: the graph reads almost all inputs),
• and log_q |S_n| ≤ w + d + 3 log_q K_n + log_q (v + 1) + β(n) (the demand: some frontier is wide),
• and w ≤ (A + η) ρ + η v + C (the supply of the layout hypothesis),

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

This is the numerical half of every frontier lower bound in this library: the circuit lower bounds apply it to s = (r - 1) times the number of gates.

theorem Cslib.Circuits.Frontier.eventually_lt_of_graph {U : Type u} [Finite U] [Nontrivial U] {S : (n : ℕ) → Set (Fin n → U)} {K : ℕ → ℕ} {r : ℕ} (hr : 2 ≤ r) {A : ℝ} (hA : 0 < A) (hlayout : LayoutBound (r + 1) A) (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, ∀ (g : ℕ) (V E : Type) [Finite V] [inst : Finite E] (G : Multigraph V E), G.toSimpleGraph.Connected → G.Loopless → G.MaxDegreeLE (r + 1) → Nat.card V ≤ 2 * r * g + 3 → ↑G.cycleRank ≤ (↑r - 1) * ↑g - ↑n + Real.logb ↑(Nat.card U) ↑(K n) + 1 → (∀ (π : Layout V), Real.logb ↑(Nat.card U) ↑(S n).ncard ≤ ↑(G.width π) + (↑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) * ↑g

Demand against supply for graphs. Assume the layout hypothesis for maximum degree r + 1 with coefficient A > 0, and let S_n be dense K_n-rectangle-free sets with log K_n = o(n). For every ε > 0 and all large n: every connected, loopless graph of maximum degree r + 1 with the bounds of the reduction theorem for g gates (at most 2 r g + 3 vertices, cycle rank at most (r - 1) g - n + log_q K_n + 1, and every layout of width at least log_q |S_n| - 3 log_q K_n - log_q (|V| + 1) - (r + 2)) has (r - 1) g > (1 + 1/A - ε) n.

This is the numerical half of the lower bound, independent of circuits: the comparison of demand and supply eventually_lt_of_frontier, with the layout hypothesis as the supply.

theorem Cslib.Circuits.Frontier.eventually_lt_mul_innerSize {U : Type u} [Finite U] [Nontrivial U] {S : (n : ℕ) → Set (Fin n → U)} {K : ℕ → ℕ} {r : ℕ} (hr : 2 ≤ r) {A : ℝ} (hA : 0 < A) (hlayout : LayoutBound (r + 1) A) (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 r → c.Decides 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 and all large n, every circuit of 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 Cslib.Circuits.Frontier.eventually_lt_innerSize {U : Type u} [Finite U] [Nontrivial U] {S : (n : ℕ) → Set (Fin n → U)} {K : ℕ → ℕ} {A : ℝ} (hA : 0 < A) (hlayout : LayoutBound 3 A) (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 + 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 eventually_lt_mul_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 (1 + 1/A - ε) n inner gates.

def Cslib.Circuits.Frontier.CircuitLowerBound (L : ℝ) : Prop

The worst-case claim with coefficient L. Let U be a finite alphabet with at least two symbols, and let S_n ⊆ U^n be K_n-rectangle-free sets 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 gates of positive arity.

The alphabet lives in the universe u and the basis in the universe v.

theorem Cslib.Circuits.Frontier.CircuitLowerBound.mono {L L' : ℝ} (h : CircuitLowerBound L) (hL : L' ≤ L) : CircuitLowerBound L'

A circuit lower bound holds for every smaller coefficient.

theorem Cslib.Circuits.Frontier.circuitLowerBound_of_layoutBound {A : ℝ} (hA : 0 < A) (hlayout : LayoutBound 3 A) : CircuitLowerBound (1 + 1 / A)

The frontier lower bound as a bundled claim. If subcubic graphs have layouts of width (A + o(1)) β₁ + o(|V|) (LayoutBound 3 A), then circuits of fan-in at most two deciding dense rectangle-free sets need more than (1 + 1/A - ε) n inner gates.