The frontier lower bound with gates of unbounded fan-in

Main theorem (eventually_lt_mul_card_of_ledger). Fix r ≥ 2 and assume the layout hypothesis LayoutBound (r + 1) A. Let S_n ⊆ U^n be dense K_n-rectangle-free sets with log K_n = o(n), as in Cslib.Circuits.Frontier.eventually_lt_mul_innerSize, and let β(n) = o(n). For every ε > 0 and all large n, every circuit deciding S_n whose gates have fan-in at most r, except for special gates of any fan-in that have a ledger in a monoid M with log |M| ≤ β(n), has s ordinary inner gates (inner gates that are not special) with

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

Constants and special gates are free; the ledger contributes only to the sublinear error. So the coefficient of the frontier method survives a sublinear amount of unbounded fan-in. For instance, k special gates that aggregate in a fixed finite commutative monoid T, such as unbounded AND, OR, parity, or counts modulo a fixed m, have a ledger with log |M| = k log |T| (Cslib.Circuits.Frontier.Ledger.ofAggregates), so k = o(n) such gates are allowed (eventually_lt_mul_card_of_aggregates). With the layout hypothesis of coefficient one (Cslib.Circuits.Frontier.layoutBound_one) the bounds are unconditional: (r - 1) s > (2 - ε) n (the module Complexity.Computability.Circuit.Frontier.Ledger.Unconditional).

Proof. Erase the special gates and lay out the live network (the graph of the erased program with every live wire as an output), one connected component after another (Cslib.Circuits.Frontier.LayoutBound.exists_layout_componentwise). Sweep the program along this layout with the ledger in the messages (Cslib.Circuits.Frontier.Ledger.sweep). At each step the transitions are bounded both by the width of the step and by the number of inputs read in the component being processed. The frontier counting lemma then finds a component W that reads almost all n inputs and whose frontier is wide, up to 2 log |M| and the usual error terms (Cslib.Circuits.Frontier.Ledger.exists_ncard_le). The cycle rank of W is at most (r - 1) s + 1 minus the number of inputs it reads (Cslib.Circuits.Frontier.Compiler.cycleRankOn_add_ncard_readIn_le), so W alone has the demand and the supply of a connected graph, and the comparison of demand and supply (Cslib.Circuits.Frontier.eventually_lt_of_frontier, with the ledger in its sublinear slack) finishes the proof.

Main results

• Cslib.Circuits.Frontier.eventually_lt_mul_card_of_ledger: the frontier lower bound with a ledger, conditional on LayoutBound.
• Cslib.Circuits.Frontier.eventually_lt_mul_card_of_aggregates: the frontier lower bound with aggregate gates, conditional on LayoutBound.

theorem Cslib.Circuits.Frontier.eventually_lt_mul_card_of_ledger {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β : β =o[Filter.atTop] fun (n : ℕ) => ↑n) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (σ : Signature) (I : Interpretation σ U) (Acc : Set U) (c : Circuit σ n 1) (special : Fin c.size → Prop) [inst : DecidablePred special] (M : Type w) [inst_1 : CommMonoid M] [Finite M], (∀ (g : Fin c.size), ¬special g → σ.Arity (c.program.lines g).op ≤ r) → ∀ (a : Ledger special c.program I M), Real.log ↑(Nat.card M) ≤ β n → c.Decides I Acc (S n) → (1 + 1 / A - ε) * ↑n < (↑r - 1) * ↑{g ∈ c.program.innerGates | ¬special g}.card

The frontier lower bound with a ledger. 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), and let β(n) = o(n). Then for every ε > 0 and all large n, every circuit deciding S_n, over any basis and interpretation on U, whose gates have fan-in at most r except for special gates of any fan-in with a ledger in a finite commutative monoid M with log |M| ≤ β(n), has s ordinary inner gates, the inner gates that are not special, with (r - 1) s > (1 + 1/A - ε) n.

theorem Cslib.Circuits.Frontier.eventually_lt_mul_card_of_aggregates {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β : β =o[Filter.atTop] fun (n : ℕ) => ↑n) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (σ : Signature) (I : Interpretation σ U) (Acc : Set U) (c : Circuit σ n 1) (special : Fin c.size → Prop) [inst : DecidablePred special] (T : Type w) [inst_1 : CommMonoid T] [Finite T], (∀ (g : Fin c.size), ¬special g → σ.Arity (c.program.lines g).op ≤ r) → (∀ (g : Fin c.size), special g → Aggregates (I (c.program.lines g).op) T) → ↑(Nat.card { g : Fin c.size // special g }) * Real.log ↑(Nat.card T) ≤ β n → c.Decides I Acc (S n) → (1 + 1 / A - ε) * ↑n < (↑r - 1) * ↑{g ∈ c.program.innerGates | ¬special g}.card

The frontier lower bound with aggregate gates. Under the hypotheses of eventually_lt_mul_card_of_ledger, for every ε > 0 and all large n, every circuit deciding S_n, over any basis and interpretation on U, whose gates have fan-in at most r except for k special gates of any fan-in that aggregate in a finite commutative monoid T, with k log |T| ≤ β(n), has s ordinary inner gates with (r - 1) s > (1 + 1/A - ε) n. For instance, the special gates may compute unbounded AND, OR, parity, or counts modulo a fixed m.