Circuit lower bounds with sublinear aggregate budgets

The circuit compiler, large-component argument, and density-preserving restriction discharge every premise of the numerical slice bound. For the mixed signature, the graph-ordering coefficient A therefore gives circuit coefficient 1 + 1/A whenever the total output-guess and finite-register budget is sublinear.

theorem Algebraic.Cutwidth.Aggregate.sliceBound_of_circuit {J : Type} {State : J → Type} [(j : J) → CommMonoid (State j)] [(j : J) → Fintype (State j)] {n g D K : ℕ} (p : Program (Aggregate.signature State) n g) (out : Wire n g) (budget : Aggregate.budget p ≤ D) (free : RectangleFree (fun (x : Cslib.BitString n) => p.trace Aggregate.interpretation x out) K) (dense : 2 ^ (n - 2) ≤ (accepting fun (x : Cslib.BitString n) => p.trace Aggregate.interpretation x out).card) (hK : 1 < K) (big : 3 * (D + Nat.clog 2 K + 3) ≤ n) {A η C : ℝ} (hAη : 0 ≤ A + η) (hC : 0 ≤ C) (order : Multigraph.OrderingBound A η C) : SliceBound A η C n g D K

Every dense rectangle-free mixed circuit admits the finite slice estimate. The budget is measured on the actual special occurrences of this circuit.

theorem Algebraic.Cutwidth.Aggregate.eventually_component_guard (D K : ℕ → ℕ) (hD : (fun (n : ℕ) => ↑(D n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (hK : (fun (n : ℕ) => Real.logb 2 ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (positive : ∀ᶠ (n : ℕ) in Filter.atTop, 1 < K n) : ∀ᶠ (n : ℕ) in Filter.atTop, 3 * (D n + Nat.clog 2 (K n) + 3) ≤ n

Sublinear budget and logarithmic threshold eventually permit the large-component argument.

theorem Algebraic.Cutwidth.Aggregate.eventually_lt_size_of_orderingBound {J : Type} {State : J → Type} [(j : J) → CommMonoid (State j)] [(j : J) → Fintype (State j)] {A : ℝ} (hA : 0 < A) (order : ∀ (η : ℝ), 0 < η → ∃ (C : ℝ), Multigraph.OrderingBound A η C) (f : (n : ℕ) → Cslib.BooleanFunction n) (D K : ℕ → ℕ) (hD : (fun (n : ℕ) => ↑(D n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (hK : (fun (n : ℕ) => Real.logb 2 ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (hard : ∀ᶠ (n : ℕ) in Filter.atTop, RectangleFree (f n) (K n) ∧ 2 ^ (n - 2) ≤ (accepting (f n)).card) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (c : Circuit (Aggregate.signature State) n 1), (c.Computes Aggregate.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f n x) → Aggregate.budget c.program ≤ D n → (1 + 1 / A - ε) * ↑n < ↑c.size

The general-coefficient lower bound for binary gates augmented by arbitrary finite commutative-monoid gates of sublinear total summary budget.