Unconditional frontier lower bounds with gates of unbounded fan-in

The frontier lower bounds with a ledger (Cslib.Circuits.Frontier.eventually_lt_mul_card_of_ledger) and with aggregate gates (Cslib.Circuits.Frontier.eventually_lt_mul_card_of_aggregates) are conditional on the layout hypothesis LayoutBound (r + 1) A. Spanning trees prove it with coefficient A = 1 in every degree (Cslib.Circuits.Frontier.layoutBound_one), and median edge-score layouts prove it with A = 2p in degree three (Cslib.Circuits.Frontier.layoutBound_gaussian), which removes the hypothesis.

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 fan-in r ≥ 2, 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 monoid M with log |M| ≤ β(n), has s ordinary inner gates with

(r - 1) s > (2 - ε) n,

and at fan-in r = 2,

s > (L - ε) n with L = 1 + π / (3 arccos ((1 + 2√2)/4)) ≈ 4.5625.

For instance, o(n) gates of unbounded fan-in computing AND, OR, parity, or counts modulo a fixed m cost nothing in the leading term.

Main results

• Cslib.Circuits.Frontier.eventually_two_sub_mul_lt_mul_card_of_ledger: with a ledger.
• Cslib.Circuits.Frontier.eventually_two_sub_mul_lt_mul_card_of_aggregates: with aggregate gates.
• Cslib.Circuits.Frontier.eventually_gaussian_sub_mul_lt_card_of_ledger, eventually_gaussian_sub_mul_lt_card_of_aggregates: the Gaussian (L - ε) n bounds at ordinary fan-in two.

theorem Cslib.Circuits.Frontier.eventually_two_sub_mul_lt_mul_card_of_ledger {U : Type u} [Finite U] [Nontrivial U] {S : (n : ℕ) → Set (Fin n → U)} {K : ℕ → ℕ} {r : ℕ} (hr : 2 ≤ r) (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) → (2 - ε) * ↑n < (↑r - 1) * ↑{g ∈ c.program.innerGates | ¬special g}.card

The unconditional frontier lower bound with a ledger. Let r ≥ 2, 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 with (r - 1) s > (2 - ε) n.

theorem Cslib.Circuits.Frontier.eventually_two_sub_mul_lt_mul_card_of_aggregates {U : Type u} [Finite U] [Nontrivial U] {S : (n : ℕ) → Set (Fin n → U)} {K : ℕ → ℕ} {r : ℕ} (hr : 2 ≤ r) (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) → (2 - ε) * ↑n < (↑r - 1) * ↑{g ∈ c.program.innerGates | ¬special g}.card

The unconditional frontier lower bound with aggregate gates. Under the hypotheses of eventually_two_sub_mul_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 > (2 - ε) n.

theorem Cslib.Circuits.Frontier.eventually_gaussian_sub_mul_lt_card_of_ledger {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β : β =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 ≤ 2) → ∀ (a : Ledger special c.program I M), Real.log ↑(Nat.card M) ≤ β n → c.Decides I Acc (S n) → (1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4)) - ε) * ↑n < ↑{g ∈ c.program.innerGates | ¬special g}.card

The Gaussian frontier lower bound with a ledger, at ordinary fan-in two. Under the hypotheses of eventually_two_sub_mul_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 two except for special gates of any fan-in with a ledger in a finite commutative monoid M with log |M| ≤ β(n), has more than (L - ε) n ordinary inner gates, where L = 1 + π / (3 arccos ((1 + 2√2)/4)) ≈ 4.5625.

theorem Cslib.Circuits.Frontier.eventually_gaussian_sub_mul_lt_card_of_aggregates {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β : β =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 ≤ 2) → (∀ (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 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4)) - ε) * ↑n < ↑{g ∈ c.program.innerGates | ¬special g}.card

The Gaussian frontier lower bound with aggregate gates, at ordinary fan-in two. Under the hypotheses of eventually_gaussian_sub_mul_lt_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 two except for k special gates of any fan-in that aggregate in a finite commutative monoid T, with k log |T| ≤ β(n), has more than (L - ε) n ordinary inner gates.