The unconditional lower bound with aggregate gates

Combining Frontier.lowerBound_aggregate with the layout bound for subcubic graphs: circuits of fan-in two over any basis, together with k = o(n) gates of unbounded fan-in that aggregate in a fixed finite commutative monoid, such as unbounded AND, OR, and parity, need more than (L - ε) n ordinary inner gates to decide a dense rectangle-free set, with L = 1 + π / (3 arccos ((1 + 2√2)/4)) ≈ 4.5625.

theorem Complexity.Frontier.lowerBound_aggregate_gaussian {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, ∀ (σ : Cslib.Circuits.Signature) (I : Cslib.Circuits.Interpretation σ U) (Acc : Set U) (c : Cslib.Circuits.Circuit σ n 1) (special : ℕ → Prop) (T : Type) [inst : 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 → Decides c I Acc (S n) → (1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4)) - ε) * ↑n < ↑(erase special c.program).innerGates.card

The (L - ε) n lower bound with aggregate gates.